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