Document Open Access Logo

Parameterized Complexity of Safety of Threshold Automata

Author A. R. Balasubramanian

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.37.pdf
  • Filesize: 0.64 MB
  • 15 pages

Document Identifiers

Author Details

A. R. Balasubramanian
  • Technische Universität München, Germany

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).

Acknowledgements

I would like to thank Prof. Javier Esparza for useful discussions regarding the paper and Christoph Welzel and Margarete Richter for their encouragement and support. I would also like to thank the anonymous reviewers whose comments greatly improved the presentation of the paper.

Cite AsGet BibTex

A. R. Balasubramanian. Parameterized Complexity of Safety of Threshold Automata. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 37:1-37:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.37

Abstract

Threshold automata are a formalism for modeling fault-tolerant distributed algorithms. In this paper, we study the parameterized complexity of reachability of threshold automata. As a first result, we show that the problem becomes W[1]-hard even when parameterized by parameters which are quite small in practice. We then consider two restricted cases which arise in practice and provide fixed-parameter tractable algorithms for both these cases. Finally, we report on experimental results conducted on some protocols taken from the literature.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Logic and verification
Keywords
  • Threshold automata
  • distributed algorithms
  • parameterized complexity

Metrics

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

References

  1. Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. Distributed Comput., 18(4):235-253, 2006. URL: https://doi.org/10.1007/s00446-005-0138-3.
  2. A. R. Balasubramanian, Javier Esparza, and Marijana Lazić. Complexity of verification and synthesis of threshold automata. In Accepted at ATVA 2020, 2020. URL: https://arxiv.org/abs/2007.06248.
  3. Nathalie Bertrand, Igor Konnov, Marijana Lazić, and Josef Widder. Verification of randomized consensus algorithms under round-rigid adversaries. In CONCUR, volume 140 of LIPIcs, pages 33:1-33:15, 2019. Google Scholar
  4. 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
  5. Michael Blondin and Christoph Haase. Logics for continuous reachability in petri nets and vector addition systems with states. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005068.
  6. Gabriel Bracha and Sam Toueg. Asynchronous consensus and broadcast protocols. J. ACM, 32(4):824-840, 1985. Google Scholar
  7. Francisco Vilar Brasileiro, Fabíola Greve, Achour Mostéfaoui, and Michel Raynal. Consensus in one communication step. In PaCT, volume 2127 of LNCS, pages 42-50, 2001. Google Scholar
  8. Tushar Deepak Chandra and Sam Toueg. Unreliable failure detectors for reliable distributed systems. J. ACM, 43(2):225-267, 1996. Google Scholar
  9. Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan. On the complexity of bounded context switching. In Kirk Pruhs and Christian Sohler, editors, 25th Annual European Symposium on Algorithms, ESA 2017, September 4-6, 2017, Vienna, Austria, volume 87 of LIPIcs, pages 27:1-27:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ESA.2017.27.
  10. Peter Chini, Roland Meyer, and Prakash Saivasan. Fine-grained complexity of safety verification. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pages 20-37. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_2.
  11. Peter Chini, Roland Meyer, and Prakash Saivasan. Complexity of liveness in parameterized systems. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 37:1-37:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.37.
  12. Peter Chini, Roland Meyer, and Prakash Saivasan. Liveness in broadcast networks. In NETYS 2019, Revised Selected Papers, pages 52-66, 2019. Google Scholar
  13. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21275-3.
  14. Dan Dobre and Neeraj Suri. One-step consensus with zero-degradation. In DSN, pages 137-146, 2006. Google Scholar
  15. Constantin Enea and Azadeh Farzan. On atomicity in presence of non-atomic writes. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 497-514. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_29.
  16. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In LICS, pages 352-359. IEEE Computer Society, 1999. Google Scholar
  17. Azadeh Farzan and P. Madhusudan. The complexity of predicting atomicity violations. In Stefan Kowalewski and Anna Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5505 of Lecture Notes in Computer Science, pages 155-169. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00768-2_14.
  18. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. Google Scholar
  19. Rachid Guerraoui. Non-blocking atomic commit in asynchronous distributed systems with failure detectors. Distributed Computing, 15(1):17-25, 2002. Google Scholar
  20. Klaus Jansen, Stefan Kratsch, Dániel Marx, and Ildikó Schlotter. Bin packing with fixed number of bins revisited. Journal of Computer and System Sciences, 79(1):39-49, 2013. URL: https://doi.org/10.1016/j.jcss.2012.04.004.
  21. Igor Konnov, Helmut Veith, and Josef Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. In CONCUR, volume 8704 of LNCS, pages 125-140, 2014. Google Scholar
  22. Igor Konnov, Helmut Veith, and Josef Widder. SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 85-102. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_6.
  23. 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
  24. Igor Konnov and Josef Widder. Bymc: Byzantine model checker. In ISoLA (3), volume 11246 of LNCS, pages 327-342. Springer, 2018. Google Scholar
  25. Igor V. Konnov, Marijana Lazic, Helmut Veith, and Josef Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In POPL 2017, pages 719-734, 2017. Google Scholar
  26. Jure Kukovec, Igor Konnov, and Josef Widder. Reachability in parameterized systems: All flavors of threshold automata. In CONCUR, pages 19:1-19:17, 2018. Google Scholar
  27. Achour Mostéfaoui, Eric Mourgaya, Philippe Raipin Parvédy, and Michel Raynal. Evaluating the condition-based approach to solve consensus. In DSN, pages 541-550, 2003. Google Scholar
  28. T.K. Srikanth and Sam Toueg. Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Dist. Comp., 2:80-94, 1987. 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 Imprint Privacy Contact