Statistical Verification of Probabilistic Properties with Unbounded Until - Formal Methods: Foundations and Applications - page 147

includes unbounded until, since that is the focus of this paper. The techniques
described later in the paper can of course be combined with the techniques de-
veloped by Younes and Simmons [26] to handle a more expressive logic. The
logic permits nested probabilistic operators, although we do not discuss such
formulae here. Younes and Simmons [26] have already shown how to deal with
nested probabilistic formulae without ties to any specific type of path formula.
We could also replace PCTL with probabilistic LTL, which would avoid nested
probabilistic operators altogether. The solution methods of this paper can be
adapted for probabilistic LTL, but we do not consider that here.
Let AP be a fixed, finite set of atomic propositions. We assume a labeled
discrete-time Markov chain

M = S, P ,L . S ,and P as above, with the addition

2 AP . L ( s ) is the set of atomic propositions a

of a labeling function L : S AP

that are valid in s . PCTL formulae (for the relevant subset that we consider)
are of the form

→ ∈

Φ ::= a ¬ Φ Φ Φ P θ [Φ ∧ U Φ] ,

where θ ∈ [0 , 1] and ∈{≤ , ≥} . Additional PCTL formulae can be derived in

the usual way. For example, ⊥≡ a ∧¬ a for some a ∈ AP , ≡¬⊥ ,Φ ∨ Ψ ≡

¬ ( ¬ ≡¬P ≥ θ [ ϕ ].

The standard logic operators have their usual meaning.

Φ ∧¬ Ψ), Φ → Ψ ≡¬ Φ ∨ Ψ, and P <θ [ ϕ ]

P θ [ ϕ ] asserts that
the probability measure over the set of trajectories satisfying the path formula ϕ
is related to θ according to . Path formulae are constructed using the temporal
path operator U (“until”). The path formula Φ U ΨassertsthatΨbecomestrue

at some time t 0 while Φ holds in all states prior to t . We can define mutually

inductive satisfaction relations for PCTL state and path formulae as follows:

≥

M ,s | = a if a ∈ L ( s )

M ,s | = ¬ Φ if M ,s | =Φ

M ,s | =Φ ∧ Ψ if ( M ,s | =Φ) ∧ ( M ,s | =Ψ)

M ,s | = P θ [ ϕ ] if μ ( { σ ∈ Path ( s ) |M ,σ | = ϕ } ) θ

i. ( j<i. M =Φ

M ,σ | =Φ U Ψ f ∃ M ,σ [ i ] | =Ψ) ∧∀ ,σ [ j ] |

The fact that is measurable can be verified from the

probability-space construction in Sect. 2.1 (cf. [1]), which makes the semantics
for PCTL well-defined.

{ σ ∈ Path ( s ) |M ,σ | = ϕ }

2.3 Error Control

Statistical solution methods cannot achieve the exact precision for probabilistic
PCTL formulae that is required by the semantics given above. Following Younes
and Simmons [25], we relax the semantics of PCTL by introducing an indifference
region of half-width δ centered around any probability thresholds. The purpose
is to quantify the error that we are willing to accept by using sampling and
simulation in place of exact computations of probability measures.