Publication Details

Towards Smaller Invariants for Proving Coverability

HOLÍK Lukáš and HOLÍKOVÁ 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
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
UT WoS
000531202800013
EID Scopus
BibTeX
@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"
}
Back to top