Game Development Reference
InDepth Information
of a play
G
(
σ,π
)
we put
ν
(
wv
)=
ν
(
v
)). For the rest of this section, we fix a
μ
valuation
ν
.
Lineartime logics
Lineartime logics specify properties of runs in transition systems. For a
given lineartime formula
ψ
, the associated temporal property is specified by
a constraint on the probability of all runs that satisfy
ψ
. This constraint is
written as a
probabilistic operator
P
, where
[0
,
1] is
a rational constant. Thus, we obtain a
lineartime objective
P
ψ
whose
intuitive meaning is 'the probability of all runs satisfying
ψ
is
∈{
>,
≥}
and
∈
related to
'.
An important subclass of lineartime objectives are
qualitative lineartime
objectives
where the constant
is either 0 or 1.
An example of a widely used lineartime logic is LTL, introduced in Pnueli
[1977]. The syntax of LTL formulae is specified by the following abstract
syntax equation:
ψ
::=
tt

a
 ¬
ψ

ψ
1
∧
ψ
2

X
ψ

ψ
1
U
ψ
2
Here
a
ranges over
Ap
. Note that the set
Ap
(
ψ
) of all atomic propositions that
appear in a given LTL formula
ψ
is finite. Every LTL formula
ψ
determines its
associated
ωlanguage L
ψ
consisting of all infinite words
u
over the alphabet
2
Ap
(
ψ
)
such that
u 
=
ψ
, where the relation

= is defined inductively as
follows (recall that the symbol
u
i
, where
i
≥
0, denotes the infinite word
u
(
i
)
,u
(
i
+1)
,...
):
u 
=
tt
u 
=
a
iff
a ∈ u
(0)
u 
=
¬ψ
iff
u 
=
ψ
u 
=
ψ
1
∧ ψ
2
iff
u 
=
ψ
1
and
u 
=
ψ
2
u

=
X
ψ
iff
u
1

=
ψ
u

=
ψ
1
U
ψ
2
iff
u
j

=
ψ
2
for some
j
≥
0 and
u
i

=
ψ
1
for all 0
≤
i<j
.
=
ν
ψ
iff
w
For a given run
w
of
G
(oraplayof
G
), we put
w
=
ψ
, where
w
is the infinite word defined by
w
(
i
)=
ν
(
w
(
i
))
∩ Ap
(
ψ
). In the following we
also use
F
ψ
and
G
ψ
as abbreviations for
ttU
ψ
and
¬
F
¬ψ
, respectively.
Another important formalism for specifying properties of runs in transition
systems are finitestate automata over infinite words with various acceptance
criteria, such as Buchi, Rabin, Street, Muller, etc. We refer to Thomas [1991]
for a more detailed overview of the results about finitestate automata over
infinite words. Let
M
be such an automaton with an input alphabet 2
Ap
(
M
)
,
where
Ap
(
M
) is a finite subset of
Ap
. Then
M
can also be understood as
a 'formula' interpreted over the runs of
G
(or a play of
G
) by stipulating


Search Nedrilad ::
Custom Search