{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T19:15:24Z","timestamp":1648926924736},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"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":[[2015,5]]},"abstract":"<jats:p>What reasoning rules can be used for the deduction of bisimulation formulas in coalgebraic specifications is problematic because those rules used in algebraic specifications possibly cannot be applied to bisimulation formulas. Although some categorical bisimulation proof methods for coalgebras have been proposed, they are not based on specification languages of coalgebras so that they cannot be used as reasoning rules. In this paper, a specification language based on paths of polynomial functors is proposed to specify polynomial coalgebras. Paths of polynomial functors give detailed observations and transitions on the state space of coalgebras so that the techniques used in transition system specifications can be applied to such a path-based language. In particular, because bisimulations can be characterized by paths, the notions of progressions, respectful functions and faithful contexts can be defined based on paths, and then bisimulation up-to proof techniques, including bisimulation up-to bisimilarities and up-to contexts for transition systems can be transformed into reasoning rules in the language. Several examples illustrate how to reason syntactically about bisimulations in the language by using the rules induced by the bisimulation proof techniques.<\/jats:p>","DOI":"10.1017\/s0960129513000030","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T11:41:28Z","timestamp":1415619688000},"page":"765-804","source":"Crossref","is-referenced-by-count":0,"title":["Bisimulation proof methods in a path-based specification language for polynomial coalgebras"],"prefix":"10.1017","volume":"25","author":[{"given":"XIAO-CONG","family":"ZHOU","sequence":"first","affiliation":[]},{"given":"YONG-JI","family":"LI","sequence":"additional","affiliation":[]},{"given":"WEN-JUN","family":"LI","sequence":"additional","affiliation":[]},{"given":"HAI-YAN","family":"QIAO","sequence":"additional","affiliation":[]},{"given":"ZHONG-MEI","family":"SHU","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129513000030_ref13","unstructured":"Jacobs B. (1999) The temporal logic of coalgebras via Galois algebras, Technical Report CSI-R9906, Computer Science Institution, University of Nijmegen."},{"key":"S0960129513000030_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00125-0"},{"key":"S0960129513000030_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.04.023"},{"key":"S0960129513000030_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.015"},{"key":"S0960129513000030_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.04.024"},{"key":"S0960129513000030_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.06.007"},{"key":"S0960129513000030_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80265-8"},{"key":"S0960129513000030_ref6","unstructured":"C\u00eerstea C. (2000) Integrating Observations and Computations in the Specification of State-based, Dynamical Systems, Ph.D. thesis, University of Oxford."},{"key":"S0960129513000030_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00042-6"},{"key":"S0960129513000030_ref17","unstructured":"Jacobs B. (2005) Introduction to Coalgebra: Towards Mathematics of States and Observations. Book Draft, Available at http:\/\/www.cs.ru.nl\/~bart."},{"key":"S0960129513000030_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.022"},{"key":"S0960129513000030_ref10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2005.11.041","article-title":"A modal proof theory for final polynomial coalgebras","volume":"360","author":"Goldblatt","year":"2006","journal-title":"Theoretical Computer Science"},{"key":"S0960129513000030_ref8","first-page":"149","volume-title":"Advances in Modal Logic","author":"Goldblatt","year":"2003"},{"key":"S0960129513000030_ref15","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2001108"},{"key":"S0960129513000030_ref29","first-page":"1","article-title":"Elements of stream calculus (an extensive exercise in coinduction)","volume":"45","author":"Rutten","year":"2001","journal-title":"Elsevier Electronic Notes in Theoretical Computer Science"},{"key":"S0960129513000030_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00201-9"},{"key":"S0960129513000030_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003900"},{"key":"S0960129513000030_ref3","first-page":"49","volume-title":"Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science","author":"Bonsangue","year":"2009"},{"key":"S0960129513000030_ref27","first-page":"175","article-title":"The coalgebraic class specification language CCSL","volume":"7","author":"Rothe","year":"2001","journal-title":"Journal of Universal Computer Science"},{"key":"S0960129513000030_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00038-1"},{"key":"S0960129513000030_ref26","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/S0304-3975(00)00128-6","article-title":"From modal logic to terminal coalgebras","volume":"260","author":"R\u00f6\u00dfiger","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"S0960129513000030_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"S0960129513000030_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47797-7_7"},{"key":"S0960129513000030_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516510"},{"key":"S0960129513000030_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_17"},{"key":"S0960129513000030_ref2","unstructured":"Bonsangue M. , Rutten J. and Silva A. (2007) Regular expressions for polynomial coalgebras. Technical Report SEN-E0703, Centrum voor Wiskunde en Informatica (CWI)."},{"key":"S0960129513000030_ref19","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:10)2008"},{"key":"S0960129513000030_ref32","volume-title":"The pi-Calculus: A Theory of Mobile Processes","author":"Sangiorgi","year":"2001"},{"key":"S0960129513000030_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80348-2"},{"key":"S0960129513000030_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80907-1"},{"key":"S0960129513000030_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0960129513000030_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00061-1"},{"key":"S0960129513000030_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80268-3"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000030","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T01:19:44Z","timestamp":1555809584000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000030\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["S0960129513000030"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000030","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}