Advertisement

Liveness in Broadcast Networks

  • Peter ChiniEmail author
  • Roland Meyer
  • Prakash Saivasan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11704)

Abstract

We study two liveness verification problems for broadcast networks, a system model of identical clients communicating via message passing. The first problem is liveness verification. It asks whether there is a computation such that one of the clients visits a final state infinitely often. The complexity of the problem has been open since 2010 when it was shown to be \(\mathsf{P}\)-hard and solvable in \(\mathsf{EXPSPACE}\). We close the gap by a polynomial-time algorithm. The algorithm relies on a characterization of live computations in terms of paths in a suitable graph, combined with a fixed-point iteration to efficiently check the existence of such paths. The second problem is fair liveness verification. It asks for a computation where all participating clients visit a final state infinitely often. We adjust the algorithm to also solve fair liveness in polynomial time.

References

  1. 1.
    Abdulla, P.A., Atig, M.F., Rezine, O.: Verification of directed acyclic ad hoc networks. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE -2013. LNCS, vol. 7892, pp. 193–208. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38592-6_14CrossRefGoogle Scholar
  2. 2.
    Akhiani, H., et al.: Cache coherence verification with TLA%. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, p. 1871. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48118-4_62CrossRefGoogle Scholar
  3. 3.
    Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Balasubramanian, A.R., Bertrand, N., Markey, N.: Parameterized verification of synchronization in constrained reconfigurable broadcast networks. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 38–54. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89963-3_3CrossRefGoogle Scholar
  5. 5.
    Bertrand, N., Fournier, P., Sangnier, A.: Playing with probabilities in reconfigurable broadcast networks. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 134–148. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54830-7_9CrossRefGoogle Scholar
  6. 6.
    Bertrand, N., Fournier, P., Sangnier, A.: Distributed local strategies in broadcast networks. In: CONCUR. LIPIcs, vol. 42, pp. 44–57. Schloss Dagstuhl (2015)Google Scholar
  7. 7.
    Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015)Google Scholar
  8. 8.
    Bouyer, P., Markey, N., Randour, M., Sangnier, A., Stan, D.: Reachability in networks of register protocols under stochastic schedulers. In: ICALP. LIPIcs, vol. 55, pp. 106:1–106:14. Schloss Dagstuhl (2016)Google Scholar
  9. 9.
    Chini, P., Meyer, R., Saivasan, P.: Fine-grained complexity of safety verification. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 20–37. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89963-3_2CrossRefGoogle Scholar
  10. 10.
    Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53–68. Springer, Heidelberg (2000).  https://doi.org/10.1007/10722167_8CrossRefzbMATHGoogle Scholar
  11. 11.
    Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS. LIPIcs, vol. 18, pp. 289–300. Schloss Dagstuhl (2012)Google Scholar
  12. 12.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15375-4_22CrossRefGoogle Scholar
  13. 13.
    Delzanno, G., Sangnier, A., Zavattaro, G.: On the power of cliques in the parameterized verification of ad hoc networks. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 441–455. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19805-2_30CrossRefzbMATHGoogle Scholar
  14. 14.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of ad hoc networks with node and communication failures. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE -2012. LNCS, vol. 7273, pp. 235–250. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-30793-5_15CrossRefGoogle Scholar
  15. 15.
    D’Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of erlang-style concurrency. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 454–476. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38856-9_24CrossRefGoogle Scholar
  16. 16.
    D’Osualdo, E., Luke Ong, C.-H.: On hierarchical communication topologies in the \(\pi \)-calculus. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 149–175. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49498-1_7CrossRefGoogle Scholar
  17. 17.
    Durand-Gasselin, A., Esparza, J., Ganty, P., Majumdar, R.: Model checking parameterized asynchronous shared-memory systems. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 67–84. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_5CrossRefGoogle Scholar
  18. 18.
    Esparza, J.: Some applications of Petri nets to the analysis of parameterised systems (talk). In: WISP (2003)Google Scholar
  19. 19.
    Esparza, J.: Keeping a crowd safe: on the complexity of parameterized verification (invited talk). In: STACS. LIPIcs, vol. 25, pp. 1–10. Schloss Dagstuhl (2014)Google Scholar
  20. 20.
    Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS, pp. 352–359. IEEE (1999)Google Scholar
  21. 21.
    Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124–140. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_8CrossRefGoogle Scholar
  22. 22.
    Esparza, J., Nielsen, M.: Decidability issues for Petri nets - a survey. Bull. EATCS 52, 244–262 (1994)zbMATHGoogle Scholar
  23. 23.
    Fournier, P.: Parameterized verification of networks of many identical processes. Ph.D. thesis, University of Rennes 1 (2015)Google Scholar
  24. 24.
    Hague, M.: Parameterised pushdown systems with non-atomic writes. In: FSTTCS. LIPIcs, vol. 13, pp. 457–468. Schloss Dagstuhl (2011)Google Scholar
  25. 25.
    Hague, M., Meyer, R., Muskalla, S., Zimmermann, M.: Parity to safety in polynomial time for pushdown and collapsible pushdown systems. In: MFCS. LIPIcs, vol. 117, pp. 57:1–57:15. Schloss Dagstuhl (2018)Google Scholar
  26. 26.
    Hüchting, R., Majumdar, R., Meyer, R.: Bounds on mobility. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 357–371. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44584-6_25CrossRefGoogle Scholar
  27. 27.
    Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214–226. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70545-1_21CrossRefzbMATHGoogle Scholar
  28. 28.
    König, B., Kozioura, V.: Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 197–211. Springer, Heidelberg (2006).  https://doi.org/10.1007/11691372_13CrossRefzbMATHGoogle Scholar
  29. 29.
    Konnov, I.V., Lazic, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL, pp. 719–734. ACM (2017)Google Scholar
  30. 30.
    Meyer, R.: On boundedness in depth in the \(\pi \)-calculus. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) TCS 2008. IIFIP, vol. 273, pp. 477–489. Springer, Boston, MA (2008).  https://doi.org/10.1007/978-0-387-09680-3_32CrossRefGoogle Scholar
  31. 31.
    Meyer, R., Strazny, T.: Petruchio: from dynamic networks to nets. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 175–179. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_19CrossRefGoogle Scholar
  32. 32.
    Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)Google Scholar
  33. 33.
    Pnueli, A., Sa’ar, Y.: All you need is compassion. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 233–247. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78163-9_21CrossRefGoogle Scholar
  34. 34.
    Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959)MathSciNetCrossRefGoogle Scholar
  35. 35.
    Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18–32. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_3CrossRefzbMATHGoogle Scholar
  36. 36.
    Singh, A., Ramakrishnan, C.R., Smolka, S.A.: Query-based model checking of ad hoc network protocols. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 603–619. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04081-8_40CrossRefGoogle Scholar
  37. 37.
    Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322–331. IEEE (1986)Google Scholar
  38. 38.
    Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-12032-9_8CrossRefzbMATHGoogle Scholar
  39. 39.
    Zufferey, D.: Analysis of Dynamic Message Passing Programs (a framework for the analysis of depth-bounded systems). Ph.D. thesis, Institute of Science and Technology (2013)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.TU BraunschweigBraunschweigGermany

Personalised recommendations