Game Development Reference

In-Depth Information

(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

very similar.

Exercise 4.7
Make the construction of the formulae
ψ
σ
explicit, and prove

that they indeed define the winning region for Player
σ
.

Theorem 4.32

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,

Search Nedrilad ::

Custom Search