Distributed versions of linear time temporal logic: A trace perspective

From MaRDI portal

DOI10.1007/3-540-65306-6_24MaRDI QIDQ4247293zbMATH OpenFDO

Authors P. S. Thiagarajan, Jesper G. Henriksen

Publication date 6 April 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-65306-6_24


zbMATH Keywords

asynchronous automataautomata over infinite objectsdistributed systemsexpressivenesslinear time temporal logicMazurkiewicz tracemodel checkingnetwork of sequential agentsproduct automataproduct languagessatisfiabilitytrace languagestrace-based logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)




Review text

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].


Recommendations



Cited in
(15)








This page was built for publication: Distributed versions of linear time temporal logic: A trace perspective

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247293)

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Distributed_versions_of_linear_time_temporal_logic:_A_trace_perspective&oldid=108454781"
Powered by MediaWiki