Detail publikace

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; IOSIF, R. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. FORMAL METHODS IN SYSTEM DESIGN, 2020, vol. 55, no. 3, p. 137-170. ISSN: 0925-9856.
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
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Radu Iosif
URL
Klíčová slova

Generic register automata, Data automata, Trace inclusion, Antichains, Interpolation, CEGAR, Simulation relations

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
DOI
10.1007/s10703-020-00345-1
UT WoS
000546198700001
EID Scopus
2-s2.0-85087658314
BibTeX 
@article{BUT170106,
  author="Lukáš {Holík} and Adam {Rogalewicz} and Tomáš {Vojnar} and Iosif {Radu}",
  title="Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems",
  journal="FORMAL METHODS IN SYSTEM DESIGN",
  year="2020",
  volume="55",
  number="3",
  pages="137--170",
  doi="10.1007/s10703-020-00345-1",
  issn="0925-9856",
  url="https://link.springer.com/article/10.1007/s10703-020-00345-1"
}
Nahoru