A Coalgebraic Foundation for Linear Time Semantics

John Power, and Daniele Turi

In Proceedings of the Eighth Category Theory in Computer Science conference, CTCS '99, M. Hofmann, D. Pavlovic, and G. Rosolini editors, volume 29 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999.

• (226K) PDF
• (214K) Postscript

Abstract

We present a coalgebraic approach to trace equivalence semantics based on lifting behaviour endofunctors for deterministic action to Kleisli categories of monads for non-deterministic choice. In Set, this gives a category with ordinary transition systems as objects and with morphisms characterised in terms of a linear notion of bisimulation. The final object in this category is the canonical abstract model for trace equivalence and can be obtained by extending the final coalgebra of the deterministic action behaviour to the Kleisli category of the non-empty powerset monad. The corresponding final coalgebra semantics is fully abstract with respect to trace equivalence.

@inProceedings{PowerTuri99,
	author = {J. Power and D. Turi},
	title = {A coalgebraic foundation for linear time semantics},
	publisher = "Elsevier",
	year = {1999},
        volume = {29},
        booktitle = {Proc.\ 8$^{\rm th}$ CTCS Conf.},
        series = "Electronic Notes in Theoretical Computer Science",
        editor =  {M. Hofmann and D. Pavlovi\'{c} and G. Rosolini},
        source = {http://www.dcs.ed.ac.uk/home/dt/}
}