Publication Details
Towards Smaller Invariants for Proving Coverability
parallel system, verification, petri nets, WSTS, CEGAR
In this paper, we explore a possibility of improving existing methods for verification of parallel systems. We particularly concentrate on safety properties of well-structured transition systems. Our work has relevance mainly to recent methods that are based on finding an inductive invariant by a sequence of refinements learned from counterexamples. Our goal is to improve the overall efficiency of this approach by concentrating on choosing refinements that lead to a more succinct invariants. For this, we propose to analyze so called minimal counterexample runs. They are digests of counterexamples concise enough to allow for a more detailed analysis. We experimented with a simple refinement algorithm based on analysing minimal runs and succeeded in generating significantly more succinct invariants than the state-of-the-art methods.
@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/"
}