{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,22]],"date-time":"2024-08-22T13:26:13Z","timestamp":1724333173105},"reference-count":44,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2015,12,9]],"date-time":"2015-12-09T00:00:00Z","timestamp":1449619200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2017,10]]},"abstract":"We present a systematic study of bisimulation-up-to techniques for coalgebras. This enhances the bisimulation proof method for a large class of state based systems, including labelled transition systems but also stream systems and weighted automata. Our approach allows for compositional reasoning about the soundness of enhancements. Applications include the soundness of bisimulation up to bisimilarity, up to equivalence and up to congruence. All in all, this gives a powerful and modular framework for simplified coinductive proofs of equivalence.<\/jats:p>","DOI":"10.1017\/s0960129515000523","type":"journal-article","created":{"date-parts":[[2015,12,9]],"date-time":"2015-12-09T17:24:53Z","timestamp":1449681893000},"page":"1236-1264","source":"Crossref","is-referenced-by-count":8,"title":["Enhanced coalgebraic bisimulation"],"prefix":"10.1017","volume":"27","author":[{"given":"JURRIAAN","family":"ROT","sequence":"first","affiliation":[]},{"given":"FILIPPO","family":"BONCHI","sequence":"additional","affiliation":[]},{"given":"MARCELLO","family":"BONSANGUE","sequence":"additional","affiliation":[]},{"given":"DAMIEN","family":"POUS","sequence":"additional","affiliation":[]},{"given":"JAN","family":"RUTTEN","sequence":"additional","affiliation":[]},{"given":"ALEXANDRA","family":"SILVA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,12,9]]},"reference":[{"key":"S0960129515000523_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"S0960129515000523_ref38","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"S0960129515000523_ref23","first-page":"230","article-title":"Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads","volume":"33","author":"Lenisa","year":"2000","journal-title":"ENTCS"},{"key":"S0960129515000523_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00895-2"},{"key":"S0960129515000523_ref19","article-title":"A linear algorithm for testing equivalence of finite automata","volume":"114","author":"Hopcroft","year":"1971","journal-title":"Technical Report"},{"key":"S0960129515000523_ref34","first-page":"252","article-title":"Relators and metric bisimulations","volume":"11","author":"Rutten","year":"1998","journal-title":"ENTCS"},{"key":"S0960129515000523_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017309"},{"key":"S0960129515000523_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.06.007"},{"key":"S0960129515000523_ref41","doi-asserted-by":"crossref","first-page":"189","DOI":"10.3233\/FI-1980-3208","article-title":"General theory of relational automata","volume":"3","author":"Trnkov\u00e1","year":"1980","journal-title":"Fundamenta Informaticae"},{"key":"S0960129515000523_ref40","article-title":"Relating coalgebraic notions of bisimulation","volume":"7","author":"Staton","year":"2011","journal-title":"LMCS"},{"key":"S0960129515000523_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-73235-5"},{"key":"S0960129515000523_ref12","volume-title":"Regular Algebra and Finite Machines","author":"Conway","year":"1971"},{"key":"S0960129515000523_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_3"},{"key":"S0960129515000523_ref11","first-page":"184","volume-title":"Lecture Notes in Computer Science","author":"Buchholz","year":"2001"},{"key":"S0960129515000523_ref4","unstructured":"Bartels F. (2004). On Generalised Coinduction and Probabilistic Specification Formats. Ph.D. thesis, CWI, Amsterdam."},{"key":"S0960129515000523_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.03.023"},{"key":"S0960129515000523_ref15","volume-title":"LUATCS 99","author":"Gumm","year":"1999"},{"key":"S0960129515000523_ref3","first-page":"529","article-title":"A duality between infinitary varieties and algebraic theories","volume":"41","author":"Ad\u00e1mek","year":"2000","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"key":"S0960129515000523_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35843-2_32"},{"key":"S0960129515000523_ref39","volume-title":"An introduction to Bisimulation and Coinduction","author":"Sangiorgi","year":"2012"},{"key":"S0960129515000523_ref22","first-page":"2","article-title":"From set-theoretic coinduction to coalgebraic coinduction: Some results, some problems","volume":"19","author":"Lenisa","year":"1999","journal-title":"ENTCS"},{"key":"S0960129515000523_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_17"},{"key":"S0960129515000523_ref18","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"S0960129515000523_ref8","first-page":"20","volume-title":"CSL-LICS 2014","author":"Bonchi","year":"2014"},{"key":"S0960129515000523_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482830-9\/50021-7"},{"key":"S0960129515000523_ref26","first-page":"150","volume-title":"Lecture Notes in Computer Science","volume":"7399","author":"Marti","year":"2012"},{"key":"S0960129515000523_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0018361"},{"key":"S0960129515000523_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"S0960129515000523_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_9"},{"key":"S0960129515000523_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200876"},{"key":"S0960129515000523_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80346-9"},{"key":"S0960129515000523_ref42","doi-asserted-by":"crossref","unstructured":"Turi D. and Plotkin G. (1997). Towards a mathematical operational semantics. In: LICS, IEEE Computer Society, 280\u2013291.","DOI":"10.1109\/LICS.1997.614955"},{"key":"S0960129515000523_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_19"},{"key":"S0960129515000523_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"S0960129515000523_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22944-2_25"},{"key":"S0960129515000523_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-6264-0"},{"key":"S0960129515000523_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80908-3"},{"key":"S0960129515000523_ref31","first-page":"233","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pous","year":"2012"},{"key":"S0960129515000523_ref9","first-page":"457","volume-title":"POPL","author":"Bonchi","year":"2013"},{"key":"S0960129515000523_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.12.002"},{"key":"S0960129515000523_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37064-9_42"},{"key":"S0960129515000523_ref13","first-page":"354","volume-title":"LNCS","author":"Endrullis","year":"2013"},{"key":"S0960129515000523_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0960129515000523_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04164-8_7"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129515000523","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,28]],"date-time":"2022-05-28T20:25:54Z","timestamp":1653769554000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129515000523\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,9]]},"references-count":44,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["S0960129515000523"],"URL":"https:\/\/doi.org\/10.1017\/s0960129515000523","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,9]]}}}