A Logic with 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 where asyncronous message passing is the only possible mechanism for communication, e.g. distributed workflow systems. We define adtl, a logic with modalities for time and locality. We introduce a complete and decidable axiom system, which characterizes the class of structures that reflect the nature of the causal relation when communications are asynchronous.