Games, Probability, and the Quantitative μ-Calculus qMμ
Logic for Programming, Artificial Intelligence, and Reasoning: 9th …, 2002•Springer
The μ-calculus is a powerful tool for specifying and verifying transition systems, including
those with demonic (universal) and angelic (existential) choice; its quantitative
generalisation qMμ extends that to probabilistic choice. We show for a finite-state system
that the straightforward denotational interpretation of the quantitative μ-calculus is equivalent
to an operational interpretation given as a turn-based gambling game between two players.
Kozen defined the standard Boolean-typed calculus denotationally; later Stirling gave it an …
those with demonic (universal) and angelic (existential) choice; its quantitative
generalisation qMμ extends that to probabilistic choice. We show for a finite-state system
that the straightforward denotational interpretation of the quantitative μ-calculus is equivalent
to an operational interpretation given as a turn-based gambling game between two players.
Kozen defined the standard Boolean-typed calculus denotationally; later Stirling gave it an …
Abstract
The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with demonic (universal) and angelic (existential) choice; its quantitative generalisation qMμ extends that to probabilistic choice. We show for a finite-state system that the straightforward denotational interpretation of the quantitative μ-calculus is equivalent to an operational interpretation given as a turn-based gambling game between two players.
Kozen defined the standard Boolean-typed calculus denotationally; later Stirling gave it an operational interpretation as a turn-based game between two players, and showed the two interpretations equivalent. By doing the same for the quantitative real-typed calculus, we set it on a par with the standard calculus, in that it too can benefit from a solid interface linking the logical and operational frameworks.
Stirling’s game analogy, as an aid to intuition, continues in the more general context to provide a surprisingly practical specification tool, meeting for example Vardi’s challenge to “figure out the meaning of AF AXp” as a branching-time formula.
We also show that memoriless strategies suffice for achieving the minimax value of a quantitative game, when the state space is finite.
Springer
以上显示的是最相近的搜索结果。 查看全部搜索结果