Skip navigation
Skip navigation

An on-the-fly Tableau-based decision procedure for PDL-satisfiability

Abate, Pietro; Gore, Rajeev; Widmann, Florian


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]

CollectionsANU Research Publications
Date published: 2009
Type: Conference paper
Source: Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)
DOI: 10.1007/978-3-642-02959-2_32


File Description SizeFormat Image
01_Abate_An_on-the-fly_Tableau-based_2009.pdf282.56 kBAdobe PDF    Request a copy

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

Updated:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator