Článek ve sborníku konference

IOSIF Radu, ROGALEWICZ Adam a 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, s. 71-89. ISBN 978-3-662-49673-2. Dostupné z: http://link.springer.com/chapter/10.1007/978-3-662-49674-9_5
Jazyk publikace:angličtina
Název publikace:Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems
Název (cs):Zjemňování abstrakce a antiřetězce pro inkluzi běhů nekonečně stavových systémů
Strany:71-89
Sborník:Tools and Algorithms for the Construction and Analysis of Systems
Konference:European Joint Conferences on Theory and Practice of Software -- ETAPS'16 (TACAS'16)
Řada knih:LNCS 9636
Místo vydání:Heidelberg, DE
Rok:2016
URL:http://link.springer.com/chapter/10.1007/978-3-662-49674-9_5
ISBN:978-3-662-49673-2
DOI:10.1007/978-3-662-49674-9_5
Vydavatel:Springer Verlag
URL:http://arxiv.org/abs/1410.5056 [PDF]
Klíčová slova
trace inclusion, data word automata, CEGAR, predicate abstraction, interpolation
Anotace
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.
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},
   doi = {10.1007/978-3-662-49674-9_5},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.cs.iso-8859-2?id=11056}
}

Vaše IPv4 adresa: 54.82.93.116
Přepnout na IPv6 spojení

DNSSEC [dnssec]