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."
Cite
@article{arxiv.0710.2505,
title = {Generic Trace Semantics via Coinduction},
author = {Ichiro Hasuo and Bart Jacobs and Ana Sokolova},
journal= {arXiv preprint arXiv:0710.2505},
year = {2015}
}
Comments
To appear in Logical Methods in Computer Science. 36 pages