Conference paper

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. 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
Publication language:english
Original title:Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems
Title (cs):Zjemňování abstrakce a antiřetězce pro inkluzi běhů nekonečně stavových systémů
Pages:71-89
Proceedings:Tools and Algorithms for the Construction and Analysis of Systems
Conference:European Joint Conferences on Theory and Practice of Software -- ETAPS'16 (TACAS'16)
Series:LNCS 9636
Place:Heidelberg, DE
Year:2016
URL:http://link.springer.com/chapter/10.1007/978-3-662-49674-9_5
ISBN:978-3-662-49673-2
Publisher:Springer Verlag
URL:http://arxiv.org/abs/1410.5056 [PDF]
Keywords
trace inclusion, data word automata, CEGAR, predicate abstraction, interpolation
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   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 = {LNCS 9636},
   year = {2016},
   location = {Heidelberg, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-662-49673-2},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=11056}
}

Your IPv4 address: 54.166.203.76
Switch to IPv6 connection

DNSSEC [dnssec]