Detail publikace

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

HOLÍK Lukáš, IOSIF Radu, ROGALEWICZ Adam a VOJNAR Tomáš. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. Formal Methods in System Design, roč. 55, č. 3, 2020, s. 137-170. ISSN 0925-9856. Dostupné z: https://link.springer.com/article/10.1007/s10703-020-00345-1
Název česky
Zjemňování abstrakce a antiřetězce pro inkluzi běhů nekonečně stavových systémů
Typ
článek v časopise
Jazyk
angličtina
Autoři
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Iosif Radu (VERIMAG)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
URL
Abstrakt

Obecný registrový automat (generic register automaton) 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ředstavujeme semi-algoritmus založený na abstrakci a zjemňování určený k řešení tohoto problému. Dále představujeme rozšíření zmíněného algoritmu pomocí techniky simulací, konkrétně simulačních relací nad datovými slovy. Algoritmus byl implementován v rámci prototypového nástroje  a funkčnost byla ověřena na netriviálních příkladech.

Rok
2020
Strany
137-170
Časopis
Formal Methods in System Design, roč. 55, č. 3, ISSN 0925-9856
Vydavatel
Springer Verlag
DOI
10.1007/s10703-020-00345-1
UT WoS
000546198700001
EID Scopus
2-s2.0-85087658314
BibTeX 
@ARTICLE{FITPUB12316,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Radu Iosif and Adam Rogalewicz and Tom\'{a}\v{s} Vojnar",
   title = "Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems",
   pages = "137--170",
   journal = "Formal Methods in System Design",
   volume = 55,
   number = 3,
   year = 2020,
   ISSN = "0925-9856",
   doi = "10.1007/s10703-020-00345-1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12316"
}
Nahoru