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

'''NB''': We are working to make the implementation of this calculus available on this website by the end of the week. '''UPDATE''': * pdlMarkedNoSnf.ml : http://twb.rsise.anu.edu.au/propositional_dynamic_logic_no_snf * pdlMarked.ml: http://twb.rsise.anu.edu.au/propositional_dynamic_logic_snf alternatively you can also check this out : http://users.rsise.anu.edu.au/~rpg/pdlweb/ paper accepted to m4m http://m4m.loria.fr/M4M5/ ==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. We implemented two provers (that will be shortly in the website demo section): ===pdlMarked.ml: === This version of PDL first transforms formulae into a *-normal form defined in the associated paper. The conversion to *-normal form can result in a blow up of the given formula e.g. < * * a > p gets converted to < (a ; *a) ; * (a ; *a) > p. Since this is suboptimal, there is another prover that does not require *-normal form. The rules of that prover are currently being written up. ===pdlMarkedNoSnf.ml: === This version of PDL uses just negation normal form and does not require a *-normal form. The rules of this prover are more complicated and their proofs are currently being written up.
AttachmentSize
abate-gore-widmann-pdl-m4m07.pdf289.97 KB