Publication result detail

Towards Smaller Invariants for Proving Coverability

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

Original Title

Towards Smaller Invariants for Proving Coverability

English Title

Towards Smaller Invariants for Proving Coverability

Type

Paper in proceedings (conference paper)

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.

English 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

Key words in English

parallel system, verification, petri nets, WSTS, CEGAR

Authors

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

RIV year

2019

Released

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

Documents

eurocast_janku_turonova_holik