Publication 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.
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
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Radu Iosif
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
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"
}
Back to top