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

@misc{citeulike:2178397, 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 (<a href="http://twb.rsise.anu.edu.au">this http URL</a>) is available.}, author = {Abate, Pietro and Gor\&\#xe9;, Rajeev and Widmann, Florian }, citeulike-article-id = {2178397}, eprint = {0711.1016}, keywords = {modal-logic}, month = {Nov}, posted-at = {2007-12-29 02:20:51}, priority = {2}, title = {An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability}, url = {http://arxiv.org/abs/0711.1016}, year = {2007} }

TY - ELEC ID - citeulike:2178397 L3 - citeulike-article-id:2178397 TI - An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability N2 - 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 (<a href="http://twb.rsise.anu.edu.au">this http URL</a>) is available. KW - modal-logic AU - Abate, Pietro AU - Gor&#xe9;, Rajeev AU - Widmann, Florian PY - 2007/Nov/07/ UR - http://arxiv.org/abs/0711.1016 ER -