Detail publikace

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

ROGALEWICZ, A. VOJNAR, T. IOSIF, R.

Originální název

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální 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

Autoři

ROGALEWICZ, A.; VOJNAR, T.; IOSIF, R.

Vydáno

9. 4. 2016

Nakladatel

Springer Verlag

Místo

Heidelberg

ISBN

978-3-662-49673-2

Kniha

Tools and Algorithms for the Construction and Analysis of Systems

Edice

Lecture Notes in Computer Science

Strany od

71

Strany do

89

Strany počet

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"
}