Distributed versions of linear time temporal logic: A trace perspective (Q4247293)

The paper provides an overview of linear time temporal logics whose models can be viewed as Mazurkiewicz traces. Basic notions of the linear time temporal logic (over a finite non-empty alphabet of actions) \(\text{LTL}(\Sigma)\) are introduced. The satisfiability problem and the model checking problem are characterized (and their automata-theoretic solutions are presented). The concept of (Mazurkiewicz) traces is introduced. An equivalence relation is induced by trace alphabets. Many properties of distributed systems respect the equivalence relation (trace consistent properties). This has important consequences for the practical verification of such properties. A useful class of distributed behaviours is described in terms of a theory of product languages and automata. Product languages constitute a well-understood class of trace languages. The automata that recognize these languages are called product automata. A method of forming distributed systems is based on the automata. The system consists of a network of sequential agents. A simple trace-based version of LTL (called product LTL) is presented. The formulas of this logic have a natural semantics in terms of the computations generated by a network of sequential agents. Solutions (based on the theory of product automata) of the satisfiability and model checking problems for product LTL are provided. Mazurkiewicz traces are represented as restricted labelled partial orders. A theory of trace languages and of asynchronous automata for recognizing trace languages is presented. Then a trace-based logic, TrPTL, is introduced. Solutions to the satisfiability and model checking problems for TrPTL are provided using asynchronous automata. Finally, various expressiveness issues associated with the temporal logics studied in the paper are considered and some remarks about branching time temporal logics (based on traces) are given. For the entire collection see [Zbl 0903.00072].