Completeness of a Temporal Logic for Asynchronous Systems
Ricciardi, Aleta M.
In this paper, we define a variant of temporal logic that is designed to capture the temporal and causal aspects of asynchronous distributed systems. In these systems, the usual physical concept of time based upon the notion of a global clock is relegated to a secondary role; causal dependency or necessary temporal precedence is fundamental. Causal dependence is just temporal order locally; globally it is based on communication. An instant of time is replaced by a consistent cut. The semantics of most temporal logics have been based on computation sequences, either linear or branching time. In these models, one views an execution of a system as a single sequence of events. In such models, a "spurious" linearization is introduced, effectively disregarding concurrency. Recently, however, partially ordered models have been considered because, it is argued, that they more accurately represent the system being studied. The main technical contribution of this paper is to show that such a logic is complete for the class of models defined by executions of asynchronous systems.
computer science; technical report
Previously Published As