Process logic: Expressiveness, decidability, completeness

Abstract

We define a process logic PL that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL is an extension of the language of Propositional Dynamic Logic (PDL). We give a deductive system for PL which includes the Segerberg axioms for PDL and prove that it is complete. We also show that PL is decidable.