Game Development Reference
(whose distances are stored in d 0 ,...,d i ) remain unchanged and the play
continues on priority j without any active backtracking moves on priorities
greater than i .
It is not di cult to express all this in first-order logic, provided an ordering
on priorities is available. For nodes where Player 1 moves the construction is
Exercise 4.7 Make the construction of the formulae ψ σ explicit, and prove
that they indeed define the winning region for Player σ .
Winning regions of simple backtracking games are definable
in IFP .
4.7 Logic and games in a quantitative setting
Common logical formalisms are two-valued and express qualitative properties.
There have been a number of proposals to extend logics such as propositional
modal logic ML, the temporal logics LTL and CTL, and the modal μ -calculus
L μ to quantitative formalisms where formulae can take, at a given state
of a system, not just the values true and false , but quantitative values, for
instance real numbers. There are several scenarios and applications where
it is desirable to replace purely qualitative statements by quantitative ones
which can be of very different nature: we may be interested in the probability
of an event, the value that we assign to an event may depend on to how
late it occurs, we can ask for the number of occurrences of an event in a
play, and so on. We can consider transition structures, where already the
atomic propositions take numeric values, or we can ask about the 'degree of
satisfaction' of a property.
While there certainly is ample motivation to extend qualitative specification
formalisms to quantitative ones, there are also problems. It has been observed
in many areas of mathematics, engineering and computer science where logical
formalisms are applied, that quantitative formalisms in general lack the clean
and clear mathematical theory of their qualitative counterparts, and that
many of the desirable mathematical and algorithmic properties tend to get
lost. Also, the definitions of quantitative formalisms are often ad hoc and do
not always respect the properties that are relevant for logical methodologies.
Here we discuss to what extent the relationship between the μ -calculus and
parity games can be extended to a quantitative μ -calculus and appropriate
quantitative model-checking games. The extension is not straightforward
and requires that one defines the quantitative μ -calculus in the 'right' way,