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
ϕ
.

Search Nedrilad ::

Custom Search