Characterizing EF over Infinite Trees and Modal Logic on Transitive Graphs
Characterizing EF over Infinite Trees and Modal Logic on Transitive Graphs
复制标题
描述无限树上的 EF 和传递图上的模态逻辑
DOI：
10.1007/978-3-642-22993-0_28
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Alessandro Facchini
中科院分区：
文献类型：
--
作者：
B. T. Cate;Alessandro Facchini
我们提供了任意树上 EF（后代关系的模态逻辑）的几个有效的等价表征。更具体地说，我们证明，对于树的 EF 互模拟不变属性，可以通过 EF 公式定义、是 Borel 集、可以用弱一元二阶逻辑定义，所有这些都是一致的。该证明建立在 Bojanczyk 和 Idziaszek 提出的有限分支树情况下 EF 的已知代数表征之上。我们还获得了传递克里普克结构上模态逻辑的表征，作为弱单子二阶逻辑和 µ 微积分的片段。
We provide several effective equivalent characterizations of EF (the modal logic of the descendant relation) on arbitrary trees. More specifically, we prove that, for EF-bisimulation invariant properties of trees, being definable by an EF formula, being a Borel set, and being definable in weak monadic second order logic, all coincide. The proof builds upon a known algebraic characterization of EF for the case of finitely branching trees due to Bojanczyk and Idziaszek. We furthermore obtain characterizations of modal logic on transitive Kripke structures as a fragment of weak monadic second order logic and of the µ-calculus.
DOI：
10.1016/j.apal.2009.04.002
发表时间：
2009
期刊：
20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05)
影响因子：
--
作者：
A. Dawar;M. Otto
通讯作者：
M. Otto