Game Development Reference
In-Depth 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 finite-state 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 branching-time objective is a state formula ϕ of a branching-time
probabilistic temporal logic. Important subclasses of branching-time objec-
tives are PCTL, PCTL , and PECTL objectives.
Let us note that state formulae of branching-time 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 non-determinism
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
|