On the expressive power of CTL
On the expressive power of CTL
复制标题
论CTL的表达能力
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
A. Rabinovich
中科院分区：
文献类型：
--
作者：
F. Moller;A. Rabinovich
我们表明，表达能力的分支时间逻辑CTL相一致的互模拟不变性质的类表示在所谓的一元路径逻辑：一元二阶逻辑，其中集量化被限制到路径。为了证明这个结果，我们首先证明了一个新的树的合成定理。这种方法是改编自Hafer和托马斯的方法，在他们的证明，CTL符合整个一元路径逻辑类的满二叉树。
We show that the expressive power of the branching time logic CTL coincides with that of the class of bisimulation invariant properties expressible in so-called monadic path logic: monadic second order logic in which set quantification is restricted to paths. In order to prove this result, we first prove a new composition theorem for trees. This approach is adapted from the approach of Hafer and Thomas in their proof that CTL coincides with the whole of monadic path logic over the class of full binary trees.