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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Description Logic
- Preliminary Experimental Result
- Transition Frame
- Propositional Dynamic Logic
- Negation Normal Form
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Fisher, M., Ladner, R.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (1979)
Pratt, V.R.: A near-optimal method for reasoning about action. Journal of Computer and System Sciences 20(2), 231–254 (1980)
Baader, F.: Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles. In: Proc. IJCAI 1991, pp. 446–451 (1991)
De Giacomo, G., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for Converse-PDL. Inf. and Comp. 162, 117–137 (2000)
Vardi, M., Wolper, P.: Automata theoretic techniques for modal logics of programs. Journal of Computer and System Sciences 32(2), 183–221 (1986)
Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for the modal logic K. Journal of Applied Non-Classical Logics 16(1-2), 169–208 (2006)
Lange, M., Stirling, C.: Focus games for satisfiability and completeness of temporal logic. In: Proc. LICS 2001, pp. 357–365. IEEE Computer Society, Los Alamitos (2001)
Brünnler, K., Lange, M.: Cut-free sequent systems for temporal logic. Journal of Logic and Algebraic Programming 76(2), 216–225 (2008)
Goré, R., Nguyen, L.A.: EXPTIME tableaux for ALC using sound global caching. In: Proc. of the International Workshop on Description Logics (DL 2007) (2007)
Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. Journal of Logic and Computation 9(3), 267–293 (1999)
Abate, P., Goré, R., Widmann, F.: An on-the-fly tableau-based decision procedure for PDL-satisfiability. Electr. Notes Theor. Comput. Sci. 231, 191–209 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goré, R., Widmann, F. (2009). An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. In: Schmidt, R.A. (eds) Automated Deduction – CADE-22. CADE 2009. Lecture Notes in Computer Science(), vol 5663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02959-2_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-02959-2_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02958-5
Online ISBN: 978-3-642-02959-2
eBook Packages: Computer ScienceComputer Science (R0)