An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability

Abstract. We give an optimal (exptime), sound and complete tableaubased 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.

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Florian Widmann, Rajeev Goré
• Keywords: Automated Reasoning, CADE 2009, Multiple Subsequent Passes, Propositional Dynamic Logic, Unoptimised Ocaml Implementation