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.

Authors

• David Harel
• Dexter Kozen
• Rohit Parikh

Keywords

• Logic
• Page description languages
• Vehicle dynamics
• Hydrogen
• Reasoning about programs
• Heuristic algorithms
• Vehicles
• System recovery
• Joining processes
• Laboratories
• Logical Process
• Temporal Logic
• Path Model
• Linear Order
• Homomorphism
• Finite Length
• Order Theory
• Proof Of The Lemma
• Induction Hypothesis
• First-order Theory
• Reverse Operation
• Previous Lemma
• Axiomatic Approach
• Logic Algorithm
• Modal Logic
• Program Behavior