• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual Symposium on Theoretical Aspects of Computer Science(STACS 2004); 20040325-20040327; Montpellier; FR >A Measured Collapse of the Modal μ-Calculus Alternation Hierarchy
【24h】

A Measured Collapse of the Modal μ-Calculus Alternation Hierarchy

机译：模态微积分交替层次的测度崩溃

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The μ-calculus model-checking problem has been of great interest in the context of concurrent programs. Beyond the need to use symbolic methods in order to cope with the state-explosion problem, which is acute in concurrent settings, several concurrency related problems are naturally solved by evaluation of μ-calculus formulas. The complexity of a naive algorithm for model checking a μ-calculus formula ψ is exponential in the alternation depth d of ψ. Recent studies of the μ-calculus and the related area of parity games have led to algorithms exponential only in d/2. No symbolic version, however, is known for the improved algorithms, sacrificing the main practical attraction of the μ-calculus. The μ-calculus can be viewed as a fragment of first-order fixpoint logic. One of the most fundamental theorems in the theory of fixpoint logic is the Collapse Theorem, which asserts that, unlike the case for the μ-calculus, the fixpoint alternation hierarchy over finite structures collapses at its first level. In this paper we show that the Collapse Theorem of fixpoint logic holds for a measured variant of the μ-calculus, which we call μ~#-calculus. While μ-calculus formulas represent characteristic functions, i.e., functions from the state space to {0,1}, formulas of the μ~#-calculus represent measure functions, which are functions from the state space to some measure domain. We prove a Measured-Collapse Theorem: every formula in the μ-calculus is equivalent to a least-fixpoint formula in the μ~#-calculus. We show that the Measured-Collapse Theorem provides a logical recasting of the improved algorithm for μ-calculus model-checking, and describe how it can be implemented symbolically using Algebraic Decision Diagrams. Thus, we describe, for the first time, a symbolic μ-calculus model-checking algorithm whose complexity matches the one of the best known enumerative algorithm.
机译：μ-演算模型检查问题在并发程序的上下文中引起了极大的兴趣。除了需要使用符号方法来解决状态爆炸问题（在并发设置中很严重）之外，通过评估微积分公式自然可以解决一些与并发相关的问题。用于检查微积分公式ψ的模型的朴素算法的复杂度在ψ的交替深度d中呈指数级。 μ演算和奇偶游戏相关领域的最新研究导致算法仅在d / 2中呈指数级。但是，对于改进的算法（牺牲微积分的主要实际吸引力），没有象征性的版本。 μ演算可以看作是一阶定点逻辑的一部分。定点逻辑理论中最基本的定理之一是崩溃定理，该定理断言，与μ演算不同，有限结构上的定点交替层次在其第一级崩溃。在本文中，我们证明了定点逻辑的崩溃定理适用于测微μ演算的变体，我们称之为μ〜＃演算。 μ演算公式表示特征函数，即从状态空间到{0,1}的函数，而μ〜＃演算的公式表示度量函数，它们是从状态空间到某个度量域的函数。我们证明了测度崩溃定理：μ演算中的每个公式都等同于μ〜＃演算中的最小定点公式。我们证明了度量折叠定理为μ演算模型检查提供了改进算法的逻辑重铸，并描述了如何使用代数决策图象征性地实现它。因此，我们首次描述了一种符号μ演算模型检查算法，该算法的复杂度与最著名的枚举算法之一相匹配。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号