PDL with data constants

DOI10.1016/0020-0190(85)90127-9MaRDI QIDQ1065545zbMATH OpenOpenAlexFDO

Authors 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

complementcomplete axiomatizationdata identitydynamic algebraintersectionprogramspropositional dynamic logicundecidabilityverification of

Mathematics Subject Classification ID

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

Recommendations

• Foundations of Software Science and Computation Structures
• The propositional dynamic logic of deterministic, well-structured programs
• Propositional dynamic logic with recursive programs
• Propositional dynamic logic with program quantifiers
• scientific article; zbMATH DE number 3845549

Cites work

• An elementary proof of the completeness of PDL
• First-order dynamic logic
• scientific article; zbMATH DE number 3843130 (Why is no real title available?)
• scientific article; zbMATH DE number 3853056 (Why is no real title available?)
• scientific article; zbMATH DE number 3731325 (Why is no real title available?)
• scientific article; zbMATH DE number 3735127 (Why is no real title available?)
• scientific article; zbMATH DE number 3266609 (Why is no real title available?)
• scientific article; zbMATH DE number 3315203 (Why is no real title available?)
• scientific article; zbMATH DE number 3198011 (Why is no real title available?)
• Propositional dynamic logic of regular programs

Cited in

(39)

• Propositional dynamic logic with local assignments
• Infinitary propositional normal modal logic
• \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs
• A modal perspective on the computational complexity of attribute value grammar
• The complexity of PDL with interleaving
• Hybrid languages
• Towards reasoning about Hoare relations
• Propositional dynamic logic with quantification over regular computation sequences
• A propositional logic of Boolean recursive programs in which predicate variables appear in conditions
• Clausal tableaux for hybrid PDL
• Well-structured program equivalence is highly undecidable
• scientific article; zbMATH DE number 2084328 (Why is no real title available?)
• scientific article; zbMATH DE number 3845549 (Why is no real title available?)
• scientific article; zbMATH DE number 3858391 (Why is no real title available?)
• PDL with intersection of programs: a complete axiomatization
• PDL with negation of atomic programs
• scientific article; zbMATH DE number 3912350 (Why is no real title available?)
• scientific article; zbMATH DE number 3924749 (Why is no real title available?)
• scientific article; zbMATH DE number 3968565 (Why is no real title available?)
• scientific article; zbMATH DE number 3979045 (Why is no real title available?)
• scientific article; zbMATH DE number 3983144 (Why is no real title available?)
• scientific article; zbMATH DE number 4010497 (Why is no real title available?)
• scientific article; zbMATH DE number 4033711 (Why is no real title available?)
• scientific article; zbMATH DE number 4045721 (Why is no real title available?)
• scientific article; zbMATH DE number 139632 (Why is no real title available?)
• Derivation rules as anti-axioms in modal logic
• scientific article; zbMATH DE number 1114354 (Why is no real title available?)
• PDL is the bisimulation-invariant fragment of weak chain logic
• Deterministic SQEMA and application for pre-contact logic
• From positive PDL to its non-classical extensions
• Automated Reasoning
• Computer Science Logic
• Propositional dynamic logic with program quantifiers
• PDL with Intersection and Converse Is 2EXP-Complete
• Undecidability of PDL with \(L=\{a^{2^ i}| i\geq 0\}\)
• 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

This page was built for publication: PDL with data constants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1065545)