Conference paper

HOLÍK Lukáš and TUROŇOVÁ Lenka. Towards Smaller Invariants for Proving Coverability. In: Computer Aided Systems Theory - EUROCAST 2017. Berlin Heidelberg: Springer Verlag, 2018, pp. 109-116. ISBN 978-3-319-74727-9.
Publication language:english
Original title:Towards Smaller Invariants for Proving Coverability
Title (cs):Směrem k menším invariantům pro dokázání spolehlivosti
Proceedings:Computer Aided Systems Theory - EUROCAST 2017
Conference:Sixteenth International Conference on Computer Aided Systems Theory
Place:Berlin Heidelberg, DE
Publisher:Springer Verlag
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.
   author = {Luk{\'{a}}{\v{s}} Hol{\'{i}}k and Lenka
   title = {Towards Smaller Invariants for Proving
   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 = {}

Your IPv4 address:
Switch to https