Result Details

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

ROGALEWICZ, A.; VOJNAR, T.; IOSIF, R. 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. Heidelberg: Springer Verlag, 2016. p. 71-89. ISBN: 978-3-662-49673-2.
Type
conference paper
Language
English
Authors
Rogalewicz Adam, doc. Mgr., Ph.D., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Radu Iosif
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.

Keywords

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

URL
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)
ISBN
978-3-662-49673-2
Publisher
Springer Verlag
Place
Heidelberg
DOI
10.1007/978-3-662-49674-9_5
UT WoS
000406428000005
EID Scopus
2-s2.0-84964010099
BibTeX 
@inproceedings{BUT130928,
  author="Adam {Rogalewicz} and Tomáš {Vojnar} and Iosif {Radu}",
  title="Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2016",
  series="Lecture Notes in Computer Science",
  volume="9636",
  pages="71--89",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-662-49674-9\{_}5",
  isbn="978-3-662-49673-2",
  url="http://link.springer.com/chapter/10.1007/978-3-662-49674-9_5"
}
Projects
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures, GACR, Standardní projekty, GA14-11384S, start: 2014-01-01, end: 2016-12-31, completed
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, start: 2016-01-01, end: 2020-12-31, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, start: 2014-01-01, end: 2016-12-31, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top