{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T20:38:22Z","timestamp":1759178302755,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662545768"},{"type":"electronic","value":"9783662545775"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54577-5_31","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T10:48:06Z","timestamp":1490870886000},"page":"535-552","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Up-To Techniques for Weighted Systems"],"prefix":"10.1007","author":[{"given":"Filippo","family":"Bonchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"K\u00fcpper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-12002-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158\u2013174. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-12002-2_14"},{"issue":"3","key":"31_CR2","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1016\/S0304-3975(02)00864-2","volume":"298","author":"L Aceto","year":"2003","unstructured":"Aceto, L., \u00c9sik, Z., Ing\u00f3lfsd\u00f3ttir, A.: Equational theories of tropical semirings. Theor. Comput. Sci. 298(3), 417\u2013469 (2003). Foundations of Software Science and Computation Structures","journal-title":"Theor. Comput. Sci."},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-642-24372-1_37","volume-title":"Automated Technology for Verification and Analysis","author":"S Almagor","year":"2011","unstructured":"Almagor, S., Boker, U., Kupferman, O.: What\u2019s decidable about weighted automata? In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 482\u2013491. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-24372-1_37"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/11753728_9","volume-title":"Computer Science \u2013 Theory and Applications","author":"M-P B\u00e9al","year":"2006","unstructured":"B\u00e9al, M.-P., Lombardy, S., Sakarovitch, J.: Conjugacy and equivalence of weighted automata and functional transducers. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 58\u201369. Springer, Heidelberg (2006). doi:10.1007\/11753728_9"},{"issue":"3","key":"31_CR5","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s00012-013-0247-y","volume":"70","author":"G Bezhanishvili","year":"2013","unstructured":"Bezhanishvili, G., Gabelaia, D., Jibladze, M.: Funayama\u2019s theorem revisited. Algebra Univers. 70(3), 271\u2013286 (2013)","journal-title":"Algebra Univers."},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.ic.2011.12.002","volume":"211","author":"F Bonchi","year":"2012","unstructured":"Bonchi, F., Bonsangue, M.M., Boreale, M., Rutten, J.J.M.M., Silva, A.: A coalgebraic perspective on linear weighted automata. Inf. Comput. 211, 77\u2013105 (2012)","journal-title":"Inf. Comput."},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Bonchi, F., K\u00f6nig, B., K\u00fcpper, S.: Up-to techniques for weighted systems (extended version) arXiv:1701.05001 (2017)","DOI":"10.1007\/978-3-662-54577-5_31"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Petrisan, D., Pous, D., Rot, J.: Coinduction up-to in a fibrational setting. In: Henzinger, T.A., Miller, D. (eds.) Proceedings of CSL-LICS 2014, pp. 20:1\u201320:9. ACM (2014)","DOI":"10.1145\/2603088.2603149"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of POPL 2013, pp. 457\u2013468. ACM (2013)","DOI":"10.1145\/2480359.2429124"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-04081-8_12","volume-title":"CONCUR 2009 - Concurrency Theory","author":"M Boreale","year":"2009","unstructured":"Boreale, M.: Weighted bisimulation in linear algebraic form. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 163\u2013177. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-04081-8_12"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-61511-3_107","volume-title":"Automated Deduction \u2014 Cade-13","author":"D Cyrluk","year":"1996","unstructured":"Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak\u2019s decision procedure for combinations of theories. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 463\u2013477. Springer, Heidelberg (1996). doi:10.1007\/3-540-61511-3_107"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Formal Models and Semantics, Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-12002-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Doyen","year":"2010","unstructured":"Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 2\u201322. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-12002-2_2"},{"key":"31_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BFb0023465","volume-title":"STACS 97","author":"S Gaubert","year":"1997","unstructured":"Gaubert, S., Plus, M.: Methods and applications of (max,+) linear algebra. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 261\u2013282. Springer, Heidelberg (1997). doi:10.1007\/BFb0023465"},{"key":"31_CR15","unstructured":"Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Technical report TR 114, Cornell University (1971)"},{"key":"31_CR16","unstructured":"K\u00f6nig, B., K\u00fcpper, S.: A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata. Soft Comput. 1\u201318 (2016). http:\/\/link.springer.com\/article\/10.1007\/s00500-016-2363-z"},{"issue":"3","key":"31_CR17","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1142\/S0218196794000063","volume":"4","author":"D Krob","year":"1994","unstructured":"Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Int. J. Algebra Comput. 4(3), 405\u2013425 (1994)","journal-title":"Int. J. Algebra Comput."},{"key":"31_CR18","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"key":"31_CR19","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"D Pous","year":"2011","unstructured":"Pous, D., Sangiorgi, D.: Enhancements of the coinductive proof method. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)"},{"key":"31_CR20","unstructured":"Rot, J., Bonchi, F., Bonsangue, M., Pous, D., Rutten, J., Silva, A.: Enhanced coalgebraic bisimulation. Math. Struct. Comput. Sci. 1\u201329 (2015). https:\/\/www.cambridge.org\/core\/journals\/mathematical-structures-in-computer-science\/article\/div-classtitleenhanced-coalgebraic-bisimulationdiv\/C588A590E7DB3A73F1C86487D0F8DE19"},{"issue":"2","key":"31_CR21","first-page":"361","volume":"8","author":"EW Stark","year":"2003","unstructured":"Stark, E.W.: On behaviour equivalence for probabilistic i\/o automata and its relationship to probabilistic bisimulation. J. Automata Lang. Comb. 8(2), 361\u2013395 (2003)","journal-title":"J. Automata Lang. Comb."},{"key":"31_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-662-44584-6_31","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"N Urabe","year":"2014","unstructured":"Urabe, N., Hasuo, I.: Generic forward and backward simulations III: quantitative simulations by matrices. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 451\u2013466. Springer, Heidelberg (2014). doi:10.1007\/978-3-662-44584-6_31"},{"key":"31_CR23","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 Wulf","year":"2006","unstructured":"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). doi:10.1007\/11817963_5"}],"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-662-54577-5_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:40:03Z","timestamp":1618972803000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54577-5_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545768","9783662545775"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54577-5_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","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":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}