Generic Trace Semantics via Coinduction
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 Kle...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2007-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/864/pdf |
| _version_ | 1797268756177616896 |
|---|---|
| author | Ichiro Hasuo Bart Jacobs Ana Sokolova |
| author_facet | Ichiro Hasuo Bart Jacobs Ana Sokolova |
| author_sort | Ichiro Hasuo |
| collection | DOAJ |
| description | 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." |
| first_indexed | 2024-04-25T01:37:32Z |
| format | Article |
| id | doaj.art-3f87bfa7ee57492eb7fb3b963a4768f8 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:32Z |
| publishDate | 2007-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-3f87bfa7ee57492eb7fb3b963a4768f82024-03-08T08:49:28ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742007-11-01Volume 3, Issue 410.2168/LMCS-3(4:11)2007864Generic Trace Semantics via CoinductionIchiro Hasuohttps://orcid.org/0000-0002-8300-4650Bart JacobsAna Sokolovahttps://orcid.org/0000-0002-8384-3438Trace 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."https://lmcs.episciences.org/864/pdfcomputer science - logic in computer sciencef.3.1f.3.2g.3 |
| spellingShingle | Ichiro Hasuo Bart Jacobs Ana Sokolova Generic Trace Semantics via Coinduction Logical Methods in Computer Science computer science - logic in computer science f.3.1 f.3.2 g.3 |
| title | Generic Trace Semantics via Coinduction |
| title_full | Generic Trace Semantics via Coinduction |
| title_fullStr | Generic Trace Semantics via Coinduction |
| title_full_unstemmed | Generic Trace Semantics via Coinduction |
| title_short | Generic Trace Semantics via Coinduction |
| title_sort | generic trace semantics via coinduction |
| topic | computer science - logic in computer science f.3.1 f.3.2 g.3 |
| url | https://lmcs.episciences.org/864/pdf |
| work_keys_str_mv | AT ichirohasuo generictracesemanticsviacoinduction AT bartjacobs generictracesemanticsviacoinduction AT anasokolova generictracesemanticsviacoinduction |