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

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.
26 pages, longer version of article in Methods for Modalities 2007; improved readability of proofs

Keywords

Logic in Computer Science

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/145382

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/0711.1016
 http://arxiv.org/abs/0711.1016

Collections

arXiv