Document Open Access Logo

Reachability in Parameterized Systems: All Flavors of Threshold Automata

Authors Jure Kukovec, Igor Konnov , Josef Widder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.19.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Author Details

Jure Kukovec
  • TU Wien, Favoritenstraße 9 - 11, 1040 Vienna, Austria
Igor Konnov
  • University of Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
Josef Widder
  • TU Wien, Favoritenstraße 9 - 11, 1040 Vienna, Austria

Funding

Supported by the Austrian Science Fund (FWF) via the National Research Network RiSE (S11403, S11405), project PRAVDA (P27722), and Doctoral College LogiCS (W1255-N23); and by the Vienna Science and Technology Fund (WWTF) via project APALACHE (ICT15-103).

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.CONCUR.2018.19

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
  • Theory of computation → Logic and verification
  • Software and its engineering → Software fault tolerance
Keywords
  • threshold & counter automata
  • parameterized verification
  • reachability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík. Parameterized verification through view abstraction. STTT, 18(5):495-516, 2016. Google Scholar
  2. Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, and Florian Zuleger. Parameterized model checking of synchronous distributed algorithms by abstraction. In VMCAI, volume 10747 of LNCS, pages 1-24, 2018. Google Scholar
  3. Ziv Bar-Joseph and Michael Ben-Or. A tight lower bound for randomized synchronous consensus. In Proceedings of the seventeenth annual ACM symposium on Principles of distributed computing, pages 193-199. ACM, 1998. Google Scholar
  4. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Laure Petrucci. Fast: acceleration from theory to practice. STTT, 10(5):401-424, 2008. Google Scholar
  5. Martin Biely, Bernadette Charron-Bost, Antoine Gaillard, Martin Hutle, André Schiper, and Josef Widder. Tolerating corrupted communication. In PODC, pages 244-253, 2007. Google Scholar
  6. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In TACAS, volume 1579 of LNCS, pages 193-207, 1999. Google Scholar
  7. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. Google Scholar
  8. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. On reducing linearizability to state reachability. In ICALP, pages 95-107, 2015. Google Scholar
  9. Bernadette Charron-Bost and André Schiper. The heard-of model: computing in distributed systems with benign faults. Distributed Computing, 22(1):49-71, 2009. Google Scholar
  10. Hubert Comon and Yan Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In CAV, pages 268-279. Springer, 1998. Google Scholar
  11. Giorgio Delzanno. A unified view of parameterized verification of abstract models of broadcast communication. STTT, 18(5):475-493, 2016. Google Scholar
  12. Cezara Drăgoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. A logic-based framework for verifying consensus algorithms. In VMCAI, volume 8318 of LNCS, pages 161-181, 2014. Google Scholar
  13. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems. Formal Methods in System Design, 50(2-3):140-167, 2017. Google Scholar
  14. Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. J. ACM, 35(2):288-323, 1988. Google Scholar
  15. E.A. Emerson and K.S. Namjoshi. Reasoning about rings. In POPL, pages 85-94, 1995. Google Scholar
  16. Javier Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundam. Inform., 31(1):13-25, 1997. Google Scholar
  17. Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proving liveness of parameterized programs. In LICS, pages 185-196, 2016. Google Scholar
  18. Laurent Fribourg and Hans Olsén. A decompositional approach for computing least fixed-points of datalog programs with z-counters. Constraints, 2(3/4):305-335, 1997. Google Scholar
  19. Zeinab Ganjei, Ahmed Rezine, Petru Eles, and Zebo Peng. Counting dynamically synchronizing processes. STTT, 18(5):517-534, 2016. Google Scholar
  20. Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116-133, 1978. Google Scholar
  21. Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder. Para²: Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods in System Design, 2017. Google Scholar
  22. Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In POPL, pages 719-734, 2017. Google Scholar
  23. Igor Konnov, Helmut Veith, and Josef Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. In CONCUR, volume 8704, pages 125-140. Elsevier, 2014. Google Scholar
  24. Igor Konnov, Helmut Veith, and Josef Widder. SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms. In CAV (Part I), volume 9206 of LNCS, pages 85-102, 2015. Google Scholar
  25. Igor Konnov, Helmut Veith, and Josef Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation, 252:95-109, 2017. Google Scholar
  26. Igor Konnov, Josef Widder, Francesco Spegni, and Luca Spalazzi. Accuracy of message counting abstraction in fault-tolerant distributed algorithms. In VMCAI, pages 347-366, 2017. Google Scholar
  27. Jure Kukovec. Generalizing threshold automata for reachability in parameterized systems. Master’s thesis, University of Ljubljana, 2016. URL: URL: http://forsyte.at/wp-content/uploads/Kukovec-27142109-2016.pdf.
  28. Leslie Lamport. The part-time parliament. ACM Trans. Comput. Syst., 16(2):133-169, 1998. Google Scholar
  29. Marijana Lazić, Igor Konnov, Josef Widder, and Roderick Bloem. Synthesis of distributed algorithms with parameterized threshold guards. In OPODIS, volume 95 of LIPIcs, pages 32:1-32:20, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.OPODIS.2017.32.
  30. Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere! In ATVA, volume 5, pages 489-503. Springer, 2005. Google Scholar
  31. Ognjen Maric, Christoph Sprenger, and David A. Basin. Cutoff bounds for consensus algorithms. In CAV, Part II, pages 217-237, 2017. Google Scholar
  32. Marvin L Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. Google Scholar
  33. Iulian Moraru, David G. Andersen, and Michael Kaminsky. There is more consensus in egalitarian parliaments. In SOSP, pages 358-372, 2013. Google Scholar
  34. Brian M. Oki and Barbara Liskov. Viewstamped replication: A general primary copy. In PODC, pages 8-17, 1988. Google Scholar
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 About DROPS Imprint Privacy Contact