Publication Details

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 9636. Heidelberg: Springer Verlag, 2016, pp. 71-89. ISBN 978-3-662-49673-2. Available from: http://link.springer.com/chapter/10.1007/978-3-662-49674-9_5
Czech title
Zjemňování abstrakce a antiřetězce pro inkluzi běhů nekonečně stavových systémů
Type
conference paper
Language
english
Authors
Iosif Radu (VERIMAG)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

trace inclusion, data word automata, CEGAR, predicate abstraction, interpolation

Abstract

A data automaton is a finite automaton equipped with variables (counters or registers) ranging over infinite data domains. A trace of a data automaton is an alternating sequence of alphabet symbols and values taken by the counters 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, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete, but whose termination is not guaranteed. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples.

Published
2016
Pages
71-89
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science
Volume
9636
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS'16 (TACAS'16), Eindhoven, NL
ISBN
978-3-662-49673-2
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
10.1007/978-3-662-49674-9_5
UT WoS
000406428000005
EID Scopus
2-s2.0-84964010099
BibTeX 
@INPROCEEDINGS{FITPUB11056,
   author = "Radu Iosif and Adam Rogalewicz and Tom\'{a}\v{s} Vojnar",
   title = "Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems",
   pages = "71--89",
   booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
   series = "Lecture Notes in Computer Science",
   volume = 9636,
   year = 2016,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-662-49673-2",
   doi = "10.1007/978-3-662-49674-9\_5",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11056"
}
Back to top