The propositional dynamic logic of deterministic, well-structured programs

DOI10.1016/0304-3975(83)90097-XMaRDI QIDQ801682zbMATH OpenOpenAlexFDO

Authors Joseph Y. Halpern, J. Reif

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)

Recommendations

• scientific article; zbMATH DE number 3848600
• Propositional dynamic logic with recursive programs
• Foundations of Software Science and Computation Structures
• Propositional dynamic logic of nonregular programs
• Decision complexity of variants of propositional dynamic logic

Cites work

• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3772936 (Why is no real title available?)
• scientific article; zbMATH DE number 3778723 (Why is no real title available?)
• scientific article; zbMATH DE number 3791602 (Why is no real title available?)
• scientific article; zbMATH DE number 3802801 (Why is no real title available?)
• scientific article; zbMATH DE number 3803410 (Why is no real title available?)
• scientific article; zbMATH DE number 3315203 (Why is no real title available?)
• scientific article; zbMATH DE number 3351505 (Why is no real title available?)
• A near-optimal method for reasoning about action
• An elementary proof of the completeness of PDL
• Deterministic propositional dynamic logic: finite models, complexity, and completeness
• Expressing program looping in regular dynamic logic
• Propositional dynamic logic of regular programs
• Relationships between nondeterministic and deterministic tape complexities
• Theory of program structures: Schemes, semantics, verification

Cited in

(51)

• A multiprocess network logic with temporal and spatial modalities
• Extracting unsatisfiable cores for LTL via temporal resolution
• scientific article; zbMATH DE number 7317262 (Why is no real title available?)
• Succinct representation of regular sets using gotos and Boolean variables
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• scientific article; zbMATH DE number 4039864 (Why is no real title available?)
• scientific article; zbMATH DE number 4045721 (Why is no real title available?)
• scientific article; zbMATH DE number 4008371 (Why is no real title available?)
• Propositional dynamic logic of context-free programs and fixpoint logic with chop
• PDL with negation of atomic programs
• Belief, awareness, and limited reasoning
• Dynamic logic of propositional assignments: a well-behaved variant of PDL
• scientific article; zbMATH DE number 3974280 (Why is no real title available?)
• scientific article; zbMATH DE number 3848600 (Why is no real title available?)
• A practical decision method for propositional dynamic logic (preliminary report)
• A probabilistic PDL
• A sound and complete Hoare logic for dynamically-typed, object-oriented programs
• The complexity of propositional linear temporal logics in simple cases
• Mechanizing common knowledge logic using COQ
• Propositional dynamic logic with program quantifiers
• scientific article; zbMATH DE number 4079387 (Why is no real title available?)
• A decision procedure for combinations of propositional temporal logic and other specialized theories
• scientific article; zbMATH DE number 4068839 (Why is no real title available?)
• Propositional dynamic logic with recursive programs
• Independence in dynamically scheduled logic languages
• On proving properties of completion strategies
• Decision complexity of variants of propositional dynamic logic
• scientific article; zbMATH DE number 3880104 (Why is no real title available?)
• From Monadic Logic to PSL
• 2-Exp Time lower bounds for propositional dynamic logics with intersection
• An essay in combinatory dynamic logic
• The complexity of reasoning about knowledge and time. I: Lower bounds
• From Philosophical to Industrial Logics
• scientific article; zbMATH DE number 3912350 (Why is no real title available?)
• Model checking propositional dynamic logic with all extras
• Dynamic logic as a uniform framework for theorem proving in intensional logic
• Well-structured program equivalence is highly undecidable
• A dynamic logic for QASM programs
• scientific article; zbMATH DE number 4143953 (Why is no real title available?)
• scientific article; zbMATH DE number 3979045 (Why is no real title available?)
• The complexity of PDL with interleaving
• Deterministic dynamic logic is strictly weaker than dynamic logic
• Classifying the computational complexity of problems
• Frame theory, dependence logic and strategies
• Propositional dynamic logic with storing, recovering and parallel composition
• Modal restriction semigroups: towards an algebra of functions.
• Propositional dynamic logic of nonregular programs
• PDL inside the \(\mu\)-calculus: a syntactic and an automata-theoretic characterization
• Automated Reasoning
• PDL with data constants
• Foundations of Software Science and Computation Structures

This page was built for publication: The propositional dynamic logic of deterministic, well-structured programs

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