Towards model-checking probabilistic timed automata against probabilistic duration properties

VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

Towards Model-checking Probabilistic Timed

Automata against Probabilistic Duration Properties^$

Van Hung Dang^1,∗, Miaomiao Zhang², Dinh Chinh Pham¹

¹VNU University of Engineering and Technology, Hanoi, Vietnam

²School of Software Engineering, Tongji University, Shanghai, China

Abstract

In this paper, we consider a subclass of Probabilistic Duration Calculus formula called Simple Probabilistic

Duration Calculus (SPDC) as a language for specifying dependability requirements for real-time systems, and

address the two problems: to decide if a probabilistic timed automaton satisﬁes a SPDC formula, and to decide

if there exists a strategy of a probabilistic timed automaton satisﬁes a SPDC formula. We prove that the both

problems are decidable for a class of SPDC called probabilistic linear duration invariants, and provide model

checking algorithms for solving these problems.

Received 25 November 2015, revised 20 December 2015, accepted 31 December 2015

Keywords: Probabilistic Duration Calculus, Probabilistic Timed Automata, Model-checking,

Markov Decision Process.

1. Introduction

developed by Dimitar Guelev [5], and in [6]

we have shown that the calculus is useful for

reasoning about QoS contracts in component-

based real-time systems.

In 1992, Chaochen Zhou, Hoare C.A.R and

Anders Ravn introduced Duration Calculus [1]

as a logic for reasoning about real-time systems.

The calculus has attracted a great deal of

attention, and was then developed further in

many other works because of its rich meanings.

Many of those works have been summarized

For Duration Calculus, some techniques for

checking if a timed automaton satisﬁes a duration

calculus formula written in the form of linear

duration invariants have been developed [7, 8,

9, 10, 11, 8]. However, to our knowledge,

not many works have been done for checking

if a probabilistic real-time system satisﬁes a

PDC formula. This is, perhaps, because in

the model of probabilistic systems, there is too

much randomization and nondeterminism, and

this makes model checking too complicated.

in the monograph [2].

For specifying the

dependability of real-time systems, a kind of

probabilistic extension of Duration Calculus has

been introduced in [3, 4]. No rigorous syntax has

been introduced in these papers, and the authors

just focused on the development of techniques

for reasoning instead of the ones for checking.

A version with a proof system of Probabilistic

Duration Calculus with inﬁnite interval was then

Kwiatkowska et al in [12, 13] proposed a

variant of probabilistic timed automata that

allows probabilistic choice only at discrete

transitions.

To resolve the nondeterminism

^$This research was funded by Vietnam National Foundation

for Science and Technology Development (NAFOSTED)

_∗under grant number 102.03-2014.23.

between the passage of time and discrete

transitions they used the concept of strategy

which is essentially a deterministic schedule

Corresponding author. Email: dvh@vnu.edu.vn

58

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

59

policy.

Then, the set of executions of a

reachability graph of the timed automaton. Then,

probabilistic timed automaton according to a

strategy forms a Markov chain, and hence the

satisfaction of a probabilistic timed CTL formula

by this set can be deﬁned, and then based on

the region graph of the timed automaton the

satisfaction of a probabilistic timed CTL formula

by the timed automaton can be also veriﬁed.

The idea of ﬁxing a strategy when studying the

probabilistic behavior of a probabilistic timed

automaton restricts the scope of the veriﬁcation

problem signiﬁcantly, making the checking

problem more tractable. Then, verifying the

set of all strategies against a given probabilistic

property can be done by searching for the “worst

case” strategy according to the probabilistic

property and then apply the veriﬁcation technique

to it. This idea is a motivation for us to reconsider

we generalize this technique to achieve our goal

with a model-checking algorithm.

The ﬁrst version of this paper was published

in [14]. In this extended version, in addition to

the problem of veriﬁcation, we formulate also

the problem of strategy synthesis, i.e. to decide

if there is a strategy for a probabilistic timed

automaton that satisﬁes a probabilistic linear

duration invariant and show that this problem is

also solvable. We provide all proof details and

algorithms for doing model-check.

Our paper is organized as follows. In the

next section we present the Probabilistic Timed

Automata model. Section 3 presents syntax

and semantics of our PDC. Our main results is

presented in Section 4 where we formulate our

model checking problem and give our solution to

it. The last section is the conclusion of the paper.

the problem of checking

a

probabilistic

timed automaton for a PDC formula that

we gave up before.

2. Probabilistic Timed Automata

In this paper, we introduced a simple

probabilistic extension of DC called Probabilistic

Duration Calculus for specifying dependability

requirements of real-time systems. The extension

is conservative in the sense that a formula of

DC is also a formula of PDC with semantics

adapted to probabilistic domain. PDC also

consists of formulas representing the constraints

for the probability of the satisfaction of a

DC formula by a strategy for an interval.

We use the behavioral model proposed by

Kwiatkowska et al to deﬁne the semantics of

our logic. Since probabilistic timed CTL and

PDC are not comparable, and since for many

probabilistic properties PDC is more convenient

to specify, a model checking technique for

checking probabilistic timed automata against

PDC properties is useful. To solve this problem,

we ﬁrst develop a technique to decide if a strategy

in a probabilistic timed automaton satisﬁes a

PDC formula of a certain form. This technique

is essentially an extension of our technique

developed earlier in [10, 9] to check if a timed

automaton satisﬁes a DC formula in the form

of linear duration invariants or discretisable DC

formulas based on searching in the integral

In this section, we recall the concepts

of probabilistic timed automata model and

probabilistic timed structure as its semantics

from [15, 12]. We use a simple model of

gas burners to illustrate the concepts as its

requirement speciﬁcation is a typical example for

time duration properties.

Probability distributions and Markov decision

processes. A discrete probability distribution

over a set S is a mapping p : S → [0, 1] such

that the set {s | s ∈ S and p(s) > 0} is ﬁnite, and

P

p(s) = 1. The set of all discrete probability

distributions over S is denoted by µ(S ).

s∈S

A Markov decision process is a tuple

(Q, Steps), where Q is a set of states, and

Steps : Q → 2^µ(Q)is a function assigning

a set of probability distributions to each state.

The intuition is that the Markov decision

process traverses the state space by making

transitions determined by Steps: in a state s, the

process selects nondeterministically a probability

distribution p in Steps(s), and then makes a

probabilistic choice according to p as to which

state to move to. As in [12] we label the action

selecting a probability distribution with a letter

60

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

from Σ, and assume that Steps : Q → 2^Σ×µ(Q)and

Σ is a set of actions. The intuition now becomes

that the Markov decision process traverses the

state space by making transitions determined by

Steps: in a state s, the process performs an

action a ∈ Σ selecting nondeterministically a

probability distribution p in Steps(s), and then

makes a probabilistic choice according to p as to

on all other clocks. For t ∈ R^≥0, we write ν + t

for the clock valuation that assigns ν(x)+t to each

clock x ∈ C. A constraint over C is an expression

of the form x_i∼ c or x_i− x_j∼ c, where i , j,

i, j ≤ n and ∼∈ {<, ≤, >, ≥} and c ∈ N. A clock

valuation ν satisﬁes a clock constraint x_i∼ c

(x_i− x_j∼ c) iﬀ ν(x_i) ∼ c (ν(x_i) − ν(x_j) ∼ c). A

zone of C is a convex subset of the valuation space

(R^≥0)^Cdescribed by a conjunction of constraints.

For a zone ζ and a set of clocks X ⊆ C the set

{ν[X := 0] | ν ∈ ζ} is also a zone, and is denoted

which state to move to. So, a transition is of the

a,p

form s −→ s⁰, where (a, p) ∈ Σ × µ(Q) is the

label of the transition. We also assume a labeling

function L : Q → 2^AP, where AP is a set of

atomic propositions, that associates a state s with

the set of atomic propositions that hold at state

s. Then, a labeled Markov decision process is

a tuple (Q, Steps, L).

by ζ[X := 0]. Let Z denote the set of all zones

C

of C.

Probabilistic timed automata and probabilistic

timed structures.

introduced in [16] as a model of real-time

systems. They are extended with discrete

Timed automata were

Labeled paths (or execution sequences)

are nonempty ﬁnite or inﬁnite sequence of

consecutive transitions of the form

probability distribution to model probabilistic

real-time systems. In the sequel, let AP be a given

set of atomic propositions.

l₀

l₁

l₂

ω = s₀−→ s₁−→ s₂−→ . . . ,

Deﬁnition 1. A probabilistic timed automaton

(PTA) is a tuple G = (S, L, s¯, C, inv, prob,

hτ_si_s∈S) consisting of

where s_iare states and l_iare labels for transitions.

For a path ω, let first(ω) denote the ﬁrst state

of ω, and if ω is ﬁnite then let last(ω) denote

the last state of ω. |ω| is the length of ω and is

deﬁned as the number of transition occurrences

in ω which is ∞ if ω is inﬁnite. For k ≤ |ω|,

let ω(k) denote the kth state of ω, and step(ω, k)

denote the label of the kth transition in ω. For

• a ﬁnite set S of nodes, a start node s¯ ∈ S, a

ﬁnite set C of clocks,

• a function L : S → 2^APassigning to

each node of the automaton a set of atomic

propositions that are supposed to be those

that are true in that node, a function inv :

l₀

l₁

l₂

two paths ω = s₀−→ s₁−→ s₂−→ . . . s_n

l₀⁰

l₁⁰

l₂⁰

and ω⁰= s⁰₀−→ s₁⁰−→ s⁰₂−→ . . . such that

s_n= s⁰₀, the concatenation of ω and ω⁰is deﬁned

S → Z assigning to each node an invariant

C

l₀⁰

l₁⁰

condition,

l₀

l₁

l₂

as ωω⁰= s₀−→ s₁−→ s₂−→ . . . s_n−→ s⁰₁−→

l₂⁰

C

• a function prob : S → 2^{µ(S×2 )}assigning

s⁰₂−→ . . ..

to each node a set of discrete probability

Clocks, clock valuations, clock constraints. Let

R^≥0denote the set of non negative real numbers.

A clock is a real-valued variable which increases

at the same rate as real time. Let C = {x₁. . . , x_n}

be a set of clocks. A clock valuation is a function

ν : C → R^≥0that assigns a real value to each

clock. Let (R^≥0)^Cdenote the set of all clock

valuations, and 0 denote the clock valuation that

assigns 0 to each clock in C. For a set of clocks

X ⊆ C we denote by ν[X := 0] the clock valuation

that assigns 0 to all clocks in X and agrees with ν

distributions on S × 2^C,

• a family of functions hτ_si_s∈Swhere, for any

s ∈ S, τ_s: prob(s) → Z assigns to each

C

p ∈ prob(s) an enabling condition.

The last item in the deﬁnition says that all the

probabilistic choices according to a probabilistic

distribution (selected at a node) have the same

enabling condition. The probabilistic timed

automaton behaves nearly in the same way as a

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

61

x>=30

function prob is given as: prob(s1) = {p0, p1},

prob(s2) = {p2}, prob(s3) = {p3}, where

p0(s3, {x}) = 1, p1(s3, {x}) = 0.8, p1(s2, ∅) =

0.2. p2(s3, {x}) = 1, p3(s1, {x}) = 1, and

τ_s1(p0) = τ_s1(p1) = {x ≤ 1}, τ_s2(p2) = {x ≤ 2}

and τ_s3(p3) = {x ≥ 30}. The function inv is

deﬁned as inv(s1) = {x ≤ 1}, inv(s2) = {x ≤ 2}

and inv(s3) = true. The labels of states are given

by function L deﬁned as L(s1) = L(s2) = leak,

and L(s3) = nonleak.

x:=0

1

d

s1

Leak

x<=1

s3

Nonleak

x<=1 1

x:=0

a

b

x<=1

x:=0

0.8 0.2

x<=2

1

s2

x<=2

Leak

c

As in [12] we use probabilistic timed structures

as underlying semantics model for PTA.

Deﬁnition 2. A probabilistic timed structure M

is a labeled Markov decision process (Q, Steps, L)

Fig. 1: A probabilistic timed automaton

for a simple gas burner.

≥0

×µ(Q)

where Q is a set of states, Steps : Q → 2^R

is a function which assigns to each state q ∈ Q

a set Steps(q) of pairs of the form (t, p), where

t ∈ R^≥0and p ∈ µ(Q), and L : Q → 2^APis a state

labeling function.

timed automaton does, except that it has to select

a probability distribution at each discrete step.

We denote by Z (G) the set of all clock zones

C

occurring in G,

Function Steps speciﬁes the set of transitions

that M can choose nondeterministically at each

state. Therefore, if at state q ∈ Q, M chooses

(t, p) ∈ Steps(q), then after t time units have

elapsed, a probabilistic transition is made to state

q⁰with probability p(q⁰). A path of M is a

nonempty ﬁnite or inﬁnite sequence:

Z (G) = {inv(s) ∈ Z | s ∈ S}∪

C

{τ_s(p) ∈ Z | s ∈ S and

C

p ∈ prob(s)}.

Example 1. Fig. 1 shows a probabilistic timed

automaton for a simple gas burner.

t₀,p₀

t₁,p₁

t₂,p₂

The system starts at the node s1, with the

gas valve is opened without ﬂame being on,

hence gas is leaking. At this state, there are

two nondeterministic choices. The ﬁrst choice

denoted by transition a is that with the probability

1, the ﬂame is turned on within one second (x ≤

1) and the system moves to node s3 for which

gas is not leaking. The second choice denoted

by transition b is as follows: with the probability

0.8, the ﬂame is turned on within one second and

the system moves to node s3 for which gas is not

leaking, and with probability 0.2 the ﬂame fails to

be on within one second, and the system moves to

node s2 for which gas is still leaking. In state

s2, with probability 1, the gas valve is closed

successfully within 2 seconds since the time the

system entered s1 last time, and the system moves

to node s3. At state s3, the gas burner will move

to the state s! only after it has stayed there at

least 30 seconds. Formally, in this example, the

ω = q₀−→ q₁−→ q₂−→ . . .

where q_i∈ Q, (t_i, p_i) ∈ Steps(s_i), and p_i(q_i+1) > 0

for all 0 ≤ i ≤ |ω|. For a given probabilistic timed

structures M we denote by Path_fin(Path_inf) the

set of ﬁnite (inﬁnite) paths, and by Path_fin(q)

(Path_inf(q)) the set of paths in Path_fin(Path_inf

that start from state q. Let ω be inﬁnite.

)

A

position of ω is a pair (i, t), where i ∈ N and

t ∈ R^≥0such that 0 ≤ t ≤ t_i. The state at

position (i, t) is denoted by state_ω(i, t). Given

two positions (i, t) and (j, t⁰) of ω, we say (j, t⁰)

precedes (i, t) (in ω, written by ( j, t⁰) ≺ (i, t)) if

j < i or j = i and t⁰< t.

Deﬁnition 3. For any path ω of a probabilistic

timed structure M and 0 ≤ i ≤ |ω| we deﬁne

D_ω(i), the elapsed time until the ith transition, as

follows: D_ω(0) = 0 and for any 1 ≤ i ≤ |ω|:

P

i−1

D_ω(i) =

_j=0t_j.

62

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

An inﬁnite path ω is said to be divergent iﬀ

for any t ∈ R^≥0, there exists j ∈ N such that

D_ω(j) > t. Let ω be inﬁnite. For each state

which for all ω⁰∈ Path^A_fincontains the sets

{ω | ω

∈

Path_i^A_nfand ω⁰is a preﬁx of ω}.

Let Prob^A_fin

:

Path^A_fin

→

[0, 1] be the

q

∈ Q, we deﬁne a {0, 1}-valued function

mapping deﬁned inductively on the length

q_ω: R^≥0→ {0, 1} as

of paths in Path^A_finas follows. If |ω| = 0 then









1

iﬀ there exists a position (i, t⁰) s.t.

t⁰> 0, state_ω(i, t⁰) = q and

t = D_ω(i) + t⁰,



Prob^A_fin(ω) = 1. Let ω⁰∈ Path^A_finbe a ﬁnite path





t,p

q (t) =

ω



of A. If ω⁰= ω −→ q for some ω ∈ Path^A_fin, then



we let Prob^A_fin(ω⁰)

=

Prob^A_fin(ω)P^A(ω, ω⁰).

0

otherwise.

Intuitively, q_ω(t) = 1 means that in the path ω,

state q is present in an interval (t − δ, t] for some

δ > 0, and otherwise q_ω(t) = 0.

The measure Prob^Aon F_Pathis the

A

unique measure such that Prob^A({ω | ω

∈

Path_i^A_nfand ω⁰is a preﬁx of ω}) = Prob^A_fin(ω⁰).

In this paper, we assume that the strategies under

consideration are divergent in the probabilistic

sense, i.e. we assume that for any strategy A,

Prob^A({ω | ω ∈ Path_i^A_nfand ω is divergent}) = 1.

We now deﬁne the behavior of probabilistic

timed automata by associating every probabilistic

timed automaton with a probabilistic timed

structure. A state of the structure consists of a

state of the automaton, and a valuation for the

clock variables.

The concept of strategy was introduced in

the literature (see, e.g. Kwiakowska [12]) as a

schedule for resolving all the nondeterministic

choices of the model.

Note that we have

restricted ourselves to discrete probability

distributions only.

Deﬁnition 4. A strategy (or scheduler) of a

probabilistic timed structure M = (Q, Steps, L)

is a function A mapping every nonempty ﬁnite

path ω of M to a pair (t, p) such that A(ω) ∈

Steps(last(ω)), and the empty path ꢀ to a state in

Q. Let A be the set of all strategies of M.

Deﬁnition 5. For any probabilistic timed

automaton G as in Deﬁnition 1, deﬁne

the probabilistic timed structure M_G

=

Let us denote a preﬁx of length i of ω by ω⁽ⁱ⁾,

and deﬁne for a given strategy A

(Q_G, Steps_G, L_G) as follows.

ꢀ





A(ꢀ) = ω⁽⁰⁾, and

step(ω, i) = A(ω⁽ⁱ⁾)

for 0 ≤ i < |ω|









• Q_G= {hs, νi | s ∈ S, ν ∈ (R^≥0)^C}

• The function Steps_G: Q_G→ 2

ꢀ

Path^A_fin= ω ∈ Path



fin



R^≥0×µ(Q_G)









ꢀ





assigns to each state in Q_Ga set of

transitions, each of which takes the form

(t, p¯) where t ∈ R^≥0and p¯ is a discrete

probabilistic distribution on Q, and is

deﬁned as:

A(ꢀ) = ω⁽⁰⁾, and

step(ω, i) = A(ω⁽ⁱ⁾)

for 0 ≤ i









Path_i^A_nf= ω ∈ Path



in f









Recall that step(ω, i) returns the label of the

ith transition in ω. From Deﬁnition 4, all ω

in Path^A_finand Path_i^A_{n f}start from the same state

deﬁned by A(ꢀ), and intuitively they represent the

behaviors of M according to the scheduler A,

– (t, p¯) ∈ Steps_G(hs, νi) if there exists

p ∈ prob(s) such that (a) the valuation

ν + t satisﬁes τ_s(p) and ν + t⁰satisﬁes

inv(s) for all 0 ≤ t⁰≤ t, and (b)

A

sequential Markov chain MC^A

=

(Path^A_fin, P^A) is associated with a strategy A

in a natural way to express the executions of M

according to A, where P^Ais deﬁned as

for any hs⁰, ν⁰i ∈ Q_G: p¯(hs⁰, ν⁰i) =

P

p(s⁰, X).

For

X⊆C∧(ν+t)[X:=0]=ν⁰

convenience, we refer to p¯ as having

type p, denoted by type(p¯) = p.





p(q) if A(ω) = (t, p) and





t,p

P^A(ω, ω⁰) =

ω⁰= ω −→ q,



– Let (t, p¯) ∈ Steps_G(hs, νi) if (a) the

valuation ν + t⁰satisﬁes inv(s) for all

0 ≤ t⁰≤ t, and (b) for any hs⁰, ν⁰i ∈





0

otherwise.

Let F_Pathbe the smallest σ-algebra on Path_i^A_nf

A

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

63

Q_G: p¯(hs⁰, ν⁰i) = 1 if hs⁰, ν⁰i =

hs, ν + ti, and p¯(hs⁰, ν⁰i = 0 otherwise.

We refer to p¯ as having type >, i.e.

type(p¯) = >.

on probabilistic timed automata, and has a

simple grammar that allows to write formulas to

reason about the probability of the satisfaction

of a duration formula by a probabilistic timed

automaton as well as to specify real-time

properties of the system itself.

• The labeling function L : Q → 2^APis deﬁned

as: L_G(hs, νi) = L(s) for all hs, νi ∈ Q_G.

Deﬁnition 6. Let R stand for relations (e.g. ≤

, =), and F stand for functions (e.g. +, −).

The syntax of Probabilistic Duration Calculus is

deﬁned as follows.

The second item of the deﬁnition of the

function Steps allows the automaton to stay in a

state forever from a time if the invariant for the

state is never violated from that time, and the

corresponding path is inﬁnite.

Any strategy for the timed structure M_G

is also called strategy for probabilistic timed

automaton G.

Φ ::= Ψ | [Ψ]_wλ| ¬Φ | Φ ∧ Φ,

Ψ ::= R(η, . . . , η) | ¬Ψ | Ψ ∧ Ψ | Ψ; Ψ,

R

η

::=

S | F(η, . . . , η),

S

::= 1 | P |¬S | S ∧ S,

where Φ stands for Probabilistic Duration

Calculus formulas, Ψ stands for Duration

Calculus formulas, η stands for duration terms,

S stands for state expressions, and P is a symbol

in the set of atomic proposition AP.

Example 2. The following path is a path of

(a strategy of) the timed structure of the timed

automaton in Fig. 1:

.9,.8

31,1

.7,.2

ω = hs1, 0i −→ hs3, 0i −→ hs1, 0i −→

hs2, .7i −^1.→^2,1hs₃, 0i −→ hs3, 30i ¹−⁰→^0,1

We will use a probabilistic timed automaton

G as underlying model to deﬁne the semantics

for Probabilistic Duration Calculus formulas as

well as for Duration Calculus formulas. Let Intv

denote the set of all intervals on R^≥0.

30,1

hs3, 130i ¹−⁰→^0,1. . . .

For

a

given inﬁnite divergent path

ω

of M_G, for an atomic proposition

P

∈

AP, let us deﬁne a {0, 1}-valued

Given a path ω of M_Gaccording to a

function P_ω: R^≥0→ {0, 1} by P_ω(t) =

max{q_ω(t) | q = hs, νi ∈ Q_Gand P ∈ L(s)} (note

that there can be several regions hs, νi in the

path ω for which P ∈ L(s)). So, P_ω(t) = 1

means that there is an semi-interval (t − δ, t] in

which P holds. Otherwise, P_ω(t) = 0. Since we

have assumed that ω is divergent, P_ωhas the

ﬁnite variability, i.e. it has only ﬁnite number of

discontinuity points within any ﬁnite interval.

strategy A. The interpretation of state expression

S is a {0, 1}-valued function I_S^ω: R^≥0

→

{0, 1} deﬁned inductively as: I^ω(t)

=

1

for all t

∈

R^≥0, I_P^ω

=

P_ωwhere P_ωis

deﬁned as in Section 2, I_¬^ω_S= 1 − I_S^ω, and

I_S^ω_{1∧S 2}= min{I_S^ω₁, I_S^ω₂}. (Note that the operations

on functions is deﬁned point-wise.)

The

interpretation of a term η is a function I_η^ω: Intv →

R

R^≥0deﬁned as I^R_S([a, b]) = ^bI_S^ω(t)dt, and

ω

a

I^ω_{f(η1,...,ηk)}([a, b]) = f(I_η^ω₁([a, b]), . . . , I_η^ω_k([a, b]))

for any interval [a, b] ∈ Intv.

3. Probabilistic Duration Calculus

A model for DC formulas is a pair (ω, [a, b])

of a divergent path ω and an interval [a, b].

The semantics of Duration Calculus formulas is

essentially the satisfaction relation |= between a

model (ω, [a, b]) and a DC formula Ψ which is

deﬁned as follows.

In this section we introduce a simple form

of Probabilistic Duration Calculus. A complete

probabilistic interval logic (which DC is based

on) with a proof system has been introduced in

[5]. However the deﬁnition of the semantics in

that paper for the calculus is rather complicated

and less intuitive.

in this paper has an intuitive semantics based

The calculus introduced

• (ω, [a, b]) |= R(η1, . . . , ηk) iﬀ

R(I_η^ω₁([a, b]), . . . , I_η^ω_k([a, b])),

64

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

• (ω, [a, b]) |= ¬Ψ iﬀ (ω, [a, b]) |= Ψ,

automaton G, any path ω of G, and any time

interval [a, b]. A PDC formula Φ is said to be

• (ω, [a, b]) |= Ψ1∧Ψ2 iﬀ (ω, [a, b]) |= Ψ1 and

valid iﬀ (A, t) |=

Φ holds for any probabilistic

PDC

(ω, [a, b]) |= Ψ2,

timed automaton G, strategy A of G, and t ∈ R^≥0.

In [17, 2] a proof system for DC for deriving

valid formulas has been presented. It follows

directly from the deﬁnition of semantics that PDC

is a conservative extension of DC. Besides, some

obvious properties of the probabilities can be

translated into valid formulas in PDC easily.

These observations are formulated in the

following theorem.

• (ω, [a, b]) |= Ψ1; Ψ2 iﬀ (ω, [a, m]) |= Ψ1 and

(ω, [m, b]) |= Ψ2 for some m ∈ [a, b].

The probability measure Prob^Awill come to

play role in the deﬁnition of semantics of PDC

formulas. A model for a PDC formula consists

of a strategy A of M_Gand a time point t (recall

that A deﬁnes an “initial” state, not necessary to

be hs¯, 0i; to be meaningful, we may need the

restriction that the “initial” state of A is hs¯, 0i,

we will assume this whenever necessary). The

Theorem 1. For any DC formulas Φ, Φ1 and Φ2

• [Φ] ⇔ Φ is a valid PDC formula,

w1

satisfaction relation |=

between PDC models

(A, t) and PDC formulas Φ is deﬁned as:

PDC

• If Φ is a valid DC formula, then it is a valid

PDC formula,

• For a DC formula Ψ, (A, t) |=

Ψ iﬀ

PDC

Prob^A({ω | ω ∈ Path_i^A_{n f}and ω is divergent

• ((Φ1 ⇒ Φ2) ∧ [Φ1] ) ⇒ [Φ2] is a valid

wλ

and

PDC formula

(ω, [0, t]) |= Ψ}) = 1,

• ¬(Φ1 ∧ Φ2) ∧ [Φ1]_wλ1∧ [Φ2]

⇒ [Φ1 ∨

wλ2

Φ2]_wλ1+λ2is a valid PDC formula.

• For a DC formula Ψ, (A, t) |=

[Ψ]_wλiﬀ

PDC

Prob^A({ω | ω ∈ Path_i^A_{n f}and ω is divergent

Proof. Straightforward from the deﬁnition of

semantics of DC and PDC.

and

2

(ω, [0, t]) |= Ψ}) ≥ λ,

As usual in DC, we use the following

R

• (A, t) |=

¬Φ iﬀ (A, t) |=

Φ

PDC

abbreviations:

`b= 1, Trueb=`

≥

0,

PDC

3Ψb=True; Ψ; True (there exists a subinterval

• (A, t) |=

Φ1 ∧ Φ2 iﬀ (A, t) |=

Φ1 and

PDC

for which Ψ is satisﬁed), 2Ψb=¬3¬Ψ (for all

R

(A, t) |=

Φ2.

subintervals Ψ is satisﬁed), dS eb= S = ` ∧ ` > 0.

Note that PDC can express the safety and

bounded liveness properties, but not unbounded

liveness properties. For example, PDC formula

2(dPe; ` > b ⇒ ` ≤ b; dQe) says that it is almost

certain that whenever P becomes true for non-

zero time period, Q must become true for non-

zero time period within b time units.

The reason for a using a strategy to deﬁne

a model of PDC formulas is clear since the

probability is deﬁned just for subsets of paths

induced by A, not for a single path. But the reason

for selecting an interval of the form [0, t] instead

of [a, b] is just for convenience. The computation

of Prob^A(B) for a set B of paths satisfying a

DC formula Ψ in an interval [a, b] needs the

preﬁxes in the whole interval [0, b] of paths in

B. Intuitively, a strategy A of probabilistic timed

automaton G satisﬁes a DC formula Ψ in the

probabilistic setting at a time t iﬀ the set of inﬁnite

divergent paths ω produced by A that satisfy Ψ in

the interval [0, t] has the probability 1.

Example 3. Let us consider the simple gas

burner in Example 1 (see Fig. 1). Let one of

the requirements for the gas burner is that for

any observation interval the length of which is

not shorter than 60 seconds, the accumulated

leakage time is not longer than 4% of the length

of the observation interval. This requirement is

A DC formula Φ is said to be valid iﬀ

(ω, [a, b]) |= Φ holds for any probabilistic timed

formalized as a DC formula R b= 2(` ≥ 60 ⇒

R

leak ≤ 4% ∗ `). (b= stands for “being by

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

65

(s1,0)

formulas is decidable (see [18]). In this section,

we develop a technique to verify if a set of all

PDC models generated by a probabilistic timed

automaton G satisﬁes a PDC formula in discrete

time. Namely, we consider the problem to decide

1

(s1,1)

0.8

0.2

(s3,0)

30

(s2,1)

1

(s3,30)

1

(s2,2)

1

A, t |=

[Ψ] for all A ∈ A and all t ∈ R^≥0,

(s1,0)

1

(s3,0)

PDC

wλ

30

where A is the set af all integral strategies of a

timed automaton G. In the sequel, for simplicity

by saying “strategy” we actually mean “integral

strategy” unless diﬀerently stated.

(s1,1)

(s3,30)

1

0.8

0.2

(s3,0)

(s2,1)

1

(s1,0)

1

30

(s2,2)

1

(s1,1)

(s3,30)

1

0.8

0.2

Depending on diﬀerent forms of model sets we

can have diﬀerent model checking problems as:

1. Single strategy single time: given a strategy

(s3,0)

30

(s2,1)

1

(s3,30)

30

(s3,60)

(s2,2)

1

(s3,30)

1

(s3,30)

1

(s3,60)

(s3,0)

(s3,30)

A, given a time t, to decide A, t |=

[Ψ] .

PDC

wλ

30

(s3,60)

30

(s3,60)

This problem is decidable. It is so because

the fact that a path ω satisﬁes Ψ in [0, t] or

not depends only on the smallest preﬁx ω⁽ⁱ⁾

such that D_ω(i) ≥ t. The set {ω⁰| ω⁰∈

(s3,30)

1

(s3,60)

(s3,30)

30

(s3,60)

1

A

0

Path_finand D_ω(|ω |) ≥ t and D_ω(|ω | −

1) < t} is ﬁnite, and computable if A

is computable. From the assumption, the

(s3,60)

Fig. 2: A part of a strategy A for the simple gas burner.

A

0

set {ω⁰| ω⁰∈ Path_finand D_ω(|ω |) ≥

0

t and D_ω(|ω |−1) < t and (ω , [0, t]) |= Ψ} is

computable, and ﬁnite. Hence, Prob^A({ω ∈

Path^A_fin| (ω, [0, t]) |= Ψ}) is computable, and

deﬁnition”). Let ω be given as in Example 2.

R

Then, (ω, [0, 60]) |= (` ≥ 60 ⇒ leak ≤ 4% ∗ `).

This is so because the accumulated time for the

leakage in the interval [0, 60] is .9+.7+1.2 = 2.8

which is longer than 4% ∗ 60 (= 2.4).

therefore, A, t |=

[Ψ]_wλis decidable.

PDC

2. Multiple strategy single time: Given a

set of strategies A which have a ﬁnite

representation, given a time t, decide

Let strategy A that schedules the system

producing the paths be as shown by the tree

in Fig. 2 in which the dashed edges represent

discrete transitions labeled with probability, and

the non-dashed edges represent time advance

transitions labeled with their corresponding

amount of time units. Only those paths that have

a preﬁx represented by the leftmost branch of

the tree, satisfy the requirement R in the interval

[0, 60]. The set of these paths has the probability

A, t |=

[Ψ] for all A ∈ A. If A is

PDC

wλ

ﬁnite, the problem is decidable. Hence the

decidability of the problem depends on the

form of the computable set A of strategies.

3. Single strategy with arbitrary time: Given a

strategy A which has a ﬁnite representation,

decide if A, t |=

[Ψ] for all t ∈

PDC

wλ

R^≥0. This problem in general is undecidable

even for λ = 1 because DC is undecidable

in general.

0.8 ∗ 0.8 = 0.64. Hence, (A, 60) |= [R] (note

w.6

4. Multiple strategy with arbitrary time: Given

that this example is for the sake of illustrating the

concepts only).

a set of strategies A which have a ﬁnite

representation, decide A, t |=

[Ψ] for

wλ

PDC

all A ∈ A and all t ∈ R^≥0. This problem is

most general, and undecidable because DC

is undecidable in general.

4. Model checking probabilistic timed

automata against PDC properties

5. Strategy synthesis: To ﬁnd a strategy A such

Duration Calculus formulas are highly

undecidable, only a very small class of chop free

that A, t |=

[Ψ]_wλfor a given t or for all t.

PDC

66

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

In this section, we will restrict ourselves to

some instances of the problems mentioned in the

items 3 and 4.

equivalence class satisfy the same set of clock

constraints as formulated as the following lemma

(taken from [16, 9]):

We are interested specially in the PDC

Lemma 1. Let ν, ν⁰∈ N^C, X ∈ 2^C, and ν ꢀ ν⁰.

formulas of the form [Ψ] , where Ψ has the form

wλ

R

P

k

Then

2(a ≤ ` ≤ b ⇒

c_iP_i≤ M) called linear

duration invariants ⁱ(⁼L¹DI) [7], where M, a and

b are integers, b could be ∞. A dependability

1. ν[X := 0] ꢀ ν⁰[X := 0]

2. for any zone ζ ∈ Z (G) appearing in the

C

requirement for the simple gas burner could be

R

description of G, ν satisﬁes ζ if and only if

ν⁰satisﬁes ζ.

expressed as [2(` ≥ 60 ⇒

leak ≤ 4% ∗

`)]

which says that with the probability .99,

w.99

the accumulated time for gas leaking is not more

than 4% of the observation time whenever the

Let G be the set of all equivalence classes of

ꢀ. An equivalence class α ∈ G satisﬁes a clock

observation time is longer than 60 seconds. So,

R

constraint ζ ∈ Z (G) iﬀ ν satisﬁes ζ for some

the (A, [0, 10⁵]) |= [2(` ≥ 60 ⇒

leak ≤

C

ν ∈ α. From the item 2 of Lemma 1, it follows

that α satisﬁes a clock constraint ζ if and only if ν

satisﬁes ζ for any ν ∈ α. An equivalence class β is

said to be the successor of an equivalence class α,

denoted by succ(α) iﬀ for each ν ∈ α, there exists

t ∈ N such that ν + t ∈ β and ν + t⁰∈ α ∪ β

for all t⁰≤ t and t⁰∈ N. Let d_α= sup{t ∈

4% ∗ `)]

for any strategy A says about the

w.99

reliability of the gas burner: its requirement is

satisﬁed with the probability .99 whenever it is

operated for less than 10⁵seconds.

For simplicity and as motivated by the

discretisability of LDI [9] (i.e. an LDI is satisﬁed

by all models if and only if it is satisﬁed by all

integral models), we restrict ourselves to those

strategies in which each transition is of the form

(t, p) where t ∈ N only.

N | ν ∈ α and ν + t ∈ succ(α) and ν + t⁰

∈

α∪β for all t⁰≤ t and t⁰∈ N}. It follows from the

deﬁnition of succ(α) that either d_α= 1 or d_α= ∞.

The latter happens only when succ(α) satisﬁes

x > c for all x ∈ C. The nondeterministic discrete

time behaviors of PTA G can now be described

by the region graph R(G) deﬁned as follows.

Now, we recall a very important technique

from timed automata with some adaptations to

probabilistic timed automata. Let, in the sequel,

G be a PTA.

Integral Region Graph. The key idea for

reducing the state space of timed automata to

a ﬁnite space is the clock equivalence relation

introduced in [16]. In this subsection we recall

this standard notions restricted to the set N^Cof

integral clock valuations. Let c be the max of

integers occurring in clock constraints in G.

Deﬁnition 8. The region graph R(G) is the

Markov decision process (V^∗, Steps^∗, L^∗), where

• the vertex set V^∗b= {hs, αi | s ∈ S and α ∈ G

and α satisﬁes inv(s)}, and

• the transition function Steps^∗: V^∗

→

∗

2^{N×µ(V )}is deﬁned as follows. For each

vertex hs, αi ∈ V^∗:

Deﬁnition 7. The valuations ν, ν⁰∈ N^Care clock

equivalent, denoted by ν ꢀ ν⁰iﬀ

1. ∀x ∈ C, either ν(x) = ν⁰(x), or both ν(x) > c

and ν⁰(x) > c,

1. If the invariant condition inv(s)

is satisﬁed by succ(α) then for

any hs⁰, βi ∈ V^∗, let p^s_su^,α_cc(hs⁰, βi)

2. ∀x, x⁰∈ C, either ν(x)−ν(x⁰) = ν⁰(x)−ν⁰(x⁰),

(

1

if hs⁰, βi = hs, succ(α)i,

or both ν(x)−ν(x⁰) > c and ν⁰(x)−ν⁰(x⁰) > c

=

0

otherwise.

s,α

One important property of the clock

equivalence relation ꢀ is that it has ﬁnite

index and the valuations from the same

Then (t, p ) ∈ Steps^∗(s, α) for any

succ

t ∈ N, 0 < t ≤ d_α. In this case, we say

s,α

type(p ) = >.

succ

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

67

2. If there exists p⁰

∈

prob(s) such

Conversely, for each transition in R(G) of the

t,p^s,α

that α satisﬁes the enabling condition

form hs, αi −→ hs⁰, βi, for any ν ∈ α there

τ_s(p⁰), then for any hs⁰, βi ∈ V^∗let

t,p¯

is a transition hs, νi −→ hs⁰, ν⁰i in M_Gwith

P

p^s_p^,₀^α(hs⁰, βi) = _{X⊆C,α[X:=0]=β}p⁰(s⁰, X).

type(p¯) = type(p^s,α) and ν⁰∈ β.

Then, (0, p^s_p^,₀^α) ∈ Steps^∗(hs, αi). In this

case, we say type(p^s_p^,₀^α) = p⁰.

From this observation each strategy A^∗of R(G)

corresponds one-to-one with an integral strategy

A of M_Gin a sense that will be made precise

soon.

In the deﬁnition of Steps^∗the item (1)

represents the time transitions, and the item (2)

represents the discrete transitions.

With each strategy A^∗of R(G) we can associate

∗

a Markov chain MC^A= (Path^A_fin, P^A) where

A^∗

for ω^∗, ω^0∗∈ Path and hs, αi, hs⁰, α⁰i such that

fin

Deﬁnition 9. A strategy A^∗on the region graph is

a function mapping every nonempty ﬁnite path ω^∗

of R(G) to a pair of integral time t and distribution

last(ω^∗) = hs, αi,

A^∗

P (ω^∗, ω^0∗) =



p^s,αif A^∗(ω^∗) = (t, p^s,α) and



Steps^∗(last(ω^∗)), and

(t,p^s,α





ω^0∗= ω^∗−→⁾hs⁰, α⁰i,

p such that (t, p)

mapping ꢀ to hs¯, 0i.

∈





0

otherwise.

∗

Then, the probabilistic measure Prob^A

By the deﬁnition of transition function Steps^∗,

the number of the (time) transitions of R(G)

between a node (s, α) and (s, succ(α)) is inﬁnite

when d_α= ∞. In the graph, those transitions

are combined into one transition which is labeled

by (∗, 1), where 1 is the probability distribution

assigning probability 1 to the transition from

(s, α) to (s, succ(α)). This transition expresses

that we can choose nondeterministically an

arbitrary integer for time step, and then with the

probability 1, move to the region (s, succ(α)).

Therefore, a strategy A of R(G) will replace ∗

by an integer each time it travels through this

transition. From the deﬁnition of the region graph

R(G) and the timed structure M_G, the paths in

A^∗

on the smallest σ-algebra F_Pathon

A^∗

inf

Path

containing the sets of the forms

A^∗

{ω^∗| ω^∗

∈

Path and ω^0∗is a preﬁx of ω^∗}

inf

A^∗

for any ω^0∗∈ Path is deﬁned as before for

fin

a probabilistic timed structure.

Recall that

from probabilistic timed automaton G, we have

deﬁned a probabilistic timed structure M_Gwhich

generates the probabilistic measure Prob^Aon

A

the smallest σ-algebra F_Pathon Path_i^A_nf. From

the relationship between strategies A^∗of R(G)

and strategies A of M_Gobserved earlier we can

∗

derive a relationship for Prob^Aand Prob^Awhich

plays key role in model checking PDC formulas.

The relation between R(G) and M_Gis expressed

formally as:

R(G) and the paths in M_Gare closely related.

t,p¯

Namely, if in M_Gthere is a transition hs, νi −→

Lemma 2. Let A be an integral strategy of

probabilistic timed automaton G (i.e. an integral

strategy of M_G). Then, there exists an strategy A^∗

of the integral region graph R(G) and an one-to-

hs⁰, ν⁰i, where type(p¯) = p⁰and t ∈ N then

t₁,p₁

t_k,p_k

in R(G) there is a path hs, α₀i −→ . . . −→

0,p^s_p^,α

k

0

hs, α_ki −→ hs⁰, βi such that type(p_i) = >,

A^∗

inf

one mappings γ : Path_i^A_nf→ Path such that:

α_i= succ(α_i−1) for 1 ≤ i ≤ k, type(p^s_p^,₀^α) = p⁰,

k

∗

A

1. Prob^A(Ω) = Prob^A(γ(Ω)) for all Ω ∈ F_Path

,

ν ∈ α₀, ν⁰∈ β, inv(s) is satisﬁed by all α_i, t =

2. P_ω(t) = P_γ(ω)(t) almost everywhere in R^≥0

t₁+ . . . + t_k, and α_ksatisﬁes τ_s(p⁰). Furthermore,

for all ω ∈ Path_i^A_nf

t,p¯

if in M_Gthere is a transition hs, νi −→ hs, ν⁰i

where type(p¯) = > and t ∈ N then in R(G)

Proof. Let γ be the homomorphism deﬁned from

the relation between transitions in M_Gand R(G)

observed as above. Given strategy A, strategy A^∗

is deﬁned based on mapping γ which simulates

t₁,p₁

t_k,p_k

there is a path hs, α₀i −→ . . . −→ hs, α_ki such

that type(p_i) = >, for 1 ≤ i ≤ k, α_i= succ(α_i−1

)

and satisﬁes inv(s), ν ∈ α₀, ν⁰∈ α_k, t = t₁+. . .+t_k.

68

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

A^∗

A by splitting one step (t, p) into several time

steps (1, 1), . . . , (1, 1), (0, p) as given by mapping

γ. Item 2 follows directly from the construction

of A^∗, and Item 1 follows from the fact that for all

graph that generate all the paths in Path that

inf

do not include any such path P (i.e. those paths

that satisfy Ψ for any interval). We assume that

any two paths in P are not nested (if for two

paths in P, one is nested in the other, we can

remove the later without changing the meaning of

P). From the labels of the constructed graph, the

probability of the set of paths can be calculated.

To apply this procedure we need: (a) a technique

to construct the ﬁnite set of paths P in R(G) that

correspond to all DC models that do not satisfy

A^∗

ω ∈ Path^A_fin, Prob^A_fin(ω) = Prob (γ(ω)). The

fin

detailed proof is omitted here.

2

Item 2 of Lemma 2 implies that (ω, [a, b]) |= Ψ

if and only if (γ(ω), [a, b]) |= Ψ for any DC

formula Ψ, for any ω ∈ Path_i^A_{n f}and interval

[a, b]. Combined with Item 1, this implies that

A, t |=

Φ if and only if A^∗, t |=

Φ for any

PDC

A^∗

inf

PDC formula Φ and t ∈ R^≥0.

Ψ1, (b) the set of paths in Path that do not

Depending on how integral strategy A of G is

given, the corresponding strategy A^∗of R(G) can

be found easily based on A. For simplicity, ﬁrstly

include any such path P are ﬁnitely representable

by a graph, and (c) a technique to compute the

probability of the set of inﬁnite paths resulting

from item (b).

Regarding Item (a), the following lemma is

from [9, 10], which says that given a linear

duration invariant Ψ, the set of paths that do not

satisfy Ψ is computable by searching in R(G).

we consider the problem to decide if A, t |=

Φ

PDC

for t ∈ R^≥0. Now consider the following case for

PDC formula Φ:

Φ = [Ψ] , Ψ = 2Ψ1

(1)

wλ

where Ψ1 is a DC formula (to be more general

Ψ is not necessary to be LDI). We have that

Lemma 3.

ꢀ

(

)

A^∗

inf

ꢀ ω ∈ Path and ω is divergent and

in f

ꢀ

1. Given a path ω ∈ Path . A linear duration

ω

ꢀ

(ω, [0, n]) |= Ψ for all n ∈ N

invariant Ψ is satisﬁed by model (ω, [a, b])

for any interval [a, b] if and only if it is

satisﬁed by model (ω, [m, n]) for any integral

interval [m, n].

ꢀ

(

)

A^∗

in f

T

ꢀ ω ∈ Path and ω is

ꢀ

=

ω

.

ꢀ

n≥0

ꢀ

divergent and (ω, [0, n]) |= Ψ

Because the set sequence

A^∗

in f

{ω | ω

∈

Path

and ω is divergent and

2. The set of paths of integral region graph

R(G) that correspond to a DC integral model

that does not satisfy Ψ is constructable.

(ω, [0, n]) |= Ψ} is decreasingly monotonic

(according to the set inclusion relation) when n

∗

A^∗

inf

increases, we have that Prob^A({ω | ω ∈ Path

and ω is divergent and (ω, [0, n]) |= Ψ for all

Regarding Item (b), we have to restrict

ourselves to the class of so-called ﬁnitely

representable strategies A^∗of the region graph

∗

n ∈ N}) = inf_n∈N{Prob^A({ω | ω ∈ Path_i^A_nfand

ω is divergent and (ω, [0, n]) |= Ψ}).

∗

Hence, if we can compute Prob^A({ω | ω ∈

R(G).

A strategy A^∗of R(G) is ﬁnitely

A^∗

inf

representable iﬀ for any path ω^∗of R(G) the value

of A^∗(ω^∗) depends only on the suﬃx of the length

k of ω^∗for a ﬁxed k. An ﬁnitely representable

strategy A^∗of R(G) for the case k = 1 is called

simple strategy. Such a ﬁnitely representable

strategy will be represented by a graph with no

nondeterminism, complete probabilistic choices,

and fully embedded in R(G).

Path and ω is divergent and (ω, [0, n]) |= Ψ for

all n ∈ N}), we can solve the problem to decide if

A^∗, t |= Φ for all t ≥ 0.

Let P be a path in the region graph R(G) that

generates a DC model not satisfying Ψ1. Assume

A^∗

that a path in Path that does not satisfy DC

in f

formula Ψ in an interval if and only if it has

a preﬁx that includes P. Then all the paths in

A^∗

inf

Path that satisfy Ψ for any interval are those

that do not include P. From integral graph R(G),

we can ﬁnd all such paths P that can generate a

DC model not satisfying Ψ1, and can construct a

Deﬁnition 10. Given a ﬁnitely representable

strategy A^∗. A graph representation of A^∗is a

deterministic Markov decision process G(A^∗) =

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

69

∗

(V_A, Steps_A_∗, L_A) which is embedded in the

Although all paths in P are not nested in one

region graph R(G)

=

(V^∗, Steps^∗, L^∗) by a

another, but some of them may overlap some

suﬃxes of ω for a given ﬁnite path ω. Let P_ω

be the set of those such paths of P, P_ω= {ω⁰∈

P|ω⁰= xz and ω = yx for some paths x , ꢀ, y, z}.

Then

mapping ρ, where ρ : V_A→ V^∗, and the

∗

following conditions are satisﬁed:

• There is an initial node called v₀, and

ρ(v₀) = hs¯, 0i,.

• G(A^∗) is deterministic, i.e. Steps_A_∗(v) has

only one element, denoted by Steps_A_∗(v)

itself,

ω∆(last(ω)) \ ∆(last(e)) =

0

∪

(ω ω⁰)ω⁰∆(last(ω⁰)),

ω ∈P_ω

where for ω = yx (x , ꢀ) and ω⁰= xz ∈ P_ω

we deﬁne ω ω⁰= y. From the deﬁnition

A_v^∗

∗

of the_∗functions Prob , v ∈ V_Ait follows

Prob^A

(∆(last(e)) \ ω∆(last(ω))) =

last(e)

∗

• L_A(v) = L (ρ(v)) for all v ∈ V_A

∗

last(e)

(∆(last(e)))−

∗

last(e)

(ω∆(last(ω)))+

• Let Steps_A_∗(v) (t, p), where p is a

=

∗

(ω ω⁰)ω⁰∆(last(ω⁰)))

last(e)

0

(∪

∗

distribution in µ(V_A). The restriction of ρ

ω ∈P_ω

on {v⁰∈ V_A| p(v⁰) > 0} is an one-to-one

∗

Because all paths in P are not nested in one

another, for eω, eω⁰⁰∈ P(v) with ω , ω⁰⁰, we

have ω∆(last(ω)) ∩ ω⁰⁰∆(last(ω⁰⁰)) = ∅. For

simplicity, we assume that for ω⁰₁, ω₂⁰∈ P_ω

mapping, and the distribution ρ_pdeﬁned by

∀s ∈ V^∗• ρ_p(s) = max{p(v⁰) | ρ(v⁰) = s} (by

our convention, max ∅ = 0) is a distribution

in µ(V^∗), and (t, ρ_p) ∈ Steps^∗(ρ(v)).

with ω⁰₁, ω⁰₂, (e(ω

ω⁰₁)ω⁰₁∆(last(ω⁰₁))) ∩

(e(ω ω⁰₂)ω₂⁰∆(last(ω⁰₂))) = ∅. (without this

assumption, we have to modify the technique

Figure 3 shows the integral region graph

of Simple Gas Burner in Fig 1 and graph

representations for ﬁnitely representable

strategies A^∗₁and A₂^∗. The embedding mapping ρ

maps a node in A^∗₁and A^∗₂to the node with the

same label in the integral region graph.

A_n^∗

a little). Therefore, the deﬁnition of Prob ,

∗

n ∈ V_Aimplies

A_v^∗

Prob (∆(v)) =

∗

P

A^∗

Prob (e)Prob^A

(∆(last(e)))−

last(e)

e∈v⁺

fin

∗

P

∗

_eω∈P(v)Prob^A_fin(eω)Prob^A

(∆(last(ω)))) +

last(ω)

P

∗

Regarding Item (c) of the condition for

applying the checking procedure, we have

(Prob^A_fin(e(ω ω⁰)ω⁰)×

eω∈P(v) ω⁰∈P_ω

∗

Prob^A

(∆(last(ω )))) Let us denote

0

last(ω )

A_v^∗

Prob (∆(v)) by P(v). This means that P(v),

Lemma 4. Given a graph representation of a

∗

v ∈ V_Asatisfy:

ﬁnitely representable strategy A^∗, G(A^∗)

=

P(v) =

∗

(V_A, Steps_A_∗, L_A). Given a ﬁnite set P of ﬁnite

paths of G(A^∗). Let Ω be the set of all inﬁnite

paths of G(A^∗) starting from v₀which do_∗not

include any path in P. The probability Prob^A(Ω)

is computable.

P

A^∗

e∈v⁺

Prob (e) ∗ P(last(e))−

fin

P

∗

_ω∈P(v)Prob^A_fin(ω) ∗ P(last(ω))+

P

∗

Prob^A_fin(e(ω

eω∈P(v) ω⁰∈P_ω

ω⁰)ω⁰)P(last(ω⁰)) and P(v) = 1 if no path

in P is reachable from v. These conditions form a

∗

linear equation system for P(v), v ∈ V_A. Solving

Proof. Let ∆(v) be the set of all inﬁnite paths

of G(A^∗) starting from v which do not include

any path in P, A^∗_vbe the strategy represented

it, we can ﬁnd the value of P(v₀) which is the

∗

value of Prob^A(Ω).

2

by G(A^∗) with v as initial node, and P(v) =

The following theorem follows immediately

from these lemmas.

A_v^∗

Prob (∆(v)). Let for each v, P(v) = {ω⁰⁰|ω⁰⁰

∈

P and ω⁰⁰starts from v}. Let v⁺be the set of one-

step paths formed by outgoing edges of v. Then,

∆(v) satisﬁes: ∆(v) =

Theorem 2. For a PDC formula Φ of the

form (1) where Ψ is a linear duration invariant,

it is decidable whether a ﬁnitely representable

+

(∪_e∈v(e∆(last(e)))) \ (∪_eω∈P(v)eω∆(last(ω))).

70

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

*,1

integral strategy A of probabilistic timed

automaton G satisﬁes Φ at any time point t.

1,1

s3,1

s3,2

s3,30

0,1

s3,>30

0,1

Decision Procedure 1. Given a PTA G, given

a ﬁnitely representable strategy A of M_G, our

0,0.8

0,1

s1,0

procedure to decide if A, t |=

Φ for all t ∈ R^≥0,

PDC

1,1

where Φ = [Ψ] , Ψ = 2Ψ1 and Ψ1 is an LDI,

wλ

s1,1

0,0.2

consists of the following steps:

1. Construct the integral region graph R(G) for

G.

0,1

1,1

s2,2

s2,1

2. Construct the ﬁnitely representable strategy

A^∗of R(G) corresponding to A according to

Lemma 2.

Fig. 3: Integral Region Graph for Gas Burner.

3. Construct the set P of all paths R(G) that

corresponds to a a DC model that does not

satisfy Ψ1 (using the technique mentioned in

Lemma 3.

that does not satisfy R. Indeed, ω containing

P₁should contain an interval with length 60 for

which the accumulated leakage time is at least

3 (3 > 2.4 = 4% ∗ 60). Any inﬁnite path

ω of strategy A^∗₁that does not contain P₁as a

sub path satisﬁes R in any interval. Using the

technique in the proof of Lemma 4, we have the

following system of linear equations P(hs1, 0i) =

P(hs1, 1i − 1 ∗ 0.2 ∗ 1 ∗ P(hs2, 2i

4. Find a graph representation of A^∗as

mentioned in Deﬁnition 10.

5. Let Ω be the set of all inﬁnite paths

of G(A^∗) starting from v₀which do not

include any path in P.

Compute the

∗

probability Prob^A(Ω) using the technique in

Lemma 4.If this probability is greater than λ,

then the answer is positive. Otherwise, give

the negative answer.

P(hs1, 1i) = 0.8P(hs3, 1i) + 0.2P(hs2, 1i)

P(hs2, 1i) = P(hs2, 2i) = P(hs3, 1i) = . . .

=

P(hs1, 0i) Solving this system, we get

P(hs1, 0i) = 0. Hence, we can conclude that A₁^∗

Note that using the same techniques, the model

checking problem mentioned in Item 3 at the

beginning of this section is solvable for a PDC

formula Φ of the form (1) where Ψ is a formula

expressing the bounded liveness 2(dPe; ` > b ⇒

` ≤ b; dQe). In general, the problem is solvable

for the case that the set of paths of integral region

graph R(G) that correspond to a DC integral

model that does not satisfy Ψ is constructable. In

[10] we proposed some form for such formulas.

does not satisﬁes requirement [R]

.

w0.6

Now consider strategy A^∗₂. The linear equation

system for this case is: P(hs1, 0i) = P(hs1, 1i −

1 ∗ 0.2 ∗ 1 ∗ P(hs2, 2i

P(hs1, 1i) = 0.8P(hs3, 1i) + 0.2P(hs2, 1i)

P(hs2, 1i) = P(hs2, 2i) = P(hs3, 1i) = . . .

= P(h(s1, 0)⁽¹⁾i) = 1

Solving this equation system, we have

P(hs1, 0i) = 0.8. Hence, (A^∗, t) |=

[R]

for

PDC

w0.8

2

all t ∈ R^≥0.

Example 4. Fig. 3 shows the integral region

graph R(G) of the simple gas burner in Fig. 1,

and Fig. 4 shows two strategies A^∗₁and A₂^∗of the

region graph. We will decide which one among

A^∗₁and A^∗₂satisﬁes the requirement R in Example

2 with a probability not lower than 0.6 using the

technique mentioned above.

Now we return to our general problem

mentioned at the beginning of this section. We

will solve this problem by analyzing the graph

R(G). Let A be the set of all strategies of R(G).

For A ∈ A let ∆ be the set of all inﬁnite paths

A

of A starting from the initial vertex of R(G) that

do not include any path in P. Recall that in

general a strategy A^∗is represented as a tree, and

is embedded in the graph R(G) in the same way as

Any inﬁnite path ω of strategy A^∗₁that goes

through the path

P₁= (s1, 0)(s1, 1)(s2, 1)(s2, 2) contains a model

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

71

1,1

s3,1

s3,2

s3,30

0,1

s3,1

s3,2

s3,30

0,0.8

s1,0

1,1

s1,1

0,0.2

s1,0

1,1

s1,1

0,0.2

0,1

1,1

s2,2

s2,1

s2,2

s2,1

(1)

s3,2

(1)

1,1

s3,1

s3,30

0,1

(1)

s1,0

1,1

(1)

0,1

s1,1

adversary A*1

adversary A*2

Fig. 4: Strategies A^∗₁and A₂^∗.

in Deﬁnition 10. Hence, we can identify a node

and a path in A^∗with a node and a path in R(G)

respectively.

Let k = 1 + max{1, 2|ω| |ω ∈ P}. From

these conditions, we have that if nodes v and

0

∗

v are k-similar then P_A(v) = P_A(v ). Hence,

we can replace v by its equivalence class of the

k-similarity relation, and get a ﬁnite equation

system which is the same as the one for some

k-ﬁnitely representable strategy B^∗₀. Therefore,

For any strategy A^∗a node v of A^∗is said to be

k-similar to a node v⁰of A^∗iﬀ any outgoing path

with the length k of v is the same (when embedded

to R(G)) as an outgoing path with the length k of

v⁰and vice-versa. Since R(G) is a ﬁnite graph,

the number of subtrees representing probabilistic

choices with the height k is ﬁnite. Hence

the k-similarity relation between nodes of A^∗

has ﬁnite index.

0

∗

P_A(v₀) = P_B(v₀) where v₀and v₀are the root

of A^∗and B^∗respectively. Consequently, for any

strategy A^∗, there is a k-ﬁnitely representable B^∗

0

∗

such that P_A(v₀) = P_B(v₀). This ensures that

inf{Prob^A(∆ ) | A ∈ A} = min{Prob^A(∆ ) | A ∈

A

A_k} where A_kdenotes the set of all k-ﬁnitely

∗

Let P_A(v) be the probability of the set of all

representable strategies in A.

inﬁnite paths of A^∗starting from the node v of the

tree representation of A^∗which do not include any

path in P (with condition that the current node is

v). Let for each node v in A^∗, P(v) and P_ωbe

deﬁned as in the proof of Lemma 4. Let v⁺_A_∗be

the set of one-step paths of A^∗formed by outgoing

edges of v in the graph R(G). Similar to the proof

Because A_kis a ﬁnite set, we can use the

technique in Lemma 4 to ﬁnd Prob^A(∆ ) for all

A

A ∈ A_k, and then compute min{Prob^A(∆ ) | A ∈

A

A_k}.

We formulate this result as the

following theorem.

Theorem 3. For a PDC formula Φ of the

form (1) where Ψ is a linear duration invariant, it

is decidable whether Φ is satisﬁed by all integral

strategies of a probabilistic timed automaton G at

any time point.

∗

of Lemma 4, P_A(v) satisﬁes:

P

A^∗

∗

e∈v⁺_A_∗

P_A(v) =

Prob_fin(e) ∗ P_A(last(e))−

P

∗

_ω∈P(v)Prob^A_fin(ω) ∗ P_A(last(ω))+

∗

A_v^∗

0

Prob (∪_eω∈P(v)

∪

(e(ω ω⁰)ω⁰)∆(last(ω⁰)))

ω ∈P_ω

72

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

The decision procedure of this theorem is

formulated as follows.

searching method in the integral region graph

of the timed automaton. The complexity of the

decision procedure is high in general. Since the

problem possesses a potential high complexity,

we have not implemented the technique yet.

Hope that with the increasing computing power

in the future, we can develop an eﬀective tool

for model-checking based on the technique. At

the mean time, we are looking for some special

cases of the problem which are simpler and still

useful for which our technique can work well, and

then implement it as a tool to assist checking the

dependability for embedded systems.

Decision Procedure 2. Given a PTA G, our

procedure to decide if A, t |=

Φ for all ﬁnitely

PDC

representable strategies A of M_G, for all t ∈ R^≥0,

where Φ = [Ψ] , Ψ = 2Ψ1 and Ψ1 is an LDI,

wλ

consists of the following steps:

1. Construct the integral region graph R(G)

for G.

2. Construct the set P of all paths R(G) that

corresponds to a a DC model that does not

satisfy Ψ1 (using the technique mentioned in

Lemma 3. Let k = 1 + max{1, 2|ω| |ω ∈ P}.

3. Construct the ﬁnite set A_kof all k-ﬁnitely

representable strategies in A.

References

4. For each A ∈ A_k, ﬁnd Prob^A(∆ ) using

A

[1] Z. Chaochen, C. Hoare, A. P. Ravn, A calculus

of durations, Information Processing Letters 40 (5)

(1992) 269–276.

[2] C. Zhou, M. R. Hansen, Duration Calculus: A Formal

Approach to Real-Time Systems, Springer-Verlag,

2004.

[3] L. Zhiming, A. Ravn, E. Sorensen, Z. Chaochen,

Towards a Calculus of Systems Dependability, Journal

of High Integrity Systems 1 (1) (1994) 49–65.

[4] D. V. Hung, Z. Chaochen, Probabilistic duration

calculus for continuous time, Formal Asp. Comput.

11 (1) (1999) 21–44.

[5] D. P. Guelev, Probabilistic interval temporal logic and

duration calculus with inﬁnite intervals: Complete

proof systems, Logical Methods in Computer Science

3 (3).

Lemma 4, where ∆ be the set of all inﬁnite

A

paths of A starting from the initial vertex of

R(G) that do not include any path in P.

5. Compute min{Prob^A(∆ ) | A ∈ A_k}. If

A

this probability is greater than λ, then the

answer is positive. Otherwise, give the

negative answer.

This procedure also helps to solve the strategy

synthesis problem. Namely, if we can ﬁnd a

strategy A ∈ A_ksuch that Prob^A(∆ ) is greater

A

than λ, then such a strategy is a solution for the

strategy synthesis problem. Therefore, we have:

[6] D. P. Guelev, D. V. Hung, Reasoning about qos

contracts in the probabilistic duration calculus, Electr.

Notes Theor. Comput. Sci. 238 (6) (2010) 41–62.

[7] C. Zhou, Linear duration invariants, in: Formal

Techniques in Real-Time and Fault-Tolerant Systems,

Third International Symposium Organized Jointly

with the Working Group Provably Correct Systems

- ProCoS, Lu¨beck, Germany, September 19-23,

Proceedings, 1994, pp. 86–109.

Theorem 4. Given a PTA G and a PDC formula

Φ = [Ψ] , where Ψ is an LDI, we can decide

wλ

if there exists a ﬁnitely representable strategy A

such that A, t |=

[Ψ] for all t, and in the

case such a strategy exists, we can ﬁnd it.

PDC

wλ

[8] M. Zhang, D. V. Hung, Z. Liu, Veriﬁcation of linear

duration invariants by model checking CTL properties,

in: J. S. Fitzgerald, A. E. Haxthausen, H. Yenigu¨n

(Eds.), Theoretical Aspects of Computing - ICTAC

2008, 5th International Colloquium, Istanbul, Turkey,

September 1-3, 2008. Proceedings, Vol. 5160 of

Lecture Notes in Computer Science, Springer, 2008,

pp. 395–409.

[9] P. H. Thai, D. V. Hung, Verifying linear duration

constraints of timed automata, in: Z. Liu, K. Araki

(Eds.), Theoretical Aspects of Computing - ICTAC

2004, First International Colloquium, Guiyang, China,

September 20-24, 2004, Revised Selected Papers, Vol.

5. Conclusion

We have presented the problem of checking

probabilistic timed automata against probabilistic

duration calculus formulas. The problem is

decidable for a class of PDC formulas of the

form [Ψ]_wλwhere Ψ is a linear duration invariant,

or a DC formula for bounded liveness. The

technique for model checking is an extension of

our techniques for checking if a timed automaton

satisﬁes a linear duration invariant using a

V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73

73

3407 of Lecture Notes in Computer Science, Springer,

2004, pp. 295–309.

[10] J. Zhao, D. V. Hung, Checking timed automata for

linear duration properties, J. Comput. Sci. Technol.

15 (5) (2000) 423–429.

timed automata against probabilistic duration

properties, in: 13th IEEE International Conference

on Embedded and Real-Time Computing Systems

and Applications (RTCSA 2007), 21-24 August 2007,

Daegu, Korea, 2007, pp. 165–172.

[11] C. Changil, D. V. Hung, On veriﬁcation of linear

occurrence properties of real-time systems, Electr.

Notes Theor. Comput. Sci. 207 (2008) 107–120.

[12] M. Kwiatkowska, G. Norman, R. Segala, J. Sproston,

Automatic veriﬁcation of real-time systems with

[15] C. Baier, M. Kwiatkowska, Model Checking for a

Probabilistic Branching Time Logic with Fairness,

Distributed Computing 11 (3) (1998) 125–155.

[16] R. Alur, D. Dill, A Theory of Timed Automata,

Theoretical Computer Science (1994) 183–235.

[17] M. R. Hansen, C. Zhou, Duration calculus: Logical

foundations, Formal Aspects of Computing 9 (1997)

283–330.

[18] Z. Chaochen, H. M. R., S. P, Decidability and

Undecidability Results in Duration Calculus, in: Proc.

of the 10th Annual Symposium on Theoretical Aspects

of Computer Science (STACS 93), no. 665 in LNCS,

Springer Verlag, 1993.

discrete probability distributions,

Theoretical

Computer Science 282 (1) (2002) 101–150.

[13] M. Kwiatkowska, D. Parker, Automated veriﬁcation

and strategy synthesis for probabilistic systems, in:

D. V. Hung, M. Ogawa (Eds.), Automated Technology

for Veriﬁcation and Analysis, 11th International

Symposium, ATVA 2013, Vol. 8172 of LNCS,

Springer, 2013, pp. 5–22.

[14] D. V. Hung, M. Zhang, On veriﬁcation of probabilistic