Computation paths logic: An expressive, yet elementary, process logic (Q1295436)

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.