An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability

Abstract. We present a tableau-based algorithm for deciding satisfiability for propositional dynamic logic (PDL) which builds a finite rooted tree with ancestor cycles and which passes extra information from children to parents to separate good cycles from bad cycles during backtracking. It is easy to implement, with potential for parallelisation, because it constructs a potential model “on the fly ” by exploring each tableau branch independently. However, its worst-case behaviour is 2EXPTIME rather than EXPTIME. We give detailed proofs of soundness and completeness in an appendix and there is a prototype implementation in the TWB (twb.rsise.anu.edu.au).