Detail publikace
Towards Smaller Invariants for Proving Coverability
V tomto článku zkoumáme možnost vylepšení stávajících metod ověřování paralelních systémů. Zvláště se soustředíme na vlastnost bezpečnosti dobře strukturovaných přechodových systémů. Naše práce je relevantní především pro nedá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 celkovou efektivitu tohoto přístupu tím, že se soustředíme na nalezení takových zjemnění, které povedou k stručnějším invariantům. Za tímto účelem navrhujeme analyzovat tzv. minimální protipříklady. Tyto protipříklady jsou dostatečně krátké, aby umožnily podrobnější analýzu. Experimentovali jsme s jednoduchým zpřesňovacím algoritmem založeným na analýze minimálních běhů a uspěli jsme ve vygenerování výrazně stručnějších invariantů než těch, které jsou generovány v nejmodernějších metodách.
@INPROCEEDINGS{FITPUB11735, author = "Luk\'{a}\v{s} Hol\'{i}k and Lenka Hol\'{i}kov\'{a}", title = "Towards Smaller Invariants for Proving Coverability", pages = "109--116", booktitle = "Computer Aided Systems Theory - EUROCAST 2017", year = 2018, location = "Berlin Heidelberg, DE", publisher = "Springer Verlag", ISBN = "978-3-319-74727-9", doi = "10.1007/978-3-319-74727-9\_13", language = "english", url = "https://www.fit.vut.cz/research/publication/11735" }