Complexity of Liveness in Parameterized Systems
Document Open Access Logo

Complexity of Liveness in Parameterized Systems

Authors Peter Chini, Roland Meyer, Prakash Saivasan

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2019.37.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Author Details

Peter Chini
  • TU Braunschweig, Germany
Roland Meyer
  • TU Braunschweig, Germany
Prakash Saivasan
  • TU Braunschweig, Germany

Acknowledgements

We thank Arnaud Sangnier for helpful discussions.

Cite As Get BibTex

Peter Chini, Roland Meyer, and Prakash Saivasan. Complexity of Liveness in Parameterized Systems. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 37:1-37:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSTTCS.2019.37

Abstract

We investigate the fine-grained complexity of liveness verification for leader contributor systems. These consist of a designated leader thread and an arbitrary number of identical contributor threads communicating via a shared memory. The liveness verification problem asks whether there is an infinite computation of the system in which the leader reaches a final state infinitely often. Like its reachability counterpart, the problem is known to be NP-complete. Our results show that, even from a fine-grained point of view, the complexities differ only by a polynomial factor.
Liveness verification decomposes into reachability and cycle detection. We present a fixed point iteration solving the latter in polynomial time. For reachability, we reconsider the two standard parameterizations. When parameterized by the number of states of the leader L and the size of the data domain D, we show an (L + D)^O(L + D)-time algorithm. It improves on a previous algorithm, thereby settling an open problem. When parameterized by the number of states of the contributor C, we reuse an O^*(2^C)-time algorithm. We show how to connect both algorithms with the cycle detection to obtain algorithms for liveness verification. The running times of the composed algorithms match those of reachability, proving that the fine-grained lower bounds for liveness verification are met.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Problems, reductions and completeness
Keywords
  • Liveness Verification
  • Fine-Grained Complexity
  • Parameterized Systems

Metrics

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

Related Versions

References

  1. P. A. Abdulla and B. Jonsson. Verifying Programs with Unreliable Channels. In LICS, pages 160-170. IEEE, 1993. Google Scholar
  2. M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan. On Bounded Reachability Analysis of Shared Memory Systems. In FSTTCS, volume 29 of LIPIcs, pages 611-623. Schloss Dagstuhl, 2014. Google Scholar
  3. N. Bertrand, P. Fournier, and A. Sangnier. Playing with Probabilities in Reconfigurable Broadcast Networks. In FOSSACS, volume 8412 of LNCS, pages 134-148. Springer, 2014. Google Scholar
  4. R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and J. Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. Google Scholar
  5. P. Chini, J. Kolberg, A. Krebs, R. Meyer, and P. Saivasan. On the Complexity of Bounded Context Switching. In ESA, volume 87, pages 27:1-27:15. Schloss Dagstuhl, 2017. Google Scholar
  6. P. Chini, R. Meyer, and P.Saivasan. Liveness in Broadcast Networks. In NETYS, 2019. Google Scholar
  7. P. Chini, R. Meyer, and P. Saivasan. Fine-Grained Complexity of Safety Verification. In TACAS, volume 10806 of LNCS, pages 20-37. Springer, 2018. Google Scholar
  8. P. Chini, R. Meyer, and P. Saivasan. Fine-Grained Complexity of Safety Verification. CoRR, abs/1802.05559, 2018. URL: http://arxiv.org/abs/1802.05559.
  9. P. Chini, R. Meyer, and P. Saivasan. Complexity of Liveness in Parameterized Systems. CoRR, abs/1909.12004, 2019. URL: http://arxiv.org/abs/1909.12004.
  10. M. Cygan, F. V. Fomin, Ł. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, and S. Saurabh. Parameterized algorithms. Springer, 2015. Google Scholar
  11. G. Delzanno, A. Sangnier, R. Traverso, and G. Zavattaro. On the Complexity of Parameterized Reachability in Reconfigurable Broadcast Networks. In FSTTCS, volume 18 of LIPIcs, pages 289-300. Schloss Dagstuhl, 2012. Google Scholar
  12. G. Delzanno, A. Sangnier, and G. Zavattaro. Parameterized Verification of Ad Hoc Networks. In CONCUR, volume 6269 of LNCS, pages 313-327. Springer, 2010. Google Scholar
  13. R. G. Downey and M. R. Fellows. Fundamentals of Parameterized Complexity. Springer, 2013. Google Scholar
  14. A. Durand-Gasselin, J. Esparza, P. Ganty, and R. Majumdar. Model Checking Parameterized Asynchronous Shared-Memory Systems. In CAV, volume 9206 of LNCS, pages 67-84. Springer, 2015. Google Scholar
  15. C. Enea and A. Farzan. On Atomicity in Presence of Non-atomic Writes. In TACAS, volume 9636 of LNCS, pages 497-514. Springer, 2016. Google Scholar
  16. J. Esparza, P. Ganty, and R. Majumdar. Parameterized Verification of Asynchronous Shared-Memory Systems. In CAV, pages 124-140, 2013. Google Scholar
  17. J. Esparza, P. Ganty, and R. Majumdar. Parameterized Verification of Asynchronous Shared-Memory Systems. JACM, 63(1):10:1-10:48, 2016. Google Scholar
  18. A. Farzan and P. Madhusudan. The Complexity of Predicting Atomicity Violations. In TACAS, volume 5505 of LNCS, pages 155-169. Springer, 2009. Google Scholar
  19. H. Fernau, P. Heggernes, and Y. Villanger. A multi-parameter analysis of hard problems on deterministic finite automata. JCSS, 81(4):747-765, 2015. Google Scholar
  20. H. Fernau and A. Krebs. Problems on Finite Automata and the Exponential Time Hypothesis. In CIAA, volume 9705 of LNCS, pages 89-100. Springer, 2016. Google Scholar
  21. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! TCS, 256(1-2):63-92, 2001. Google Scholar
  22. F. V. Fomin and D. Kratsch. Exact Exponential Algorithms. Texts in Theoretical Computer Science. Springer, 2010. Google Scholar
  23. M. Fortin, A. Muscholl, and I. Walukiewicz. Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems. In CAV, volume 8044 of LNCS, pages 155-175. Springer, 2017. Google Scholar
  24. P. Fournier. Parameterized verification of networks of many identical processes. PhD thesis, University of Rennes 1, 2015. Google Scholar
  25. S. M. German and A. P. Sistla. Reasoning about Systems with Many Processes. JACM, 39(3):675-735, 1992. Google Scholar
  26. M. Hague. Parameterised Pushdown Systems with Non-Atomic Writes. In FSTTCS, volume 13 of LIPIcs, pages 457-468. Schloss Dagstuhl, 2011. Google Scholar
  27. M. Hague, R. Meyer, S. Muskalla, and M. Zimmermann. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. In MFCS, volume 117 of LIPIcs, pages 57:1-57:15. Schloss Dagstuhl, 2018. Google Scholar
  28. R. Impagliazzo and R. Paturi. On the Complexity of k-SAT. JCSS, 62(2):367-375, 2001. Google Scholar
  29. I. V. Konnov, M. Lazic, H. Veith, and J. Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In POPL, pages 719-734. ACM, 2017. Google Scholar
  30. S. R. Kosaraju and G. F. Sullivan. Detecting Cycles in Dynamic Graphs in Polynomial Time (Preliminary Version). In STOC, pages 398-406. ACM, 1988. Google Scholar
  31. S. La Torre, A. Muscholl, and I. Walukiewicz. Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. In CONCUR, volume 42 of LIPIcs, pages 72-84. Schloss Dagstuhl, 2015. Google Scholar
  32. O. Padon, J. Hoenicke, G. Losa, A. Podelski, M. Sagiv, and S. Shoham. Reducing liveness to safety in first-order logic. PACMPL, 2(POPL):26:1-26:33, 2018. Google Scholar
  33. S. Qadeer and J. Rehof. Context-Bounded Model Checking of Concurrent Software. In TACAS, volume 3440 of LNCS, pages 93-107. Springer, 2005. Google Scholar
  34. A. Singh, C. R. Ramakrishnan, and S. A. Smolka. Query-Based Model Checking of Ad Hoc Network Protocols. In CONCUR, volume 5710 of LNCS, pages 603-619. Springer, 2009. Google Scholar
  35. R. E. Tarjan. Depth-First Search and Linear Graph Algorithms. SICOMP, 1(2):146-160, 1972. Google Scholar
  36. T. Wareham. The Parameterized Complexity of Intersection and Composition Operations on Sets of Finite-State Automata. In CIAA, volume 2088 of LNCS, pages 302-310. Springer, 2000. Google Scholar
  37. G. Winskel. The formal semantics of programming languages - an introduction. Foundation of computing series. MIT Press, 1993. 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