Publication detail

Towards Smaller Invariants for Proving Coverability

HOLÍK, L. HOLÍKOVÁ, L.

Original Title

Towards Smaller Invariants for Proving Coverability

Type

conference paper

Language

English

Original 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.

Keywords

parallel system, verification, petri nets, WSTS, CEGAR

Authors

HOLÍK, L.; HOLÍKOVÁ, L.

Released

26. 1. 2018

Publisher

Springer Verlag

Location

Berlin Heidelberg

ISBN

978-3-319-74727-9

Book

Computer Aided Systems Theory - EUROCAST 2017

Pages from

109

Pages to

116

Pages count

8

URL

https://www.fit.vut.cz/research/publication/11735/

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/"
}