PDL with data constants

DOI10.1016/0020-0190(85)90127-9zbMath0577.68046MaRDI 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

undecidability; intersection; complement; propositional dynamic logic; complete axiomatization; programs; data identity; dynamic algebra; verification of

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q65: Abstract data types; algebraic specification

Related Items

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

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