An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability

Rajeev Goré*, Florian Widmann

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    22 Citations (Scopus)

    Abstract

    We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic. Our main contribution is a sound method to track unfulfilled eventualities "on the fly" which allows us to detect "bad loops" sooner rather than in multiple subsequent passes. We achieve this by propagating and updating the "status" of nodes throughout the underlying graph as soon as is possible. We give sufficient details to enable an easy implementation by others. Preliminary experimental results from our unoptimised OCaml implementation indicate that our algorithm is feasible.

    Original languageEnglish
    Title of host publicationAutomated Deduction - CADE-22 - 22nd International Conference on Automated Deduction, Proceedings
    Pages437-452
    Number of pages16
    DOIs
    Publication statusPublished - 2009
    Event22nd International Conference on Automated Deduction, CADE-22 - Montreal, QC, Canada
    Duration: 2 Aug 20097 Aug 2009

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume5663 LNAI
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference22nd International Conference on Automated Deduction, CADE-22
    Country/TerritoryCanada
    CityMontreal, QC
    Period2/08/097/08/09

    Fingerprint

    Dive into the research topics of 'An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability'. Together they form a unique fingerprint.

    Cite this