A Higher Order Modal Fixed Point Logic
A Higher Order Modal Fixed Point Logic
复制标题
高阶模态定点逻辑
DOI：
10.1007/978-3-540-28644-8_33
复制
发表时间：
2004
影响因子：
0.5
通讯作者：
R. Viswanathan
中科院分区：
文献类型：
--
作者：
Mahesh Viswanathan;R. Viswanathan
我们提出了一种高阶模态不动点逻辑（HFL），它扩展了模态μ演算，允许在谓词上使用递归定义的高阶函数来指定状态（状态集）上的谓词。逻辑HFL将否定作为一级构造，并使用一个简单的类型系统来识别单调函数，在单调函数上应用不动点算子是有语义意义的。有限过渡系统上HFL的模型检验问题是可判定的，但其表达形式丰富。我们构造了有限跃迁系统在不动点逻辑中不能用Chop[1]表示，但可以用HFL表示的一个性质。在无限过渡系统上，HFL可以表示下推自动机的双模拟和仿真，以及表示自然数的一类过渡系统的任何递归可枚举性质。
We present a higher order modal fixed point logic (HFL) that extends the modal μ-calculus to allow predicates on states (sets of states) to be specified using recursively defined higher order functions on predicates. The logic HFL includes negation as a first-class construct and uses a simple type system to identify the monotonic functions on which the application of fixed point operators is semantically meaningful. The model checking problem for HFL over finite transition systems remains decidable, but its expressiveness is rich. We construct a property of finite transition systems that is not expressible in the Fixed Point Logic with Chop [1] but which can be expressed in HFL. Over infinite transition systems, HFL can express bisimulation and simulation of push down automata, and any recursively enumerable property of a class of transition systems representing the natural numbers.