Game Development Reference
In-Depth Information
so as to ensure that it has appropriate closure and duality properties (such
as closure under negation, De Morgan equalities, quantifier and fixed-point
dualities) to make it amenable to a game-based approach. But once this is
done, one can indeed construct a quantitative variant of parity games, and
prove that they are the appropriate model-checking games for the quantitative
μ -calculus. As in the classical setting the correspondence goes both ways: The
value of a formula in a structure coincides with the value of the associated
model-checking game, and conversely, the value of quantitative parity games
(with a bounded number of priorities) are definable in the quantitative μ -
calculus. However, the mathematical properties of quantitative parity games
are different from their qualitative counterparts. In particular, they are, in
general, not positionally determined, not even up to approximation, and
the proof that the quantitative model-checking games correctly describe the
value of the formulae is considerably more di cult than for the classical case.
As in the classical case, model-checking games lead to a better understand-
ing of the semantics and expressive power of the quantitative μ -calculus.
Further, the game-based approach also sheds light on the consequences of
different choices in the design of the quantitative formalism, which are far
less obvious than for classical logics.
4.7.1 Quantitative transition systems and quantitative μ -calculus
We write R
+ for the set of non-negative real numbers, and R
+
+
∪{∞} .
Quantitative transition systems (QTS) are directed graphs equipped
with quantities at states and with discounts of edges. They have the form
K
:= R
=( V,E,δ,
{
P i } i∈I ) where ( V,E ) is a directed graph, with a discount
+
+
function δ : E
, that assign to
each state the values of the predicates at that state. A transition system is
qualitative if all functions P i assign only the values 0 or
R
\{
0
}
and functions P i : V
R
, where 0 stands
for false and
for true , and it is non-discounted if δ ( e ) = 1 for all e
E .
+ and constants
Given predicate functions
{
P i } i∈I , discount factors d
R
+ , the quantitative μ -calculus is built in a similar way to the
modal μ -calculus, with the following two modifications.
c
R
(1) Atomic formulae have the form |P i
c
|
.
(2) If ϕ is a -formula, then so is d
·
ϕ ,
, and fixed-point
operators μ , ν are used as in the syntax of L μ . The semantics, however, is
quite different.
Formulae of are interpreted over quantitative transition systems
Boolean connectives
,
, modal operators
and
K
=