Modal µ-Calculus and Alternating Tree Automata
Modal µ-Calculus and Alternating Tree Automata
复制标题
模态 µ 微积分和交替树自动机
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
J. Zappe
中科院分区：
文献类型：
--
作者：
J. Zappe
模态 μ 演算是一种将简单模态运算符与定点运算符相结合以提供递归形式的逻辑。我们今天使用的模态 μ 微积分是由 Dexter Kozen [100] 于 1983 年提出的。它非常适合指定过渡系统的属性。因此，人们对模型检查和可满足性问题的有效解决方案产生了极大的兴趣。
The modal μ-calculus is a logic that combines simple modal operators with fixed point operators to provide a form of recursion. The modal μ-calculus—as we use it today—was introduced in 1983 by Dexter Kozen [100]. It is well suited for specifying properties of transition systems. For this reason, there is a great interest in efficient solutions of the model checking and the satisfiability problem.