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
Share
Rating

### 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.

•

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;

•

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;

Citations

• #### 0

Altmetric

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