Přístupnostní navigace
E-application
Search Search Close
Publication detail
ROGALEWICZ, A. VOJNAR, T. IOSIF, R.
Original Title
Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems
Type
conference paper
Language
English
Original 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
Authors
ROGALEWICZ, A.; VOJNAR, T.; IOSIF, R.
Released
9. 4. 2016
Publisher
Springer Verlag
Location
Heidelberg
ISBN
978-3-662-49673-2
Book
Tools and Algorithms for the Construction and Analysis of Systems
Edition
Lecture Notes in Computer Science
Pages from
71
Pages to
89
Pages count
19
URL
http://link.springer.com/chapter/10.1007/978-3-662-49674-9_5
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" }