Detail publikace

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.
Název česky
Zjemňování abstrakce a antiřetězce pro inkluzi běhů nekonečně stavových systémů
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Radu Iosif
URL
Klíčová slova

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

Abstrakt

Datový automat je varianta konečného automatu vybaveného datovými proměnnými nad nekonečnými doménami (např. celá čísla). Běh takovéhoto automatu je pak alternující sekvence symbolů konečné abecedy a datových hodnot, kterých nabývají proměnné v jednotlivých krocích. Problém adresovaný v tomto článku se ptá, zda datový jazyk (množina možných běhů) jednoho automatu je součástí datového jazyka druhého automatu. Tento problém je obecně nerozhodnutelný. V rámci článku představujemé semi-algoritmus založený na abstrakci a zjemňování určený k řešení tohoto problému.

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), Eindhoven, NL
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"
}
Nahoru