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
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Holíková 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
10.1007/978-3-319-74727-9_13
UT WoS
000531202800013
EID Scopus
2-s2.0-85041711934
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