Skip to main content
SpringerLink
Log in

Liveness in Broadcast Networks

  • Conference paper
  • First Online:
Networked Systems (NETYS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNCCN,volume 11704))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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_14

    Chapter  Google Scholar 

  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_62

    Chapter  Google Scholar 

  3. Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)

    Article  MathSciNet  Google Scholar 

  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_3

    Chapter  Google Scholar 

  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_9

    Chapter  Google Scholar 

  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. Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015)

    Google Scholar 

  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. 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_2

    Chapter  Google Scholar 

  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_8

    Chapter  MATH  Google Scholar 

  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. 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_22

    Chapter  Google Scholar 

  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_30

    Chapter  MATH  Google Scholar 

  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_15

    Chapter  Google Scholar 

  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_24

    Chapter  Google Scholar 

  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_7

    Chapter  Google Scholar 

  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_5

    Chapter  Google Scholar 

  18. Esparza, J.: Some applications of Petri nets to the analysis of parameterised systems (talk). In: WISP (2003)

    Google Scholar 

  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. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS, pp. 352–359. IEEE (1999)

    Google Scholar 

  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_8

    Chapter  Google Scholar 

  22. Esparza, J., Nielsen, M.: Decidability issues for Petri nets - a survey. Bull. EATCS 52, 244–262 (1994)

    MATH  Google Scholar 

  23. Fournier, P.: Parameterized verification of networks of many identical processes. Ph.D. thesis, University of Rennes 1 (2015)

    Google Scholar 

  24. Hague, M.: Parameterised pushdown systems with non-atomic writes. In: FSTTCS. LIPIcs, vol. 13, pp. 457–468. Schloss Dagstuhl (2011)

    Google Scholar 

  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. 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_25

    Chapter  Google Scholar 

  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_21

    Chapter  MATH  Google Scholar 

  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_13

    Chapter  MATH  Google Scholar 

  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. 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_32

    Chapter  Google Scholar 

  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_19

    Chapter  Google Scholar 

  32. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)

    Google Scholar 

  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_21

    Chapter  Google Scholar 

  34. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959)

    Article  MathSciNet  Google Scholar 

  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_3

    Chapter  MATH  Google Scholar 

  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_40

    Chapter  Google Scholar 

  37. Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322–331. IEEE (1986)

    Google Scholar 

  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_8

    Chapter  MATH  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. TU Braunschweig, Braunschweig, Germany

    Peter Chini, Roland Meyer & Prakash Saivasan

Authors
  1. Peter Chini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roland Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Prakash Saivasan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Chini .

Editor information

Editors and Affiliations

  1. Uppsala University, Uppsala, Uppsala Län, Sweden

    Mohamed Faouzi Atig

  2. Augusta University, Augusta, GA, USA

    Alexander A. Schwarzmann

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Chini, P., Meyer, R., Saivasan, P. (2019). Liveness in Broadcast Networks. In: Atig, M., Schwarzmann, A. (eds) Networked Systems. NETYS 2019. Lecture Notes in Computer Science(), vol 11704. Springer, Cham. https://doi.org/10.1007/978-3-030-31277-0_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31277-0_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31276-3

  • Online ISBN: 978-3-030-31277-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation