The Hybrid µ-Calculus
The Hybrid µ-Calculus
复制标题
DOI：
10.1007/3-540-45744-5_7
复制
发表时间：
2001-06
期刊：
影响因子：
--
通讯作者：
U. Sattler;Moshe Y. Vardi
中科院分区：
文献类型：
--
作者：
U. Sattler;Moshe Y. Vardi
我们提出了一个用标称和通用程序扩展的全μ-微积分（包括逆程序）的ExpTime决策过程，从而设计了一个新的、高表达的ExpTime逻辑。该决策过程基于树自动机，并明确了由标称引起的问题以及如何克服这些问题。粗略地说，我们展示了如何使用具有树模型属性的逻辑技术在缺乏树模型属性的逻辑中进行推理。本文的贡献是双重的：我们扩展了ExpTime逻辑家族，并且我们提出了一种在标称存在下进行推理的技术。
We present an ExpTime decision procedure for the full μ- Calculus (including converse programs) extended with nominals and a universal program, thus devising a new, highly expressive ExpTime logic. The decision procedure is based on tree automata, and makes explicit the problems caused by nominals and how to overcome them. Roughly speaking, we show how to reason in a logic lacking the tree model property using techniques for logics with the tree model property. The contribution of the paper is two-fold: we extend the family of ExpTime logics, and we present a technique to reason in the presence of nominals.