Publication Details

Towards Smaller Invariants for Proving Coverability

HOLÍK, L.; HOLÍKOVÁ, L. Towards Smaller Invariants for Proving Coverability. In Computer Aided Systems Theory - EUROCAST 2017. Berlin Heidelberg: Springer Verlag, 2018. p. 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
ISBN
978-3-319-74727-9
Publisher
Springer Verlag
Place
Berlin Heidelberg
DOI
UT WoS
000531202800013
EID Scopus
BibTeX
@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/"
}
Back to top