  We introduce a temporal logic to reason on global applications in an
asynchronous setting. First, we define the Distributed States Logic (DSL), 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. The contribution is that it is
possible to reason about properties that involve several components, even in
the absence of a global clock. Then, we define the Distributed States Temporal
Logic (DSTL) by introducing temporal operators a' la Unity. We support our
proposal by working out a pair of examples: a simple secure communication
system, and an algorithm for distributed leader election.
  The motivation for this work is that the existing logics for distributed
systems do not have the right expressive power to reason on the systems
behaviour, when the communication is based on asynchronous message passing. On
the other side, asynchronous communication is the most used abstraction when
modelling global applications.
