Generic Trace Semantics via Coinduction

Ichiro Hasuo; Bart Jacobs; Ana Sokolova

doi:10.2168/LMCS-3(4:11)2007

Ichiro Hasuo ; Bart Jacobs ; Ana Sokolova - Generic Trace Semantics via Coinduction

lmcs:864 - Logical Methods in Computer Science, November 19, 2007, Volume 3, Issue 4 - https://doi.org/10.2168/LMCS-3(4:11)2007

Generic Trace Semantics via CoinductionArticle

Authors: Ichiro Hasuo ; Bart Jacobs ; Ana Sokolova

Trace semantics has been defined for various kinds of state-based systems, notably with different forms of branching such as non-determinism vs.
probability. In this paper we claim to identify one underlying mathematical structure behind these "trace semantics," namely coinduction in a Kleisli category. This claim is based on our technical result that, under a suitably order-enriched setting, a final coalgebra in a Kleisli category is given by an initial algebra in the category Sets. Formerly the theory of coalgebras has been employed mostly in Sets where coinduction yields a finer process semantics of bisimilarity. Therefore this paper extends the application field of coalgebras, providing a new instance of the principle "process semantics via coinduction."

Comment: To appear in Logical Methods in Computer Science. 36 pages

https://doi.org/10.2168/LMCS-3(4:11)2007

Source: arXiv.org:0710.2505

Volume: Volume 3, Issue 4

Published on: November 19, 2007

Imported on: July 21, 2007

Keywords: Computer Science - Logic in Computer Science, F.3.1, F.3.2, G.3

Licence: arXiv.org - Assumed non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Concurrent Programming with Threading by Appointment; Code: P 18913

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

78 Documents citing this article

Kazuki Watanabe;Sebastian Junges;Jurriaan Rot;Ichiro Hasuo, 2025, A Unifying Approach to Product Constructions for Quantitative Temporal Inference, Proceedings of the ACM on Programming Languages, 9, OOPSLA1, pp. 1575-1603, 10.1145/3720501, https://doi.org/10.1145/3720501.

Sergey Goncharov;Pouya Partow;Stelios Tsampas, 2025, Big Steps in Higher-Order Mathematical Operational Semantics, Proceedings of the ACM on Programming Languages, 9, ICFP, pp. 1007-1035, 10.1145/3747540, https://doi.org/10.1145/3747540.

Jonas Forster;Lutz Schröder;Paul Wild;Harsh Beohar;Sebastian Gurke;Karla Messing, 2024, Graded Semantics and Graded Logics for Eilenberg-Moore Coalgebras, SPIRE - Sciences Po Institutional REpository, pp. 114-134, 10.1007/978-3-031-66438-0_6, https://inria.hal.science/hal-05000832.

Wojciech Różowski;Alexandra Silva, 2024, A Completeness Theorem for Probabilistic Regular Expressions, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 1-14, 10.1145/3661814.3662084.

Jules Jacobs;Thorsten Wißmann, 2023, Fast Coalgebraic Bisimilarity Minimization, Proceedings of the ACM on Programming Languages, 7, POPL, pp. 1514-1541, 10.1145/3571245, https://doi.org/10.1145/3571245.

Chase Ford;Stefan Milius;Lutz Schröder;Harsh Beohar;Barbara König, 2022, Graded Monads and Behavioural Equivalence Games, Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 1-13, 10.1145/3531130.3533374.

Florian Frank;Stefan Milius;Henning Urbat, 2022, Coalgebraic Semantics for Nominal Automata, Lecture notes in computer science, pp. 45-66, 10.1007/978-3-031-10736-8_3.

Harsh Beohar;Barbara König;Sebastian Küpper;Christina Mika-Michalski, 2022, Predicate and Relation Liftings for Coalgebras with Side Effects: An Application in Coalgebraic Modal Logic, Lecture notes in computer science, pp. 1-22, 10.1007/978-3-031-10736-8_1.

Niels F. W. Voorneveld, 2022, Runners for Interleaving Algebraic Effects, Lecture notes in computer science, pp. 407-424, 10.1007/978-3-031-17715-6_26.

Schmid, Todd;Różowski, Wojciech;Rot, Jurriaan;Silva, Alexandra, 2022, Processes Parametrised by an Algebraic Theory, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.icalp.2022.132, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.132.

Ana Neri;Rui Soares Barbosa;Jose N. Oliveira, 2021, Compiling Quantamorphisms for the IBM Q Experience, arXiv (Cornell University), 48, 11, pp. 4339-4356, 10.1109/tse.2021.3117515, http://arxiv.org/abs/2010.10510.

Chase Ford;Stefan Milius;Lutz Schroder, 2021, Behavioural Preorders via Graded Monads, arXiv (Cornell University), 10.1109/lics52264.2021.9470517, http://arxiv.org/abs/2011.14339.

Filippo Bonchi;Alessio Santamaria, 2021, Combining Semilattices and Semimodules, Lecture notes in computer science, pp. 102-123, 10.1007/978-3-030-71995-1_6, https://doi.org/10.1007/978-3-030-71995-1_6.

Jurriaan Rot;Bart Jacobs;Paul Blain Levy, 2021, Steps and traces, Journal of Logic and Computation, 31, 6, pp. 1482-1525, 10.1093/logcom/exab050, https://doi.org/10.1093/logcom/exab050.

Kori, Mayuko;Hasuo, Ichiro;Katsumata, Shin-ya, 2021, Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.concur.2021.21, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.21.

Swaraj Dash;Sam Staton, 2021, A Monad for Probabilistic Point Processes, Electronic Proceedings in Theoretical Computer Science, 333, pp. 19-32, 10.4204/eptcs.333.2, https://doi.org/10.4204/eptcs.333.2.

Stelios Tsampas;Andreas Nuyts;Dominique Devriese;Frank Piessens, 2020, A Categorical Approach to Secure Compilation, arXiv (Cornell University), pp. 155-179, 10.1007/978-3-030-57201-3_9, http://arxiv.org/abs/2004.03557.

Tsampas, Stelios;Williams, Christian;Nuyts, Andreas;Devriese, Dominique;Piessens, Frank, 2020, Abstract Congruence Criteria for Weak Bisimilarity, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.mfcs.2021.88, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.88.

Andreas Lochbihler;S. Reza Sefidgar;David Basin;Ueli Maurer, 2019, Formalizing Constructive Cryptography using CryptHOL, 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), pp. 152-15214, 10.1109/csf.2019.00018.

Filippo Bonchi;Ana Sokolova;Valeria Vignudelli, 2019, The Theory of Traces for Systems with Nondeterminism and Probability, CINECA IRIS Institutial research information system (University of Pisa), pp. 1-14, 10.1109/lics.2019.8785673.

Thorsten Wißmann;Jérémy Dubut;Shin-ya Katsumata;Ichiro Hasuo, 2019, Path Category for Free, Lecture notes in computer science, pp. 523-540, 10.1007/978-3-030-17127-8_30, https://doi.org/10.1007/978-3-030-17127-8_30.

Bart Jacobs;Paul Levy;Jurriaan Rot, 2018, Steps and Traces, pp. 122-143, 10.1007/978-3-030-00389-0_8, https://inria.hal.science/hal-02044644.

Fredrik Dahlqvist;Louis Parlant;Alexandra Silva, 2018, Layer by Layer – Combining Monads, arXiv (Cornell University), pp. 153-172, 10.1007/978-3-030-02508-3_9, http://arxiv.org/abs/1712.01113.

Nathan Bowler;Paul Blain Levy;Gordon Plotkin, 2018, Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies, Electronic Notes in Theoretical Computer Science, 341, pp. 23-44, 10.1016/j.entcs.2018.11.003, https://doi.org/10.1016/j.entcs.2018.11.003.

Natsuki Urabe;Ichiro Hasuo, 2018, Categorical Büchi and Parity Conditions via Alternating Fixed Points of Functors, SPIRE - Sciences Po Institutional REpository, pp. 214-234, 10.1007/978-3-030-00389-0_12, https://inria.hal.science/hal-02044648.

Paolo Baldan;Filippo Bonchi;Henning Kerstan;Barbara König, 2018, Coalgebraic Behavioral Metrics, Logical Methods in Computer Science, Volume 14, Issue 3, 10.23638/lmcs-14(3:20)2018, https://doi.org/10.23638/lmcs-14(3:20)2018.

ICHIRO HASUO;TOSHIKI KATAOKA;KENTA CHO, 2017, Coinductive predicates and final sequences in a fibration, Mathematical Structures in Computer Science, 28, 4, pp. 562-611, 10.1017/s0960129517000056, https://doi.org/10.1017/s0960129517000056.

Ichiro Hasuo, 2017, Metamathematics for Systems Design, New Generation Computing, 35, 3, pp. 271-305, 10.1007/s00354-017-0023-1, https://doi.org/10.1007/s00354-017-0023-1.

Jean-Paul Mavoungou, 2017, Extensional quotient coalgebras, Acta Universitatis Sapientiae Mathematica, 9, 2, pp. 303-323, 10.1515/ausm-2017-0023, https://doi.org/10.1515/ausm-2017-0023.

Natsuki Urabe;Masaki Hara;Ichiro Hasuo, 2017, Categorical liveness checking by corecursive algebras, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1-12, 10.1109/lics.2017.8005151.

Ichiro Hasuo;Naohiko Hoshino, 2016, Semantics of higher-order quantum computation via geometry of interaction, Annals of Pure and Applied Logic, 168, 2, pp. 404-469, 10.1016/j.apal.2016.10.010.

Ichiro Hasuo;Shunsuke Shimizu;Corina Cîrstea, 2016, Lattice-theoretic progress measures and coalgebraic model checking, ePrints Soton (University of Southampton), pp. 718-732, 10.1145/2837614.2837673.

Ichiro Hasuo;Shunsuke Shimizu;Corina Cîrstea, 2016, Lattice-theoretic progress measures and coalgebraic model checking, ACM SIGPLAN Notices, 51, 1, pp. 718-732, 10.1145/2914770.2837673.

Natsuki Urabe;Ichiro Hasuo, 2016, Quantitative simulations by matrices, arXiv (Cornell University), 252, pp. 110-137, 10.1016/j.ic.2016.03.007, http://arxiv.org/abs/1810.09146.

Alexander Kurz;Jiří Velebil, 2015, Relation lifting, a survey, Leicester Research Archive (University of Leicester), 85, 4, pp. 475-499, 10.1016/j.jlamp.2015.08.002, http://www.sciencedirect.com/science/article/pii/S2352220815000802.

Alexander Kurz;Stefan Milius;Dirk Pattinson;Lutz Schröder, 2015, Simplified Coalgebraic Trace Equivalence, arXiv (Cornell University), pp. 75-90, 10.1007/978-3-319-15545-6_8, http://arxiv.org/abs/1410.2463.

Bartek Klin;Jurriaan Rot, 2015, Coalgebraic Trace Semantics via Forgetful Logics, Lecture notes in computer science, pp. 151-166, 10.1007/978-3-662-46678-0_10.

DUSKO PAVLOVIC;BERTFRIED FAUSER, 2015, Smooth coalgebra: testing vector analysis, Mathematical Structures in Computer Science, 27, 7, pp. 1195-1235, 10.1017/s0960129515000511, https://doi.org/10.1017/s0960129515000511.

Daniel Murta;José Nuno Oliveira, 2015, A study of risk-aware program transformation, Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT), 110, pp. 51-77, 10.1016/j.scico.2015.04.008, http://repositorio.inesctec.pt/handle/123456789/6598.

Ichiro Hasuo, 2015, Generic weakest precondition semantics from monads enriched with order, Theoretical Computer Science, 604, pp. 2-29, 10.1016/j.tcs.2015.03.047.

José Nuno Oliveira;Victor Cacciari Miraldo, 2015, “Keep definition, change category” — A practical approach to state-based system calculi, Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT), 85, 4, pp. 449-474, 10.1016/j.jlamp.2015.11.007, http://repositorio.inesctec.pt/handle/123456789/6542.

Tomasz Brengos;Marino Miculan;Marco Peressotti, 2015, Behavioural equivalences for coalgebras with unobservable moves, arXiv (Cornell University), 84, 6, pp. 826-852, 10.1016/j.jlamp.2015.09.002, http://arxiv.org/abs/1411.0090.

Bart Jacobs;Alexandra Silva, 2014, Initial Algebras of Terms with Binding and Algebraic Structure, Lecture notes in computer science, pp. 211-234, 10.1007/978-3-642-54789-8_12.

F. BONCHI;M. BONSANGUE;G. CALTAIS;J. RUTTEN;A. SILVA, 2014, A coalgebraic view on decorated traces, Mathematical Structures in Computer Science, 26, 7, pp. 1234-1268, 10.1017/s0960129514000449, https://doi.org/10.1017/s0960129514000449.

Frank Roumen, 2014, Coalgebraic Quantum Computation, Electronic Proceedings in Theoretical Computer Science, 158, pp. 29-38, 10.4204/eptcs.158.3, https://doi.org/10.4204/eptcs.158.3.

José N. Oliveira, 2014, Preparing Relational Algebra for “Just Good Enough” Hardware, Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT), pp. 119-138, 10.1007/978-3-319-06251-8_8, http://repositorio.inesctec.pt/handle/123456789/6653.

Marcello Bonsangue;Jurriaan Rot;Davide Ancona;Frank de Boer;Jan Rutten, 2014, A Coalgebraic Foundation for Coinductive Union Types, Lecture notes in computer science, pp. 62-73, 10.1007/978-3-662-43951-7_6.

Natsuki Urabe;Ichiro Hasuo, 2014, Generic Forward and Backward Simulations III: Quantitative Simulations by Matrices, Lecture notes in computer science, pp. 451-466, 10.1007/978-3-662-44584-6_31.

Paweł Sobociński, 2014, Relational presheaves, change of base and weak simulation, Journal of Computer and System Sciences, 81, 5, pp. 901-910, 10.1016/j.jcss.2014.12.007.

Sergey Goncharov;Dirk Pattinson, 2014, Coalgebraic Weak Bisimulation from Recursive Equations over Monads, Lecture notes in computer science, pp. 196-207, 10.1007/978-3-662-43951-7_17.

Tetsuya Sato, 2014, Identifying All Preorders on the Subdistribution Monad, Electronic Notes in Theoretical Computer Science, 308, pp. 309-327, 10.1016/j.entcs.2014.10.017, https://doi.org/10.1016/j.entcs.2014.10.017.

Alexandra Silva;Bram Westerbaan, 2013, A Coalgebraic View of ε-Transitions, Lecture notes in computer science, pp. 267-281, 10.1007/978-3-642-40206-7_20.

Corina Cirstea, 2013, From Branching to Linear Time, Coalgebraically, Electronic Proceedings in Theoretical Computer Science, 126, pp. 11-27, 10.4204/eptcs.126.2, https://doi.org/10.4204/eptcs.126.2.

Faris Abou-Saleh;Dirk Pattinson, 2013, Comodels and Effects in Mathematical Operational Semantics, Lecture notes in computer science, pp. 129-144, 10.1007/978-3-642-37075-5_9, https://doi.org/10.1007/978-3-642-37075-5_9.

Henning Kerstan;Barbara König, 2013, Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems, Logical Methods in Computer Science, Volume 9, Issue 4, 10.2168/lmcs-9(4:16)2013, https://doi.org/10.2168/lmcs-9(4:16)2013.

Maciej Piróg;Jeremy Gibbons, 2013, Monads for Behaviour, Electronic Notes in Theoretical Computer Science, 298, pp. 309-324, 10.1016/j.entcs.2013.09.019, https://doi.org/10.1016/j.entcs.2013.09.019.

Marcello M. Bonsangue;Stefan Milius;Alexandra Silva, 2013, Sound and Complete Axiomatizations of Coalgebraic Language Equivalence, arXiv (Cornell University), 14, 1, pp. 1-52, 10.1145/2422085.2422092, http://arxiv.org/abs/1104.2803.

Sergey Goncharov;Lutz Schroder, 2013, A Relatively Complete Generic Hoare Logic for Order-Enriched Effects, University of Birmingham Research Portal (University of Birmingham), pp. 273-282, 10.1109/lics.2013.33.

Bart Jacobs;Alexandra Silva;Ana Sokolova, 2012, Trace Semantics via Determinization, Lecture notes in computer science, pp. 109-129, 10.1007/978-3-642-32784-1_7, https://doi.org/10.1007/978-3-642-32784-1_7.

Filippo Bonchi;Marcello Bonsangue;Georgiana Caltais;Jan Rutten;Alexandra Silva, 2012, Final Semantics for Decorated Traces, Electronic Notes in Theoretical Computer Science, 286, pp. 73-86, 10.1016/j.entcs.2012.08.006, https://doi.org/10.1016/j.entcs.2012.08.006.

Paweł Sobociński, 2012, Relational Presheaves as Labelled Transition Systems, pp. 40-50, 10.1007/978-3-642-32784-1_3, https://inria.hal.science/hal-01539889.

Alexandra Silva;Ana Sokolova, 2011, Sound and Complete Axiomatization of Trace Semantics for Probabilistic Systems, Electronic Notes in Theoretical Computer Science, 276, pp. 291-311, 10.1016/j.entcs.2011.09.027, https://doi.org/10.1016/j.entcs.2011.09.027.

Bart Jacobs;Jan Rutten, 2011, An introduction to (co)algebra and (co)induction, Cambridge University Press eBooks, pp. 38-99, 10.1017/cbo9780511792588.003.

Bartek Klin, 2011, Bialgebras for structural operational semantics: An introduction, Theoretical Computer Science, 412, 38, pp. 5043-5069, 10.1016/j.tcs.2011.03.023.

Clemens Kupke;Dirk Pattinson, 2011, Coalgebraic semantics of modal logics: An overview, Theoretical Computer Science, 412, 38, pp. 5070-5094, 10.1016/j.tcs.2011.04.023.

Corina Cîrstea, 2011, Maximal traces and path-based coalgebraic temporal logics, Theoretical Computer Science, 412, 38, pp. 5025-5042, 10.1016/j.tcs.2011.04.025.

Faris Abou-Saleh;Dirk Pattinson, 2011, Towards Effects in Mathematical Operational Semantics, Electronic Notes in Theoretical Computer Science, 276, pp. 81-104, 10.1016/j.entcs.2011.09.016, https://doi.org/10.1016/j.entcs.2011.09.016.

Ichiro Hasuo, 2011, The Microcosm Principle and Compositionality of GSOS-Based Component Calculi, Lecture notes in computer science, pp. 222-236, 10.1007/978-3-642-22944-2_16.

Ichiro Hasuo;Naohiko Hoshino, 2011, Semantics of Higher-Order Quantum Computation via Geometry of Interaction, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp. 237-246, 10.1109/lics.2011.26.

Keiko Nakata, 2011, Resumption-based big-step and small-step interpreters for While with interactive I/O, Electronic Proceedings in Theoretical Computer Science, 66, pp. 226-235, 10.4204/eptcs.66.12, https://doi.org/10.4204/eptcs.66.12.

Corina Cîrstea, 2010, Generic Infinite Traces and Path-Based Coalgebraic Temporal Logics, Electronic Notes in Theoretical Computer Science, 264, 2, pp. 83-103, 10.1016/j.entcs.2010.07.015, https://doi.org/10.1016/j.entcs.2010.07.015.

Ichiro Hasuo, 2010, Generic Forward and Backward Simulations II: Probabilistic Simulation, Lecture notes in computer science, pp. 447-461, 10.1007/978-3-642-15375-4_31.

Ichiro Hasuo;Yoshinobu Kawabe;Hideki Sakurada, 2010, Probabilistic anonymity via coalgebraic simulations, Theoretical Computer Science, 411, 22-24, pp. 2239-2259, 10.1016/j.tcs.2010.01.031.

Keiko Nakata;Tarmo Uustalu, 2010, A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While, Lecture notes in computer science, pp. 488-506, 10.1007/978-3-642-11957-6_26, https://doi.org/10.1007/978-3-642-11957-6_26.

Bart Jacobs;Ana Sokolova, 2009, Traces, Executions and Schedulers, Coalgebraically, Lecture notes in computer science, pp. 206-220, 10.1007/978-3-642-03741-2_15.

Keiko Nakata;Tarmo Uustalu, 2009, Trace-Based Coinductive Operational Semantics for While, Lecture notes in computer science, pp. 375-390, 10.1007/978-3-642-03359-9_26.

Eric Badouel;Maurice Tchoupé Tchendji, 2008, Merging Hierarchically-Structured Documents in Workflow Systems, Electronic Notes in Theoretical Computer Science, 203, 5, pp. 3-24, 10.1016/j.entcs.2008.05.017, https://doi.org/10.1016/j.entcs.2008.05.017.

Ichiro Hasuo;Bart Jacobs;Ana Sokolova, 2008, The Microcosm Principle and Concurrency in Coalgebra, Lecture notes in computer science, pp. 246-260, 10.1007/978-3-540-78499-9_18, https://doi.org/10.1007/978-3-540-78499-9_18.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3811 times.

This article's PDF has been downloaded 942 times.