关于定量μ演算qMu的结果
Results on the quantitative mu-calculus qMu
摘要：
μ演算是一个强大的工具，用于指定和验证过渡系统，包括那些恶魔和天使的选择;其定量推广qMu扩展到概率选择。我们表明，对于有限状态系统的qMu的逻辑解释，通过在一个域中的实值函数到[0，1]的不动点，是相当于一个操作的解释作为一个基于回合的赌博游戏之间的两个球员。逻辑解释提供了对公理、定律和元定理的直接存取。可操作的、基于游戏的解释有助于直觉，并在更一般的上下文中继续提供令人惊讶的实用规范工具。我们的证明的一个推论是埃弗雷特的单嵌套游戏的结果在有限的回合制的情况下的延伸：我们证明了良好的定义的极大极小值，并存在固定的无记忆策略，为所有qMu游戏/公式，任意（包括交替）嵌套结构。
英文摘要：
The mu-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic and angelic choice; its quantitative generalisation qMu extends that to probabilistic choice. We show that for a finite-state system the logical interpretation of qMu, via fixed-points in a domain of real-valued functions into [0,1], is equivalent to an operational interpretation given as a turn-based gambling game between two players. The logical interpretation provides direct access to axioms, laws and meta-theorems. The operational, game- based interpretation aids the intuition and continues in the more general context to provide a surprisingly practical specification tool. A corollary of our proofs is an extension of Everett's singly-nested games result in the finite turn-based case: we prove well-definedness of the minimax value, and existence of fixed memoriless strategies, for all qMu games/formulae, of arbitrary (including alternating) nesting structure.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
