一种基于 tableau 的 PDL 可满足性即时判定过程
计算机科学中的逻辑
2008-01-08 v2
摘要
我们提出了一种基于 tableau 的算法，用于判定命题动态逻辑 (PDL) 的可满足性。该算法构建一个带有祖先循环的有限根树，并在回溯过程中将额外信息从子节点传递到父节点，以区分好循环与坏循环。该算法易于实现且具有并行化潜力，因为它通过独立探索每个 tableau 分支来“即时”构建伪模型。但其最坏情况时间复杂度为 2EXPTIME 而非 EXPTIME。基于 TWB (http://twb.rsise.anu.edu.au) 的原型实现可供使用。
引用
@article{arxiv.0711.1016,
title = {An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability},
author = {Pietro Abate and Rajeev Goré and Florian Widmann},
journal= {arXiv preprint arXiv:0711.1016},
year = {2008}
}
评论
26 pages, longer version of article in Methods for Modalities 2007; improved readability of proofs