Skip navigation
Skip navigation

An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability

Request a Copy

link to publisher version

  • Altmetric Citations

Gore, Rajeev; Widmann, Florian

Description

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...[Show more]

dc.contributor.authorGore, Rajeev
dc.contributor.authorWidmann, Florian
dc.coverage.spatialMontreal Canada
dc.date.accessioned2015-12-07T22:18:46Z
dc.date.createdAugust 2-7 2009
dc.identifier.isbn3642029582
dc.identifier.urihttp://hdl.handle.net/1885/18980
dc.description.abstractWe 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.
dc.publisherSpringer
dc.relation.ispartofseriesInternational Conference on Automated Deduction (CADE 2009)
dc.sourceProceedings of the 22nd International Conference on Automated Deduction
dc.source.urihttp://www.springerlink.com/content/978-3-642-02958-5/
dc.subjectKeywords: Decision procedure; On the flies; On-the-fly; Propositional dynamic logic; Satisfiability; Underlying graphs; Automation; Embedded systems
dc.titleAn Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability
dc.typeConference paper
local.description.notesImported from ARIES
local.description.refereedYes
dc.date.issued2009
local.identifier.absfor010107 - Mathematical Logic, Set Theory, Lattices and Universal Algebra
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.ariespublicationu4607519xPUB6
local.type.statusPublished Version
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANU
local.contributor.affiliationWidmann, Florian, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.startpage437
local.bibliographicCitation.lastpage452
local.identifier.doi10.1007/978-3-642-02959-2_32
dc.date.updated2016-02-24T11:13:56Z
local.identifier.scopusID2-s2.0-69949184446
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Gore_An_Optimal_On-the-fly_2009.pdf281.84 kBAdobe PDF    Request a copy
Show simple item record


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator