Game Development Reference
InDepth Information
equations:
ψ
::=
ϕ
 ¬
ψ

ψ
1
∧
ψ
2

X
ψ

ψ
1
U
ψ
2
P
ψ
ϕ
::=
tt

a
 ¬
ϕ

ϕ
1
∧
ϕ
2

Note that all LTL formulae are PCTL
∗
path formulae. In the case of PCTL,
the syntax of path formulae is restricted to
ψ
::=
ϕ 
X
ψ  ψ
1
U
ψ
2
. Since the
expressive power of LTL is strictly smaller than that of finitestate automata
over infinite words (see the previous section), the logic CTL
∗
can be further
enriched by allowing arbitrary
automata connectives
in path formulae (see
Wolper [1981]). The resulting logic is known as
extended CTL
∗
(ECTL
∗
)
,
and its probabilistic variant as PECTL
∗
.
Let
G
(
σ,π
)
be a play of
G
. For every run
w ∈ Run
(
G
(
σ,π
)
) and every path
μ
μ
=
ν
ψ
in the same way as in the previous
formula
ψ
we define the relation
w

=
ν
ϕ
(see below). For every state
s
of
G
(
σ,π
)
=
ν
ϕ
iff
w
(0)
section, where
w


μ
=
ν
and every state formula
ϕ
we define the relation
s

ϕ
inductively as
follows:
=
ν
tt
s

=
ν
a
s

iff
a
∈
ν
(
s
)
=
ν
s

¬
ϕ
iff
s

=
ϕ
=
ν
ϕ
1
∧
=
ν
ϕ
1
and
s
=
ν
ϕ
2
s

ϕ
2
iff
s


=
ν
P
ψ
=
ν
ψ
s

iff
P
s
(
{
w
∈
Run
(
s
)

w

}
)
A state formula
ϕ
is
qualitative
if each occurrence of the probabilistic operator
in
ϕ
is of the form
P
0
or
P
1
. General (not necessarily qualitative) state
formulae are also called
quantitative
.
A
branchingtime objective
is a state formula
ϕ
of a branchingtime
probabilistic temporal logic. Important subclasses of branchingtime objec
tives are PCTL, PCTL
∗
, and PECTL
∗
objectives.
Let us note that state formulae of branchingtime probabilistic logics
are sometimes interpreted directly on vertices of Markov decision processes
(see Bianco and de Alfaro [1995]) and stochastic games (see de Alfaro and
Majumdar [2004]). Path formulae are interpreted over the runs of
G
in
the same way as above, and all state formulae except for
P
ψ
are also
interpreted in the natural way. Due to the presence of nondeterminism
in
G
, it is not possible to measure the probability of runs in
G
, and the
probabilistic operator
P
has a different meaning defined as follows:
v 
=
ν
P
ψ
∃σ ∈
Σ
∀π ∈
Π:
P
v
(
{w ∈ Run
(
G
(
σ,π
)
,v
)
 w 
=
ν
ψ}
)
.
iff
v
=
ν
P
ψ
iff for every strategy
τ
If
G
is a Markov decision process, then
v

Search Nedrilad ::
Custom Search