{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:14Z","timestamp":1784793794061,"version":"3.55.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We study concurrent graph games where\n                    <jats:italic>n<\/jats:italic>\n                    players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden from the opponent and from each other.\n                  <\/jats:p>\n                  <jats:p>\n                    We show that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that not only places the problem in the Existential Theory of the Reals (\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\exists \\mathbb {R}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mo>\u2203<\/mml:mo>\n                            <mml:mi>R<\/mml:mi>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    ) but also enables the construction of value iteration algorithms. We additionally show that the threshold problem is\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{NP}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>NP<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -hard. For the almost-sure reachability problem, we prove\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{NP}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>NP<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -completeness.\n                  <\/jats:p>\n                  <jats:p>We introduce Individually Randomised Alternating-time Temporal Logic (IRATL). This logic extends the standard ATL framework to reason about probability thresholds, with semantics explicitly designed for coalitions that lack a shared source of randomness. On the practical side, we implement and evaluate a solver for the threshold and almost-sure problem based on the algorithms that we develop.<\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_12","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:58Z","timestamp":1784791078000},"page":"215-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Randomise Alone, Reach as\u00a0a\u00a0Team"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7748-7716","authenticated-orcid":false,"given":"L\u00e9onard","family":"Brice","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2985-7724","authenticated-orcid":false,"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3262-9332","authenticated-orcid":false,"given":"Alipasha","family":"Montaseri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-5947-1946","authenticated-orcid":false,"given":"Ali","family":"Shafiee","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6077-7514","authenticated-orcid":false,"given":"K. S.","family":"Thejaswini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"de Alfaro, L., Henzinger, T.A., Jhala, R.: Compositional methods for probabilistic systems. In: CONCUR 2001 \u2013 Concurrency Theory, pp. 351\u2013365. Springer, Berlin Heidelberg, Berlin, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44685-0_24","DOI":"10.1007\/3-540-44685-0_24"},{"issue":"5","key":"12_CR2","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002). https:\/\/doi.org\/10.1145\/585265.585270","journal-title":"J. ACM"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Aminof, B., Kwiatkowska, M., Maubert, B., Murano, A., Rubin, S.: Probabilistic strategy logic, pp. 32\u201338 (2019). https:\/\/doi.org\/10.24963\/ijcai.2019\/5","DOI":"10.24963\/ijcai.2019\/5"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Attoui, A.: Multi-agent based method for reactive systems formal specification and validation. IFAC Proc. Vol. 29(2), 1\u20136 (1996). https:\/\/doi.org\/10.1016\/S1474-6670(17)43768-2. 5th IFAC\/IFIP\/GI\/GMA Workshop on Experience With the Management of Software Projects 1995 (MSP \u201995)","DOI":"10.1016\/S1474-6670(17)43768-2"},{"issue":"4","key":"12_CR5","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s00236-012-0156-0","volume":"49","author":"C Baier","year":"2012","unstructured":"Baier, C., Br\u00e1zdil, T., Gr\u00f6\u00dfer, M., Ku\u010dera, A.: Stochastic game logic. Acta Inf. 49(4), 203\u2013224 (2012). https:\/\/doi.org\/10.1007\/s00236-012-0156-0","journal-title":"Stochastic game logic. Acta Inf."},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Bouyer, P., Lapointe, L., Mascle, C.: Reach together: how populations win repeated games. CoRR abs\/2510.02984 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2510.02984","DOI":"10.48550\/ARXIV.2510.02984"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Bouyer, P., Majumdar, A.: Concurrent parameterized games. In: FSTTCS 2019. LIPIcs, vol. 150, pp. 31:1\u201331:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2019.31","DOI":"10.4230\/LIPICS.FSTTCS.2019.31"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Bouyer, P., Majumdar, A.: Synthesizing safe coalition strategies. In: FSTTCS 2020. LIPIcs, vol. 182, pp. 39:1\u201339:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2020.39","DOI":"10.4230\/LIPICS.FSTTCS.2020.39"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Brice, L., Henzinger, T.A., Montaseri, A., Shafiee, A., Thejaswini, K.S.: Randomise alone, reach as a team. CoRR abs\/2603.07094 (2026). https:\/\/doi.org\/10.48550\/ARXIV.2603.07094","DOI":"10.48550\/ARXIV.2603.07094"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Brice, L., Henzinger, T.A., Thejaswini, K.S.: Dicey games: shared sources of randomness in distributed systems (2026). https:\/\/doi.org\/10.48550\/arXiv.2601.18303","DOI":"10.48550\/arXiv.2601.18303"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. In: Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing STOC, pp. 460\u2013467. STOC \u201988, Association for Computing Machinery (1988). https:\/\/doi.org\/10.1145\/62212.62257","DOI":"10.1145\/62212.62257"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Strategy improvement for concurrent reachability and safety games. CoRR abs\/1201.2834 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2012.12.001, https:\/\/arxiv.org\/abs\/1201.2834. preprint version of the combined QEST\/SODA results","DOI":"10.1016\/j.jcss.2012.12.001"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Inf. Comput. 208(6), 677\u2013693 (2010). https:\/\/doi.org\/10.1016\/j.ic.2009.07.004. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540110000192. special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007)","DOI":"10.1016\/j.ic.2009.07.004"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Prism-games: a model checker for stochastic multi-player games. In: TACAS 2013. Lecture Notes in Computer Science, vol. 7795, pp. 185\u2013191. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_13","DOI":"10.1007\/978-3-642-36742-7_13"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-28756-5_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Chen","year":"2012","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 315\u2013330. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_22"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Chen, T., Lu, J.: Probabilistic alternating-time temporal logic and model checking algorithm. In: Lei, J. (ed.) FSKD 2007, pp. 35\u201339. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/FSKD.2007.458","DOI":"10.1109\/FSKD.2007.458"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. Theoret. Comput. Sci. 386(3), 188\u2013217 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2007.07.008. expressiveness in Concurrency","DOI":"10.1016\/j.tcs.2007.07.008"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Etessami, K., Yannakakis, M.: Recursive markov decision processes and recursive stochastic games. J. ACM 62(2) (2015). https:\/\/doi.org\/10.1145\/2699431","DOI":"10.1145\/2699431"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems, pp. 53\u2013113. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Guestrin, C., Koller, D., Parr, R.: Multiagent planning with factored MDPs. In: Advances in Neural Information Processing Systems (NIPS). vol. 14, pp. 1523\u20131530. MIT Press (2002). https:\/\/doi.org\/10.5555\/2980539.2980737","DOI":"10.5555\/2980539.2980737"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Gutierrez, J., Najib, M., Perelli, G., Wooldridge, M.J.: EVE: a tool for temporal equilibrium analysis. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, 7\u201310 October 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 551\u2013557. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_35","DOI":"10.1007\/978-3-030-01090-4_35"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Hansen, K.A., Ibsen-Jensen, R., Miltersen, P.B.: The complexity of solving reachability games using value and strategy iteration. In: Computer Science - Theory and Applications. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-20712-9_7","DOI":"10.1007\/978-3-642-20712-9_7"},{"issue":"4","key":"12_CR23","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 384\u2013406 (1981). https:\/\/doi.org\/10.1016\/0022-0000(81)90039-8, https:\/\/api.semanticscholar.org\/CorpusID:40753086","DOI":"10.1016\/0022-0000(81)90039-8"},{"key":"12_CR25","unstructured":"Kok, J.R., Vlassis, N.: Collaborative multiagent reinforcement learning by payoff propagation. J. Mach. Learn. Res. (JMLR) 7(65), 1789\u20131828 (2006). https:\/\/jmlr.org\/papers\/v7\/kok06a.html"},{"key":"12_CR26","unstructured":"Kraft, D.: A software package for sequential quadratic programming. Tech. Rep. Forschungsbericht FB 88\u201328, Deutsche Forschungs- und Versuchsanstalt f\u00fcr Luft- und Raumfahrt (DFVLR), K\u00f6ln, Germany (1988). https:\/\/degenerateconic.com\/uploads\/2018\/03\/DFVLR_FB_88_28.pdf"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Prism-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, 21\u201324 July 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 475\u2013487. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automatic verification of concurrent stochastic systems. Formal Methods Syst. Design, 188\u2013250 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00356-y","DOI":"10.1007\/s10703-020-00356-y"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Weininger, M.: Stopping criteria for value iteration on stochastic games with quantitative objectives. In: 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201314 (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175771","DOI":"10.1109\/LICS56636.2023.10175771"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Lef\u00e8vre, C.: Optimal control of a birth and death epidemic process. Oper. Res. 29(5), 971\u2013982 (1981). https:\/\/doi.org\/10.1287\/opre.29.5.971, http:\/\/www.jstor.org\/stable\/170234","DOI":"10.1287\/opre.29.5.971"},{"issue":"1","key":"12_CR31","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/S10009-015-0378-X","volume":"19","author":"A Lomuscio","year":"2017","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1), 9\u201330 (2017). https:\/\/doi.org\/10.1007\/S10009-015-0378-X","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Lyu, G., Fazlirad, A., Brennan, R.W.: Multi-agent modeling of cyber-physical systems for IEC 61499 based distributed automation. Procedia Manufact. 51, 1200\u20131206 (2020). https:\/\/doi.org\/10.1016\/j.promfg.2020.10.168. 30th International Conference on Flexible Automation and Intelligent Manufacturing (FAIM2021)","DOI":"10.1016\/j.promfg.2020.10.168"},{"key":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Nguyen, H., Rakib, A.: A probabilistic logic for resource-bounded multi-agent systems, pp. 521\u2013527 (2019). https:\/\/doi.org\/10.24963\/ijcai.2019\/74","DOI":"10.24963\/ijcai.2019\/74"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"Parsons, T.D.: Pursuit-evasion in a graph. In: Theory and Applications of Graphs: Proceedings, Michigan 11\u201315 May 1976, pp. 426\u2013441. Springer (2006). https:\/\/doi.org\/10.1007\/BFb0070400","DOI":"10.1007\/BFb0070400"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Schaefer, M., Cardinal, J., Miltzow, T.: The existential theory of the reals as a complexity class: a compendium. CoRR abs\/2407.18006 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2407.18006","DOI":"10.48550\/ARXIV.2407.18006"},{"issue":"1","key":"12_CR37","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1109\/TAC.2016.2541919","volume":"62","author":"D Shi","year":"2016","unstructured":"Shi, D., Elliott, R.J., Chen, T.: On finite-state stochastic modeling and secure estimation of cyber-physical systems. IEEE Trans. Autom. Control 62(1), 65\u201380 (2016). https:\/\/doi.org\/10.1109\/TAC.2016.2541919","journal-title":"IEEE Trans. Autom. Control"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Song, F., Chen, T., Tang, Y., Xu, Z.: Probabilistic alternating-time $$\\upmu $$-calculus. In: Proceedings of the AAAI Conference on Artificial Intelligence vol. 33, pp. 6179\u20136186 (2019). https:\/\/doi.org\/10.1609\/aaai.v33i01.33016179","DOI":"10.1609\/aaai.v33i01.33016179"},{"key":"12_CR39","unstructured":"Sorensson, N.: Minisat 2.2 and minisat++ 1.1. http:\/\/baldur.iti.uka.de\/sat-race-2010\/descriptions\/solver_25+ 26.pdf (2010). https:\/\/www.semanticscholar.org\/paper\/MINISAT-2.2-and-MINISAT%2B%2B-1.1-S%C3%B6rensson\/e46a90899c7ca924c30983cf4cede5804df7ab7f"},{"key":"12_CR40","doi-asserted-by":"publisher","unstructured":"Virtanen, P., et al.: SciPy 1.0 Contributors: SciPy 1.0: Fundamental algorithms for scientific computing in python. Nat. Methods 17, 261\u2013272 (2020). https:\/\/doi.org\/10.1038\/s41592-019-0686-2","DOI":"10.1038\/s41592-019-0686-2"},{"key":"12_CR41","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15240-5_6","volume-title":"Theoretical Computer Science","author":"C Zhang","year":"2010","unstructured":"Zhang, C., Pang, J.: On probabilistic alternating simulations. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IAICT, vol. 323, pp. 71\u201385. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15240-5_6"},{"key":"12_CR42","doi-asserted-by":"publisher","unstructured":"Zhang, K., Yang, Z., Ba\u015far, T.: Multi-agent reinforcement learning: a selective overview of theories and algorithms. In: Handbook of Reinforcement Learning and Control, pp. 321\u2013384 (2021). https:\/\/doi.org\/10.1007\/978-3-030-60990-0_12","DOI":"10.1007\/978-3-030-60990-0_12"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:01Z","timestamp":1784791081000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}