{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:37:12Z","timestamp":1742981832294,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031753862"},{"type":"electronic","value":"9783031753879"}],"license":[{"start":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T00:00:00Z","timestamp":1729900800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T00:00:00Z","timestamp":1729900800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>System behaviors are traditionally evaluated through binary classifications of correctness, which do not suffice for properties involving quantitative aspects of systems and executions. Quantitative automata offer a more nuanced approach, mapping each execution to a real number by incorporating weighted transitions and value functions generalizing acceptance conditions. In this paper, we introduce QuAK, the first tool designed to automate the analysis of quantitative automata. QuAK currently supports a variety of quantitative automaton types, including <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{Inf}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Inf<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{Sup}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Sup<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{LimInf}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LimInf<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{LimSup}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LimSup<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{LimInfAvg}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LimInfAvg<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{LimSupAvg}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LimSupAvg<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> automata, and implements decision procedures for problems such as emptiness, universality, inclusion, equivalence, as well as for checking whether an automaton is safe, live, or constant. Additionally, QuAK is able to compute extremal values when possible, construct safety-liveness decompositions, and monitor system behaviors. We demonstrate the effectiveness of QuAK through experiments focusing on the inclusion, constant-function check, and monitoring problems.<\/jats:p>","DOI":"10.1007\/978-3-031-75387-9_1","type":"book-chapter","created":{"date-parts":[[2024,10,25]],"date-time":"2024-10-25T08:02:14Z","timestamp":1729843334000},"page":"3-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["QuAK: Quantitative Automata Kit"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1132-5516","authenticated-orcid":false,"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2985-7724","authenticated-orcid":false,"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6425-5369","authenticated-orcid":false,"given":"Nicolas","family":"Mazzocchi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2866-8078","authenticated-orcid":false,"given":"N.\u00a0Ege","family":"Sara\u00e7","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,26]]},"reference":[{"issue":"3","key":"1_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987). https:\/\/doi.org\/10.1007\/BF01782772","journal-title":"Distrib. Comput."},{"issue":"2","key":"1_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"1_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/INCO.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35\u201377 (1993). https:\/\/doi.org\/10.1006\/INCO.1993.1025","journal-title":"Inf. Comput."},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254\u2013257. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Boker, U.: Quantitative vs. weighted automata. In: Proceedings of Reachability Problems, pp. 1\u201316 (2021)","DOI":"10.1007\/978-3-030-89716-1_1"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Boker, U.: Discounted-sum automata with real-valued discount factors. In: Sobocinski, P., Lago, U.D., Esparza, J. (eds.) Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, 8\u201311 July 2024, pp. 15:1\u201315:14. ACM (2024). https:\/\/doi.org\/10.1145\/3661814.3662090","DOI":"10.1145\/3661814.3662090"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Boker, U., Henzinger, T.A.: Exact and approximate determinization of discounted-sum automata. Log. Methods Comput. Sci. 10(1) (2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:10)2014","DOI":"10.2168\/LMCS-10(1:10)2014"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Boker, U., Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Safety and liveness of quantitative automata. In: P\u00e9rez, G.A., Raskin, J. (eds.) 34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium, 18\u201323 September 2023. LIPIcs, vol.\u00a0279, pp. 17:1\u201317:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.17","DOI":"10.4230\/LIPICS.CONCUR.2023.17"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Boker, U., Henzinger, T.A., Otop, J.: The target discounted-sum problem. In: 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6\u201310 July 2015, pp. 750\u2013761. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/LICS.2015.74","DOI":"10.1109\/LICS.2015.74"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274\u2013287. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_25"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-642-15375-4_19","volume-title":"CONCUR 2010 - Concurrency Theory","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Edelsbrunner, H., Henzinger, T.A., Rannou, P.: Mean-payoff automaton expressions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 269\u2013283. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_19"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4), 23:1\u201323:38 (2010). https:\/\/doi.org\/10.1145\/1805950.1805953","DOI":"10.1145\/1805950.1805953"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/3-540-45657-0_41","volume-title":"Computer Aided Verification","author":"M Chechik","year":"2002","unstructured":"Chechik, M., Gurfinkel, A., Devereux, B.: XChek: a multi-valued model-checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 505\u2013509. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_41"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-15205-4_22","volume-title":"Computer Science Logic","author":"A Degorre","year":"2010","unstructured":"Degorre, A., Doyen, L., Gentilini, R., Raskin, J.-F., Toru\u0144czyk, S.: Energy and mean-payoff games with imperfect information. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 260\u2013274. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_22"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-39274-0_12","volume-title":"Implementation and Application of Automata","author":"A Demaille","year":"2013","unstructured":"Demaille, A., Duret-Lutz, A., Lombardy, S., Sakarovitch, J.: Implementation concepts in Vaucanson 2. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 122\u2013133. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39274-0_12"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_17"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Doveri, K., Ganty, P., Mazzocchi, N.: FORKLIFT (v1.0). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.6552870. Maintained at https:\/\/github.com\/Mazzocchi\/FORKLIFT","DOI":"10.5281\/zenodo.6552870"},{"key":"1_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-031-13188-2_6","volume-title":"CAV 2022, Part II","author":"K Doveri","year":"2022","unstructured":"Doveri, K., Ganty, P., Mazzocchi, N.: FORQ-based language inclusion formal testing. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, Part II. LNCS, vol. 13372, pp. 109\u2013129. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_6"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Doveri, K., Ganty, P., Parolini, F., Ranzato, F.: Inclusion testing of b\u00fcchi automata based on well-quasiorders. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, 24\u201327 August 2021, Virtual Conference. LIPIcs, vol.\u00a0203, pp. 3:1\u20133:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2021.3","DOI":"10.4230\/LIPICS.CONCUR.2021.3"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BF01768705","volume":"8","author":"A Ehrenfeucht","year":"1979","unstructured":"Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Internat. J. Game Theory 8, 109\u2013113 (1979)","journal-title":"Internat. J. Game Theory"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27\u201330 July 1996, pp. 278\u2013292. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561342","DOI":"10.1109\/LICS.1996.561342"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"TA Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: HyTech: the Cornell hybrid technology tool. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 265\u2013293. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60472-3_14"},{"key":"1_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-031-17196-3_11","volume-title":"RV 2022","author":"TA Henzinger","year":"2022","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Abstract monitors for quantitative specifications. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 200\u2013220. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_11"},{"key":"1_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-031-30829-1_17","volume-title":"ETAPS 2023","author":"TA Henzinger","year":"2023","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Quantitative safety and liveness. In: Kupferman, O., Sobocinski, P. (eds.) ETAPS 2023. LNCS, vol. 13992, pp. 349\u2013370. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30829-1_17"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Quantitative and approximate monitoring. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pp. 1\u201314. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470547","DOI":"10.1109\/LICS52264.2021.9470547"},{"issue":"3","key":"1_CR26","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001). https:\/\/doi.org\/10.1023\/A:1011254632723","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation: Modelling Techniques and Tools","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200\u2013204. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46029-2_13"},{"issue":"1\u20132","key":"1_CR28","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/S100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/S100090050010","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR29","unstructured":"Lombardy, S., Marsault, V., Sakarovitch, J.: Awali, a library for weighted automata and transducers (version 2.3) (2022). Software available at http:\/\/vaucanson-project.org\/Awali\/2.3\/"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45089-0_10","volume-title":"Implementation and Application of Automata","author":"S Lombardy","year":"2003","unstructured":"Lombardy, S., Poss, R., R\u00e9gis-Gianas, Y., Sakarovitch, J.: Introducing Vaucanson. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 96\u2013107. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45089-0_10"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Michaliszyn, J., Otop, J.: Approximate learning of limit-average automata. In: Fokkink, W.J., van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, the Netherlands, 27\u201330 August 2019. LIPIcs, vol.\u00a0140, pp. 17:1\u201317:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2019.17","DOI":"10.4230\/LIPICS.CONCUR.2019.17"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Michaliszyn, J., Otop, J.: Minimization of limit-average automata. In: Zhou, Z. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event \/ Montreal, Canada, August 19\u201327 2021, pp. 2819\u20132825. ijcai.org (2021). https:\/\/doi.org\/10.24963\/IJCAI.2021\/388","DOI":"10.24963\/IJCAI.2021\/388"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Mysore, S., Mabsout, B., Mancuso, R., Saenko, K.: Regularizing action policies for smooth control with reinforcement learning. In: IEEE International Conference on Robotics and Automation, ICRA 2021, Xi\u2019an, China, May 30 - June 5, 2021, pp. 1810\u20131816. IEEE (2021). https:\/\/doi.org\/10.1109\/ICRA48506.2021.9561138. https:\/\/doi.org\/10.1109\/ICRA48506.2021.9561138","DOI":"10.1109\/ICRA48506.2021.9561138"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-030-59152-6_34","volume-title":"Automated Technology for Verification and Analysis","author":"D Ni\u010dkovi\u0107","year":"2020","unstructured":"Ni\u010dkovi\u0107, D., Yamaguchi, T.: RTAMT: online robustness monitors from STL. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 564\u2013571. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_34"},{"issue":"2\u20133","key":"1_CR36","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/S0019-9958(61)80020-X","volume":"4","author":"MP Sch\u00fctzenberger","year":"1961","unstructured":"Sch\u00fctzenberger, M.P.: On the definition of a family of automata. Inf. Control 4(2\u20133), 245\u2013270 (1961). https:\/\/doi.org\/10.1016\/S0019-9958(61)80020-X","journal-title":"Inf. Control"},{"issue":"10","key":"1_CR37","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"LS Shapley","year":"1953","unstructured":"Shapley, L.S.: Stochastic games. Proc. Natl. Acad. Sci. 39(10), 1095\u20131100 (1953)","journal-title":"Proc. Natl. Acad. Sci."},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M De Wulf","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17\u201330. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_5"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75387-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,25]],"date-time":"2024-10-25T08:05:50Z","timestamp":1729843550000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75387-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,26]]},"ISBN":["9783031753862","9783031753879"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75387-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,26]]},"assertion":[{"value":"26 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}