The propositional dynamic logic of deterministic, well-structured programs

DOI10.1016/0304-3975(83)90097-XzbMATH Open0552.68035OpenAlexW2101982422MaRDI QIDQ801682FDOQ801682

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

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

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)

Cites Work

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

Cited In (51)

• Title not available (Why is that?)
• A multiprocess network logic with temporal and spatial modalities
• Extracting unsatisfiable cores for LTL via temporal resolution
• Succinct representation of regular sets using gotos and Boolean variables
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• PDL with negation of atomic programs
• Propositional dynamic logic of context-free programs and fixpoint logic with chop
• Belief, awareness, and limited reasoning
• Dynamic logic of propositional assignments: a well-behaved variant of PDL
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Propositional dynamic logic with program quantifiers
• Mechanizing common knowledge logic using COQ
• Title not available (Why is that?)
• A decision procedure for combinations of propositional temporal logic and other specialized theories
• Title not available (Why is that?)
• 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
• From Monadic Logic to PSL
• 2-Exp Time lower bounds for propositional dynamic logics with intersection
• Title not available (Why is that?)
• An essay in combinatory dynamic logic
• The complexity of reasoning about knowledge and time. I: Lower bounds
• From Philosophical to Industrial Logics
• Title not available (Why is that?)
• Dynamic logic as a uniform framework for theorem proving in intensional logic
• Model checking propositional dynamic logic with all extras
• Well-structured program equivalence is highly undecidable
• Title not available (Why is that?)
• Title not available (Why is that?)
• Deterministic dynamic logic is strictly weaker than dynamic logic
• Classifying the computational complexity of problems
• The complexity of PDL with interleaving
• A dynamic logic for QASM programs
• Frame theory, dependence logic and strategies
• Propositional dynamic logic with storing, recovering and parallel composition
• Modal restriction semigroups: towards an algebra of functions.
• PDL inside the \(\mu\)-calculus: a syntactic and an automata-theoretic characterization
• Automated Reasoning
• Propositional dynamic logic of nonregular programs
• Foundations of Software Science and Computation Structures
• PDL with data constants

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)