On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic
On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic
复制标题
DOI：
10.1007/3-540-61604-7_60
复制
发表时间：
1996-08
期刊：
影响因子：
--
通讯作者：
David Janin;I. Walukiewicz
中科院分区：
文献类型：
--
作者：
David Janin;I. Walukiewicz
考虑过渡系统上的一元二阶逻辑（MSOL）。结果表明，每一个不区分双相似模型的MSOL公式都等价于命题M-演算的一个公式。这种表达完整性结果意味着在互模拟下不变且可转化为 MSOL 的过渡系统上的每个逻辑也可以转化为 M-演算。这给大多数程序命题逻辑可以转化为M-演算的说法提供了精确的含义。
Monadic second order logic (MSOL) over transition systems is considered. It is shown that every formula of MSOL which does not distinguish between bisimilar models is equivalent to a formula of the propositionalΜ-calculus. This expressive completeness result implies that every logic over transition systems invariant under bisimulation and translatable into MSOL can be also translated into theΜ-calculus. This gives a precise meaning to the statement that most propositional logics of programs can be translated into theΜ-calculus.