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

TL;DR

This paper introduces a tableau-based decision procedure for PDL satisfiability that constructs pseudo-models dynamically, enabling easier implementation and potential parallelization, despite its worst-case complexity being 2EXPTIME.

Contribution

It presents a novel on-the-fly tableau algorithm for PDL satisfiability that separates good and bad loops during backtracking, with a prototype implementation.

Findings

Algorithm is easy to implement and parallelize.

Constructs pseudo-models on the fly for each tableau branch.

Worst-case complexity is 2EXPTIME.

Abstract

We present a tableau-based algorithm for deciding satisfiability for propositional dynamic logic (PDL) which builds a finite rooted tree with ancestor loops and passes extra information from children to parents to separate good loops from bad loops during backtracking. It is easy to implement, with potential for parallelisation, because it constructs a pseudo-model ``on the fly'' by exploring each tableau branch independently. But its worst-case behaviour is 2EXPTIME rather than EXPTIME. A prototype implementation in the TWB (http://twb.rsise.anu.edu.au) is available.