Game Development Reference
In-Depth Information
atomic formulae of the form p i ,
Boolean combinations, and
temporal operators:
···
···
F ϕ
'eventually ϕ '
ϕ
ϕ ··· ϕ
ϕ ···
G ϕ
'always ϕ '
ϕ
ϕ
ϕ
···
···
X ϕ
'next ϕ '
ϕ
ϕ ··· ϕ
···
ϕ U ψ
' ϕ until ψ '
ϕ
ϕ
ψ
The semantics of the operators is already illustrated in the drawings. We do
not give the formal definition here but prefer to explain the semantics using
some examples. An atomic formula p i is true if p i is true at the beginning
of the word, i.e., if the i th entry of the first vector is 1. A formula X ϕ is
true if ϕ is true in the model starting from the second position. For example,
p 1 ∧ X¬p 2 is true in
1
1
1
0
0
1
0
0
···
as witnessed by the underlined entries.
A formula F ϕ is true if there exists some position i ≥ 0 in the word such
that ϕ is true in this position (i.e. in the su x of the word starting at this
position i ). A formula G ϕ is true if ϕ is true at each position of the word.
For example, G p 2 F p 1 is true in
0
1
0
1
0
1
0
1
1
1
0
1
0
1
1
1
···
···
again witnessed by the underlined entries.
A formula ϕ U ψ is true if there is some position where ψ is true, and ϕ is
true in all previous positions. Consider the formula F( p 3 X(
p 2 U p 1 )). It
states that there is some position where p 3 is true such that from the next
position p 2 is false until a position is reached where p 1 is true. The words
satisfying this formula are of the following shape, where again the underlined
entries are those making the formula true:
¬
0
1
0
0
0
1
1
0
1
0
0
1
0
0
1
0
0
0
1
1
0
···
···
We are interested in games with LTL winning conditions, i.e., games of the
form ( G, ϕ ) for an LTL formula ϕ . Eva wins the game if the play satisfies ϕ .