Graded Computation Tree Logic with Binary Coding
Graded Computation Tree Logic with Binary Coding
复制标题
具有二进制编码的分级计算树逻辑
DOI：
10.1007/978-3-642-15205-4_13
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. Murano
中科院分区：
文献类型：
--
作者：
A. Bianco;F. Mogavero;A. Murano
渐变路径量词作为一种有效的框架被引入和研究，用于推广分支时间时间逻辑CTL （GCTL）中的标准存在路径量词和全称路径量词，使它们能够表达关于最小和保守数量的可达路径的陈述。这些量词自然地将分级世界模态的概念扩展到路径，这一概念已经被μ-微积分（Gμ-微积分）深入研究，它允许表达关于给定数量的可立即访问的世界的陈述。对于“非分级”情况，GCTL和Gμ-微积分的可满足性问题是一致的，特别是在exptime内仍然是可解的。然而，GCTL只研究了以一元编码的w.r.t.分级数，而Gμ- calculususfor此为二进制编码，并且决定相同的结果是否适用于二进制GCTL仍然是一个开放的问题。在本文中，通过利用自动机理论方法，其中涉及到一个与卫星交替的自动机模型，我们积极地回答了这个问题。我们进一步研究了二进制GCTL的简洁性，并证明它至少比Gμ-微积分在指数上更简洁性。
Graded path quantifiershave been recently introduced and investigated as a useful framework for generalizing standard existential and universal path quantifiers in the branching-time temporal logic CTL (GCTL), in such a way that they can express statements about a minimal and conservative number of accessible paths. These quantifiers naturally extend to paths the concept ofgraded world modalities, which has been deeply investigated for theμ- Calculus(Gμ- Calculus) where it allows to express statements about a given number of immediately accessible worlds. As for the ”non-graded” case, it has been shown that the satisfiability problem for GCTL and the Gμ- Calculuscoincides and, in particular, it remains solvable inExpTime. However, GCTL has been only investigated w.r.t. graded numbers coded in unary, while Gμ- Calculususes for this a binary coding, and it was left open the problem to decide whether the same result may or may not hold for binary GCTL. In this paper, by exploiting an automata theoretic-approach, which involves a model of alternating automata with satellites, we answer positively to this question. We further investigate the succinctness of binary GCTL and show that it is at least exponentially more succinct than Gμ- Calculus.