Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 3/2020

08-07-2020

Abstraction refinement and antichains for trace inclusion of infinite state systems

Authors: Lukáš Holík, Radu Iosif, Adam Rogalewicz, Tomáš Vojnar

Published in: Formal Methods in System Design | Issue 3/2020

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.
next article Multi-scale verification of distributed synchronisation

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
1
Generic register automata were called data automata in our preliminary work [24]. We have decided to change the name in order to avoid confusion with some other formalisms.
 
2
Note that the presented trace inclusion method can be used with any data domain supported by the underlying SMT solver including integers or reals.
 
4
Note that there is not a fixed set of predefined predicates. New predicates are discovered during refinement phase.
 
5
This option covers the case of data values allowed by the network \({\langle A_1,A_2 \rangle }\) that are not covered by a data constraint of any B-transition.
 
6
Our reduction to the emptiness of product automata is at least exponential.
 
7
For (in)finite words, the class of LTL-definable languages coincides with the star-free languages, which are a strict subclass of (\(\omega \)-)regular languages.
 
8
Called data automata in [24].
 
9
Note that the empty disjunction is equivalent to \(\bot \). Hence \(\theta ({\mathbf {x}},{\mathbf {x}}')\) satisfiable implies that for all \(p' \in P'\) there exists \(p \in P\) and a rule \(p \xrightarrow {{\scriptscriptstyle \sigma ,\psi }}{} p' \in \Delta \).
 
10
For timed automata, this is the case since the only shared variable is the time, and the observer may have local clocks.
 
11
The formal definition of antichain trees will be given as Definition 1 later in this section.
 
12
Note that the above choice of the product state in the form \(s=({\mathbf {q}},P,\Phi )\) is not straightforward and resulted from several previous unsuccessful attempts. For example, if one chooses to associate separate formulae for the valuations of the variables with \({\mathbf {q}}\) and each of the states in P, which seems to be a quite natural choice, the construction becomes unsound. Intuitively, when a successor state of such a product state is computed, the disjunction of the formulae joint with the successors of P may entail the formula joint with the successor of \({\mathbf {q}}\). However, that does not mean that all pairs of source/target valuations possible in \({\mathcal {A}}^e\) are possible in \({\overline{B}}\) too. More details are provided in “Appendix 1”.
 
13
A fact is a formula in \(\text{ Form }({\mathcal {D}})\).
 
14
If \(\theta ({\mathbf {x}}'_{{\mathcal {A}}}, {\mathbf {x}}_{{\mathcal {A}}})\) is unsatisfiable, then s does not contain a valuation of the variables that would allow one to do a step following the rule \(({\mathbf {q}},P) \xrightarrow {{\scriptscriptstyle \sigma ,\theta }}{} ({\mathbf {r}},S)\).
 
15
Taking a bigger K leads to a more precise \( Sim _{ij}\), but, on the other hand, it can significantly increase the computation time.
 
16
Many realistic systems comply with this restriction, take, for instance, shared-memory multithreading in Java.
 
18
The size of a formula is measured in the number of nodes of its MathSAT graph-based representation.
 
19
A simulation R is trivial iff \(\forall x,y\in Q: x\ne y \rightarrow (x,\bot ,y)\in R\).
 
Literature
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
2.
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 (2015) Horn clause solvers for program verification. Springer, Cham, pp 24–51MATH
6.
Bojańczyk M, David C, Muscholl A, Schwentick T, Segoufin L (2011) Two-variable logic on data words. ACM Trans Comput Logic 12(4):27:1–27:26MathSciNetCrossRef
7.
Bonchi F, Pous D (2013) Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of POPL’13. ACM
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
9.
Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT solver. In: Proceedings of TACAS, LNCS, vol 7795
10.
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
12.
Craig W (1957) Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3):269–285MathSciNetCrossRef
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
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
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
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
21.
Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Proceedings of POPL’02. ACM
22.
Henzinger TA, Jhala R, Majumdar R, Sutre G (2003) Software verification with blast. In: Proceedings of 10th SPIN workshop, LNCS, vol 2648
23.
Henzinger TA, Nicollin X, Sifakis J, Yovine S (1992) Symbolic model checking for real-time systems. Inf Comput 111:394–406MathSciNetMATH
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
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
26.
27.
McMillan KL (2006) Lazy abstraction with interpolants. In: Proceedings of CAV’06, LNCS, vol 4144. Springer
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 (1967) Computation: finite and infinite machines. Prentice-Hall, Upper Saddle RiverMATH
31.
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
36.
Zbrzezny A, Polrola A (2007) Sat-based reachability checking for timed automata with discrete data. Fundam Inf 79:1–15MathSciNetMATH
Metadata
Title
Abstraction refinement and antichains for trace inclusion of infinite state systems
Authors
Lukáš Holík
Radu Iosif
Adam Rogalewicz
Tomáš Vojnar
Publication date
08-07-2020
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 3/2020
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-020-00345-1

Premium Partner

    Image Credits