Detail výsledku

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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Rogalewicz Adam, doc. Mgr., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Radu Iosif
Abstrakt

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.

Klíčová slova

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

URL
Rok
2016
Strany
71–89
Sborník
Tools and Algorithms for the Construction and Analysis of Systems
Řada
Lecture Notes in Computer Science
Svazek
9636
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'16 (TACAS'16)
ISBN
978-3-662-49673-2
Vydavatel
Springer Verlag
Místo
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"
}
Projekty
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí, GAČR, Standardní projekty, GA14-11384S, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
Spolehlivost a bezpečnost v IT, VUT, Vnitřní projekty VUT, FIT-S-14-2486, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru