Modalities for Asynchronous Distributed Systems

The purpose of this work is to establish some foundational ground for the logics that can be used to reason on distributed systems communicating asyncronously via message passing, e.g. distributed workflow systems. These systems rule out synchronized local clocks, and reasoning on global time or state: message passing is the only possible mechanism for communication, and therefore for causality across components. We introduce {\em adtl}, a logic with modalities for time and locality. We show that its axiom system characterizes the class of structures that reflect the nature of the causal relation when communication is asyncronous. Correspondingly, the axioms are such that any attempt to formulate in the logic properties about the unspeakable entities, like a global state, results in a contradiction.