The propositional dynamic logic of deterministic, well-structured programs

DOI10.1016/0304-3975(83)90097-XzbMath0552.68035OpenAlexW2101982422MaRDI QIDQ801682

John H. Reif, Joseph Y. Halpern

Publication date: 1983

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(83)90097-x

zbMATH Keywords

determinismexpressivenesspropositional dynamic logicdecision procedurepolynomial space completenessregular programsvalidity problemswell- structured programs

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Complexity of computation (including implicit computational complexity) (03D15)

Related Items

Extracting unsatisfiable cores for LTL via temporal resolution, On proving properties of completion strategies, Frame Theory, Dependence Logic and Strategies, Belief, awareness, and limited reasoning, A decision procedure for combinations of propositional temporal logic and other specialized theories, Succinct representation of regular sets using gotos and Boolean variables, Mechanizing common knowledge logic using COQ, The complexity of reasoning about knowledge and time. I: Lower bounds, Classifying the computational complexity of problems, Enhancing unsatisfiable cores for LTL with information on temporal relevance, From Philosophical to Industrial Logics, From Monadic Logic to PSL, MODAL RESTRICTION SEMIGROUPS: TOWARDS AN ALGEBRA OF FUNCTIONS, A multiprocess network logic with temporal and spatial modalities, The complexity of propositional linear temporal logics in simple cases, An essay in combinatory dynamic logic

Cites Work

• A near-optimal method for reasoning about action
• An elementary proof of the completeness of PDL
• Expressing program looping in regular dynamic logic
• Theory of program structures: Schemes, semantics, verification
• Propositional dynamic logic of regular programs
• Deterministic propositional dynamic logic: finite models, complexity, and completeness
• Relationships between nondeterministic and deterministic tape complexities
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item