Abstract
The analysis of concurrent and reactive systems is based to a large degree on various notions of process equivalence, ranging, on the so-called linear-time/branching-time spectrum, from fine-grained equivalences such as strong bisimilarity to coarse-grained ones such as trace equivalence. The theory of concurrent systems at large has benefited from developments in coalgebra, which has enabled uniform definitions and results that provide a common umbrella for seemingly disparate system types including non-deterministic, weighted, probabilistic, and game-based systems. In particular, there has been some success in identifying a generic coalgebraic theory of bisimulation that matches known definitions in many concrete cases. The situation is currently somewhat less settled regarding trace equivalence. A number of coalgebraic approaches to trace equivalence have been proposed, none of which however cover all cases of interest; notably, all these approaches depend on explicit termination, which is not always imposed in standard systems, e.g. labelled transition systems. Here, we discuss a joint generalization of these approaches based on embedding functors modelling various aspects of the system, such as transition and braching, into a global monad; this approach appears to cover all cases considered previously and some additional ones, notably standard and probabilistic labelled transition systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aceto, L., Ingólfsdóttir, A., Larsen, K., Srba, J.: Reactive systems: modelling, specification and verification. Cambridge University Press (2007)
Aczel, P.: Non-Well-Founded Sets. CSLI, Stanford (1988)
Adámek, J.: Free algebras and automata realizations in the language of categories. Comment. Math. Univ. Carolin. 15, 589–602 (1974)
Adámek, J., Rosický, J.: Locally presentable and accessible categories. Cambridge University Press (1994)
Barr, M.: Coequalizers and free triples. Math. Zeitschr. 116, 307–322 (1970)
Bonchi, F., Bonsangue, M., Caltais, G., Rutten, J., Silva, A.: Final semantics for decorated traces. In: Mathematical Foundations of Programming Semantics, MFPS 2012. ENTCS, vol. 286, pp. 73–86. Elsevier (2012)
Bonsangue, M.M., Milius, S., Silva, A.: Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log. 14(1:7) (2013)
Cîrstea, C.: A coalgebraic approach to linear-time logics. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol. 8412, pp. 426–440. Springer, Heidelberg (2014)
Giarratana, V., Gimona, F., Montanari, U.: Observability concepts in abstract data type specifications. In: Mazurkiewicz, A. (ed.) MFCS 1976. LNCS, vol. 45, pp. 576–587. Springer, Heidelberg (1976)
Goguen, J., Thatcher, J.: Initial algebra semantics. In: Switching and Automata Theory, SWAT (FOCS) 1974, pp. 63–77. IEEE Computer Society (1974)
Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3 (2007)
Hennicker, R., Wirsing, M.: Observational Specification: A Birkhoff Theorem. In: Workshop on Theory and Applications of Abstract Data Types, WADT 1985, Selected Papers, pp. 119–135. Springer (1985)
Hoare, A.: Communicating sequential processes. Prentice-Hall (1985)
Jacobs, B., Silva, A., Sokolova, A.: Trace semantics via determinization. In: Pattinson, D., Schröder, L. (eds.) CMCS 2012. LNCS, vol. 7399, pp. 109–129. Springer, Heidelberg (2012)
Kelly, M.: A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bull. Austral. Math. Soc. 22, 1–83 (1980)
Kissig, C., Kurz, A.: Generic trace logics. arXiv preprint 1103.3239 (2011)
Power, J., Turi, D.: A coalgebraic foundation for linear time semantics. In: Coalgebraic Methods in Computer Science, CMCS 1999. ENTCS, vol. 29, pp. 259–274. Elsevier (1999)
Reichel, H.: Behavioural equivalence — a unifying concept for initial and final specification methods. In: Math. Models in Comp. Systems, Proc. 3rd Hungarian Comp. Sci. Conference, pp. 27–39 (1981)
Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Generalizing the powerset construction, coalgebraically. In: Lodaya, K., Mahajan, M. (eds.) Proc. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), vol. 8, pp. 272–283 (2010)
Silva, A., Bonchi, F., Bonsangue, M.M., Rutten, J.J.M.M.: Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci. 9(1:9) (2013)
Tao, T.: An Introduction to Measure Theory. AMS (2011)
Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Logic in Computer Science, LICS 1997, pp. 280–291 (1997)
van Glabbeek, R.: The linear time-branching time spectrum (extended abstract). In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)
Worrell, J.: On the final sequence of a finitary set functor. Theoret. Comput. Sci. 338, 184–199 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Kurz, A., Milius, S., Pattinson, D., Schröder, L. (2015). Simplified Coalgebraic Trace Equivalence. In: De Nicola, R., Hennicker, R. (eds) Software, Services, and Systems. Lecture Notes in Computer Science, vol 8950. Springer, Cham. https://doi.org/10.1007/978-3-319-15545-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-15545-6_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15544-9
Online ISBN: 978-3-319-15545-6
eBook Packages: Computer ScienceComputer Science (R0)