PDL with data constants

DOI10.1016/0020-0190(85)90127-9zbMath0577.68046OpenAlexW2036328670MaRDI QIDQ1065545

Solomon Passy, Tinko Tinchev

Publication date: 1985

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(85)90127-9

zbMATH Keywords

undecidabilityintersectioncomplementpropositional dynamic logiccomplete axiomatizationprogramsdata identitydynamic algebraverification of

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (13)

Derivation rules as anti-axioms in modal logic ⋮ Infinitary propositional normal modal logic ⋮ A propositional logic of Boolean recursive programs in which predicate variables appear in conditions ⋮ Hybrid languages ⋮ Towards reasoning about Hoare relations ⋮ Unnamed Item ⋮ Determinism and looping in combinatory PDL ⋮ The many faces of counts-as: A formal analysis of constitutive rules ⋮ Clausal Tableaux for Hybrid PDL ⋮ PDL with intersection of programs: a complete axiomatization ⋮ A modal perspective on the computational complexity of attribute value grammar ⋮ An essay in combinatory dynamic logic ⋮ On the undecidability of logics with converse, nominals, recursion and counting

Cites Work

• An elementary proof of the completeness of PDL
• First-order dynamic logic
• Propositional dynamic logic of regular programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: PDL with data constants