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

DOI10.1006/INCO.1999.2852zbMATH Open1045.68090OpenAlexW2087882226MaRDI QIDQ1854371FDOQ1854371

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)

Cites Work

• Propositional dynamic logic of regular programs
• Title not available (Why is that?)
• Reasoning about infinite computations
• Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
• A guide to completeness and complexity for modal logics of knowledge and belief
• 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
• Title not available (Why is that?)
• Proof methods for modal and intuitionistic logics
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• Strongly analytic tableaux for normal modal logics
• A practical decision method for propositional dynamic logic (Preliminary Report)
• Local model checking in the modal mu-calculus
• Tableaux and algorithms for Propositional Dynamic Logic with Converse
• A modal perspective on the computational complexity of attribute value grammar
• The KL-ONE family
• Eliminating ``converse from converse PDL

Cited In (15)

• A calculus for automatic verification of Petri nets based on resolution and dynamic logics
• Extending propositional dynamic logic for Petri nets
• Converse-PDL with regular inclusion axioms: a framework for MAS logics
• Data complexity of query answering in expressive description logics via tableaux
• Terminating Tableaux for Hybrid Logic with Eventualities
• Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
• Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition
• Clausal tableaux for hybrid PDL
• A Tableau Calculus for Regular Grammar Logics with Converse
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• A goal-directed decision procedure for hybrid PDL
• Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
• ExpTime tableau decision procedures for regular grammar logics with converse
• Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics
• Testing XML constraint satisfiability

   Recommendations

• Tableaux and algorithms for Propositional Dynamic Logic with Converse 👍 👎
• Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse 👍 👎
• And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL 👍 👎
• Model checking propositional dynamic logic with all extras 👍 👎
• An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability 👍 👎

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

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