A near-optimal method for reasoning about action

DOI10.1016/0022-0000(80)90061-6zbMath0424.03010OpenAlexW1997716585MaRDI QIDQ1134756

Vaughan R. Pratt

Publication date: 1980

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(80)90061-6

zbMATH Keywords

satisfiability problemtableau methodpropositional dynamic logicprogram verificationexponential timeacceptance problem for linear-space-bounded alternating Turing machinedecision methodHintikka set

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 (44)

Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL ⁺ ⋮ Automata-theoretic techniques for modal logics of programs ⋮ Converse-PDL with regular inclusion axioms: a framework for MAS logics ⋮ Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition ⋮ The complexity of PDL with interleaving ⋮ ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching ⋮ Dynamic extensions of arrow logic ⋮ On the complexity of input/output logic ⋮ On the Decision Problem for Two-Variable First-Order Logic ⋮ Unnamed Item ⋮ Free Kleene algebras with domain ⋮ Mathematical modal logic: A view of its evolution ⋮ Process logic: Expressiveness, decidability, completeness ⋮ On the computational complexity of satisfiability in propositional logics of programs ⋮ Logical approaches to deontic reasoning: From basic questions to dynamic solutions ⋮ Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic ⋮ Dynamic algebras: Examples, constructions, applications ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ Tableaux and algorithms for Propositional Dynamic Logic with Converse ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ Terminating Tableaux for Hybrid Logic with Eventualities ⋮ A Tableau Calculus for Regular Grammar Logics with Converse ⋮ An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability ⋮ From Philosophical to Industrial Logics ⋮ Fuzzy Description Logic Reasoning Using a Fixpoint Algorithm ⋮ From Monadic Logic to PSL ⋮ PDL with intersection and converse: satisfiability and infinite-state model checking ⋮ ExpTime tableaux with global caching for hybrid PDL ⋮ Clausal Tableaux for Hybrid PDL ⋮ An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability ⋮ ExpTime tableau decision procedures for regular grammar logics with converse ⋮ BDD-based decision procedures for the modal logic K ★ ⋮ The model checking fingerprints of CTL operators ⋮ Deterministic propositional dynamic logic: finite models, complexity, and completeness ⋮ The temporal logic of branching time ⋮ Propositional dynamic logic of nonregular programs ⋮ Combining deduction and model checking into tableaux and algorithms for converse-PDL. ⋮ Module checking ⋮ Tarskian set constraints ⋮ The propositional dynamic logic of deterministic, well-structured programs ⋮ Results on the propositional \(\mu\)-calculus ⋮ A modal logic of epistemic games ⋮ Complexity analysis of propositional concurrent programs using domino tiling ⋮ A goal-directed decision procedure for hybrid PDL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mathematical thought. An introduction to the philosophy of mathematics
• The intrinsically exponential complexity of the circularity problem for attribute grammars
• Prospects and Limitations of Automatic Assertion Generation for Loop Programs
• Programming as a Discipline of Mathematical Nature
• The synthesis of loop predicates
• A practical decision method for propositional dynamic logic (Preliminary Report)
• Trees and nest structures
• An axiomatic basis for computer programming
• Characterizations of Pushdown Machines in Terms of Time-Bounded Computers

This page was built for publication: A near-optimal method for reasoning about action