{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:24:12Z","timestamp":1740108252348,"version":"3.37.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"10","license":[{"start":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T00:00:00Z","timestamp":1628553600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T00:00:00Z","timestamp":1628553600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004871","name":"Technische Universit\u00e4t Braunschweig","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004871","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Computing"],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study liveness and model checking problems for broadcast networks, a system model of identical clients communicating via message passing. The first problem that we consider is <jats:italic>Liveness Verification<\/jats:italic>. It asks whether there is a computation such that one clients visits a final state infinitely often. The complexity of the problem has been open. It was shown to be <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt {P}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-hard but in <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\texttt {EXPSPACE}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>EXPSPACE<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. We close the gap by a polynomial-time algorithm. The latter 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 <jats:italic>Fair Liveness Verification<\/jats:italic>. 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. Both problems can be instrumented to answer model checking questions for broadcast networks against linear time temporal logic specifications. The first problem in this context is <jats:italic>Fair Model Checking<\/jats:italic>. It demands that for all computations of a broadcast network, all participating clients satisfy the specification. We solve the problem via the Vardi\u2013Wolper construction and a reduction to <jats:italic>Liveness Verification<\/jats:italic>. The second problem is <jats:italic>Sparse Model Checking<\/jats:italic>. It asks whether each computation has a participating client that satisfies the specification. We reduce the problem to <jats:italic>Fair Liveness Verification<\/jats:italic>.<\/jats:p>","DOI":"10.1007\/s00607-021-00986-y","type":"journal-article","created":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T12:02:42Z","timestamp":1628596962000},"page":"2203-2223","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Liveness in broadcast networks"],"prefix":"10.1007","volume":"104","author":[{"given":"Peter","family":"Chini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,10]]},"reference":[{"key":"986_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Atig MF, Rezine O (2013) Verification of directed acyclic ad hoc networks. In: FORTE, volume 7892 of LNCS. Springer, pp 193\u2013208","DOI":"10.1007\/978-3-642-38592-6_14"},{"key":"986_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Sistla AP, Talupur M (2018) Model checking parameterized systems. In: Handbook of model checking, pp 685\u2013725","DOI":"10.1007\/978-3-319-10575-8_21"},{"key":"986_CR3","doi-asserted-by":"crossref","unstructured":"Akhiani H, Doligez D, Harter P, Lamport L, Scheid J, Tuttle MR, Yu Y (1999) Cache coherence verification with TLA+. In: FM, volume 1709 of LNCS. Springer, pp 1871\u20131872","DOI":"10.1007\/3-540-48118-4_62"},{"issue":"6","key":"986_CR4","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt KR, Kozen D (1986) Limits for automatic verification of finite-state concurrent systems. Inf Process Lett 22(6):307\u2013309","journal-title":"Inf Process Lett"},{"key":"986_CR5","doi-asserted-by":"crossref","unstructured":"Balasubramanian AR, Bertrand N, Markey N (2018) Parameterized verification of synchronization in constrained reconfigurable broadcast networks. In: TACAS, volume 10806 of LNCS. Springer, pp 38\u201354","DOI":"10.1007\/978-3-319-89963-3_3"},{"key":"986_CR6","doi-asserted-by":"crossref","unstructured":"Bertrand N, Fournier P, Sangnier A (2014) Playing with probabilities in reconfigurable broadcast networks. In: FOSSACS, volume 8412 of LNCS. Springer, pp 134\u2013148","DOI":"10.1007\/978-3-642-54830-7_9"},{"key":"986_CR7","unstructured":"Bertrand N, Fournier P, Sangnier A (2015) Distributed local strategies in broadcast networks. In: CONCUR, volume\u00a042 of LIPIcs. Schloss Dagstuhl, pp 44\u201357"},{"key":"986_CR8","doi-asserted-by":"crossref","unstructured":"Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J (2015) Decidability of parameterized verification. Synthesis lectures on distributed computing theory. Morgan and Claypool Publishers","DOI":"10.1007\/978-3-031-02011-7"},{"key":"986_CR9","unstructured":"Bouyer P, Markey N, Randour M, Sangnier A, Stan D (2016) Reachability in networks of register protocols under stochastic schedulers. In: ICALP, volume\u00a055 of LIPIcs. Schloss Dagstuhl, pp 106:1\u2013106:14"},{"key":"986_CR10","doi-asserted-by":"crossref","unstructured":"Chini P, Meyer R, Saivasan P (2018) Fine-grained complexity of safety verification. In: TACAS, volume 10806 of LNCS. Springer, pp 20\u201337","DOI":"10.1007\/978-3-319-89963-3_2"},{"key":"986_CR11","unstructured":"Chini P, Meyer R, Saivasan P (2019) Complexity of liveness in parameterized systems. In: FSTTCS, volume 150 of LIPIcs. Schloss Dagstuhl, pp 37:1\u201337:15"},{"key":"986_CR12","doi-asserted-by":"crossref","unstructured":"Chini P, Meyer R, Saivasan P (2019) Liveness in broadcast networks. In: NETYS, volume 11704 of LNCS. Springer, pp 52\u201366","DOI":"10.1007\/978-3-030-31277-0_4"},{"key":"986_CR13","doi-asserted-by":"crossref","unstructured":"Chini P, Meyer R, Saivasan P (2019) Liveness in broadcast networks. CoRR. arXiv:1904.00833","DOI":"10.1007\/978-3-030-31277-0_4"},{"issue":"7","key":"986_CR14","doi-asserted-by":"publisher","first-page":"1419","DOI":"10.1007\/s10817-020-09572-x","volume":"64","author":"P Chini","year":"2020","unstructured":"Chini P, Meyer R, Saivasan P (2020) Fine-grained complexity of safety verification. J Autom Reason 64(7):1419\u20131444","journal-title":"J Autom Reason"},{"key":"986_CR15","doi-asserted-by":"crossref","unstructured":"Delzanno G (2000) Automatic verification of parameterized cache coherence protocols. In: CAV, volume 1855 of LNCS. Springer, pp 53\u201368","DOI":"10.1007\/10722167_8"},{"key":"986_CR16","unstructured":"Delzanno G, Sangnier A, Traverso R, Zavattaro G (2012) On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS, volume\u00a018 of LIPIcs. Schloss Dagstuhl, pp 289\u2013300"},{"key":"986_CR17","doi-asserted-by":"crossref","unstructured":"Delzanno G, Sangnier A, Zavattaro G (2010) Parameterized verification of ad hoc networks. In: CONCUR, volume 6269 of LNCS. Springer, pp 313\u2013327","DOI":"10.1007\/978-3-642-15375-4_22"},{"key":"986_CR18","doi-asserted-by":"crossref","unstructured":"Delzanno G, Sangnier A, Zavattaro G (2011) On the power of cliques in the parameterized verification of ad hoc networks. In: FOSSACS, volume 6604 of LNCS. Springer, pp 441\u2013455","DOI":"10.1007\/978-3-642-19805-2_30"},{"key":"986_CR19","doi-asserted-by":"crossref","unstructured":"Delzanno G, Sangnier A, Zavattaro G (2012) Verification of ad hoc networks with node and communication failures. In: FORTE, volume 7273 of LNCS . Springer, pp 235\u2013250","DOI":"10.1007\/978-3-642-30793-5_15"},{"key":"986_CR20","doi-asserted-by":"crossref","unstructured":"D\u2019Osualdo E, Kochems J, Luke Ong C-H (2013) Automatic verification of erlang-style concurrency. In: SAS, volume 7935 of tLNCS. Springer, pp 454\u2013476","DOI":"10.1007\/978-3-642-38856-9_24"},{"key":"986_CR21","doi-asserted-by":"crossref","unstructured":"D\u2019Osualdo E, Luke Ong C-H (2016) On hierarchical communication topologies in the $$\\pi $$-calculus. In: ESOP, volume 9632 of LNCS. Springer, pp 149\u2013175","DOI":"10.1007\/978-3-662-49498-1_7"},{"key":"986_CR22","doi-asserted-by":"crossref","unstructured":"Durand-Gasselin A, Esparza J, Ganty P, Majumdar R (2015) Model checking parameterized asynchronous shared-memory systems. In: CAV, volume 9206 of LNCS. Springer, pp 67\u201384","DOI":"10.1007\/978-3-319-21690-4_5"},{"key":"986_CR23","unstructured":"Esparza J (2003) Some applications of Petri nets to the analysis of parameterised systems (talk). WISP"},{"key":"986_CR24","unstructured":"Esparza J (2014) Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In: STACS, volume\u00a025 of LIPIcs. Schloss Dagstuhl, pp 1\u201310"},{"key":"986_CR25","doi-asserted-by":"crossref","unstructured":"Esparza J, Finkel A, Mayr R (1999) On the verification of broadcast protocols. In: LICS. IEEE, pp 352\u2013359","DOI":"10.1109\/LICS.1999.782630"},{"key":"986_CR26","doi-asserted-by":"crossref","unstructured":"Esparza J, Ganty P, Majumdar R (2013) Parameterized verification of asynchronous shared-memory systems. In: CAV, volume 8044 of LNCS. Springer, pp 124\u2013140","DOI":"10.1007\/978-3-642-39799-8_8"},{"key":"986_CR27","first-page":"244","volume":"52","author":"J Esparza","year":"1994","unstructured":"Esparza J, Nielsen M (1994) Decidability issues for Petri nets\u2014a survey. Bull EATCS 52:244\u2013262","journal-title":"Bull EATCS"},{"key":"986_CR28","unstructured":"Fournier P (2015) Parameterized verification of networks of many identical processes. Ph.D. thesis, University of Rennes 1"},{"key":"986_CR29","unstructured":"Hague M (2011) Parameterised pushdown systems with non-atomic writes. In: FSTTCS, volume\u00a013 of LIPIcs. Schloss Dagstuhl, pp 457\u2013468"},{"key":"986_CR30","unstructured":"Hague M, Meyer R, Muskalla S, Zimmermann M (2018) Parity to safety in polynomial time for pushdown and collapsible pushdown systems. In: MFCS, volume 117 of LIPIcs. Schloss Dagstuhl, pp 57:1\u201357:15"},{"key":"986_CR31","doi-asserted-by":"crossref","unstructured":"H\u00fcchting R, Majumdar R, Meyer R (2014) Bounds on mobility. In: CONCUR, volume 8704 of LNCS. Springer, pp 357\u2013371","DOI":"10.1007\/978-3-662-44584-6_25"},{"key":"986_CR32","doi-asserted-by":"crossref","unstructured":"Joshi S, K\u00f6nig B (2008) Applying the graph minor theorem to the verification of graph transformation systems. In: CAV, volume 5123 of LNCS. Springer, pp 214\u2013226","DOI":"10.1007\/978-3-540-70545-1_21"},{"key":"986_CR33","doi-asserted-by":"crossref","unstructured":"Khoussainov B, Nerode A (2001) Automata theory and its applications. Birkhauser, Boston","DOI":"10.1007\/978-1-4612-0171-7"},{"key":"986_CR34","doi-asserted-by":"crossref","unstructured":"K\u00f6nig B, Kozioura V (2006) Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In: TACAS, volume 3920 of LNCS. Springer, pp 197\u2013211","DOI":"10.1007\/11691372_13"},{"key":"986_CR35","doi-asserted-by":"crossref","unstructured":"Konnov IV, Lazic M, Veith H, Widder J (2017) A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL. ACM, pp 719\u2013734","DOI":"10.1145\/3093333.3009860"},{"key":"986_CR36","doi-asserted-by":"crossref","unstructured":"Kosaraju SR, Sullivan GF (1988) Detecting cycles in dynamic graphs in polynomial time (preliminary version). In: STOC. ACM, pp 398\u2013406","DOI":"10.1145\/62212.62251"},{"key":"986_CR37","doi-asserted-by":"crossref","unstructured":"Meyer R (2008) On boundedness in depth in the $$\\pi $$-calculus. In: IFIP TCS, volume 273 of IFIP. Springer, pp 477\u2013489","DOI":"10.1007\/978-0-387-09680-3_32"},{"key":"986_CR38","doi-asserted-by":"crossref","unstructured":"Meyer R, Strazny T (2010) Petruchio: From dynamic networks to nets. In: CAV, volume 6174 of LNCS. Springer, pp 175\u2013179","DOI":"10.1007\/978-3-642-14295-6_19"},{"key":"986_CR39","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: FOCS. IEEE, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"986_CR40","doi-asserted-by":"crossref","unstructured":"Pnueli A, Sa\u2019ar Y (2008) All you need is compassion. In: VMCAI, volume 4905 of LNCS. Springer, pp 233\u2013247","DOI":"10.1007\/978-3-540-78163-9_21"},{"issue":"2","key":"986_CR41","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"MO Rabin","year":"1959","unstructured":"Rabin MO, Scott D (1959) Finite automata and their decision problems. IBM J Res Dev 3(2):114\u2013125","journal-title":"IBM J Res Dev"},{"key":"986_CR42","doi-asserted-by":"crossref","unstructured":"Saksena M, Wibling O, Jonsson B (2008) Graph grammar modeling and verification of ad hoc routing protocols. In: TACAS, volume 4963 of LNCS. Springer, pp 18\u201332","DOI":"10.1007\/978-3-540-78800-3_3"},{"key":"986_CR43","doi-asserted-by":"crossref","unstructured":"Singh A, Ramakrishnan CR, Smolka SA (2009) Query-based model checking of ad hoc network protocols. In: CONCUR, volume 5710 of LNCS. Springer, pp 603\u2013619","DOI":"10.1007\/978-3-642-04081-8_40"},{"key":"986_CR44","unstructured":"Vardi M, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: LICS. IEEE, pp 322\u2013331"},{"key":"986_CR45","doi-asserted-by":"crossref","unstructured":"Wies T, Zuffrey D, Henzinger TA (2010) Forward analysis of depth-bounded processes. In: FoSSaCS, volume 6014 of LNCS. Springer, pp 94\u2013108","DOI":"10.1007\/978-3-642-12032-9_8"},{"key":"986_CR46","unstructured":"Zufferey D (2013) Analysis of Dynamic Message Passing Programs (a framework for the analysis of depth-bounded systems). Ph.D. thesis, Institute of Science and Technology"}],"container-title":["Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-021-00986-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00607-021-00986-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-021-00986-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,15]],"date-time":"2022-09-15T18:14:31Z","timestamp":1663265671000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00607-021-00986-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,10]]},"references-count":46,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["986"],"URL":"https:\/\/doi.org\/10.1007\/s00607-021-00986-y","relation":{},"ISSN":["0010-485X","1436-5057"],"issn-type":[{"type":"print","value":"0010-485X"},{"type":"electronic","value":"1436-5057"}],"subject":[],"published":{"date-parts":[[2021,8,10]]},"assertion":[{"value":"30 June 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 July 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 August 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}