Game Development Reference
InDepth Information
so as to ensure that it has appropriate closure and duality properties (such
as closure under negation, De Morgan equalities, quantifier and fixedpoint
dualities) to make it amenable to a gamebased approach. But once this is
done, one can indeed construct a quantitative variant of parity games, and
prove that they are the appropriate modelchecking 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
modelchecking 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 modelchecking games correctly describe the
value of the formulae is considerably more di
cult than for the classical case.
As in the classical case, modelchecking games lead to a better understand
ing of the semantics and expressive power of the quantitative
μ
calculus.
Further, the gamebased 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 nonnegative 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
nondiscounted
if
δ
(
e
) = 1 for all
e
∈
E
.
+
and constants
Given predicate functions
{
P
i
}
i∈I
, discount factors
d
∈
R
+
, the
quantitative
μ
calculus
Qμ
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
Qμ
formula, then so is
d
·
ϕ
,
, and fixedpoint
operators
μ
,
ν
are used as in the syntax of
L
μ
. The semantics, however, is
quite different.
Formulae of
Qμ
are interpreted over quantitative transition systems
Boolean connectives
∧
,
∨
, modal operators
♦
and
K
=
Search Nedrilad ::
Custom Search