{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T04:04:29Z","timestamp":1746245069561,"version":"3.40.4"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906428","type":"print"},{"value":"9783031906435","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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>\n          <jats:p>Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize acceptance conditions of boolean <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-automata. Despite the theoretical advances in systems analysis through quantitative automata, the first comprehensive software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was developed only recently. QuAK implements algorithms for solving standard decision problems, e.g., emptiness and universality, as well as constructions for safety and liveness of quantitative automata. We present the architecture of QuAK, which reflects that all of these problems reduce to either checking inclusion between two quantitative automata or computing the highest value achievable by an automaton\u2014its so-called top value. We improve QuAK by extending these two algorithms with an option to return, alongside their results, an ultimately periodic word witnessing the algorithm\u2019s output, as well as implementing a new safety-liveness decomposition algorithm that can handle nondeterministic automata, making QuAK more informative and capable.<\/jats:p>","DOI":"10.1007\/978-3-031-90643-5_16","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T11:19:33Z","timestamp":1746184773000},"page":"303-312","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automating the Analysis of Quantitative Automata with QuAK"],"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. Ege","family":"Sara\u00e7","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","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","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"16_CR2","doi-asserted-by":"publisher","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","DOI":"10.1006\/INCO.1993.1025"},{"key":"16_CR3","doi-asserted-by":"publisher","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.) Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06605, pp. 254\u2013257. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"16_CR4","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, July 8-11, 2024. pp. 15:1\u201315:14. ACM (2024). https:\/\/doi.org\/10.1145\/3661814.3662090","DOI":"10.1145\/3661814.3662090"},{"key":"16_CR5","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":"16_CR6","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, September 18-23, 2023, Antwerp, Belgium. 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":"16_CR7","doi-asserted-by":"publisher","unstructured":"Boker, U., Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Safety and liveness of quantitative properties and automata. Log. Methods Comput. Sci. 21(2) (2025). https:\/\/doi.org\/10.46298\/lmcs-21(2:2)2025, https:\/\/lmcs.episciences.org\/13149. ISSN 1860-5974","DOI":"10.46298\/lmcs-21(2:2)2025"},{"key":"16_CR8","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, July 6-10, 2015. pp. 750\u2013761. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/LICS.2015.74","DOI":"10.1109\/LICS.2015.74"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) Computer Aided Verification, 11th International Conference, CAV \u201999, Trento, Italy, July 6-10, 1999, Proceedings. Lecture Notes in Computer Science, vol.\u00a01633, pp. 274\u2013287. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_25","DOI":"10.1007\/3-540-48683-6_25"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: QuAK - Quantitative Automata Kit (2024), maintained at https:\/\/github.com\/ista-vamos\/QuAK","DOI":"10.1007\/978-3-031-75387-9_1"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Quak: Quantitative automata kit (2024), https:\/\/arxiv.org\/abs\/2409.03569","DOI":"10.1007\/978-3-031-75387-9_1"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Doyen, L., Edelsbrunner, H., Henzinger, T.A., Rannou, P.: Mean-payoff automaton expressions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06269, pp. 269\u2013283. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_19","DOI":"10.1007\/978-3-642-15375-4_19"},{"key":"16_CR13","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":"16_CR14","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A., Otop, J.: Nested weighted automata. ACM Trans. Comput. Log. 18(4), 31:1\u201331:44 (2017). https:\/\/doi.org\/10.1145\/3152769","DOI":"10.1145\/3152769"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Chechik, M., Gurfinkel, A., Devereux, B.: chi-chek: A multi-valued model-checker. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02404, pp. 505\u2013509. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_41","DOI":"10.1007\/3-540-45657-0_41"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Degorre, A., Doyen, L., Gentilini, R., Raskin, J., Torunczyk, S.: Energy and mean-payoff games with imperfect information. In: Dawar, A., Veith, H. (eds.) Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06247, pp. 260\u2013274. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_22","DOI":"10.1007\/978-3-642-15205-4_22"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Dehnert, C., Junges, S., Katoen, J., Volk, M.: A storm is coming: A modern probabilistic model checker. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10427, pp. 592\u2013600. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31, https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Demaille, A., Duret-Lutz, A., Lombardy, S., Sakarovitch, J.: Implementation concepts in vaucanson 2. In: Konstantinidis, S. (ed.) Implementation and Application of Automata - 18th International Conference, CIAA 2013, Halifax, NS, Canada, July 16-19, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07982, pp. 122\u2013133. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39274-0_12","DOI":"10.1007\/978-3-642-39274-0_12"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Donz\u00e9, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P.B. (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06174, pp. 167\u2013170. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_17","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Doveri, K., Ganty, P., Mazzocchi, N.: Forq-based language inclusion formal testing. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 109\u2013129. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_6","DOI":"10.1007\/978-3-031-13188-2_6"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Fijalkow, N., Bertrand, N., Bouyer-Decitre, P., Brenguier, R., Carayol, A., Fearnley, J., Gimbert, H., Horn, F., Ibsen-Jensen, R., Markey, N., Monmege, B., Novotn\u00fd, P., Randour, M., Sankur, O., Schmitz, S., Serre, O., Skomra, M.: Games on graphs. CoRR abs\/2305.10546 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2305.10546, https:\/\/doi.org\/10.48550\/arXiv.2305.10546","DOI":"10.48550\/ARXIV.2305.10546"},{"key":"16_CR22","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, July 27-30, 1996. pp. 278\u2013292. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561342","DOI":"10.1109\/LICS.1996.561342"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Ho, P.: HYTECH: the cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems II, Proceedings of the Third International Workshop on Hybrid Systems, Ithaca, NY, USA, October 1994. Lecture Notes in Computer Science, vol.\u00a0999, pp. 265\u2013293. Springer (1994). https:\/\/doi.org\/10.1007\/3-540-60472-3_14","DOI":"10.1007\/3-540-60472-3_14"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Abstract monitors for quantitative specifications. In: Dang, T., Stolz, V. (eds.) Runtime Verification - 22nd International Conference, RV 2022, Tbilisi, Georgia, September 28-30, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13498, pp. 200\u2013220. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_11","DOI":"10.1007\/978-3-031-17196-3_11"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Mazzocchi, N., Sara\u00e7, N.E.: Quantitative safety and liveness. In: Kupferman, O., Sobocinski, P. (eds.) Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13992, pp. 349\u2013370. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30829-1_17","DOI":"10.1007\/978-3-031-30829-1_17"},{"key":"16_CR26","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"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Hunter, P., Pauly, A., P\u00e9rez, G.A., Raskin, J.: Mean-payoff games with partial observation. Theor. Comput. Sci. 735, 82\u2013110 (2018). https:\/\/doi.org\/10.1016\/J.TCS.2017.03.038, https:\/\/doi.org\/10.1016\/j.tcs.2017.03.038","DOI":"10.1016\/J.TCS.2017.03.038"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04349, pp. 199\u2013213. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_14","DOI":"10.1007\/978-3-540-69738-1_14"},{"key":"16_CR29","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J.T., Harder, U. (eds.) Computer Performance Evaluation, Modelling Techniques and Tools 12th International Conference, TOOLS 2002, London, UK, April 14-17, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02324, pp. 200\u2013204. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-46029-2_13","DOI":"10.1007\/3-540-46029-2_13"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1-2), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/S100090050010","DOI":"10.1007\/S100090050010"},{"key":"16_CR31","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":"16_CR32","doi-asserted-by":"publisher","unstructured":"Lombardy, S., Poss, R., R\u00e9gis-Gianas, Y., Sakarovitch, J.: Introducing VAUCANSON. In: Ibarra, O.H., Dang, Z. (eds.) Implementation and Application of Automata, 8th International Conference, CIAA 2003, Santa Barbara, California, USA, July 16-18, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02759, pp. 96\u2013107. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-45089-0_10","DOI":"10.1007\/3-540-45089-0_10"},{"key":"16_CR33","doi-asserted-by":"publisher","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a03253, pp. 152\u2013166. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"16_CR34","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, August 27-30, 2019, Amsterdam, the Netherlands. 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":"16_CR35","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, 19-27 August 2021. pp. 2819\u20132825. ijcai.org (2021). https:\/\/doi.org\/10.24963\/IJCAI.2021\/388","DOI":"10.24963\/IJCAI.2021\/388"},{"key":"16_CR36","doi-asserted-by":"publisher","unstructured":"Sch\u00fctzenberger, M.P.: On the definition of a family of automata. Inf. Control. 4(2-3), 245\u2013270 (1961). https:\/\/doi.org\/10.1016\/S0019-9958(61)80020-X","DOI":"10.1016\/S0019-9958(61)80020-X"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Yamaguchi, T., Hoxha, B., Nickovic, D.: RTAMT - runtime robustness monitors with application to CPS and robotics. Int. J. Softw. Tools Technol. Transf. 26(1), 79\u201399 (2024). https:\/\/doi.org\/10.1007\/S10009-023-00720-3, https:\/\/doi.org\/10.1007\/s10009-023-00720-3","DOI":"10.1007\/S10009-023-00720-3"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90643-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T11:19:36Z","timestamp":1746184776000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90643-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906428","9783031906435"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90643-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}