Distributed states logic

We introduce a temporal logic to reason on global applications. First, we define a modal logic for localities that embeds the local theories of each component into a theory of the distributed states of the system. We provide the logic with a sound and complete axiomatization. Then, we extend the logic with a temporal operator. The contribution is that it is possible to reason about properties that involve several components in a natural way, even in the absence of a global clock, as required in an asynchronous setting.