Process logic: Expressiveness, decidability, completeness

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.