Process logic: Expressiveness, decidability, completeness

DOI10.1016/0022-0000(82)90003-4zbMath0494.03016OpenAlexW1967494119MaRDI QIDQ1168965

Rohit Parikh, Dexter Kozen, David Harel

Publication date: 1982

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(82)90003-4

zbMATH Keywords

temporal logicaxiomatizationprocess logicextending propositional dynamic logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items

Compositionality of Hennessy-Milner logic by structural operational semantics ⋮ Strategies in Games: A Logic-Automata Study ⋮ The complementation problem for Büchi automata with applications to temporal logic ⋮ An overview of transaction logic ⋮ Functional Specification of Hardware via Temporal Logic ⋮ On proving properties of completion strategies ⋮ Trace Semantics for IPDL ⋮ Computable execution traces ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ A dynamic logic with branching modalities ⋮ A program logic to verify signal temporal logic specifications of hybrid systems ⋮ Branching versus linear logics yet again ⋮ Execution trace sets for real computation ⋮ Mathematical modal logic: A view of its evolution ⋮ Modal logic for modelling actions and agents ⋮ Calculational design of a regular model checker by abstract interpretation ⋮ \(R\)-generability, and definability in branching time logics ⋮ Compositional reasoning using intervals and time reversal ⋮ A decision procedure for propositional projection temporal logic with infinite models ⋮ Process and action: Relevant theory and logics ⋮ Alternative semantics for temporal logics ⋮ From Philosophical to Industrial Logics ⋮ From Monadic Logic to PSL ⋮ Complexity of propositional projection temporal logic with star ⋮ Natural strategic ability ⋮ Computation paths logic: An expressive, yet elementary, process logic ⋮ Dynamic linear time temporal logic ⋮ Computation paths logic: An expressive, yet elementary, process logic ⋮ A simple deduction method for modal logic ⋮ Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus. ⋮ Process logic with regular formulas

Cites Work

• Two results on process logic
• Descriptively complete process logic
• A near-optimal method for reasoning about action
• An elementary proof of the completeness of PDL
• Definability in dynamic logic
• First-order dynamic logic
• Propositional dynamic logic of regular programs
• Equations between Regular Terms and an Application to Process Logic
• A practical decision method for propositional dynamic logic (Preliminary Report)
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item