Computation paths logic: An expressive, yet elementary, process logic Original Research Article

A new process logic is defined, called computation paths logic (CPL), which treats formulas and programs essentially alike. CPL is a pathwise extension of PDL, following the basic process logic of Harel, Kozen and Parikh and is close in spirit to the logic R of Harel and Peleg. It enjoys most of the advantages of previous process logics, yet is decidable in elementary time. We also offer extensions for modeling asynchronous/synchronous concurrency and infinite computations. All extensions are also shown to be decidable in elementary time.