A Decision Procedure for CTL* Based on Tableaux and Automata
A Decision Procedure for CTL* Based on Tableaux and Automata
复制标题
DOI：
10.1007/978-3-642-14203-1_28
复制
发表时间：
2010-07
期刊：
影响因子：
--
通讯作者：
Oliver Friedmann;Markus Latte;M. Lange
中科院分区：
文献类型：
--
作者：
Oliver Friedmann;Markus Latte;M. Lange
给出了一个基于无限分支上全局条件表的全分支时间逻辑CTL*的决策过程。这些条件可以用自动机机器来检查。然后，决策过程由解决奇偶对策问题的双指数化简组成。这比现有的CTL*决策过程，特别是自动机理论的决策过程有优势：底层表只对输入公式的子公式起作用。这种表格的结构和输入公式之间的关系是由非常直观的表格规则给出的。此外，在theMLSolvertool中使用该过程的实现进行的运行时实验表明，在问题的计算复杂度为2EXPTIME-complete的限制下，该方法具有实用性。
We present a decision procedure for the full branching-time logic CTL*which is based on tableaux with global conditions on infinite branches. These conditions can be checked using automata-theoretic machinery. The decision procedure then consists of a doubly exponential reduction to the problem of solving a parity game. This has advantages over existing decision procedures for CTL*, in particular the automata-theoretic ones: the underlying tableaux only work on subformulas of the input formula. The relationship between the structure of such tableaux and the input formula is given by very intuitive tableau rules. Furthermore, runtime experiments with an implementation of this procedure in theMLSolvertool show the practicality of this approach within the limits of the problem’s computational complexity of being 2EXPTIME-complete.