Process logic: Expressiveness, decidability, completeness

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

David Harel, Rohit Parikh, Dexter Kozen

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 logic; axiomatization; process logic; extending propositional dynamic logic

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

68Q65: Abstract data types; algebraic specification

68N01: General topics in the theory of software

Related Items

From Monadic Logic to PSL, Branching versus linear logics yet again, A simple deduction method for modal logic, Process logic with regular formulas, The complementation problem for Büchi automata with applications to temporal logic, \(R\)-generability, and definability in branching time logics, Process and action: Relevant theory and logics, Dynamic linear time temporal logic, Computation paths logic: An expressive, yet elementary, process logic, An overview of transaction logic, Mathematical modal logic: A view of its evolution, Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus., Alternative semantics for temporal logics, Compositionality of Hennessy-Milner logic by structural operational semantics, A decision procedure for propositional projection temporal logic with infinite models, From Philosophical to Industrial Logics, Complexity of propositional projection temporal logic with star

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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