VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73
Towards Model-checking Probabilistic Timed
Automata against Probabilistic Duration PropertiesI
Van Hung Dang1;, Miaomiao Zhang2, Dinh Chinh Pham1
1 VNU University of Engineering and Technology, Hanoi, Vietnam
2School 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
In 1992, Chaochen Zhou, Hoare C.A.R and
reasoning about QoS contracts in component-
Anders Ravn introduced Duration Calculus [1]
based real-time systems.
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
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
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.
Kwiatkowska et al in [12, 13] proposed a
variant of probabilistic timed automata that
allows probabilistic choice only at discrete
I ThisresearchwasfundedbyVietnamNationalFoundation
for Science and Technology Development (NAFOSTED)
under grant number 102.03-2014.23.
 Corresponding author. Email: dvh@vnu.edu.vn
transitions. To resolve the nondeterminism
between the passage of time and discrete
transitions they used the concept of strategy
which is essentially a deterministic schedule
58
P
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
we generalize this technique to achieve our goal
strategy forms a Markov chain, and hence the
with a model-checking algorithm.
satisfaction of a probabilistic timed CTL formula
The ﬁrst version of this paper was published
by this set can be deﬁned, and then based on
in [14].
In this extended version, in addition to
the
region
graph
of
the
timed
automaton
the
the problem of veriﬁcation, we formulate also
satisfaction of a probabilistic timed CTL formula
the problem of strategy synthesis, i.e.
to decide
by the timed automaton can be also veriﬁed.
if there is a strategy for a probabilistic timed
The idea of ﬁxing a strategy when studying the
automaton
that
satisﬁes
a
probabilistic
linear
probabilistic behavior of a probabilistic timed
duration invariant and show that this problem is
automaton restricts the scope of the veriﬁcation
also solvable.
We provide all proof details and
problem
signiﬁcantly,
making
the
checking
algorithms for doing model-check.
problem more tractable.
Then,
verifying the
Our paper is organized as follows.
In the
set of all strategies against a given probabilistic
next section we present the Probabilistic Timed
property can be done by searching for the “worst
Automata
model.
Section
3
presents
syntax
case”
strategy
according
to
the
probabilistic
and semantics of our PDC. Our main results is
propertyandthenapplytheveriﬁcationtechnique
presented in Section 4 where we formulate our
toit. Thisideaisamotivationforustoreconsider
model checking problem and give our solution to
the
problem
of
checking
a
probabilistic
it. The last section is the conclusion of the paper.
timed
automaton
for
a
PDC
formula
that
we gave up before.
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
2. Probabilistic Timed Automata
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.
for
the
probability
of
the
satisfaction
of
a
Probability distributions and Markov decision
DC
formula
by
a
strategy
for
an
interval.
processes.
A discrete probability distribution
We
use
the
behavioral
model
proposed
by
over a set S is a mapping p : S
! [0;1] such
Kwiatkowska et al to deﬁne the semantics of
our logic. Since probabilistic timed CTL and
PDC are not comparable, and since for many
that the set fs j s 2 S and p(s) > 0g is ﬁnite, and
s2S p(s) = 1. The set of all discrete probability
distributions over S is denoted by (S).
probabilistic properties PDC is more convenient
A
Markov
decision
process
is
a
tuple
to
specify,
a
model
checking
technique
for
(Q;Steps),
where
Q
is
a
set
of
states,
and
checking
probabilistic
timed
automata
against
Steps
:
Q
!
2(Q)
is a function assigning
PDC properties is useful. To solve this problem,
a set of probability distributions to each state.
weﬁrstdevelopatechniquetodecideifastrategy
The
intuition
is
that
the
Markov
decision
in
a
probabilistic
timed
automaton
satisﬁes
a
process
traverses
the
state
space
by
making
PDC formula of a certain form.
This technique
transitions determined by Steps: in a state s, the
is
essentially
an
extension
of
our
technique
process selects nondeterministically a probability
developed earlier in [10, 9] to check if a timed
distribution
p
in
Steps(s),
and
then
makes
a
automaton satisﬁes a DC formula in the form
probabilistic choice according to p as to which
of linear duration invariants or discretisable DC
state to move to.
As in [12] we label the action
formulas
based
on
searching
in
the
integral
selecting a probability distribution with a letter
a;p
l
l l
0
1 2
l
l l
0
1 2
l
l l
0
1 2
0
1 2
0
l
l
l
l l
0
0
1
1 2
1
l
2
2
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
on all other clocks. For t 2 R0, we write  + t
 is a set of actions. The intuition now becomes
fortheclockvaluationthatassigns(x)+t toeach
that the Markov decision process traverses the
clock x 2 C. A constraint over C is an expression
state space by making transitions determined by
of the form xi  c or xi xj  c, where i ,
j,
Steps:
in a state
s,
the process performs an
i; j  n and 2 f<;;>;g and c 2 N. A clock
action a
2
 selecting nondeterministically a
valuation  satisﬁes a clock constraint xi

c
probability distribution p in Steps(s), and then
(xi xj  c) i (xi)  c ((xi) (xj)  c). A
makes a probabilistic choice according to p as to
which state to move to. So, a transition is of the
form s ! s0, where (a; p) 2   (Q) is the
zoneofCisaconvexsubsetofthevaluationspace
(R0)C described by a conjunction of constraints.
For a zone  and a set of clocks X  C the set
label of the transition. We also assume a labeling
f[X := 0] j  2 g is also a zone, and is denoted
function L
:
Q
!
2AP, where AP is a set of
by [X := 0]. Let ZC denote the set of all zones
atomic propositions, that associates a state s with
of C.
the set of atomic propositions that hold at state
s. Then, a labeled Markov decision process is
a tuple (Q;Steps;L).
Labeled paths (or execution sequences)
are nonempty ﬁnite or inﬁnite sequence of
consecutive transitions of the form
Probabilistictimedautomataandprobabilistic
timed structures. Timed automata were
introduced in [16] as a model of real-time
systems. They are extended with discrete
probability distribution to model probabilistic
real-timesystems. Inthesequel,let APbeagiven
!
=
s0 ! s1 ! s2 ! :::;
set of atomic propositions.
where si arestatesandli arelabelsfortransitions.
For a path !, let first(!) denote the ﬁrst state
of !, and if ! is ﬁnite then let last(!) denote
Deﬁnition 1. A probabilistic timed automaton
(PTA) is a tuple G = (S;L;s¯;C;inv; prob;
hsis2S) consisting of
the last state of !. j!j is the length of ! and is
deﬁned as the number of transition occurrences
in ! which is 1 if ! is inﬁnite. For k  j!j,
 a ﬁnite set S of nodes, a start node s¯ 2 S, a
ﬁnite set C of clocks,
let !(k) denote the kth state of !, and step(!;k)
denote the label of the kth transition in !. For
two paths ! = s0 ! s1 ! s2 ! :::sn
0 0 0
and !0 = s0 ! s0 ! s0 ! ::: such that
sn = s0, the concatenation of ! and !0 is deﬁned
0 0
as !!0 = s0 ! s1 ! s2 ! :::sn ! s0 !
0
s0 ! :::.
Clocks,clockvaluations,clockconstraints. Let
R0 denote the set of non negative real numbers.
 a function L : S ! 2AP assigning 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 :
S ! ZC assigningtoeachnodeaninvariant
condition,
 a function prob : S ! 2(S2C) assigning
to each node a set of discrete probability
distributions on S2C,
A clock is a real-valued variable which increases
at the same rate as real time. Let C = fx1 :::;xng
be a set of clocks. A clock valuation is a function
 : C ! R0 that assigns a real value to each
clock. Let (R0)C denote the set of all clock
 a family of functions hsis2S where, for any
s 2 S, s : prob(s) ! ZC assigns to each
p 2 prob(s) an enabling condition.
The last item in the deﬁnition says that all the
valuations, and 0 denote the clock valuation that
probabilistic choices according to a probabilistic
assigns 0 to each clock in C. For a set of clocks
distribution (selected at a node) have the same
X  Cwedenoteby[X := 0]theclockvaluation
enabling
condition.
The
probabilistic
timed
that assigns 0 to all clocks in X and agrees with 
automaton behaves nearly in the same way as a

# Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties

Đăng ngày | Thể loại: | Lần tải: 0 | Lần xem: 1 | Page: 16 | FileSize: 0.00 M | File type: PDF
1 lần xem

## Nội dung

VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73 Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration PropertiesI Van Hung Dang1;, Miaomiao Zhang2, Dinh Chinh Pham1 1 VNU University of Engineering and Technology, Hanoi, Vietnam 2School 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 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 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 I ThisresearchwasfundedbyVietnamNationalFoundation for Science and Technology Development (NAFOSTED) under grant number 102.03-2014.23. Corresponding author. Email: dvh@vnu.edu.vn 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. 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. 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 between the passage of time and discrete transitions they used the concept of strategy which is essentially a deterministic schedule 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 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 automaton restricts the scope of the veriﬁcation also solvable. We provide all proof details and problem signiﬁcantly, making the checking algorithms for doing model-check. problem more tractable. Then, verifying the Our paper is organized as follows. In the set of all strategies against a given probabilistic next section we present the Probabilistic Timed property can be done by searching for the “worst Automata model. Section 3 presents syntax case” strategy according to the probabilistic and semantics of our PDC. Our main results is propertyandthenapplytheveriﬁcationtechnique toit. Thisideaisamotivationforustoreconsider presented in Section 4 where we formulate our model checking problem and give our solution to the problem of checking a probabilistic it. The last section is the conclusion of the paper. timed automaton for a PDC formula that we gave up before. 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 2. Probabilistic Timed Automata 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. for the probability of the satisfaction of a Probability distributions and Markov decision DC formula by a strategy for an interval. processes. A discrete probability distribution We use the behavioral model proposed by over a set S is a mapping p : S ! [0;1] such Kwiatkowska et al to deﬁne the semantics of our logic. Since probabilistic timed CTL and PDC are not comparable, and since for many that the set fs j s 2 S and p(s) > 0g is ﬁnite, and s2S p(s) = 1. The set of all discrete probability distributions over S is denoted by (S). probabilistic properties PDC is more convenient A Markov decision process is a tuple to specify, a model checking technique for checking probabilistic timed automata against PDC properties is useful. To solve this problem, (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. weﬁrstdevelopatechniquetodecideifastrategy The intuition is that the Markov decision in a probabilistic timed automaton satisﬁes a process traverses the state space by making PDC formula of a certain form. This technique transitions determined by Steps: in a state s, the is essentially an extension of our technique process selects nondeterministically a probability developed earlier in [10, 9] to check if a timed distribution p in Steps(s), and then makes a automaton satisﬁes a DC formula in the form of linear duration invariants or discretisable DC probabilistic choice according to p as to which state to move to. As in [12] we label the action formulas based on searching in the integral 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 2 selecting nondeterministically a probability distribution p in Steps(s), and then makes a probabilistic choice according to p as to which state to move to. So, a transition is of the form s ! s0, where (a; p) 2 (Q) is the label of the transition. We also assume a labeling function L : Q ! 2AP, 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). Labeled paths (or execution sequences) are nonempty ﬁnite or inﬁnite sequence of consecutive transitions of the form on all other clocks. For t 2 R0, we write + t fortheclockvaluationthatassigns(x)+t toeach clock x 2 C. A constraint over C is an expression of the form xi c or xi xj c, where i , j, i; j n and 2 f<;;>;g and c 2 N. A clock valuation satisﬁes a clock constraint xi c (xi xj c) i (xi) c ((xi) (xj) c). A zoneofCisaconvexsubsetofthevaluationspace (R0)C described by a conjunction of constraints. For a zone and a set of clocks X C the set f[X := 0] j 2 g is also a zone, and is denoted by [X := 0]. Let ZC denote the set of all zones of C. Probabilistictimedautomataandprobabilistic timed structures. Timed automata were introduced in [16] as a model of real-time systems. They are extended with discrete probability distribution to model probabilistic real-timesystems. Inthesequel,let APbeagiven ! = s0 ! s1 ! s2 ! :::; set of atomic propositions. where si arestatesandli arelabelsfortransitions. For a path !, let first(!) denote the ﬁrst state of !, and if ! is ﬁnite then let last(!) denote the last state of !. j!j is the length of ! and is deﬁned as the number of transition occurrences in ! which is 1 if ! is inﬁnite. For k j!j, let !(k) denote the kth state of !, and step(!;k) denote the label of the kth transition in !. For two paths ! = s0 ! s1 ! s2 ! :::sn 0 0 0 and !0 = s0 ! s0 ! s0 ! ::: such that sn = s0, the concatenation of ! and !0 is deﬁned 0 0 as !!0 = s0 ! s1 ! s2 ! :::sn ! s0 ! 0 s0 ! :::. Clocks,clockvaluations,clockconstraints. Let R0 denote 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 = fx1 :::;xng be a set of clocks. A clock valuation is a function : C ! R0 that assigns a real value to each clock. Let (R0)C denote 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 Deﬁnition 1. A probabilistic timed automaton (PTA) is a tuple G = (S;L;s¯;C;inv; prob; hsis2S) consisting of a ﬁnite set S of nodes, a start node s¯ 2 S, a ﬁnite set C of clocks, a function L : S ! 2AP assigning 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 : S ! ZC assigningtoeachnodeaninvariant condition, a function prob : S ! 2(S2C) assigning to each node a set of discrete probability distributions on S2C, a family of functions hsis2S where, for any s 2 S, s : prob(s) ! ZC assigns to each p 2 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 X Cwedenoteby[X := 0]theclockvaluation enabling condition. The probabilistic timed that assigns 0 to all clocks in X and agrees with 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 1 s3 Nonleak x:=0 x>=30 x:=0 d s1 x:=0 x<=1 1 x<=1 a x:=0 b x<=1 0.8 0.2 function prob is given as: prob(s1) = fp0; p1g, prob(s2) = fp2g, prob(s3) = fp3g, where p0(s3;fxg) = 1, p1(s3;fxg) = 0:8, p1(s2;;) = 0:2. p2(s3;fxg) = 1, p3(s1;fxg) = 1, and s1(p0) = s1(p1) = fx 1g, s2(p2) = fx 2g and s3(p3) = fx 30g. The function inv is deﬁned as inv(s1) = fx 1g, inv(s2) = fx 2g and inv(s3) = true. The labels of states are given x<=2 1 c s2 x<=2 Leak by function L deﬁned as L(s1) = L(s2) = leak, and L(s3) = nonleak. Asin[12]weuseprobabilistictimedstructures as underlying semantics model for PTA. Fig. 1: A probabilistic timed automaton for a simple gas burner. timed automaton does, except that it has to select a probability distribution at each discrete step. We denote by ZC(G) the set of all clock zones occurring in G, ZC(G) = finv(s) 2 ZC j s 2 Sg[ fs(p) 2 ZC j s 2 S and p 2 prob(s)g: Example 1. Fig. 1 shows a probabilistic timed automaton for a simple gas burner. 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 denotedbytransitionaisthatwiththeprobability 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,andwithprobability0:2theﬂamefailsto beonwithinonesecond,andthesystemmovesto 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 systementered s1lasttime,andthesystemmoves 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 Deﬁnition 2. A probabilistic timed structure M isalabeledMarkovdecisionprocess(Q;Steps;L) where Q is a set of states, Steps : Q ! 2R0(Q) is a function which assigns to each state q 2 Q a set Steps(q) of pairs of the form (t; p), where t 2 R0 and p 2 (Q), and L : Q ! 2AP is a state labeling function. Function Steps speciﬁes the set of transitions that M can choose nondeterministically at each state. Therefore, if at state q 2 Q, M chooses (t; p) 2 Steps(q), then after t time units have elapsed, a probabilistic transition is made to state q0 with probability p(q0). A path of M is a nonempty ﬁnite or inﬁnite sequence: ! = q0 ! q1 ! q2 ! ::: where qi 2 Q, (ti; pi) 2 Steps(si), and pi(qi+1) > 0 for all 0 i j!j. For a given probabilistic timed structures M we denote by Pathfin (Pathinf) the set of ﬁnite (inﬁnite) paths, and by Pathfin(q) (Pathinf(q)) the set of paths in Pathfin (Pathinf) that start from state q. Let ! be inﬁnite. A position of ! is a pair (i;t), where i 2 N and t 2 R0 such that 0 t ti. The state at position (i;t) is denoted by state!(i;t). Given two positions (i;t) and (j;t0) of !, we say (j;t0) precedes (i;t) (in !, written by (j;t0) (i;t)) if j < i or j = i and t0 < t. Deﬁnition 3. For any path ! of a probabilistic timed structure M and 0 i j!j we deﬁne D!(i), the elapsed time until the ith transition, as follows: D!(0) = 0 and for any 1 i j!j: D!(i) = Pj=0 tj: 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 2 R0, there exists j 2 N such that D!(j) > t. Let ! be inﬁnite. For each state q 2 Q, we deﬁne a f0;1g-valued function q : R0 ! f0;1g as > 1 i there exists a position (i;t0) s.t. > t0 > 0, state!(i;t0) = q and > t = D!(i)+t0, 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 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(!) 2 which for all !0 2 Pathfin contains the sets f! j ! 2 Pathinf and !0 is a preﬁx of !g. Let ProbA : PathA ! [0;1] be the mapping deﬁned inductively on the length of paths in Pathfin as follows. If j!j = 0 then Probfin(!) = 1. Let !0 2 Pathfin be a ﬁnite path of A. If !0 = ! ! q for some ! 2 Pathfin, then we let Probfin(!0) = Probfin(!)PA(!;!0). The measure ProbA on FA is the unique measure such that ProbA(f! j ! 2 PathA and !0 is a preﬁx of !g) = ProbA (!0). 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, ProbA(f! j ! 2 PathA and ! is divergentg) = 1. We now deﬁne the behavior of probabilistic timedautomata by associatingevery 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. 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 Let us denote a preﬁx of length i of ! by !(i), and deﬁne for a given strategy A > A() = !(0); and > PathA = >! 2 Pathfin step(!;i) = A(!(i)) > for 0 i < j!j 8 A() = !(0); and 9 PathA = >! 2 Pathinf step(!;i) = A(!(i)) > for 0 i Recall that step(!;i) returns the label of the ith transition in !. From Deﬁnition 4, all ! in PathA and PathA start from the same state deﬁned by A(), and intuitively they represent the behaviors of M according to the scheduler A, A sequential Markov chain MCA = (PathA ;PA) is associated with a strategy A in a natural way to express the executions of M according to A, where PA is deﬁned as > p(q) if A(!) = (t; p) and PA(!;!0) = > !0 = ! ! q, 0 otherwise. Let FPath be the smallest -algebra on Pathinf the probabilistic timed structure MG = (QG;StepsG;LG) as follows. QG = fhs;i j s 2 S; 2 (R0)Cg The function StepsG : QG ! 2R0(QG) assigns to each state in QG a set of transitions, each of which takes the form (t; p¯) where t 2 R0 and p¯ is a discrete probabilistic distribution on Q, and is deﬁned as: – (t; p¯) 2 StepsG(hs;i) if there exists p 2 prob(s) such that (a) the valuation + t satisﬁes s(p) and + t0 satisﬁes inv(s) for all 0 t0 t, and (b) for any hs0;0i 2 QG: p¯(hs0;0i) = XC^(+t)[X:=0]=0 p(s0;X). For convenience, we refer to p¯ as having type p, denoted by type(p¯) = p. – Let (t; p¯) 2 Steps (hs;i) if (a) the valuation + t0 satisﬁes inv(s) for all 0 t0 t, and (b) for any hs0;0i 2 V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73 63 QG: p¯(hs0;0i) = 1 if hs0;0i = hs; + ti, and p¯(hs0;0i = 0 otherwise. We refer to p¯ as having type >, i.e. type(p¯) = >. ThelabelingfunctionL : Q ! 2AP isdeﬁned as: LG(hs;i) = L(s) for all hs;i 2 QG. 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 MG is also called strategy for probabilistic timed automaton G. Example 2. The following path is a path of (a strategy of) the timed structure of the timed automaton in Fig. 1: ! = hs1;0i ! hs3;0i ! hs1;0i ! hs2;:7i ! hs3;0i ! hs3;30i ! hs3;130i ! :::: For a given inﬁnite divergent path ! of MG, for an atomic proposition P 2 AP, let us deﬁne a f0;1g-valued function P! : R0 ! f0;1g by P!(t) = maxfq!(t) j q = hs;i 2 QG and P 2 L(s)g (note that there can be several regions hs;i in the path ! for which P 2 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. 3. Probabilistic Duration Calculus 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. The calculus introduced in this paper has an intuitive semantics based 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. 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. ::= j [ ]w j : j ^; ::= R(;:::;) j : j ^ j ; ; ::= S j F(;:::;); S ::= 1 j P j:S j 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. 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 R0. Given a path ! of MG according to a strategy A. The interpretation of state expression S is a f0;1g-valued function I! : R0 ! f0;1g deﬁned inductively as: I!(t) = 1 for all t 2 R0, I! = P! where P! is deﬁned as in Section 2, I! = 1 I!, and I! = minfI! ;I! g. (Note that the operations on functions is deﬁned point-wise.) The interpretationofatermisafunctionI! : Intv ! R0 deﬁned as I!S([a;b]) = a IS (t)dt, and I! ([a;b]) = f(I! ([a;b]);:::;I! ([a;b])) for any interval [a;b] 2 Intv. 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 j= between a model (!;[a;b]) and a DC formula which is deﬁned as follows. (!;[a;b]) j= R(1;:::;k) i R(I1([a;b]);:::;Ik([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]) j= : i (!;[a;b]) j= , automaton G, any path ! of G, and any time (!;[a;b]) j= (!;[a;b]) j= 1^ 2i(!;[a;b]) j= 1and 2, interval [a;b]. A PDC formula is said to be valid i (A;t) j=PDC holds for any probabilistic timed automatonG, strategy A ofG, and t 2 R0. (!;[a;b]) j= 1; 2 i (!;[a;m]) j= 1 and (!;[m;b]) j= 2 for some m 2 [a;b]. The probability measure ProbA will 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 MG and 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 satisfaction relation j=PDC between PDC models (A;t) and PDC formulas is deﬁned as: For a DC formula , (A;t) j=PDC i ProbA(f! j ! 2 PathA and ! is divergent and (!;[0;t]) j= g) = 1, For a DC formula , (A;t) j=PDC [ ]w i ProbA(f! j ! 2 PathA and ! is divergent and (!;[0;t]) j= g) , (A;t) j=PDC : i (A;t) j=PDC (A;t) j=PDC 1 ^ 2 i (A;t) j=PDC 1 and (A;t) j=PDC 2. 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 inducedby A,notforasinglepath. Butthereason for selecting an interval of the form [0;t] instead of [a;b] is just for convenience. The computation of ProbA(B) for a set B of paths satisfying a In [17, 2] a proof system for DC for deriving valid formulas has been presented. It follows directlyfromthedeﬁnitionofsemanticsthatPDC 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. Theorem 1. For any DC formulas , 1 and 2 []w1 , is a valid PDC formula, If is a valid DC formula, then it is a valid PDC formula, ((1 ) 2) ^ [1]w) ) [2]w is a valid PDC formula :(1 ^ 2) ^ [1]w1 ^ [2]w2 ) [1 _ 2]w1+2 is a valid PDC formula. Proof. Straightforward from the deﬁnition of semantics of DC and PDC. 2 As usual in DC, we use the following abbreviations: ‘b= 1, Trueb=‘ 0, 3 b=True; ;True (there exists a subinterval for which is satisﬁed), 2 b=:3: (for all subintervals is satisﬁed), dSeb= 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. DC formula in an interval [a;b] needs the Example 3. Let us consider the simple gas preﬁxes in the whole interval [0;b] of paths in burner in Example 1 (see Fig. 1). Let one of B. Intuitively, a strategy A of probabilistic timed the requirements for the gas burner is that for automaton G satisﬁes a DC formula in the any observation interval the length of which is probabilisticsettingatatimetithesetofinﬁnite not shorter than 60 seconds, the accumulated divergent paths ! produced by A that satisfy in the interval [0;t] has the probability 1. 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]) j= holds for any probabilistic timed formalized as a DC formula R b= 2(‘ 60 ) 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 0.8