Detail publikačního výsledku

Towards Smaller Invariants for Proving Coverability

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

Originální název

Towards Smaller Invariants for Proving Coverability

Anglický název

Towards Smaller Invariants for Proving Coverability

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

parallel system, verification, petri nets, WSTS, CEGAR

Klíčová slova v angličtině

parallel system, verification, petri nets, WSTS, CEGAR

Autoři

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

Rok RIV

2019

Vydáno

26.01.2018

Nakladatel

Springer Verlag

Místo

Berlin Heidelberg

ISBN

978-3-319-74727-9

Kniha

Computer Aided Systems Theory - EUROCAST 2017

Strany od

109

Strany do

116

Strany počet

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

Dokumenty

eurocast_janku_turonova_holik