{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:56Z","timestamp":1775868536750,"version":"3.50.1"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,6,25]],"date-time":"2016-06-25T00:00:00Z","timestamp":1466812800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s00236-016-0271-4","type":"journal-article","created":{"date-parts":[[2016,6,26]],"date-time":"2016-06-26T11:45:33Z","timestamp":1466941533000},"page":"127-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["A general account of coinduction up-to"],"prefix":"10.1007","volume":"54","author":[{"given":"Filippo","family":"Bonchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniela","family":"Petri\u015fan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damien","family":"Pous","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,25]]},"reference":[{"key":"271_CR1","doi-asserted-by":"publisher","unstructured":"Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Handbook of Process Algebra, pp. 197\u2013292. Elsevier (2001). doi: 10.1016\/B978-044482830-9\/50021-7","DOI":"10.1016\/B978-044482830-9\/50021-7"},{"key":"271_CR2","doi-asserted-by":"publisher","unstructured":"Balan, A., Kurz, A.: Finitary functors: from set to preord and poset. In: CALCO, LNCS, vol. 6859, pp. 85\u201399. Springer (2011). doi: 10.1007\/978-3-642-22944-2_7","DOI":"10.1007\/978-3-642-22944-2_7"},{"key":"271_CR3","doi-asserted-by":"publisher","unstructured":"Balan, A., Kurz, A., Velebil, J.: Positive fragments of coalgebraic logics. In: CALCO, LNCS, vol. 8089, pp. 51\u201365. Springer (2013). doi: 10.1007\/978-3-642-40206-7_6","DOI":"10.1007\/978-3-642-40206-7_6"},{"issue":"2","key":"271_CR4","first-page":"321","volume":"13","author":"F Bartels","year":"2003","unstructured":"Bartels, F.: Generalised coinduction. MSCS 13(2), 321\u2013348 (2003)","journal-title":"MSCS"},{"issue":"1&2","key":"271_CR5","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0304-3975(94)00152-9","volume":"146","author":"B Bloom","year":"1995","unstructured":"Bloom, B.: Structural operational semantics for weak bisimulations. Theor. Comput. Sci. 146(1&2), 25\u201368 (1995). doi: 10.1016\/0304-3975(94)00152-9","journal-title":"Theor. Comput. Sci."},{"key":"271_CR6","doi-asserted-by":"publisher","unstructured":"Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can\u2019t be traced. In: POPL, pp. 229\u2013239. ACM (1988). doi: 10.1145\/73560.73580","DOI":"10.1145\/73560.73580"},{"key":"271_CR7","doi-asserted-by":"crossref","unstructured":"Bojanczyk, M., Klin, B., Lasota, S.: Automata with group actions. In: LICS, pp. 355\u2013364 (2011)","DOI":"10.1109\/LICS.2011.48"},{"key":"271_CR8","doi-asserted-by":"crossref","unstructured":"Bojanczyk, M., Klin, B., Lasota, S., Torunczyk, S.: Turing machines with atoms. In: LICS, pp. 183\u2013192 (2013)","DOI":"10.1109\/LICS.2013.24"},{"key":"271_CR9","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.ic.2011.12.002","volume":"211","author":"F Bonchi","year":"2012","unstructured":"Bonchi, F., Bonsangue, M., Boreale, M., Rutten, J., Silva, A.: A coalgebraic perspective on linear weighted automata. Inf. Comput. 211, 77\u2013105 (2012)","journal-title":"Inf. Comput."},{"key":"271_CR10","doi-asserted-by":"publisher","unstructured":"Bonchi, F., Petri\u015fan, D., Pous, D., Rot, J.: Coinduction up-to in a fibrational setting. In: CSL-LICS\u201914, Article 20, pp. 1\u20139. ACM (2014). doi: 10.1145\/2603088.2603149","DOI":"10.1145\/2603088.2603149"},{"key":"271_CR11","doi-asserted-by":"publisher","unstructured":"Bonchi, F., Petrisan, D., Pous, D., Rot, J.: Lax bialgebras and up-to techniques for weak bisimulations. In: 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, pp. 240\u2013253 (2015). doi: 10.4230\/LIPIcs.CONCUR.2015.240","DOI":"10.4230\/LIPIcs.CONCUR.2015.240"},{"key":"271_CR12","doi-asserted-by":"publisher","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: POPL, pp. 457\u2013468. ACM (2013). doi: 10.1145\/2429069.2429124","DOI":"10.1145\/2429069.2429124"},{"issue":"2","key":"271_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-11(2:14)2015","volume":"11","author":"T Brengos","year":"2015","unstructured":"Brengos, T.: Weak bisimulation for coalgebras over order enriched monads. Log. Methods Comput. Sci. 11(2), 1\u201344 (2015)","journal-title":"Log. Methods Comput. Sci."},{"issue":"6","key":"271_CR14","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1016\/j.jlamp.2015.09.002","volume":"84","author":"T Brengos","year":"2015","unstructured":"Brengos, T., Miculan, M., Peressotti, M.: Behavioural equivalences for coalgebras with unobservable moves. J. Log. Algebr. Methods Program. 84(6), 826\u2013852 (2015)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"4","key":"271_CR15","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964)","journal-title":"J. ACM"},{"key":"271_CR16","doi-asserted-by":"crossref","unstructured":"Caucal, D.: Graphes canoniques de graphes alg\u00e9briques. ITA 24, 339\u2013352 (1990). http:\/\/archive.numdam.org\/article\/ITA_1990__24_4_339_0.pdf","DOI":"10.1051\/ita\/1990240403391"},{"issue":"1","key":"271_CR17","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1093\/comjnl\/bxp004","volume":"54","author":"C C\u00eerstea","year":"2011","unstructured":"C\u00eerstea, C., Kurz, A., Pattinson, D., Schr\u00f6der, L., Venema, Y.: Modal logics are coalgebraic. Comput. J. 54(1), 31\u201341 (2011)","journal-title":"Comput. J."},{"key":"271_CR18","doi-asserted-by":"crossref","unstructured":"Dam, M.: Compositional proof systems for model checking infinite state processes. In: CONCUR, LNCS, vol. 962, pp. 12\u201326. Springer (1995)","DOI":"10.1007\/3-540-60218-6_2"},{"issue":"2","key":"271_CR19","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/j.ic.2007.12.005","volume":"207","author":"M Fiore","year":"2009","unstructured":"Fiore, M., Staton, S.: A congruence rule format for name-passing process calculi. Inf. Comput. 207(2), 209\u2013236 (2009)","journal-title":"Inf. Comput."},{"key":"271_CR20","unstructured":"Fiore, M., Staton, S.: Positive structural operational semantics and monotone distributive laws. In: CMCS, p.\u00a08 (2010)"},{"key":"271_CR21","doi-asserted-by":"crossref","unstructured":"Goncharov, S., Pattinson, D.: Coalgebraic weak bisimulation from recursive equations over monads. In: ICALP (2), Lecture Notes in Computer Science, vol. 8573, pp. 196\u2013207. Springer (2014)","DOI":"10.1007\/978-3-662-43951-7_17"},{"key":"271_CR22","doi-asserted-by":"crossref","unstructured":"Hasuo, I., Cho, K., Kataoka, T., Jacobs, B.: Coinductive predicates and final sequences in a fibration. In: MFPS (2013)","DOI":"10.1016\/j.entcs.2013.09.014"},{"key":"271_CR23","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1006\/inco.1998.2725","volume":"145","author":"C Hermida","year":"1997","unstructured":"Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145, 107\u2013152 (1997)","journal-title":"Inf. Comput."},{"key":"271_CR24","unstructured":"Hopcroft, J.E., Karp, R.M.: A Linear Algorithm for Testing Equivalence of Finite Automata. Tech. Rep. 114, Cornell Univ. (1971). http:\/\/techreports.library.cornell.edu:8081\/Dienst\/UI\/1.0\/Display\/cul.cs\/TR71-114"},{"issue":"1\u20132","key":"271_CR25","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/j.tcs.2004.07.022","volume":"327","author":"J Hughes","year":"2004","unstructured":"Hughes, J., Jacobs, B.: Simulations in coalgebra. TCS 327(1\u20132), 71\u2013108 (2004)","journal-title":"TCS"},{"key":"271_CR26","volume-title":"Categorical Logic and Type Theory","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)"},{"key":"271_CR27","unstructured":"Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations (2014). Draft"},{"key":"271_CR28","doi-asserted-by":"crossref","unstructured":"Klin, B.: Bialgebraic operational semantics and modal logic. In: LICS, pp. 336\u2013345. IEEE (2007)","DOI":"10.1109\/LICS.2007.13"},{"issue":"38","key":"271_CR29","doi-asserted-by":"crossref","first-page":"5043","DOI":"10.1016\/j.tcs.2011.03.023","volume":"412","author":"B Klin","year":"2011","unstructured":"Klin, B.: Bialgebras for structural operational semantics: an introduction. TCS 412(38), 5043\u20135069 (2011)","journal-title":"TCS"},{"key":"271_CR30","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. In: Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201991), Amsterdam, The Netherlands, July 15\u201318, 1991, pp. 214\u2013225 (1991). doi: 10.1109\/LICS.1991.151646","DOI":"10.1109\/LICS.1991.151646"},{"key":"271_CR31","first-page":"2","volume":"19","author":"M Lenisa","year":"1999","unstructured":"Lenisa, M.: From set-theoretic coinduction to coalgebraic coinduction: some results, some problems. ENTCS 19, 2\u201322 (1999)","journal-title":"ENTCS"},{"key":"271_CR32","first-page":"230","volume":"33","author":"M Lenisa","year":"2000","unstructured":"Lenisa, M., Power, J., Watanabe, H.: Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. ENTCS 33, 230\u2013260 (2000)","journal-title":"ENTCS"},{"issue":"1","key":"271_CR33","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/j.entcs.2006.06.007","volume":"164","author":"L Luo","year":"2006","unstructured":"Luo, L.: An effective coalgebraic bisimulation proof method. Electr. Notes Theor. Comput. Sci. 164(1), 105\u2013119 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"271_CR34","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)"},{"key":"271_CR35","doi-asserted-by":"crossref","unstructured":"Montanari, U., Pistore, M.: History-dependent automata: An introduction. In: SFM, LNCS, pp. 1\u201328. Springer (2005)","DOI":"10.1007\/11419822_1"},{"key":"271_CR36","doi-asserted-by":"publisher","unstructured":"Montanari, U., Sassone, V.: CCS dynamic bisimulation is progressing. In: MFCS, pp. 346\u2013356 (1991). doi: 10.1007\/3-540-54345-7_78","DOI":"10.1007\/3-540-54345-7_78"},{"key":"271_CR37","doi-asserted-by":"publisher","unstructured":"Parrow, J., Sj\u00f6din, P.: Multiway synchronization verified with coupled simulation. In: Cleaveland, R. (ed.) CONCUR \u201992, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings, Lecture Notes in Computer Science, vol. 630, pp. 518\u2013533. Springer (1992). doi: 10.1007\/BFb0084813","DOI":"10.1007\/BFb0084813"},{"key":"271_CR38","unstructured":"Petri\u015fan, D.: Investigations into Algebra and Topology Over Nominal Sets. Ph.D. Thesis, University of Leicester (2012)"},{"key":"271_CR39","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139084673","volume-title":"Nominal Sets","author":"AM Pitts","year":"2013","unstructured":"Pitts, A.M.: Nominal Sets. Cambridge University Press, Cambridge (2013)"},{"key":"271_CR40","doi-asserted-by":"publisher","unstructured":"Pous, D.: Complete lattices and up-to techniques. In: APLAS, LNCS, vol. 4807, pp. 351\u2013366. Springer (2007). doi: 10.1007\/978-3-540-76637-7_24","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"271_CR41","unstructured":"Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: Advanced Topics in Bisimulation and Coinduction, pp. 233\u2013289. Cambridge University Press (2012). http:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item6542021"},{"key":"271_CR42","unstructured":"Rot, J.: Enhanced Coinduction. Ph.D. Thesis, Leiden University (2015)"},{"key":"271_CR43","doi-asserted-by":"publisher","unstructured":"Rot, J., Bonchi, F., Bonsangue, M., Pous, D., Rutten, J., Silva, A.: Enhanced coalgebraic bisimulation. MSCS 1\u201329 (2016). doi: 10.1017\/S0960129515000523","DOI":"10.1017\/S0960129515000523"},{"issue":"1","key":"271_CR44","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. TCS 249(1), 3\u201380 (2000)","journal-title":"TCS"},{"key":"271_CR45","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1017\/S0960129598002527","volume":"8","author":"D Sangiorgi","year":"1998","unstructured":"Sangiorgi, D.: On the bisimulation proof method. MSCS 8, 447\u2013479 (1998). doi: 10.1017\/S0960129598002527","journal-title":"MSCS"},{"key":"271_CR46","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011). http:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item6542019\/","DOI":"10.1017\/CBO9780511777110"},{"key":"271_CR47","unstructured":"Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Generalizing the powerset construction, coalgebraically. In: FSTTCS, pp. 272\u2013283 (2010)"},{"key":"271_CR48","first-page":"287","volume":"60\u201361","author":"A Simpson","year":"2004","unstructured":"Simpson, A.: Sequent calculi for process verification: Hennessy\u2013Milner logic for an arbitrary GSOS. JLAP 60\u201361, 287\u2013322 (2004)","journal-title":"JLAP"},{"issue":"38","key":"271_CR49","doi-asserted-by":"crossref","first-page":"5095","DOI":"10.1016\/j.tcs.2011.05.008","volume":"412","author":"A Sokolova","year":"2011","unstructured":"Sokolova, A.: Probabilistic systems coalgebraically: a survey. Theor. Comput. Sci. 412(38), 5095\u20135110 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"271_CR50","first-page":"93","volume":"19","author":"A Sokolova","year":"2009","unstructured":"Sokolova, A., de Vink, E.P., Woracek, H.: Coalgebraic weak bisimulation for action-type systems. Sci. Ann. Comput. Sci. 19, 93\u2013144 (2009)","journal-title":"Sci. Ann. Comput. Sci."},{"key":"271_CR51","doi-asserted-by":"crossref","unstructured":"Staton, S.: Relating coalgebraic notions of bisimulation. Logic. Methods Comp. Sci. 7(1:13), 1\u201321 (2011)","DOI":"10.2168\/LMCS-7(1:13)2011"},{"key":"271_CR52","doi-asserted-by":"publisher","unstructured":"Street, R.: Fibrations and Yoneda\u2019s lemma in a 2-category. In: Kelly, G. (ed.) Category Seminar, Lecture Notes in Mathematics, vol. 420, pp. 104\u2013133. Springer, Berlin, Heidelberg (1974). doi: 10.1007\/BFb0063102","DOI":"10.1007\/BFb0063102"},{"key":"271_CR53","unstructured":"Thijs, A.M.: Simulation and Fixpoint Semantics. Ph.D. Thesis, Univ. of Groningen (1996)"},{"key":"271_CR54","doi-asserted-by":"crossref","unstructured":"Turi, D., Plotkin, G.D.: Towards a mathematical operational semantics. In: LICS, pp. 280\u2013291. IEEE (1997)","DOI":"10.1109\/LICS.1997.614955"},{"issue":"28","key":"271_CR55","doi-asserted-by":"publisher","first-page":"3283","DOI":"10.1016\/j.tcs.2011.02.036","volume":"412","author":"R Glabbeek van","year":"2011","unstructured":"van Glabbeek, R.: On cool congruence formats for weak bisimulations. Theor. Comput. Sci. 412(28), 3283\u20133302 (2011). doi: 10.1016\/j.tcs.2011.02.036 . (Festschrift in Honour of Jan Bergstra)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"271_CR56","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R Glabbeek van","year":"1996","unstructured":"van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996). doi: 10.1145\/233551.233556","journal-title":"J. ACM"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0271-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0271-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0271-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0271-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,10]],"date-time":"2019-09-10T06:44:20Z","timestamp":1568097860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0271-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,25]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["271"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0271-4","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,25]]}}}