Combining deduction and model checking into tableaux and algorithms for converse-PDL.

DOI10.1006/inco.1999.2852zbMath1045.68090OpenAlexW2087882226MaRDI QIDQ1854371

Giuseppe De Giacomo, Fabio Massacci

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/35641317eceb456014a1e333f89a73301b81abbc

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Related Items (15)

Extending propositional dynamic logic for Petri nets ⋮ Converse-PDL with regular inclusion axioms: a framework for MAS logics ⋮ Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition ⋮ Data complexity of query answering in expressive description logics via tableaux ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ A calculus for automatic verification of Petri nets based on resolution and dynamic logics ⋮ Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse ⋮ 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 ⋮ Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs ⋮ Clausal Tableaux for Hybrid PDL ⋮ ExpTime tableau decision procedures for regular grammar logics with converse ⋮ Testing XML constraint satisfiability ⋮ A goal-directed decision procedure for hybrid PDL

Cites Work

• Unnamed Item
• Unnamed Item
• Proof methods for modal and intuitionistic logics
• Automata-theoretic techniques for modal logics of programs
• An automata theoretic decision procedure for the propositional mu- calculus
• A near-optimal method for reasoning about action
• Local model checking in the modal mu-calculus
• A guide to completeness and complexity for modal logics of knowledge and belief
• The KL-ONE family
• Propositional dynamic logic of regular programs
• A modal perspective on the computational complexity of attribute value grammar
• Reasoning about infinite computations
• Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
• Eliminating ``converse from converse PDL
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• Tableaux and algorithms for Propositional Dynamic Logic with Converse
• Strongly analytic tableaux for normal modal logics
• A practical decision method for propositional dynamic logic (Preliminary Report)

This page was built for publication: Combining deduction and model checking into tableaux and algorithms for converse-PDL.