Publication Details

Towards Smaller Invariants for Proving Coverability

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.
Czech title
Směrem k menším invariantům pro dokázání spolehlivosti
Type
conference paper
Language
english
Authors
Holík Lukáš, Mgr., Ph.D. (DITS FIT BUT)
Turoňová Lenka, Ing. (DITS FIT BUT)
Keywords
parallel system, verification, petri nets, WSTS, CEGAR
Abstract
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.
Published
2018
Pages
109-116
Proceedings
Computer Aided Systems Theory - EUROCAST 2017
Conference
Sixteenth International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, ES
ISBN
978-3-319-74727-9
Publisher
Springer Verlag
Place
Berlin Heidelberg, DE
DOI
BibTeX
@INPROCEEDINGS{FITPUB11735,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Lenka Turo\v{n}ov\'{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"
}
Back to top