Detail publikace
Towards Smaller Invariants for Proving Coverability
parallel system, verification, petri nets, WSTS, CEGAR
V tomto článku zkoumáme možnost vylepšení stávajících metodověřování paralelních systémů. Zvláště se soustředíme na vlastnost bezpečnosti dobřestrukturovaných přechodových systémů. Naše práce je relevantní především pronedávné metody, které jsou založeny na hledání induktivních invariantů pomocísekvence zjemňování získaných z protipříkladů. Naším cílem je zlepšit celkovouefektivitu tohoto přístupu tím, že se soustředíme na nalezení takovýchzjemnění, které povedou k stručnějším invariantům. Za tímto účelem navrhujemeanalyzovat tzv. minimální protipříklady. Tyto protipříklady jsou dostatečněkrátké, aby umožnily podrobnější analýzu. Experimentovali jsme s jednoduchýmzpřesňovacím algoritmem založeným na analýze minimálních běhů a uspěli jsme vevygenerování výrazně stručnějších invariantů než těch, které jsou generovány vnejmodernějších metodách.
@inproceedings{BUT155053,
author="Lukáš {Holík} and Lenka {Holíková}",
title="Towards Smaller Invariants for Proving Coverability",
booktitle="Computer Aided Systems Theory - EUROCAST 2017",
year="2018",
pages="109--116",
publisher="Springer Verlag",
address="Berlin Heidelberg",
doi="10.1007/978-3-319-74727-9\{_}13",
isbn="978-3-319-74727-9",
url="https://www.fit.vut.cz/research/publication/11735/"
}