1 Search Results for "Kukovec, Jure"

Document
DOI: 10.4230/LIPIcs.CONCUR.2018.19
Reachability in Parameterized Systems: All Flavors of Threshold Automata

Authors: Jure Kukovec, Igor Konnov, and Josef Widder

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Threshold automata, and the counter systems they define, were introduced as a framework for parameterized model checking of fault-tolerant distributed algorithms. This application domain suggested natural constraints on the automata structure, and a specific form of acceleration, called single-rule acceleration: consecutive occurrences of the same automaton rule are executed as a single transition in the counter system. These accelerated systems have bounded diameter, and can be verified in a complete manner with bounded model checking. We go beyond the original domain, and investigate extensions of threshold automata: non-linear guards, increments and decrements of shared variables, increments of shared variables within loops, etc., and show that the bounded diameter property holds for several extensions. Finally, we put single-rule acceleration in the scope of flat counter automata: although increments in loops may break the bounded diameter property, the corresponding counter automaton is flattable, and reachability can be verified using more permissive forms of acceleration.
Cite as

Jure Kukovec, Igor Konnov, and Josef Widder. Reachability in Parameterized Systems: All Flavors of Threshold Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kukovec_et_al:LIPIcs.CONCUR.2018.19,
  author =	{Kukovec, Jure and Konnov, Igor and Widder, Josef},
  title =	{{Reachability in Parameterized Systems: All Flavors of Threshold Automata}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.19},
  URN =		{urn:nbn:de:0030-drops-95578},
  doi =		{10.4230/LIPIcs.CONCUR.2018.19},
  annote =	{Keywords: threshold \& counter automata, parameterized verification, reachability}
}
  • Refine by Author
  • 1 Konnov, Igor
  • 1 Kukovec, Jure
  • 1 Widder, Josef

  • Refine by Classification
  • 1 Software and its engineering → Software fault tolerance
  • 1 Software and its engineering → Software verification
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 parameterized verification
  • 1 reachability
  • 1 threshold & counter automata

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact