{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T23:48:15Z","timestamp":1777765695929,"version":"3.51.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031974380","type":"print"},{"value":"9783031974397","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-97439-7_20","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:04:10Z","timestamp":1756551850000},"page":"408-424","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Termination in\u00a0Extended Probabilistic Threshold Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5160-0327","authenticated-orcid":false,"given":"Mouhammad","family":"Sakr","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8020-4446","authenticated-orcid":false,"given":"Marcus","family":"V\u00f6lp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","unstructured":"Baier, C., et al.: Chiefly symmetric: results on the scalability of probabilistic model checking for operating-system code. In: Prof. of the 7th Conference on Systems Software Verification (SSV\u201912). Electronic Proceedings in Theoretical Computer Science, vol.\u00a0102, pp. 156\u2013166 (2012). https:\/\/doi.org\/10.4204\/EPTCS.102.14","DOI":"10.4204\/EPTCS.102.14"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Balasubramanian, A., Esparza, J., Lazi\u0107, M.: Complexity of verification and synthesis of threshold automata. In: International Symposium on Automated Technology for Verification and Analysis, pp. 144\u2013160. Springer (2020)","DOI":"10.1007\/978-3-030-59152-6_8"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Baumeister, T., Eichler, P., Jacobs, S., Sakr, M., V\u00f6lp, M.: Parameterized verification of round-based distributed algorithms via extended threshold automata. In: International Symposium on Formal Methods, pp. 638\u2013657. Springer (2024)","DOI":"10.1007\/978-3-031-71162-6_33"},{"key":"20_CR4","doi-asserted-by":"publisher","unstructured":"Ben-Or, M.: Another advantage of free choice (extended abstract): completely asynchronous agreement protocols. In: Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, PODC \u201983, pp. 27\u201330. Association for Computing Machinery, New York (1983).https:\/\/doi.org\/10.1145\/800221.806707","DOI":"10.1145\/800221.806707"},{"key":"20_CR5","unstructured":"Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013), pp. 501\u2013513. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2013)"},{"key":"20_CR6","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Konnov, I., Lazi\u0107, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. Int. J. Softw. Tools Technol. Transfer, 1\u201325 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00603-x","DOI":"10.1007\/s10009-020-00603-x"},{"key":"20_CR7","doi-asserted-by":"publisher","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 123\u2013138. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_14","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"20_CR8","doi-asserted-by":"publisher","unstructured":"Gao, S., Zhan, B., Wu, Z., Zhang, L.: Verifying randomized consensus protocols with common coins. In: 2024 54th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 403\u2013415 (2024).https:\/\/doi.org\/10.1109\/DSN58291.2024.00047","DOI":"10.1109\/DSN58291.2024.00047"},{"key":"20_CR9","doi-asserted-by":"publisher","unstructured":"Guerraoui, R., Kuznetsov, P., Monti, M., Pavlovic, M., Seredinschi, D.: Scalable byzantine reliable broadcast. In: Suomela, J. (ed.) 33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary. LIPIcs, vol.\u00a0146, pp. 1\u201316. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019).https:\/\/doi.org\/10.4230\/LIPICS.DISC.2019.22","DOI":"10.4230\/LIPICS.DISC.2019.22"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Sakr, M.: Analyzing guarded protocols: better cutoffs, more systems, more expressivity. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 247\u2013268. Springer (2018)","DOI":"10.1007\/978-3-319-73721-8_12"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Sakr, M., Zimmermann, M.: Promptness and bounded fairness in concurrent and parameterized systems. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 337\u2013359. Springer (2020)","DOI":"10.1007\/978-3-030-39322-9_16"},{"issue":"2","key":"20_CR12","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/s10703-017-0297-4","volume":"51","author":"I Konnov","year":"2017","unstructured":"Konnov, I., Lazi\u0107, M., Veith, H., Widder, J.: Para 2: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods Syst. Des. 51(2), 270\u2013307 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Konnov, I., Lazi\u0107, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 719\u2013734 (2017)","DOI":"10.1145\/3009837.3009860"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Konnov, I., Widder, J.: BYMC: byzantine model checker. In: International Symposium on Leveraging Applications of Formal Methods, pp. 327\u2013342. Springer (2018)","DOI":"10.1007\/978-3-030-03424-5_22"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Larsen, C.A., Schmidt, S.M., Steensgaard, J., Jakobsen, A.B., de\u00a0Pol, J.V., Pavlogiannis, A.: A truly symbolic linear-time algorithm for SCC decomposition. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 353\u2013371. Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_22"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Leng\u00e1l, O., Lin, A.W., Majumdar, R., R\u00fcmmer, P.: Fair termination for parameterized probabilistic concurrent systems. In: Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22\u201329, 2017, Proceedings, Part I 23, pp. 499\u2013517. Springer (2017)","DOI":"10.1007\/978-3-662-54577-5_29"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Lin, A.W., R\u00fcmmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In: International Conference on Computer Aided Verification, pp. 112\u2013133. Springer (2016)","DOI":"10.1007\/978-3-319-41540-6_7"},{"key":"20_CR18","doi-asserted-by":"publisher","unstructured":"Malkhi, D., Reiter, M.: Byzantine quorum systems. In: Proceedings of the Twenty-Ninth Annual ACM Symposium on Theory of Computing, STOC \u201997, pp. 569\u2013578. Association for Computing Machinery, New York (1997). https:\/\/doi.org\/10.1145\/258533.258650","DOI":"10.1145\/258533.258650"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Neiheiser, R., Matos, M., Rodrigues, L.: Kauri: scalable BFT consensus with pipelined tree-based dissemination and aggregation. In: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, pp. 35\u201348 (2021)","DOI":"10.1145\/3477132.3483584"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. In: Proceedings of the third annual ACM Symposium on Principles of Distributed Computing, pp. 12\u201327 (1984)","DOI":"10.1145\/800222.806732"},{"issue":"4","key":"20_CR21","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I Suzuki","year":"1988","unstructured":"Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213\u2013214 (1988)","journal-title":"Inf. Process. Lett."},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Zamani, M., Movahedi, M., Raykova, M.: RapidChain: scaling blockchain via full sharding. In: Lie, D., Mannan, M., Backes, M., Wang, X. (eds.) Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15\u201319, 2018, pp. 931\u2013948. ACM (2018). https:\/\/doi.org\/10.1145\/3243734.3243853","DOI":"10.1145\/3243734.3243853"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Zarbafian, P., Gramoli, V.: Lyra: fast and scalable resilience to reordering attacks in blockchains. In: 2023 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 929\u2013939. IEEE (2023)","DOI":"10.1109\/IPDPS54959.2023.00097"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Zuck, L.D., McMillan, K.L., Torf, J.: Planner-less proofs of probabilistic parameterized protocols. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 336\u2013357. Springer (2017)","DOI":"10.1007\/978-3-319-73721-8_16"}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T15:28:19Z","timestamp":1777476499000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}