{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:41:47Z","timestamp":1742928107669,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_21","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"438-455","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Convex Lattice Equation Systems"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Bacci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giovanni","family":"Bacci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias Claus","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"issue":"7","key":"21_CR1","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1016\/0169-7552(93)90048-9","volume":"25","author":"B Algayres","year":"1993","unstructured":"Algayres, B., Coelho, V., Doldi, L., Garavel, H., Lejeune, Y., Rodr\u00edguez, C.: VESAR: a pragmatic approach to formal specification and verification. Comput. Netw. ISDN Syst. 25(7), 779\u2013790 (1993)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-55253-7_1","volume-title":"ESOP \u201992","author":"HR Andersen","year":"1992","unstructured":"Andersen, H.R.: Model checking and Boolean graphs. In: Krieg-Br\u00fcckner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 1\u201319. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55253-7_1"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-319-25150-9_33","volume-title":"Theoretical Aspects of Computing - ICTAC 2015","author":"JR Andersen","year":"2015","unstructured":"Andersen, J.R., et al.: CAAL: concurrency workbench, Aalborg edition. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 573\u2013582. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_33"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-642-40313-2_9","volume-title":"Mathematical Foundations of Computer Science 2013","author":"G Bacci","year":"2013","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: Computing behavioral distances, compositionally. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 74\u201385. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40313-2_9"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-36742-7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Bacci","year":"2013","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On-the-fly exact computation of bisimilarity distances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 1\u201315. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_1"},{"key":"21_CR6","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: Complete axiomatization for the bisimilarity distance on Markov chains. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, Qu\u00e9bec City, Canada, 23\u201326 August 2016, volume 59 of LIPIcs, pp. 21:1\u201321:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: Complete axiomatization for the total variation distance of Markov chains. In: Staton, S. (ed.) Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, 6\u20139 June 2018, volume 341 of Electronic Notes in Theoretical Computer Science, pp. 27\u201339. Elsevier (2018)","DOI":"10.1016\/j.entcs.2018.03.014"},{"key":"21_CR8","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R., Tang, Q., van Breugel, F.: Computing probabilistic bisimilarity distances for probabilistic automata. Log. Methods Comput. Sci. 17(1) (2021)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-56922-7_21","volume-title":"Computer Aided Verification","author":"K \u010cer\u0101ns","year":"1993","unstructured":"\u010cer\u0101ns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification\u2014Theory and tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253\u2013267. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_21"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-642-28729-9_29","volume-title":"Foundations of Software Science and Computational Structures","author":"D Chen","year":"2012","unstructured":"Chen, D., van Breugel, F., Worrell, J.: On the complexity of computing probabilistic bisimilarity. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 437\u2013451. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28729-9_29"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-52148-8_3","volume-title":"Automatic Verification Methods for Finite State Systems","author":"R Cleaveland","year":"1990","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 24\u201337. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_3"},{"key":"21_CR12","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pp. 51\u201372. DIMACS\/AMS (1990)"},{"issue":"2","key":"21_CR13","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203\u2013224 (1992)","journal-title":"Inf. Comput."},{"issue":"3","key":"21_CR14","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.tcs.2003.09.013","volume":"318","author":"J Desharnais","year":"2004","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323\u2013354 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), Saint-Malo, France, 14\u201317 September 2008, pp. 264\u2013273. IEEE Computer Society (2008)","DOI":"10.1109\/QEST.2008.42"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Easterbrook, S.M., Chechik, M.: A framework for multi-valued reasoning over inconsistent viewpoints. In: M\u00fcller, H.A., Harrold, M.J., Sch\u00e4fer, W. (eds.) Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, Toronto, Ontario, Canada, 12\u201319 May 2001, pp. 411\u2013420. IEEE Computer Society (2001)","DOI":"10.1109\/ICSE.2001.919114"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Fahrenberg, U., Thrane, C.R., Larsen, K.G.: Distances for weighted transition systems: games and properties. In: Massink, M., Norman, G. (eds.) Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages, QAPL 2011, Saarbr\u00fccken, Germany, 1\u20133 April 2011, volume 57 of EPTCS, pp. 134\u2013147 (2011)","DOI":"10.4204\/EPTCS.57.10"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-19835-9_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Garavel","year":"2011","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372\u2013387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_33"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-78499-9_23","volume-title":"Foundations of Software Science and Computational Structures","author":"J Goubault-Larrecq","year":"2008","unstructured":"Goubault-Larrecq, J.: Prevision domains and convex powercones. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 318\u2013333. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78499-9_23"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: From Boolean to quantitative notions of correctness. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17\u201323 January 2010, pp. 157\u2013158. ACM (2010)","DOI":"10.1145\/1706299.1706319"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11603009_18","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"TA Henzinger","year":"2005","unstructured":"Henzinger, T.A., Majumdar, R., Prabhu, V.S.: Quantifying similarities between timed systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 226\u2013241. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11603009_18"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11813040_1","volume-title":"FM 2006: Formal Methods","author":"TA Henzinger","year":"2006","unstructured":"Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 1\u201315. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_1"},{"key":"21_CR23","unstructured":"Juba, B.: On the hardness of simple stochastic games. Master\u2019s thesis, Carnegie Mellon University, Pittsburgh, PA, USA, May 2005"},{"issue":"2","key":"21_CR24","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1142\/S0129054110007192","volume":"21","author":"O Kupferman","year":"2010","unstructured":"Kupferman, O., Lustig, Y.: Latticed simulation relations and games. Int. J. Found. Comput. Sci. 21(2), 167\u2013189 (2010)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"28","key":"21_CR25","doi-asserted-by":"publisher","first-page":"3358","DOI":"10.1016\/j.tcs.2011.04.003","volume":"412","author":"KG Larsen","year":"2011","unstructured":"Larsen, K.G., Fahrenberg, U., Thrane, C.R.: Metrics for weighted transition systems: axiomatization and complexity. Theoret. Comput. Sci. 412(28), 3358\u20133369 (2011)","journal-title":"Theoret. Comput. Sci."},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-56496-9_4","volume-title":"Computer Aided Verification","author":"KG Larsen","year":"1993","unstructured":"Larsen, K.G.: Efficient local correctness checking. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 30\u201343. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56496-9_4"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, 11\u201313 January 1989, pp. 344\u2013352. ACM Press (1989)","DOI":"10.1145\/75277.75307"},{"issue":"4","key":"21_CR28","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1137\/1011093","volume":"11","author":"T Liggett","year":"1969","unstructured":"Liggett, T., Lippman, S.A.: Stochastic games with perfect information and time average payoff. SIAM Rev. 11(4), 604\u2013607 (1969)","journal-title":"SIAM Rev."},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BFb0055040","volume-title":"Automata, Languages and Programming","author":"X Liu","year":"1998","unstructured":"Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53\u201366. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055040"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Man, K.L.: $$\\upmu $$CRL: a computer science based approach for specification and verification of hardware circuits, vol. 01, pp. I-387\u2013I-390 (2008)","DOI":"10.1109\/SOCDC.2008.4815653"},{"key":"21_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/3-540-44618-4_26","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"M Mislove","year":"2000","unstructured":"Mislove, M.: Nondeterminism and probabilistic choice: obeying the laws. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 350\u2013365. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44618-4_26"},{"key":"21_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-030-29662-9_12","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Rosenmann","year":"2019","unstructured":"Rosenmann, A.: On the distance between timed automata. In: Andr\u00e9, \u00c9., Stoelinga, M. (eds.) FORMATS 2019. LNCS, vol. 11750, pp. 199\u2013215. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29662-9_12"},{"key":"21_CR33","unstructured":"Tang, Q., van Breugel, F.: Computing probabilistic bisimilarity distances via policy iteration. In: CONCUR, volume 59 of LIPIcs, pp. 22:1\u201322:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"issue":"2","key":"21_CR34","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"issue":"7","key":"21_CR35","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1016\/j.jlap.2010.07.010","volume":"79","author":"CR Thrane","year":"2010","unstructured":"Thrane, C.R., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. J. Log. Algebr. Methods Program. 79(7), 689\u2013703 (2010)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"21_CR36","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.01.002","volume":"222","author":"R Tix","year":"2009","unstructured":"Tix, R., Keimel, K., Plotkin, G.D.: Semantic domains for combining probability and non-determinism. Electron. Notes Theoret. Comput. Sci. 222, 3\u201399 (2009)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"issue":"1","key":"21_CR37","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1017\/S0960129505005074","volume":"16","author":"D Varacca","year":"2006","unstructured":"Varacca, D., Winskel, G.: Distributing probability over non-determinism. Math. Struct. Comput. Sci. 16(1), 87\u2013113 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"key":"21_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/BFb0039080","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"Y Wang","year":"1990","unstructured":"Wang, Y.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 502\u2013520. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039080"},{"key":"21_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-54233-7_136","volume-title":"Automata, Languages and Programming","author":"W Yi","year":"1991","unstructured":"Yi, W.: CCS + time = an interleaving model for real time systems. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 217\u2013228. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54233-7_136"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:55:29Z","timestamp":1728615329000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}