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

P θ [ ϕ ], and let p be the proba-
bility measure for the set of trajectories that start in s and satisfy ϕ .If

Consider the model-checking problem M ,s | =

| p − θ | <δ ,

then the truth value of P θ [ ϕ ] is undetermined (“too close to call”) under the

relaxed semantics; otherwise, it is the same as for PCTL.
Formally, given δ> 0, we define two relations:

|≈

δ

(approximate satisfaction)

δ
⊥

δ δ

⊥

|≈ |≈ |≈

and (approximate “unsatisfaction”). The definitions of and coincide

with | =and | =, respectively, except for probabilistic formulae where we instead

have:

δ δ

M ,s |≈

P ≥ θ [ ϕ ]

if μ ( { σ ∈ Path ( s ) |M ,σ |≈ ϕ } ) ≥ θ + δ

δ
⊥ P ≥ θ [ ϕ ]

δ
⊥

M ,s |≈ if μ ( { σ ∈ Path ( s ) |M ,σ |≈ ϕ } ) ≤ θ − δ

δ δ

M ,s |≈

P ≤ θ [ ϕ ]

if μ ( { σ ∈ Path ( s ) |M ,σ |≈ ϕ } ) ≤ θ − δ

δ
⊥ P ≤ θ [ ϕ ]

δ
⊥

M ,s |≈ if μ ( { σ ∈ Path ( s ) |M ,σ |≈ ϕ } ) ≥ θ + δ

Let M , s accept Φ represent the fact that Φ is accepted as true in state s of

A

M by a model-checking algorithm A ,and M ,sreject

A

Φ that Φ is rejected as

false in state s of . The solution methods we present aim to guarantee

the following error bounds:

M by A

δ

Pr[ M ,sreject

A

Φ] ≤ α if M ,s |≈ Φ (4)

δ
⊥

Pr[ M , s accept Φ] ≤ β if M ,s |≈ Φ (5)

A

The parameters α and β allow a user to control the probability of false negatives
and false positives, respectively. For example, consider the formula Ψ]

and let p denote the probability measure of trajectories that start in some state
s and satisfy Φ

P ≥ 0 . 5 [Φ U

Ψ. Let δ =0 . 01. The statistical model-checking algorithms in
this paper aim to guarantee that we reject the formula as false with probability
at most α if p

U

0 . 5+ δ =0 . 51, and that we accept the formula as true with
probability at most β if p

≥

δ =0 . 49. The three parameters α , β ,and δ
determine the precision of the model-checking algorithm. It is up to the user to
set these to his or her satisfaction, with the understanding that higher precision
will result in longer model-checking times.

≤ 0 . 5 −

3 Sampling-Based Verification of Unbounded Until

This section presents two methods for verifying probabilistic properties with
unbounded until, based on statistical sampling. For the model-checking problem
M ,s | = P θ [Φ U Ψ], define the random variable X : Path ( s ) →{ 0 , 1 } as follows:

X ( σ )= 1 f

M ,σ | U

=Φ Ψ

. (6)

0 f M ,σ | =Φ U Ψ

X represents a Bernoulli trial (i.e., outcomes are limited to 0 and 1). The ex-
pectation of X is

E[ X ]= μ ( { σ ∈ Path ( s ) |M ,σ | =Φ U Ψ } ) . (7)