{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T06:18:22Z","timestamp":1784873902167,"version":"3.55.0"},"reference-count":45,"publisher":"Oxford University Press (OUP)","issue":"6","license":[{"start":{"date-parts":[[2021,8,24]],"date-time":"2021-08-24T00:00:00Z","timestamp":1629763200000},"content-version":"vor","delay-in-days":1,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["320571"],"award-info":[{"award-number":["320571"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,9,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>In the theory of coalgebras, trace semantics can be defined in various distinct ways, including through algebraic logics, the Kleisli category of a monad or its Eilenberg\u2013Moore category. This paper elaborates two new unifying ideas: (i) coalgebraic,draftrules trace semantics is naturally presented in terms of corecursive algebras, and (ii) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof and allows to derive conditions under which some of them coincide.<\/jats:p>","DOI":"10.1093\/logcom\/exab050","type":"journal-article","created":{"date-parts":[[2021,7,14]],"date-time":"2021-07-14T19:10:25Z","timestamp":1626289825000},"page":"1482-1525","source":"Crossref","is-referenced-by-count":7,"title":["Steps and traces"],"prefix":"10.1093","volume":"31","author":[{"given":"Jurriaan","family":"Rot","sequence":"first","affiliation":[{"name":"Institute for Computing and Information Sciences, Radboud Universiteit, Nijmegen 6525 EC, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[{"name":"Institute for Computing and Information Sciences, Radboud Universiteit, Nijmegen 6525 EC, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul Blain","family":"Levy","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, Birmingham B15 2TT, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"286","published-online":{"date-parts":[[2021,8,23]]},"reference":[{"key":"2021092001212755700_ref1","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1017\/S0960129502003900","article-title":"Generalised coinduction","volume":"13","author":"Bartels","year":"2003","journal-title":"Mathematical Structures in Computer Science"},{"key":"2021092001212755700_ref2","first-page":"23:1","article-title":"The power of convex algebras","volume-title":"CONCUR","author":"Bonchi","year":"2017"},{"key":"2021092001212755700_ref3","first-page":"455","article-title":"Duality for logics of transition systems","volume-title":"FoSSaCS","author":"Bonsangue","year":"2005"},{"key":"2021092001212755700_ref4","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/2422085.2422092","article-title":"Sound and complete axiomatizations of coalgebraic language equivalence","volume":"14","author":"Bonsangue","year":"2013","journal-title":"ACM Transactions on Computational Logic"},{"key":"2021092001212755700_ref5","first-page":"23","article-title":"Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies","volume-title":"MFPS","author":"Bowler","year":"2018"},{"key":"2021092001212755700_ref6","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1016\/j.ic.2005.08.005","article-title":"Recursive coalgebras from comonads","volume":"204","author":"Capretta","year":"2006","journal-title":"Information and Computation"},{"key":"2021092001212755700_ref7","first-page":"84","article-title":"A study of general structured corecursion","volume-title":"SBMF","author":"Capretta","year":"2009"},{"key":"2021092001212755700_ref8","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.entcs.2014.10.007","article-title":"On a categorical framework for coalgebraic modal logic","volume":"308","author":"Chen","year":"2014","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2021092001212755700_ref9","article-title":"A coalgebraic approach to quantitative linear time logics","author":"C\u00eerstea","year":"2016"},{"key":"2021092001212755700_ref10","first-page":"36:1","article-title":"Graded monads and graded logics for the linear time\u2014branching time spectrum","volume-title":"CONCUR","author":"Dorsch","year":"2019"},{"key":"2021092001212755700_ref11","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1016\/S1571-0661(05)80305-6","article-title":"Coalgebra-to-algebra morphisms","volume":"29","author":"Eppendahl","year":"1999","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2021092001212755700_ref12","volume-title":"Proofs and Types","author":"Girard","year":"1988"},{"key":"2021092001212755700_ref13","first-page":"158","article-title":"Trace semantics via generic observations","volume-title":"CALCO","author":"Goncharov","year":"2013"},{"key":"2021092001212755700_ref14","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/j.apal.2005.05.022","article-title":"Programming interfaces and basic topology","volume":"137","author":"Hancock","year":"05 2009","journal-title":"Annals of Pure and Applied Logic"},{"key":"2021092001212755700_ref15","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.tcs.2015.03.047","article-title":"Generic weakest precondition semantics from monads enriched with order","volume":"604","author":"Hasuo","year":"2015","journal-title":"Theoretical Computer Science"},{"key":"2021092001212755700_ref16","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-3(4:11)2007","article-title":"Generic trace semantics via coinduction","volume":"3","author":"Hasuo","year":"2007","journal-title":"Logical Methods in Computer Science"},{"key":"2021092001212755700_ref17","doi-asserted-by":"crossref","DOI":"10.1145\/2933575.2935319","article-title":"Healthiness from duality","volume-title":"LICS","author":"Hino","year":"2016"},{"key":"2021092001212755700_ref18","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1145\/2676726.2676989","article-title":"Conjugate hylomorphisms\u2014or: the mother of all structured recursion schemes","volume-title":"POPL","author":"Hinze","year":"2015"},{"key":"2021092001212755700_ref19","first-page":"375","article-title":"A bialgebraic review of deterministic automata, regular expressions and languages","volume-title":"Essays Dedicated to Joseph A. Goguen","author":"Jacobs","year":"2006"},{"key":"2021092001212755700_ref20","article-title":"A recipe for state and effect triangles","volume":"13","author":"Jacobs","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"2021092001212755700_ref21","first-page":"122","article-title":"Steps and traces","volume-title":"CMCS","author":"Jacobs","year":"2018"},{"key":"2021092001212755700_ref22","doi-asserted-by":"crossref","first-page":"859","DOI":"10.1016\/j.jcss.2014.12.005","article-title":"Trace semantics via determinization","volume":"81","author":"Jacobs","year":"2015","journal-title":"Journal of Computer and System Sciences"},{"key":"2021092001212755700_ref23","doi-asserted-by":"crossref","first-page":"1041","DOI":"10.1093\/logcom\/exn093","article-title":"Exemplaric expressivity of modal logics","volume":"20","author":"Jacobs","year":"2010","journal-title":"Journal of Logic and Computation"},{"key":"2021092001212755700_ref24","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1218563.1218577","article-title":"Open bisimulation for aspects","volume-title":"AOSD","author":"Jagadeesan","year":"2007"},{"key":"2021092001212755700_ref25","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1112\/blms\/7.3.294","article-title":"Adjoint lifting theorems for categories of algebras","volume":"7","author":"Johnstone","year":"1975","journal-title":"Bulletin of the London Mathematical Society"},{"key":"2021092001212755700_ref26","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0063101","article-title":"Review of the elements of 2-categories","volume-title":"Category Seminar: Proceedings Sydney Category Seminar 1972\/1973","author":"Kelly","year":"1974"},{"key":"2021092001212755700_ref27","first-page":"168","article-title":"Lifting adjunctions to coalgebras to (re)discover automata constructions","volume-title":"CMCS","author":"Kerstan","year":"2014"},{"key":"2021092001212755700_ref28","doi-asserted-by":"crossref","DOI":"10.1016\/j.entcs.2007.02.034","article-title":"Coalgebraic modal logic beyond sets","volume-title":"MFPS","author":"Klin","year":"2007"},{"key":"2021092001212755700_ref29","article-title":"Coalgebraic trace semantics via forgetful logics","volume-title":"Logical Methods in Computer Science","author":"Klin","year":"2016"},{"key":"2021092001212755700_ref30","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/j.entcs.2018.11.013","article-title":"Iterated covariant powerset is not a monad","volume":"341","author":"Klin","year":"2018","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2021092001212755700_ref31","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-319-15545-6_8","article-title":"Simplified coalgebraic trace equivalence","volume-title":"Software, Services, and Systems","author":"Kurz","year":"2015"},{"key":"2021092001212755700_ref32","first-page":"667","article-title":"A fully abstract trace semantics for general references","volume-title":"ICALP","author":"Laird","year":"2007"},{"key":"2021092001212755700_ref33","first-page":"283","article-title":"Typed normal form bisimulation","volume-title":"CSL","author":"Lassen","year":"2007"},{"key":"2021092001212755700_ref34","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511525896","volume-title":"Higher Operads, Higher Categories","author":"Leinster","year":"2004"},{"key":"2021092001212755700_ref35","first-page":"221","article-title":"Final coalgebras from corecursive algebras","volume-title":"CALCO","author":"Levy","year":"2015"},{"key":"2021092001212755700_ref36","doi-asserted-by":"crossref","first-page":"64:1","DOI":"10.1145\/2603088.2603150","article-title":"Transition systems over games","volume-title":"CSL-LICS","author":"Levy","year":"2014"},{"key":"2021092001212755700_ref37","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2004.05.003","article-title":"Completely iterative algebras and completely iterative monads","volume":"196","author":"Milius","year":"2005","journal-title":"Information and Computation"},{"key":"2021092001212755700_ref38","first-page":"253","article-title":"Generic trace semantics and graded monads","volume-title":"CALCO","author":"Milius","year":"2015"},{"key":"2021092001212755700_ref39","first-page":"304","article-title":"Lifting theorems for Kleisli categories","volume-title":"MFPS","author":"Mulry","year":"1993"},{"key":"2021092001212755700_ref40","first-page":"308","article-title":"Testing semantics: connecting processes and process logics","volume-title":"AMAST","author":"Pavlovic","year":"2006"},{"key":"2021092001212755700_ref41","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","article-title":"A theory of communicating sequential processes","volume":"31","author":"Roscoe","year":"1984","journal-title":"Journal of the ACM"},{"key":"2021092001212755700_ref42","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.entcs.2016.09.042","article-title":"Coalgebraic minimization of automata by initiality and finality","volume":"325","author":"Rot","year":"2016","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2021092001212755700_ref43","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-9(1:9)2013","article-title":"Generalizing determinization from automata to coalgebras","volume":"9","author":"Silva","year":"2013","journal-title":"Logical Methods in Computer Science"},{"key":"2021092001212755700_ref44","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0022-4049(72)90019-9","article-title":"The formal theory of monads","author":"Street","year":"1972","journal-title":"Journal of Pure and Applied Algebra"},{"key":"2021092001212755700_ref45","first-page":"280","article-title":"Towards a mathematical operational semantics","volume-title":"LICS","author":"Turi","year":"1997"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/31\/6\/1482\/40407880\/exab050.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/31\/6\/1482\/40407880\/exab050.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,20]],"date-time":"2021-09-20T01:22:10Z","timestamp":1632100930000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/31\/6\/1482\/6355531"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,23]]},"references-count":45,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2021,8,23]]},"published-print":{"date-parts":[[2021,9,3]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exab050","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2021,9]]},"published":{"date-parts":[[2021,8,23]]}}}