Game Development Reference
In-Depth Information
of a play G ( σ,π )
we put ν ( wv )= ν ( v )). For the rest of this section, we fix a
μ
valuation ν .
Linear-time logics
Linear-time logics specify properties of runs in transition systems. For a
given linear-time 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 linear-time objective P ψ whose
intuitive meaning is 'the probability of all runs satisfying ψ is
∈{
>,
≥}
and
-related to '.
An important subclass of linear-time objectives are qualitative linear-time
objectives where the constant is either 0 or 1.
An example of a widely used linear-time 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 finite-state 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 finite-state 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
|
|