Detail publikace

Towards Smaller Invariants for Proving Coverability

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

Originální název

Towards Smaller Invariants for Proving Coverability

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

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.

Klíčová slova

parallel system, verification, petri nets, WSTS, CEGAR

Autoři

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

Vydáno

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