Abstraction refinement and antichains for trace inclusion of infinite state systems. (English) Zbl 07307310

Summary: A generic register automaton is a finite automaton equipped with variables (which may be viewed as counters or, more generally, registers) ranging over infinite data domains. A trace of a generic register automaton is an alternating sequence of alphabet symbols and values taken by the variables during an execution of the automaton. The problem addressed in this paper is the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable in general, we give a semi-algorithm based on a combination of abstraction refinement and antichains, which is proved to be sound and complete, but whose termination is not guaranteed. Moreover, we further enhance the proposed algorithm by exploiting a concept of data simulations, i.e., simulation relations aware of the data associated with the words. We have implemented our technique in a prototype tool and show promising results on multiple non-trivial examples.


68-XX Computer science
Full Text: DOI arXiv HAL


[1] Abdulla P, Chen YF, Holik L, Mayr R, Vojnar T (2010) When simulation meets antichains. In: Proceedings of TACAS’10, LNCS, vol 6015. Springer, pp 158-174 · Zbl 1284.68337
[2] Alur, R.; Dill, DL, A theory of timed automata, Theor Comput Sci, 126, 2, 183-235 (1994) · Zbl 0803.68071
[3] Bardin S, Finkel A, Leroux J, Petrucci L (2003) Fast: fast acceleration of symbolic transition systems. In: Proceedings of CAV’03, LNCS, vol 2725. Springer
[4] Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified horn clauses. In: Proceedings of CAV’13, LNCS, vol 8044. Springer
[5] Bjørner, N.; Gurfinkel, A.; McMillan, K.; Rybalchenko, A., Horn clause solvers for program verification, 24-51 (2015), Cham: Springer, Cham · Zbl 1465.68044
[6] Bojańczyk, M.; David, C.; Muscholl, A.; Schwentick, T.; Segoufin, L., Two-variable logic on data words, ACM Trans Comput Logic, 12, 4, 27:1-27:26 (2011) · Zbl 1352.03041
[7] Bonchi F, Pous D (2013) Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of POPL’13. ACM · Zbl 1301.68169
[8] Bozga M, Habermehl P, Iosif R, Konecný F, Vojnar T (2009) Automatic verification of integer array programs. In: Proceedings of CAV’09, LNCS, vol 5643, pp 157-172 · Zbl 1242.68063
[9] Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT solver. In: Proceedings of TACAS, LNCS, vol 7795 · Zbl 1381.68153
[10] Comon H, Dauchet M, Gilleron R, Löding C, Jacquemard F, Lugiez D, Tison, S, Tommasi M (2007) Tree automata techniques and applications. http://www.grappa.univ-lille3.fr/tata. Release 12 Oct 2007
[11] Cook B, Khlaaf H, Piterman N (2015) On automation of CTL* verification for infinite-state systems. In: Proceedings of CAV’15, LNCS, vol 9206. Springer · Zbl 1381.68154
[12] Craig, W., Three uses of the herbrand-gentzen theorem in relating model theory and proof theory, J. Symb. Log., 22, 3, 269-285 (1957) · Zbl 0079.24502
[13] D’Antoni L, Alur R (2014) Symbolic visibly pushdown automata. In: Proceedings of CAV’14, LNCS, vol 8559. Springer
[14] Decker N, Habermehl P, Leucker M, Thoma D (2014) Ordered navigation on multi-attributed data words. In: Proceedings of CONCUR’14, LNCS, vol 8704, pp 497-511 · Zbl 1417.68082
[15] Dhar A (2014) Algorithms for model-checking flat counter systems. Ph.D. thesis, Univ. Paris 7
[16] Fribourg L (1998) A closed-form evaluation for extended timed automata. Tech. rep, CNRS et Ecole Normale Supérieure de Cachan
[17] Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: ACM SIGPLAN conference on programming language design and implementation, PLDI ’12, Beijing, China—June 11-16, 2012, pp 405-416
[18] Habermehl P, Iosif R, Vojnar T (2008) A logic of singly indexed arrays. In: Proceedings of LPAR’08, LNCS, vol 5330, pp 558-573 · Zbl 1182.03032
[19] Habermehl P, Iosif R, Vojnar T (2008) What else is decidable about integer arrays? In: Proceedings of FOSSACS’08, LNCS, vol 4962, pp 474-489 · Zbl 1139.03007
[20] Henzinger MR, Henzinger TA, Kopke PW (1995) Computing simulations on finite and infinite graphs. In: Proceedings of the 36th annual symposium on foundations of computer science, FOCS ’95, pp 453 · Zbl 0938.68538
[21] Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Proceedings of POPL’02. ACM · Zbl 1323.68374
[22] Henzinger TA, Jhala R, Majumdar R, Sutre G (2003) Software verification with blast. In: Proceedings of 10th SPIN workshop, LNCS, vol 2648 · Zbl 1023.68532
[23] Henzinger, TA; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Inf Comput, 111, 394-406 (1992) · Zbl 0806.68080
[24] Iosif R, Rogalewicz A, Vojnar T (2016) Abstraction refinement and antichains for trace inclusion of infinite state systems. In: Proceedings of TACAS’16, LNCS, vol 9636. Springer, pp 71-89 · Zbl 1420.68107
[25] Iosif R, Xu X (2018) Abstraction refinement for emptiness checking of alternating data automata. In: Proceedings of TACAS’18, LNCS, vol 10806. Springer, pp 93-111 · Zbl 1423.68255
[26] Kaminski, M.; Francez, N., Finite-memory automata, Theor Comput Sci, 134, 2, 329-363 (1994) · Zbl 0938.68711
[27] McMillan KL (2006) Lazy abstraction with interpolants. In: Proceedings of CAV’06, LNCS, vol 4144. Springer · Zbl 1188.68196
[28] McMillan KL (2011) Interpolants from z3 proofs. In: Proceedings of the international conference on formal methods in computer-aided design, FMCAD ’11, pp 19-27. FMCAD Inc
[29] Milner R (1971) An algebraic definition of simulation between programs. In: Proceedings of of IJCAI’71. Morgan Kaufmann Publishers Inc
[30] Minsky, M., Computation: finite and infinite machines (1967), Upper Saddle River: Prentice-Hall, Upper Saddle River · Zbl 0195.02402
[31] Numerical Transition Systems Repository (2012). http://nts.imag.fr/index.php/Flata
[32] Ouaknine J, Worrell J (2004) On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of LICS’04. IEEE Computer Society
[33] Smrcka A, Vojnar T (2007) Verifying parametrised hardware designs via counter automata. In: HVC’07, pp 51-68
[34] Tripakis S (1998) The analysis of timed systems in practice. Ph.D. thesis, Univ. Joseph Fourier, Grenoble (December)
[35] Wulf MD, Doyen L, Henzinger TA, Raskin J (2006) Antichains: a new algorithm for checking universality of finite automata. In: Proceedings of CAV’06, LNCS, vol 4144. Springer · Zbl 1188.68171
[36] Zbrzezny, A.; Polrola, A., Sat-based reachability checking for timed automata with discrete data, Fundam Inf, 79, 1-15 (2007) · Zbl 1124.68061
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.