 |
 |
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)2007Generic Trace Semantics via CoinductionArticle
Authors: Ichiro Hasuo 
; Bart Jacobs ; Ana Sokolova 0000-0002-8300-4650##NULL##0000-0002-8384-3438Ichiro 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."
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
Funding:
- Source : OpenAIRE Graph
- Concurrent Programming with Threading by Appointment; Code: P 18913
Bibliographic References
70 Documents citing this article
- 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, arXiv (Cornell University), Graded Monads and Behavioural Equivalence Games, 2022, Haifa Israel, 10.1145/3531130.3533374, https://arxiv.org/abs/2203.15467.
- Florian Frank;Stefan Milius;Henning Urbat, arXiv (Cornell University), Coalgebraic Semantics for Nominal Automata, pp. 45-66, 2022, 10.1007/978-3-031-10736-8_3, http://arxiv.org/abs/2202.06546.
- Harsh Beohar;Barbara König;Sebastian Küpper;Christina Mika-Michalski, Lecture notes in computer science, Predicate and Relation Liftings for Coalgebras with Side Effects: An Application in Coalgebraic Modal Logic, pp. 1-22, 2022, 10.1007/978-3-031-10736-8_1.
- Niels F. W. Voorneveld, Lecture notes in computer science, Runners for Interleaving Algebraic Effects, pp. 407-424, 2022, 10.1007/978-3-031-17715-6_26.
- 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, https://arxiv.org/abs/2010.10510.
- Chase Ford;Stefan Milius;Lutz Schroder, arXiv (Cornell University), Behavioural Preorders via Graded Monads, 2021, Rome, Italy, 10.1109/lics52264.2021.9470517, https://arxiv.org/abs/2011.14339.
- Filippo Bonchi;Alessio Santamaria, Lecture notes in computer science, Combining Semilattices and Semimodules, pp. 102-123, 2021, 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.
- Swaraj Dash;Sam Staton, 2021, A Monad for Probabilistic Point Processes, arXiv (Cornell University), 333, pp. 19-32, 10.4204/eptcs.333.2.
- Stelios Tsampas;Andreas Nuyts;Dominique Devriese;Frank Piessens, A Categorical Approach to Secure Compilation, pp. 155-179, 2020, 10.1007/978-3-030-57201-3_9, https://hal.inria.fr/hal-03232345.
- Andreas Lochbihler;S. Reza Sefidgar;David Basin;Ueli Maurer, 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), Formalizing Constructive Cryptography using CryptHOL, 2019, Hoboken, NJ, USA, 10.1109/csf.2019.00018.
- Filippo Bonchi;Ana Sokolova;Valeria Vignudelli, The Theory of Traces for Systems with Nondeterminism and Probability, 2019, Vancouver, BC, Canada, 10.1109/lics.2019.8785673, https://hal.archives-ouvertes.fr/hal-02187093.
- Thorsten Wissmann;Jérémy Dubut;Shin-Ya Katsumata;Ichiro Hasuo, Lecture notes in computer science, Path Category for Free, pp. 523-540, 2019, 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, Steps and Traces, pp. 122-143, 2018, 10.1007/978-3-030-00389-0_8, https://hal.inria.fr/hal-02044644.
- Fredrik Dahlqvist;Louis Parlant;Alexandra Silva, UCL Discovery (University College London), Layer by Layer – Combining Monads, pp. 153-172, 2018, 10.1007/978-3-030-02508-3_9, https://discovery.ucl.ac.uk/id/eprint/10061790/.
- 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, Categorical Büchi and Parity Conditions via Alternating Fixed Points of Functors, pp. 214-234, 2018, 10.1007/978-3-030-00389-0_12, https://hal.inria.fr/hal-02044648.
- 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, arXiv (Cornell University), Categorical liveness checking by corecursive algebras, 59, pp. 1-12, 2017, Reykjavik, Iceland, 10.1109/lics.2017.8005151, https://arxiv.org/abs/1704.04872.
- Ichiro Hasuo;Naohiko Hoshino, 2016, Semantics of higher-order quantum computation via geometry of interaction, arXiv (Cornell University), 168, 2, pp. 404-469, 10.1016/j.apal.2016.10.010, https://arxiv.org/abs/1605.05079.
- Ichiro Hasuo;Shunsuke Shimizu;Corina Cîrstea, 2016, Lattice-theoretic progress measures and coalgebraic model checking, ePrints Soton (University of Southampton), 51, 1, pp. 718-732, 10.1145/2914770.2837673, https://eprints.soton.ac.uk/386126/1/POPL_accepted.pdf.
- Ichiro Hasuo;Shunsuke Shimizu;Corina Cîrstea, ePrints Soton (University of Southampton), Lattice-theoretic progress measures and coalgebraic model checking, 2016, St. Petersburg FL USA, 10.1145/2837614.2837673, https://eprints.soton.ac.uk/386126/1/POPL_accepted.pdf.
- Natsuki Urabe;Ichiro Hasuo, 2016, Quantitative simulations by matrices, Information and Computation, 252, pp. 110-137, 10.1016/j.ic.2016.03.007, https://doi.org/10.1016/j.ic.2016.03.007.
- Alexander Kurz;Jiří Velebil, 2015, Relation lifting, a survey, Journal of Logical and Algebraic Methods in Programming, 85, 4, pp. 475-499, 10.1016/j.jlamp.2015.08.002, https://doi.org/10.1016/j.jlamp.2015.08.002.
- Alexander Kurz;Stefan Milius;Dirk Pattinson;Lutz Schröder, arXiv (Cornell University), Simplified Coalgebraic Trace Equivalence, pp. 75-90, 2015, 10.1007/978-3-319-15545-6_8, https://arxiv.org/abs/1410.2463.
- Bartek Klin;Jurriaan Rot, Lecture notes in computer science, Coalgebraic Trace Semantics via Forgetful Logics, pp. 151-166, 2015, 10.1007/978-3-662-46678-0_10, https://doi.org/10.1007/978-3-662-46678-0_10.
- Daniel Murta;José Nuno Oliveira, 2015, A study of risk-aware program transformation, Science of Computer Programming, 110, pp. 51-77, 10.1016/j.scico.2015.04.008, https://doi.org/10.1016/j.scico.2015.04.008.
- 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.
- 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, https://doi.org/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, Journal of Logical and Algebraic Methods in Programming, 85, 4, pp. 449-474, 10.1016/j.jlamp.2015.11.007, https://doi.org/10.1016/j.jlamp.2015.11.007.
- 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, https://arxiv.org/abs/1411.0090.
- Bart Jacobs;Alexandra Silva, CiteSeer X (The Pennsylvania State University), Initial Algebras of Terms with Binding and Algebraic Structure, pp. 211-234, 2014, 10.1007/978-3-642-54789-8_12, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.822.8321.
- 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, arXiv (Cornell University), 158, pp. 29-38, 10.4204/eptcs.158.3.
- José N. Oliveira, Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT), Preparing Relational Algebra for “Just Good Enough” Hardware, pp. 119-138, 2014, 10.1007/978-3-319-06251-8_8, http://repositorio.inesctec.pt/handle/123456789/6653.
- Marcello M. Bonsangue;Jurriaan Rot;Davide Ancona;Frank S. de Boer;Jan J. M. M. Rutten, Lecture notes in computer science, A Coalgebraic Foundation for Coinductive Union Types, pp. 62-73, 2014, 10.1007/978-3-662-43951-7_6.
- Natsuki Urabe;Ichiro Hasuo, Lecture notes in computer science, Generic Forward and Backward Simulations III: Quantitative Simulations by Matrices, pp. 451-466, 2014, 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, arXiv (Cornell University), Coalgebraic Weak Bisimulation from Recursive Equations over Monads, pp. 196-207, 2014, 10.1007/978-3-662-43951-7_17, http://arxiv.org/abs/1404.1215.
- 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, CiteSeer X (The Pennsylvania State University), A Coalgebraic View of ε-Transitions, pp. 267-281, 2013, 10.1007/978-3-642-40206-7_20, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.718.7520.
- Corina Cirstea, 2013, From Branching to Linear Time, Coalgebraically, arXiv (Cornell University), 126, pp. 11-27, 10.4204/eptcs.126.2.
- Faris Abou-Saleh;Dirk Pattinson, Lecture notes in computer science, Comodels and Effects in Mathematical Operational Semantics, pp. 129-144, 2013, 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 28th Annual ACM/IEEE Symposium on Logic in Computer Science, A Relatively Complete Generic Hoare Logic for Order-Enriched Effects, 2, pp. 273-282, 2013, New Orleans, LA, USA, 10.1109/lics.2013.33.
- Bart Jacobs;Alexandra Silva;Ana Sokolova, Lecture notes in computer science, Trace Semantics via Determinization, pp. 109-129, 2012, 10.1007/978-3-642-32784-1_7, https://doi.org/10.1007/978-3-642-32784-1_7.
- Filippo Bonchi;Marcello Bonsangue;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, Lecture notes in computer science, Relational Presheaves as Labelled Transition Systems, pp. 40-50, 2012, 10.1007/978-3-642-32784-1_3, https://doi.org/10.1007/978-3-642-32784-1_3.
- 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, Cambridge University Press eBooks, An introduction to (co)algebra and (co)induction, pp. 38-99, 2011, 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, https://doi.org/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, https://doi.org/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, https://doi.org/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, Lecture notes in computer science, The Microcosm Principle and Compositionality of GSOS-Based Component Calculi, pp. 222-236, 2011, 10.1007/978-3-642-22944-2_16.
- Ichiro Hasuo;Naohiko Hoshino, arXiv (Cornell University), Semantics of Higher-Order Quantum Computation via Geometry of Interaction, pp. 237-246, 2011, Toronto, ON, Canada, 10.1109/lics.2011.26, https://arxiv.org/abs/1605.05079.
- Keiko Nakata, 2011, Resumption-based big-step and small-step interpreters for While with interactive I/O, arXiv (Cornell University), 66, pp. 226-235, 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, Lecture notes in computer science, Generic Forward and Backward Simulations II: Probabilistic Simulation, pp. 447-461, 2010, 10.1007/978-3-642-15375-4_31.
- Ichiro Hasuo;Yoshinobu Kawabe;Hideki Sakurada, 2010, Probabilistic anonymity via coalgebraic simulations, Kyoto University Research Information Repository (Kyoto University), 411, 22-24, pp. 2239-2259, 10.1016/j.tcs.2010.01.031, https://hdl.handle.net/2433/128862.
- Keiko Nakata;Tarmo Uustalu, Lecture notes in computer science, A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While, pp. 488-506, 2010, 10.1007/978-3-642-11957-6_26, https://doi.org/10.1007/978-3-642-11957-6_26.
- Bart Jacobs;Ana Sokolova, Radboud Repository (Radboud University), Traces, Executions and Schedulers, Coalgebraically, pp. 206-220, 2009, 10.1007/978-3-642-03741-2_15, https://repository.ubn.ru.nl//bitstream/handle/2066/75653/75653.pdf.
- Keiko Nakata;Tarmo Uustalu, Lecture notes in computer science, Trace-Based Coinductive Operational Semantics for While, pp. 375-390, 2009, 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, Springer eBooks, The Microcosm Principle and Concurrency in Coalgebra, pp. 246-260, 2008, 10.1007/978-3-540-78499-9_18.
Share and export
Consultation statistics
This page has been seen 1782 times.
This article's PDF has been downloaded 565 times.