logo

SCIENCE CHINA Information Sciences, Volume 61, Issue 5: 052105(2018) https://doi.org/10.1007/s11432-017-9133-4

Anti-chain based algorithms for timed/probabilistic refinement checking

More info
  • ReceivedMay 22, 2017
  • AcceptedJun 9, 2017
  • PublishedDec 6, 2017

Abstract

Refinement checking answers the question on whether an implementation model is a refinement of a specification model, which is of great value for system verification. Some refinement relationships, e.g., trace refinement and failures/divergence refinement, have been recognized for different verification purposes. In general, refinement checking algorithms often rely on subset construction, which incurs in the state space explosion problem. Recently the anti-chain based approach has been suggested for trace refinement checking, and the results show a significant improvement. In this paper, we investigate the problems of applying the anti-chain approach to timed refinement checking (a timed implementation vs. a timed or untimed specification) and probabilistic refinement checking (a probabilistic implementation vs. a non-probabilistic specification), and show that the state space can be reduced considerably by employing the anti-chain approach. All the algorithms have been integrated into the model checking tool PAT, and the experiments have been conducted to show the efficiency of the application of anti-chains.


Acknowledgment

This work was supported by National Natural Science Foundation of China (Grant Nos. 61602412, 61103044, U1509214, 61402406) and Natural Science Foundation of Zhejiang Province of China (Grant No. LY16F020035).


Supplement

Appendix

Proofs for all the sections

Theorem 1. Given a timed automaton ${\cal~A}$ and an LTS ${\cal~L}$, ${\rm~traces}_{\rm~ZG}({\cal~A})~\subseteq~{\rm~traces}({\cal~L})$ iff there is no reachable state $(s,~\delta,~\emptyset)$ in ${\rm~ZG}_{\rm~AL}$.

proof (if) Let $|\pi|$ be the length of a trace $\pi$. If ${\rm~traces}_{\rm~ZG}({\cal~A})~\subsetneq~{\rm~traces}({\cal~L})$, there is a trace $\pi_A$ in ${\rm~traces}_{\rm~ZG}({\cal~A})$ and a trace $\pi_L$ in ${\rm~traces}({\cal~L})$, such that $\pi_L$ is a maximal prefix of $\pi_A$ satisfying (1) $|\pi_L|~=~|\pi_A|-1$; (2) $\pi_A$ is not in ${\rm~traces}({\cal~L})$. Let $(s,~\delta,~W)$ be the abstract configuration, where $(s,~\delta)$ is a state in ${\rm~ZG}({\cal~A})$ with which a run of ${\rm~ZG}({\cal~A})$ exhibiting $\pi_L$ ends, and $W$ is a state in ${\rm~det}(\cal~L)$ with which a run of ${\rm~det}(\cal~L)$ exhibiting $\pi_L$ ends. Notice that $W$ is not empty. Next, $(s,\delta)$ can perform an event and transit to $(s',~\delta')$ (exhibiting $\pi_A$), but none of $y$ in $W$ can perform the same event because $\pi_A$ is not in ${\rm~traces}({\cal~L})$. Thus, an abstract configuration $(s',~\delta',~\emptyset)$ is reachable. As a result, if there is no reachable state $(s,~\delta,~\emptyset)$ in ${\rm~ZG}_{\rm~AL}$, ${\rm~traces}_{\rm~ZG}({\cal~A})~\subseteq~{\rm~traces}({\cal~L})$ holds.

(only-if) It is proved straightforwardly. If ${\rm~traces}_{\rm~ZG}({\cal~A})~\subseteq~{\rm~traces}({\cal~L})$, then any trace $\pi$ performed by ${\rm~ZG}({\cal~A})$ can also be performed by ${\cal~L}$. Thus $(s,~\delta,~\emptyset)$ is not reachable.

Lemma 2. Let $(s,~\delta,~W)$ and $(s,~\delta',~W')$ be two abstract configurations in $\mathit{{\rm~ZG}_{\rm~AL}}$. If $(s,~\delta,~W)~\lesssim~(s,~\delta',~W')$, then a TATR-witness state is reachable from $(s,~\delta,~W)$ implies a TATR-witness state is reachable from $(s,~\delta',~W')$.

proof By induction. (1) First, the base case is that $(s,~\delta,~W)$ is a TATR-witness state (that is, $W~=~\emptyset$), because $W'~\subseteq~W$, $W~=~\emptyset$ and therefore $(s,~\delta',~W')$ is also a TATR-witness state. (2) For the induction step, suppose that $(s,~\delta,~W)~\lesssim~(s,~\delta',~W')$, and a TATR-witness state is reachable from $(s,~\delta,~W)$ implies a TATR-witness state is reachable from $(s,~\delta',~W')$. Given that $((s_0,~\delta_0,~W_0),~e,~(s,~\delta,~W))$ is a transition in ${\rm~ZG}_{\rm~AL}$, and $(s_0,~\delta_0',~W_0')$ satisfies $\delta_0~\subseteq~\delta_0'$ and $W_0'~\subseteq~W_0$ (i.e., $(s_0,~\delta_0,~W_0)~\lesssim~(s_0,~\delta_0',~W_0')$). Then there is also a transition labelled with $e$ from $(s_0,~\delta_0',~W_0')$, since the first parts of $(s_0,~\delta_0,~W_0)$ and $(s_0,~\delta_0',~W_0')$ are the same. Thus we can get $((s_0,~\delta_0',~W_0'),~e,~(s,~\delta',~W'))$ is a transition in ${\rm~ZG}_{\rm~AL}$, where $\delta~\subseteq~\delta'$ and $W'~\subseteq~W$, because by the same transition and event from $s_0$, $W_0'~\subseteq~W_0$ implies $W'~\subseteq~W$, and $\delta_0~\subseteq~\delta_0'$ implies $\delta~\subseteq~\delta'$. Therefore, the induction step holds.

When exploring $\mathit{{\rm~ZG}_{\rm~AL}}$, $(s,~\delta,~W)$ is found and there exists a configuration $(s,~\delta',~W')$ (which has been visited before) satisfying $(s,~\delta,~W)~\lesssim~(s,~\delta',~W')$, then we do not need to search from $(s,~\delta,~W)$. The above induction will end until $(s,~\delta,~W)$ and $(s,~\delta',~W')$ have been reached. As a summary, the lemma holds.

Theorem 2. Algorithm sect. 3.2 returns true iff ${\rm~traces}_{\rm~ZG}({\cal~A})~\subseteq~{\rm~traces}({\cal~L})$.

proof Because the zones are finite (with normalization), the number of product states is finite and the algorithm eventually terminates. Let ${\rm~ps}$ be an abstract configuration in $\mathit{{\rm~ZG}_{\rm~AL}}$. Define ${\rm~Dist}({\rm~ps})~\in~N\cup\{\infty\}$ as the length of the shortest TATR-witness trace from ${\rm~ps}$ (if a TATR-witness state is not reachable from ${\rm~ps}$, ${\rm~Dist}({\rm~ps})=\infty$). For a set of states $S$, if $S=\emptyset$, ${\rm~Dist}(S)=\infty$, otherwise, ${\rm~Dist}(S)=\min_{s\in~S}{{\rm~Dist}(s)}$. We prove the correctness of the algorithm using the following invariants which are quite similar to [16].

If there exists a TATR-witness state ${\rm~ps}$ in working $\cup$ anti, then ${\rm~ps}$ is reachable from a state in ${\rm~Init}$.

If there is a reachable TATR-witness state, then Dist(anti) $>$ Dist(working).

Algorithm sect. 3.2 returns false only if the set $W$ is empty on line 8. In this case, $(s,\delta,~W)$ is a TATR-witness state, and hence there exists a TATR-witness state in working $\cup$ anti. By the first invariant, ${\cal~A}$ cannot refine ${\cal~L}$ in trace semantics. Algorithm sect. 3.2 returns true only when working is empty, which implies that Dist(anti)$>$Dist(working) is not true. By the second invariant, there is no reachable TATR-witness state and ${\cal~A}$ refines ${\cal~L}$ in trace semantics.

Theorem 4. ${\rm~tmtraces}({\cal~P})~\subseteq~{\rm~tmtraces}({\cal~Q})$ iff there is no reachable state $(s_p,~\emptyset,~\delta)$ in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$ where $\delta$ is not false.

proof (if) For a timed trace ${\rm~tt}~=~\langle(d_1,~e_1),~(d_2,~e_2),~\ldots,~(d_n,~e_n)~\rangle$, let $|{\rm~tt}|=n$ be the length of ${\rm~tt}$. If ${\rm~tmtraces}({\cal~P})~\subsetneq~{\rm~tmtraces}({\cal~Q})$, there is a timed trace ${\rm~tt}_{\cal~P}$ in ${\rm~tmtraces}({\cal~P})$ and a timed trace ${\rm~tt}_{\cal~Q}$ in ${\rm~tmtraces}({\cal~Q})$, such that ${\rm~tt}_{\cal~Q}$ is a maximal prefix of ${\rm~tt}_{\cal~P}$ satisfying (1) $|{\rm~tt}_{\cal~Q}|~=~|{\rm~tt}_{\cal~P}|-1$; (2) ${\rm~tt}_{\cal~P}$ is not in ${\rm~tmtraces}({\cal~Q})$. Let ${\rm~tt}_{\cal~P}~=~\langle(d_1,~e_1),~(d_2,~e_2),~\ldots,~(d_{n-1},~e_{n-1}),\linebreak~(d_n,~e_n)~\rangle$, and ${\rm~tt}_{\cal~Q}~=~\langle(d_1,~e_1),~(d_2,~e_2),~\ldots,~(d_{n-1},~e_{n-1})~\rangle$. Let $((s_p,~v_p),~X)$ be the state in ${\cal~P}~\otimes~{\cal~Q}$ with which a concrete run of ${\cal~P}~\otimes~{\cal~Q}$ exhibiting ${\rm~tt}_{\cal~Q}$ ends. Notice that $X$ must not be empty. Next, $(s_p,~v_p)$ can perform a timed event $(d_n,~e_n)$, but no $x$ in $X$ can perform the same timed event. Because zone abstraction preserves reachability, the concrete run is abstracted by an abstract run in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$, and there exists an abstract state $(s_p,~X',~\delta)$ in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$ such that $(s_p,~X',~v)$ is a concrete configuration of $(s_p,~X',~\delta)$ and it is the same as $((s_p,~v_p),~X)$. With $(s_p,~X',~v)$, since $(d_n,~e_n)$ can be performed by $\cal~P$, $v~+~d_n$ satisfies the guard $g$ of a transition labeled with $e_n$ from $s_p$. Since $\cal~Q$ cannot perform $(d,~e_n)$, $v~+~d_n$ must satisfy negCons. Therefore $\delta~\wedge~g~\wedge$ negCons cannot be false, and hence there is a successor $(s_p',~X'',~\delta')$ such that $\delta'$ is not false. Because negCons is the conjunction of negations of all $e_n$-transitions from any state in $X'$, $X''$ is $\emptyset$. Thus, $(s_p',~\emptyset,~\delta')$ where $\delta'$ is not false is reachable. As a result, if there is no reachable state $(s_p,~\emptyset,~\delta)$ in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$ where $\delta$ is not false, ${\rm~tmtraces}({\cal~P})~\subseteq~{\rm~tmtraces}({\cal~Q})$ holds.

(only-if) It is proved straightforwardly. If ${\rm~tmtraces}({\cal~P})~\subseteq~{\rm~tmtraces}({\cal~Q})$, then any timed trace performed by ${\cal~P}$ can also be performed by ${\cal~Q}$. Thus $(s_p,~\emptyset,~\delta)$ is not reachable.

Lemma 3. Let $(s_p,~X_q,~\delta)$ and $(s_p,~X_q',~\delta')$ be two abstract configurations in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$. If $(s_p,~X_q',~\delta')~\preccurlyeq~(s_p,~X_q,~\delta)$, then a TTR-witness state is reachable from $(s_p,~X_q',~\delta')$ implies a TTR-witness state is reachable from $(s_p,~X_q,~\delta)$.

proof By induction. (1) First, the base case is that if $(s_p,~X_q',~\delta')$ is a TTR-witness state (that is, $X_q'~=~\emptyset$), because $(s_p,~X_q',~\delta')~\preccurlyeq~(s_p,~X_q,~\delta)$ (and $X_q~\subseteq_m~X_q'$), $X_q~=~\emptyset$ and $(s_p,~X_q,~\delta)$ is also a TTR-witness state. (2) For the induction step, we show that if $(s,~X_0,~\delta_0)~\preccurlyeq~(s,~X_1,~\delta_1)$, then for all $e$, such that $((s,~X_0,~\delta_0),~e,~(s',~X_0',~\delta_0'))$ is a transition in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$, there exists $(s',~X_1',~\delta_1')$ such that $((s,~X_1,~\delta_1),~e,~(s',~X_1',~\delta_1'))$ is a transition in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$ and $(s',~X_0',~\delta_0')~\preccurlyeq~(s',~X_1',~\delta_1')$. For simplicity of the proof, a state $(s,~C_{q\oplus})$ in $X_q$ is written as $(s,~A)$.

Let $(s,~X_0,~v_0)~\in~(s,~X_0,~\delta_0)$ be a concrete configuration. Since $(s,~X_0,~\delta_0)~\preccurlyeq~(s,~X_1,~\delta_1)$ by definition, there is a concrete configuration $(s,~X_1,~v_1)~\in~(s,~X_1,~\delta_1)$ such that $v_0[{\rm~maps}(m)]~=~m(v_1)$ for some $m$. Let $((s,~v_0[C_p]),~(d,e),~(s',~v_0'))$ be a concrete transition in $\cal~P$. For each state $(s_1,~A_1)$ in $X_1$ such that $(((s_1,A_1),~v_1[A_1]),~(d,~e),~((s_1',~A_1'),~v_1'))$ is a concrete transition of ${\cal~Q}$, there is a corresponding state $(s_0',~A_0')~\in~X_0$ such that $(((s_0,A_0),~v_0[A_0]),~(d,~e),~((s_0',~A_0'),~v_0'))$ is a transition of ${\cal~Q}$ where $s_0~=~s_1$, $s_0'~=~s_1'$, and $v_0'$ and $v_1'$ ($A_0'$ and $A_1'$, respectively) are equivalent up to clock renaming. Since $(s,~X_0,~v_0)$ is arbitrary, $X_1'~\subseteq_m~X_0'$ holds for some mapping $m$. Since $\delta_0~\subseteq_m~\delta_1$ for some $m$, $\delta_0'~\subseteq_m~\delta_1'$ holds for some $m$ and thus $\delta_1'$ is not empty if $\delta_0'$ is not. Therefore, we conclude that if $((s,~X_0,~\delta_0),~e,~(s',~X_0',~\delta_0'))$ is a transition in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$, then $((s_1,~X_1,~\delta_1),~e,~(s_1',~X_1',~\delta_1'))$ is a transition in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$ and $(s_0',~X_0',~\delta_0')~\preccurlyeq~(s_1',~X_1',~\delta_1')$. Thus, the induction step holds.

When exploring ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$, $(s_p,~X_q',~\delta')$ is found and there exists a configuration $(s_p,~X_q,~\delta)$ (which has been visited before) satisfying $(s_p,~X_q',~\delta')~\preccurlyeq~(s_p,~X_q,~\delta)$, then we don not need to search from $(s_p,~X_q',~\delta')$. The above induction will end until $(s_p,~X_q',~\delta')$ and $(s_p,~X_q,~\delta)$ have been reached. As a summary, the lemma holds.

Theorem 5. Algorithm sect. 3.3.3 returns true iff ${\rm~tmtraces}({\cal~P})~\subseteq~{\rm~tmtraces}({\cal~Q})$.

proof Let ${\rm~ps}$ be an abstract configuration in ${\cal~Z}({\cal~P}~\otimes~{\cal~Q})$. We prove the correctness of the algorithm using the following invariants which are quite similar to Theorem 2.

If there exists a TTR-witness state ${\rm~ps}$ in working $\cup$ anti, then ${\rm~ps}$ is reachable from a state in ${\rm~Init}$.

If there is a reachable TTR-witness state, then Dist(anti) $>$ Dist(working).

Lemma 4. Given an MDP ${\cal~M}$, an LTS ${\cal~L}$. Let ${\cal~D}~=~{\cal~M}~\times~{\rm~det}({\cal~L})$, and the set $G_t$ containing all the PR-witness states of ${\cal~D}$. For any product states $(s_1,~N_1)$ and $(s_2,~N_2)$ of ${\cal~D}$ s.t. $(s_2,~N_2)~\preceq~(s_1,~N_1)$, ${\rm~Pr}_{\rm~max}({\cal~D},~(s_1,~N_1),~G_t)~\geq~{\rm~Pr}_{\rm~max}({\cal~D},~(s_2,~N_2),~G_t)$ and ${\rm~Pr}_{\rm~min}({\cal~D},~(s_1,~N_1),~G_t)~\geq~{\rm~Pr}_{\rm~min}({\cal~D},~(s_2,~N_2),~G_t)$.

proof By induction. (1) First, the base case is that $(s_2,N_2)$ is in $G_t$. Since for any $n_1~\in~N_1$, there is $n_2~\in~N_2$ where $n_1~\prec~n_2$, then $(s_1,N_1)$ should be in $G_t$. So the lemma holds since the maximal/minimal reachability probability of a state in $G_t$ is always 1.

(2) For the induction step, suppose that $(s_1',~N_1')$ and $(s_2',~N_2')$ can satisfy the lemma above, i.e., for any $(s_1',~N_1')$ such that $(s_2',~N_2')~\preceq~(s_1',~N_1')$, the lemma holds. Given a state $(s_2,~N_2)$ and any state $(s_1,~N_1)$ such that $(s_2,~N_2)~\preceq~(s_1,~N_1)$, if there is a distribution $\mu_2$ from $(s_2,~N_2)$, there must exist a distribution $\mu_1$ from $(s_1,~N_1)$ by Definition sect. 4.1 such that: for any $\mu_2((s_2',~N_2'))>0$, there exists $(s_1',N_1')$ such that $\mu_2((s_2',~N_2'))~=~\mu_1((s_1',~N_1'))$, and $(s_2',~N_2')~\preceq~(s_1',~N_1')$. By induction hypothesis, we have ${\rm~Pr}_{\rm~max}({\cal~D},~(s_1',~N_1'),~G_t)~\geq~{\rm~Pr}_{\rm~max}({\cal~D},~(s_2',~N_2'),~G_t)$ and ${\rm~Pr}_{\rm~min}({\cal~D},~(s_1',~N_1'),~G_t)~\geq~{\rm~Pr}_{\rm~min}({\cal~D},~(s_2',~N_2'),~G_t)$. Thus ${\rm~Pr}_{\rm~max}({\cal~D},~(s_1,~N_1),~G_t)~\geq~{\rm~Pr}_{\rm~max}({\cal~D},~(s_2,~N_2),~G_t)$ and ${\rm~Pr}_{\rm~min}({\cal~D},\allowbreak~(s_1,~N_1),~G_t)~\geq~{\rm~Pr}_{\rm~min}({\cal~D},~\allowbreak(s_2,~N_2),~G_t)$ hold. Therefore the lemma holds.

When exploring ${\cal~D}$, $(s_2,~N_2)$ is found and there exists a configuration $(s_1,~N_1)$ (which has been visited before) satisfying $(s_2,~N_2)~\preceq~(s_1,~N_1)$, then $(s_2,~N_2)$ is added into $(s_1,~N_1).ac$. The above induction will end until $(s_1,~N_1)$ and $(s_2,~N_2)$ have been reached. As a summary, the lemma holds.


References

[1] Roscoe A W. Model-Checking CSP. Upper Saddle River: Prentice-Hall, 1994. Google Scholar

[2] Baier C, Katoen J P. Principles of Model Checking. Cambridge: The MIT Press, 2008. Google Scholar

[3] Li W, Li N. A formal semantics for program debugging. Sci China Inf Sci, 2012, 55: 133-148 CrossRef Google Scholar

[4] Li H, Luo J, Li W. A formal semantics for debugging synchronous message passing-based concurrent programs. Sci China Inf Sci, 2014, 57: 128101. Google Scholar

[5] Che X P, Maag S. Testing protocols in internet of things by a formal passive technique. Sci China Inf Sci, 2014, 57: 032101. Google Scholar

[6] Hoare C A R. Communicating sequential processes. In: The Origin of Concurrent Programming. Berlin: Springer, 1985. 413--443. Google Scholar

[7] Roscoe A W. On the expressive power of CSP refinement. Form Asp Comp, 2005, 17: 93-112 CrossRef Google Scholar

[8] Sun J, Song S, Liu Y. Model checking hierarchical probabilistic systems. In: Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM), Shanghai, 2010. 388--403. Google Scholar

[9] Abdulla P A, Ouaknine J, Quaas K, et al. Zone-based universality analysis for single-clock timed automata. In: Proceedings of International Conference on Fundamentals of Software Engineering (FSE), Luxembourg, 2007. 98--112. Google Scholar

[10] Baier C, Bertrand N, Bouyer P, et al. When are timed automata determinizable? In: Proceedings of International Colloquium on Automata, Languages, and Programming (ICALP), Rhodes, 2009. 43--54. Google Scholar

[11] Ouaknine J, Worrell J. On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS), Turku, 2004. 54--63. Google Scholar

[12] Wulf M D, Doyen L, Henzinger T A, et al. Antichains: a new algorithm for checking universality of finite automata. In: Proceedings of the 18th International Conference on Computer Aided Verification (CAV), Seattle, 2006. 17--30. Google Scholar

[13] Bengtsson J, Yi W. Timed automata: semantics, algorithms and tools. In: Lectures on Concurrency and Petri Nets. Berlin: Springer, 2004. 87--124. Google Scholar

[14] Wang T, Sun J, Liu Y, et al. Are timed automata bad for a specification language? Language inclusion checking for timed automata. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, 2014. 310--325. Google Scholar

[15] Liu Y, Sun J, Dong J S. Developing model checkers using PAT. In: Proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Singapore, 2010. 371--377. Google Scholar

[16] Abdulla P A, Chen Y F, Holk L, et al. When simulation meets antichains. In: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Paphos, 2010. 158--174. Google Scholar

[17] Henzinger T A, Nicollin X, Sifakis J. Symbolic Model Checking for Real-Time Systems. Inf Computation, 1994, 111: 193-244 CrossRef Google Scholar

[18] Bouyer P. Forward Analysis of Updatable Timed Automata. Formal Methods Syst Des, 2004, 24: 281-320 CrossRef Google Scholar

[19] Rokicki T G. Representing and modeling digital circuits. Dissertation for Ph.D. Degree. San Francisco: Stanford University, 1993. Google Scholar

[20] Tripakis S. Checking timed buchi automata emptiness on simulation graphs. ACM Trans Comput Logic, 2009, 10: 1--19. Google Scholar

[21] Behrmann G, Bouyer P, Larsen K G, et al. Lower and upper bounds in zonebased abstractions of timed automata. Int J Softw Tools Technol Trans, 2004, 8: 204--215. Google Scholar

[22] Puterman M L. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Hoboken: John Wiley and Sons, 1994. Google Scholar

[23] Vereijken J J. Fischer's Protocol in Timed Process Algebra. Technical Report. 1994. Google Scholar

[24] Lynch N, Shavit N. Timing-based mutual exclusion. In: Proceedings of Real-Time Systems Symposium (RTSS), Phoenix, 1992. 2--11. Google Scholar

[25] Behrmann G, David R, Larsen K G. A tutorial on uppaal. In: Formal Methods for the Design of Real-Time Systems. Berlin: Springer, 2004. 200--236. Google Scholar

[26] Daws C, Tripakis S. Model checking of real-time reachability properties using abstractions. In: Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lisbon, 1998. 313--329. Google Scholar

[27] Duflot M, Fribourg L, Herault T. Probabilistic Model Checking of the CSMA/CD Protocol Using PRISM and APMC. Electron Notes Theor Comput Sci, 2005, 128: 195-214 CrossRef Google Scholar

[28] Gruhn V, Laue R. Patterns for timed property specifications. Electron Notes Theor Comput Sci, 2006, 153: 117--133. Google Scholar

[29] Treiber R K. Systems Programming: Coping with Parallelism. Technical Report, IBM Almaden Research Center. 1986. Google Scholar

[30] Attiya H, Welch J. Distributed Computing: Fundamentals, Simulations, and Advanced Topics. 2nd ed. Oxford: The Oxford University Press, 2004. Google Scholar

[31] Doyen L, Raskin J F. Antichains for the automata-based approach to model checking. Logical Meth Comput Sci, 2009, 5: 1--20. Google Scholar

[32] Wulf M D, Doyen L, Maquet N, et al. Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, 2008. 63--77. Google Scholar

[33] Bouajjani A, Habermehl P, Holk L, et al. Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Proceedings of the 13th International Conference on Implementation and Application of Automata (CIAA), San Francisco, 2008. 57--67. Google Scholar

[34] Filiot E, Jin N, Raskin J F. An antichain algorithm for LTL realizability. In: Proceedings of the 21st International Conference on Computer Aided Verification (CAV), Grenoble, 2009. 263--277. Google Scholar

[35] Alur R, Dill D L. A theory of timed automata. Theor Comput Sci, 1994, 126: 183-235 CrossRef Google Scholar

[36] Suman P V, Pandya P K, Krishna S N, et al. Timed automata with integer resets: language inclusion and expressiveness. In: Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Saint-Malo, 2008. 78--92. Google Scholar

[37] Alur R, Fix L, Henzinger T A. Event-clock automata: a determinizable class of timed automata. Theor Comput Sci, 1999, 211: 253-273 CrossRef Google Scholar

[38] Larsen K G, Pettersson P, Yi W. Uppaal in a nutshell. STTT, 1997, 1: 134-152 CrossRef Google Scholar

[39] Yovine S. KRONOS: a verification tool for real-time systems. STTT, 1997, 1: 123-133 CrossRef Google Scholar

  • Figure 1

    Synchronous product of a TA and an LTS.

  • Figure 2

    Synchronous product of two timed automata.

  • Figure 3

    Synchronous product of an MDP and an LTS.

  • Table 1   Tests on refinement checking of TA and LTS
    System Time Visited states
    Without AC (s) AC (s) Ratio Without AC AC Ratio
    FIS$\times$6(2) 12.2 8.9 1.37 260.7 K 172.7 K 1.51
    FIS$\times$6(6) 22.9 6.3 3.63 497.0 K 100.2 K 4.96
    FIS$\times$8(1) 4.2 4.9 0.86 88.4 K 88.4 K 1.00
    RW$\times$6(3) 1.53 0.68 2.25 68.7 K 23.0 K 2.99
    RW$\times$8(3) 124.1 42.3 2.93 4.3 M 1.1 M 3.91
    LYN$\times$7(2) 4.5 3.5 1.29 165.0 K 130.0 K 1.27
    LYN$\times$8(2) 26.0 19.3 1.35 659.1 K 519.0 K 1.27
    CSMA$\times$7(1) 15.6 16.9 0.92 146.2 K 146.2 K 1.00
  •   

    Algorithm 1 Anti-chain based trace refinement checking for timed automata

    algsetupindent=2em

    Let ${\rm~working}~:=~{\rm~Init}$;

    Let ${\rm~anti}~:=~\emptyset~$;

    while ${\rm~working}~\neq~\emptyset$ do

    remove ${\rm~ps}~:=~(s,~\delta,~W)$ from working;

    remove all ${\rm~ps}'~\in~{\rm~anti}$ s.t. ${\rm~ps}'~\lesssim~{\rm~ps}$;

    add ps into anti;

    if $W~=~\emptyset$ then

    return false;

    end if

    for all $(s',~\delta',~W')~\in~{\rm~post}({\rm~ps},~{\rm~ZG}_{\rm~AL})$

    ${\rm~ps}''~:=~{\rm~LU}((s',~\delta',~W'))$;

    if $\nexists$ ${\rm~ps}'~\in~{\rm~anti}$ s.t. ${\rm~ps}''~\lesssim~{\rm~ps}'$ then

    add ${\rm~ps}''$ into working;

    end if

    end for

    end while

    return true;

  • Table 2   Tests on refinement checking between TA
    System Time Visited states
    Without AC (s) AC (s) Ratio Without AC AC Ratio
    FIS$\times$6(1) 1.4 0.7 2.00 7.1 K 4.4 K 1.61
    FIS$\times$7(1) 8.9 4.6 1.93 31.3 K 20.0 K 1.57
    FIS$\times$8(1) 57.9 29.7 1.95 138.7 K 91.6 K 1.51
    RW$\times$6(6) 8.9 7.0 1.27 27.9 K 23.3 K 1.20
    RW$\times$7(1) 18.5 12.9 1.43 126.9 K 99.5 K 1.28
    LYN$\times$5(2) 48.8 2.3 21.2 63.6 K 8.1 K 7.85
    LYN$\times$6(1) 69.5 4.0 17.4 120.9 K 16.8 K 7.20
    FDDI$\times$7(7) 36.1 8.0 4.51 8.1 K 1.2 K 6.75
    CSMA$\times$5(1) 3.4 0.2 17.0 2.5 K 0.9 K 2.78
  •   

    Algorithm 2 Anti-chain based timed trace refinement checking between timed automata

    algsetupindent=2em

    Let working $:=~{\rm~Init}$;

    Let anti $:=~\emptyset~$;

    while working $\neq~\emptyset$ do

    remove ${\rm~ps}~:=~(s_p,~X_q,~\delta)$ from working;

    remove all ${\rm~ps}'~\in$ anti s.t. ${\rm~ps}'~\preccurlyeq$ ps;

    add ${\rm~ps}$ into anti;

    if $X_q~=~\emptyset$ then

    return false;

    end if

    for all $(s_p',~X_q',~\delta')~\in~{\rm~post}({\rm~ps},~{\cal~Z}({\cal~P}~\otimes~{\cal~Q}))$

    if $\nexists$ ${\rm~ps}'~\in$ anti s.t. $(s_p',~X_q',~\delta')~\preccurlyeq~{\rm~ps}'$ then

    add $(s_p',~X_q',~\delta')$ into working;

    end if

    end for

    end while

    return true;

  • Table 3   Tests on refinement checking of MDP and LTS
    System States Time States during iterations
    Without AC (s) AC (s) Ratio Without AC AC Ratio
    CSI(3) 46 K 2.7 2.2 1.23 4.2 M 3.0 M 1.40
    CSI(4) 87 K 16.0 12.0 1.33 18.6 M 11.7 M 1.59
    CSI(5) 117 K 123.9 80.8 1.53 130.7 M 76.3 M 1.71
    CSI(6) 231 K 271.2 182.6 1.49 272.1 M 160.7 M 1.69
    CSI(7) 343 K 511.1 340.3 1.50 515.2 M 298.8 M 1.72
    MRS(3) 8 K 2.5 2.8 0.89 4.9 M 4.8 M 1.02
    MRS(4) 59 K 47.1 49.3 0.96 43.4 M 43.3 M 1.00

Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1