Towards model - Checking probabilistic timed automata against probabilistic duration properties

 all paths in P are not nested in one
 00 00
 mapping, and the distribution ρp defined by another, for eω, eω ∈ P(v) with ω , ω , we
 ∗ 0 0 00 00
 ∀s ∈ V • ρp(s) = max{p(v ) | ρ(v ) = s} (by have ω∆(last(ω)) ∩ ω ∆(last(ω )) = ∅. For
 0 0
 our convention, max ∅ = 0) is a distribution simplicity, we assume that for ω1, ω2 ∈ Pω
 ∗ ∗ 0 0 0 0 0
 in µ(V ), and (t, ρp) ∈ Steps (ρ(v)). with ω1 , ω2,(e(ω ω1)ω1∆(last(ω1))) ∩
 0 0 0
 (e(ω ω2)ω2∆(last(ω2))) = ∅. (without this
 Figure 3 shows the integral region graph assumption, we have to modify the technique
 ∗
of Simple Gas Burner in Fig 1 and graph a little). Therefore, the definition of ProbAn ,
representations for finitely representable n ∈ VA∗ implies
 ∗
strategies A∗ and A∗. The embedding mapping ρ ProbAv (∆(v)) =
 1 2 ∗
 ∗ ∗ P A∗ A
 + Prob (e)Prob last(e) (∆(last(e)))−
maps a node in A1 and A2 to the node with the e∈v f in
 ∗ ∗
same label in the integral region graph. P A Alast(ω)
 eω∈P(v) Prob f in(eω)Prob (∆(last(ω)))) +
 Regarding Item (c) of the condition for P P A∗ 0 0
 0 ×
 eω∈P(v) ω ∈Pω (Prob f in(e(ω ω )ω )
applying the checking procedure, we have A∗
 Prob last(ω0) (∆(last(ω0)))) Let us denote
 ∗
 Av
Lemma 4. Given a graph representation of a Prob (∆(v)) by P(v). This means that P(v),
 v ∈ V ∗
finitely representable strategy A∗,G(A∗) = A satisfy:
 P(v) =
 ∗ ∗ ∗ P
(VA , StepsA , LA ). Given a finite set of finite P A∗
 ∗ e∈v+ Prob f in(e) ∗ P(last(e))−
paths of G(A ). Let Ω be the set of all infinite ∗
 ∗ P ProbA ω ∗ P last ω
paths of G(A ) starting from v0 which do not ω∈P(v) f in( ) ( ( ))+
 A∗ P P A∗
 P 0 
include any path in . The probability Prob (Ω) eω∈P(v) ω ∈Pω Prob f in(e(ω
is computable. ω0)ω0)P(last(ω0)) and P(v) = 1 if no path
 in P is reachable from v. These conditions form a
Proof. Let ∆(v) be the set of all infinite paths linear equation system for P(v), v ∈ VA∗ . Solving
 ∗
of G(A ) starting from v which do not include it, we can find the value of P(v0) which is the
 ∗ A∗
any path in P, Av be the strategy represented value of Prob (Ω). 2
by G(A∗) with v as initial node, and P(v) = The following theorem follows immediately
 ∗ 00 00
ProbAv (∆(v)). Let for each v, P(v) = {ω |ω ∈ from these lemmas.
P and ω00 starts from v}. Let v+ be the set of one-
step paths formed by outgoing edges of v. Then, Theorem 2. For a PDC formula Φ of the
∆(v) satisfies: ∆(v) = form (1) where Ψ is a linear duration invariant,
 (∪e∈v+ (e∆(last(e)))) \ (∪eω∈P(v)eω∆(last(ω))). it is decidable whether a finitely representable
70 V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73
integral strategy A of probabilistic timed *,1
automaton G satisfies Φ at any time point t. 1,1 1,1
 s3,1 s3,2 s3,30 s3,>30
Decision Procedure 1. Given a PTA G, given 0,1 0,1
 0,0.8
a finitely representable strategy A of MG, our s1,0
 ≥0
procedure to decide if A, t |=PDC Φ for all t ∈ R ,
 1,1
where Φ = [Ψ]wλ, Ψ = 2Ψ1 and Ψ1 is an LDI, 0,1
consists of the following steps: s1,1
 0,0.2
 1. Construct the integral region graph R(G) for 0,1
 1,1
 G. s2,2 s2,1
 2. Construct the finitely 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
 that does not satisfy R. Indeed, ω containing
 satisfy Ψ1 (using the technique mentioned in
 P should contain an interval with length 60 for
 Lemma 3. 1
 ∗ which the accumulated leakage time is at least
 4. Find a graph representation of A as 3 (3 > 2.4 = 4% ∗ 60). Any infinite path
 mentioned in Definition 10. ∗
 ω of strategy A1 that does not contain P1 as a
 5. Let Ω be the set of all infinite paths sub path satisfies R in any interval. Using the
 ∗
 of G(A ) starting from v0 which do not technique in the proof of Lemma 4, we have the
 include any path in P. Compute the following system of linear equations P(hs1, 0i) =
 A∗
 probability Prob (Ω) using the technique in P(hs1, 1i − 1 ∗ 0.2 ∗ 1 ∗ P(hs2, 2i
 Lemma 4.If this probability is greater than λ, P(hs1, 1i) = 0.8P(hs3, 1i) + 0.2P(hs2, 1i)
 then the answer is positive. Otherwise, give P(hs2, 1i) = P(hs2, 2i) = P(hs3, 1i) = ...
 the negative answer. = P(hs1, 0i) Solving this system, we get
 ∗
 Note that using the same techniques, the model P(hs1, 0i) = 0. Hence, we can conclude that A1
checking problem mentioned in Item 3 at the does not satisfies requirement [R]w0.6.
 ∗
beginning of this section is solvable for a PDC Now consider strategy A2. The linear equation
formula Φ of the form (1) where Ψ is a formula system for this case is: P(hs1, 0i) = P(hs1, 1i −
expressing the bounded liveness 2(dPe; ` > b ⇒ 1 ∗ 0.2 ∗ 1 ∗ P(hs2, 2i
` ≤ b; dQe). In general, the problem is solvable P(hs1, 1i) = 0.8P(hs3, 1i) + 0.2P(hs2, 1i)
for the case that the set of paths of integral region P(hs2, 1i) = P(hs2, 2i) = P(hs3, 1i) = ...
graph R(G) that correspond to a DC integral = P(h(s1, 0)(1)i) = 1
model that does not satisfy Ψ is constructable. In Solving this equation system, we have
[10] we proposed some form for such formulas. ∗
 P(hs1, 0i) = 0.8. Hence, (A2, t) |=PDC [R]w0.8 for
 ≥
Example 4. Fig. 3 shows the integral region all t ∈ R 0.
graph R(G) of the simple gas burner in Fig. 1, Now we return to our general problem
 ∗ ∗
and Fig. 4 shows two strategies A1 and A2 of the mentioned at the beginning of this section. We
region graph. We will decide which one among will solve this problem by analyzing the graph
 ∗ ∗
A1 and A2 satisfies the requirement R in Example R(G). Let A be the set of all strategies of R(G).
2 with a probability not lower than 0.6 using the For A ∈ A let ∆A be the set of all infinite paths
technique mentioned above. of A starting from the initial vertex of R(G) that
 ∗
 Any infinite path ω of strategy A1 that goes do not include any path in P. Recall that in
through the path general a strategy A∗ is represented as a tree, and
P1 = (s1, 0)(s1, 1)(s2, 1)(s2, 2) contains a model is embedded in the graph R(G) in the same way as
 V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73 71
 1,1 1,1
 s3,1 s3,2 s3,30 s3,1 s3,2 s3,30
 0,1
 0,0.8 0,0.8
 s1,0 s1,0
 1,1 1,1
 s1,1 s1,1
 0,0.2 0,0.2 0,1
 0,1 0,1
 1,1 1,1
 s2,2 s2,1 s2,2 s2,1
 (1) (1) (1)
 1,1
 s3,1 s3,2 s3,30
 0,1
 (1)
 s1,0
 1,1
 0,1
 s1,1 (1)
 adversary A*1 adversary A*2
 ∗ ∗
 Fig. 4: Strategies A1 and A2.
in Definition 10. Hence, we can identify a node Let k = 1 + max{1, 2|ω| |ω ∈ P}. From
and a path in A∗ with a node and a path in R(G) these conditions, we have that if nodes v and
 0 0
respectively. v are k-similar then PA∗ (v) = PA∗ (v ). Hence,
 we can replace v by its equivalence class of the
 For any strategy A∗ a node v of A∗ is said to be
 k-similarity relation, and get a finite equation
k-similar to a node v0 of A∗ iff any outgoing path
 system which is the same as the one for some
with the length k of v is the same (when embedded
 k-finitely representable strategy B∗. Therefore,
to R(G)) as an outgoing path with the length k of 0 0
 P ∗ (v ) = P ∗ (v ) where v and v are the root
v0 and vice-versa. Since R(G) is a finite graph, A 0 B 0 0 0
 of A∗ and B∗ respectively. Consequently, for any
the number of subtrees representing probabilistic
 strategy A∗, there is a k-finitely representable B∗
choices with the height k is finite. Hence 0
 such that P ∗ (v ) = P ∗ (v ). This ensures that
the k-similarity relation between nodes of A∗ A 0 B 0
 inf{ProbA(∆ ) | A ∈ A} = min{ProbA(∆ ) | A ∈
has finite index. A A
 Ak} where Ak denotes the set of all k-finitely
 Let PA∗ (v) be the probability of the set of all representable strategies in A.
 ∗
infinite paths of A starting from the node v of the Because Ak is a finite set, we can use the
 ∗ A
tree representation of A which do not include any technique in Lemma 4 to find Prob (∆A) for all
 P A
path in (with condition that the current node is A ∈ Ak, and then compute min{Prob (∆A) | A ∈
 ∗ P P
v). Let for each node v in A , (v) and ω be Ak}. We formulate this result as the
 +
defined as in the proof of Lemma 4. Let vA∗ be following theorem.
the set of one-step paths of A∗ formed by outgoing
edges of v in the graph R(G). Similar to the proof Theorem 3. For a PDC formula Φ of the
of Lemma 4, PA∗ (v) satisfies:
 P A∗ form (1) where Ψ is a linear duration invariant, it
PA∗ (v) = ∈ + Prob (e) ∗ PA∗ (last(e))−
 e vA∗ f in
 ∗ is decidable whether Φ is satisfied by all integral
 P A ∗
 ω∈P(v) Prob f in(ω) ∗ PA (last(ω))+ strategies of a probabilistic timed automaton G at
 ∗ 0 0 0
 Av 0
 Prob (∪eω∈P(v)∪ω ∈Pω (e(ω ω )ω )∆(last(ω ))) any time point.
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 searching method in the integral region graph
formulated as follows. of the timed automaton. The complexity of the
Decision Procedure 2. Given a PTA G, our decision procedure is high in general. Since the
procedure to decide if A, t |=PDC Φ for all finitely problem possesses a potential high complexity,
 ≥0 we have not implemented the technique yet.
representable strategies A of MG, for all t ∈ R ,
where Φ = [Ψ]wλ, Ψ = 2Ψ1 and Ψ1 is an LDI, Hope that with the increasing computing power
consists of the following steps: in the future, we can develop an effective tool
 for model-checking based on the technique. At
 1. Construct the integral region graph R(G) the mean time, we are looking for some special
 for G. cases of the problem which are simpler and still
 2. Construct the set P of all paths R(G) that useful for which our technique can work well, and
 corresponds to a a DC model that does not then implement it as a tool to assist checking the
 satisfy Ψ1 (using the technique mentioned in dependability for embedded systems.
 Lemma 3. Let k = 1 + max{1, 2|ω| |ω ∈ P}.
 3. Construct the finite set Ak of all k-finitely
 representable strategies in A. References
 4. For each A ∈ A , find ProbA(∆ ) using
 k A [1] Z. Chaochen, C. Hoare, A. P. Ravn, A calculus
 Lemma 4, where ∆A be the set of all infinite of durations, Information Processing Letters 40 (5)
 paths of A starting from the initial vertex of (1992) 269–276.
 R(G) that do not include any path in P. [2] C. Zhou, M. R. Hansen, Duration Calculus: A Formal
 Approach to Real-Time Systems, Springer-Verlag,
 5. Compute min{ProbA(∆ ) | A ∈ A }. If
 A k 2004.
 this probability is greater than λ, then the [3] L. Zhiming, A. Ravn, E. Sorensen, Z. Chaochen,
 answer is positive. Otherwise, give the Towards a Calculus of Systems Dependability, Journal
 negative answer. of High Integrity Systems 1 (1) (1994) 49–65.
 [4] D. V. Hung, Z. Chaochen, Probabilistic duration
 This procedure also helps to solve the strategy calculus for continuous time, Formal Asp. Comput.
synthesis problem. Namely, if we can find a 11 (1) (1999) 21–44.
 A ∈ A ProbA [5] D. P. Guelev, Probabilistic interval temporal logic and
strategy k such that (∆A) is greater duration calculus with infinite intervals: Complete
than λ, then such a strategy is a solution for the proof systems, Logical Methods in Computer Science
strategy synthesis problem. Therefore, we have: 3 (3).
 [6] D. P. Guelev, D. V. Hung, Reasoning about qos
Theorem 4. Given a PTA G and a PDC formula contracts in the probabilistic duration calculus, Electr.
Φ = [Ψ] , where Ψ is an LDI, we can decide Notes Theor. Comput. Sci. 238 (6) (2010) 41–62.
 wλ [7] C. Zhou, Linear duration invariants, in: Formal
if there exists a finitely representable strategy A Techniques in Real-Time and Fault-Tolerant Systems,
such that A, t |=PDC [Ψ]wλ for all t, and in the Third International Symposium Organized Jointly
case such a strategy exists, we can find it. with the Working Group Provably Correct Systems
 - ProCoS, Lubeck,¨ Germany, September 19-23,
 Proceedings, 1994, pp. 86–109.
5. Conclusion [8] M. Zhang, D. V. Hung, Z. Liu, Verification of linear
 duration invariants by model checking CTL properties,
 We have presented the problem of checking in: J. S. Fitzgerald, A. E. Haxthausen, H. Yenigun¨
probabilistic timed automata against probabilistic (Eds.), Theoretical Aspects of Computing - ICTAC
 2008, 5th International Colloquium, Istanbul, Turkey,
duration calculus formulas. The problem is September 1-3, 2008. Proceedings, Vol. 5160 of
decidable for a class of PDC formulas of the Lecture Notes in Computer Science, Springer, 2008,
form [Ψ]wλ where Ψ is a linear duration invariant, pp. 395–409.
or a DC formula for bounded liveness. The [9] P. H. Thai, D. V. Hung, Verifying linear duration
technique for model checking is an extension of constraints of timed automata, in: Z. Liu, K. Araki
 (Eds.), Theoretical Aspects of Computing - ICTAC
our techniques for checking if a timed automaton 2004, First International Colloquium, Guiyang, China,
satisfies a linear duration invariant using a September 20-24, 2004, Revised Selected Papers, Vol.
 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, timed automata against probabilistic duration
 2004, pp. 295–309. properties, in: 13th IEEE International Conference
[10] J. Zhao, D. V. Hung, Checking timed automata for on Embedded and Real-Time Computing Systems
 linear duration properties, J. Comput. Sci. Technol. and Applications (RTCSA 2007), 21-24 August 2007,
 15 (5) (2000) 423–429. Daegu, Korea, 2007, pp. 165–172.
[11] C. Changil, D. V. Hung, On verification of linear [15] C. Baier, M. Kwiatkowska, Model Checking for a
 occurrence properties of real-time systems, Electr. Probabilistic Branching Time Logic with Fairness,
 Notes Theor. Comput. Sci. 207 (2008) 107–120. Distributed Computing 11 (3) (1998) 125–155.
[12] M. Kwiatkowska, G. Norman, R. Segala, J. Sproston, [16] R. Alur, D. Dill, A Theory of Timed Automata,
 Automatic verification of real-time systems with Theoretical Computer Science (1994) 183–235.
 discrete probability distributions, Theoretical [17] M. R. Hansen, C. Zhou, Duration calculus: Logical
 Computer Science 282 (1) (2002) 101–150. foundations, Formal Aspects of Computing 9 (1997)
[13] M. Kwiatkowska, D. Parker, Automated verification 283–330.
 and strategy synthesis for probabilistic systems, in: [18] Z. Chaochen, H. M. R., S. P, Decidability and
 D. V. Hung, M. Ogawa (Eds.), Automated Technology Undecidability Results in Duration Calculus, in: Proc.
 for Verification and Analysis, 11th International of the 10th Annual Symposium on Theoretical Aspects
 Symposium, ATVA 2013, Vol. 8172 of LNCS, of Computer Science (STACS 93), no. 665 in LNCS,
 Springer, 2013, pp. 5–22. Springer Verlag, 1993.
[14] D. V. Hung, M. Zhang, On verification of probabilistic