Computation paths logic: An expressive, yet elementary, process logic

computation paths logic concurrency concurrent processes dynamic logic elementary decidability expressing properties of infinite computations process logic temporal logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

A new process logic is introduced, called computation paths logic (CPL) that is ``compositional, uniform in its treatment of programs and formulas, expressive enough to capture the interesting path properties mentioned in the literature in a natural way, explicit in its treatment of concurrency, and elementarily decidable. It builds on previous approaches to process logic [see \textit{D. Harel, D. Kozen} and \textit{R. Parikh}, J. Comput. Syst. Sci. 25, 144-170 (1982; Zbl 0494.03016); \textit{D. Harel} and \textit{D. Peleg}, Theor. Comput. Sci. 38, 307-322 (1985; Zbl 0572.03010); \textit{M. Y. Vardi} and \textit{P. Wolper}, Logics of programs, Lect. Notes Comput. Sci. 164, 501-512 (1984; Zbl 0549.68020)]. The syntax and semantics of CPL are introduced and a proof of its elementary decidability is presented. Extensions of CPL are proposed for modeling asynchronous and synchronous concurrent processes, and for expressing properties of infinite computations. They are proved to be elementarily decidable, too, using automata.

Recommendations

Cites work

Cited in

(2)

This page was built for publication: Computation paths logic: An expressive, yet elementary, process logic

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