A near-optimal method for reasoning about action
From MaRDI portal
Publication:1134756
DOI10.1016/0022-0000(80)90061-6zbMath0424.03010OpenAlexW1997716585MaRDI QIDQ1134756
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
satisfiability problemtableau methodpropositional dynamic logicprogram verificationexponential timeacceptance problem for linear-space-bounded alternating Turing machinedecision methodHintikka set
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
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
