Generic Trace Semantics via Coinduction

Abstract

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."

To appear in Logical Methods in Computer Science. 36 pages

Cited by in corpus (16)

• Sound and complete axiomatizations of coalgebraic language equivalence
• Behavioural equivalences for coalgebras with unobservable moves
• A Monad for Probabilistic Point Processes
• Quantitative Simulations by Matrices
• The Theory of Traces for Systems with Nondeterminism, Probability, and Termination
• From Branching to Linear Time, Coalgebraically
• Resumption-based big-step and small-step interpreters for While with interactive I/O
• Smooth coalgebra: testing vector analysis
• Behavioural equivalences for timed systems
• Coalgebras for Bisimulation of Weighted Automata over Semirings
• Coalgebraic Quantum Computation
• Combining Semilattices and Semimodules
• On Kleisli liftings and decorated trace semantics
• A coalgebraic take on regular and $\omega$-regular behaviours
• Stream processors and comodels
• Big Steps in Higher-Order Mathematical Operational Semantics