An Optimal Tableau Decision Procedure for Converse-PDL
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Conference paper (Refereed)
Proceedings of the 1st International Conference on Knowlegde and Systems Engineering (KSE)
2009 International Conference on Knowledge and Systems Engineering, Hanoi, 13-17 Oct.
IEEE Computer Society
Engineering and Technology
We give a novel tableau calculus and an optimal (EXPTIME) tableau decision procedure based on the calculus for the satisfiability problem of propositional dynamic logic with converse. Our decision procedure is formulated with global caching and can be implemented together with useful optimization techniques.