Abstract
Coalgebras are categorical presentations of state-based systems. In investigating parallel composition of coalgebras (realizing concurrency), we observe that the same algebraic theory is interpreted in two different domains in a nested manner, namely: in the category of coalgebras, and in the final coalgebra as an object in it. This phenomenon is what Baez and Dolan have called the microcosm principle, a prototypical example of which is “a monoid in a monoidal category.” In this paper we obtain a formalization of the microcosm principle in which such a nested model is expressed categorically as a suitable lax natural transformation. An application of this account is a general compositionality result which supports modular verification of complex systems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baez, J.C., Dolan, J.: Higher dimensional algebra III: n-categories and the algebra of opetopes. Adv. Math. 135, 145–206 (1998)
Barr, M., Wells, C.: Toposes, Triples and Theories. Springer, Berlin (1985)
Bartels, F.: On generalised coinduction and probabilistic specification formats. Distributive laws in coalgebraic modelling. PhD thesis, Free Univ. Amsterdam (2004)
Borceux, F.: Handbook of Categorical Algebra. Encyclopedia of Mathematics, vol. 50, 51, 52. Cambridge Univ. Press, Cambridge (1994)
Hasuo, I.: Generic forward and backward simulations. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 406–420. Springer, Heidelberg (2006)
Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in Comp. Sci. 3(4–11) (2007)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Hyland, M., Power, A.J.: Discrete Lawvere theories and computational effects. Theor. Comp. Sci. 366(1–2), 144–162 (2006)
Jacobs, B.: Categorical Logic and Type Theory. North Holland, Amsterdam (1999)
Jacobs, B.: Trace semantics for coalgebras. In: Adámek, J., Milius, S. (eds.) Coalgebraic Methods in Computer Science. Elect. Notes in Theor. Comp. Sci., vol. 106, Elsevier, Amsterdam (2004)
Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations (2005) Draft of a book, www.cs.ru.nl/B.Jacobs/PAPERS/index.html
Jacobs, B.: A bialgebraic review of deterministic automata, regular expressions and languages. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 375–404. Springer, Heidelberg (2006)
Johnstone, P.T., Power, A.J., Tsujishita, T., Watanabe, H., Worrell, J.: An axiomatics for categories of transition systems as coalgebras. In: Logic in Computer Science, IEEE, Computer Science Press, Los Alamitos (1998)
Kick, M., Power, A.J., Simpson, A.: Coalgebraic semantics for timed processes. Inf. & Comp. 204(4), 588–609 (2006)
Klin, B.: From bialgebraic semantics to congruence formats. In: Workshop on Structural Operational Semantics (SOS 2004). Elect. Notes in Theor. Comp. Sci. 128, 3–37 (2005)
Klin, B.: Bialgebraic operational semantics and modal logic. In: Logic in Computer Science, pp. 336–345. IEEE Computer Society, Los Alamitos (2007)
Kock, A., Reyes, G.E.: Doctrines in categorical logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 283–313. North-Holland, Amsterdam (1977)
Lawvere, F.W.: Functorial Semantics of Algebraic Theories and Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, 1963. Reprints in Theory and Applications of Categories 5, 1–121 (2004)
Lee, E.A.: Making concurrency mainstream, Invited talk at CONCUR 2006 (2006)
Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Springer, Berlin (1998)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Moggi, E.: Notions of computation and monads. Inf. & Comp. 93(1), 55–92 (1991)
Mousavi, M.R., Reniers, M.A., Groote, J.F.: A syntactic commutativity format for SOS. Inform. Process. Lett. 93(5), 217–223 (2005)
Nishizawa, K., Power, A.J.: Lawvere theories enriched over a general base. Journ. of Pure & Appl. Algebra (to appear, 2006)
Power, J., Turi, D.: A coalgebraic foundation for linear time semantics. In: Category Theory and Computer Science. Elect. Notes in Theor. Comp. Sci., vol. 29, Elsevier, Amsterdam (1999)
Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comp. Sci. 249, 3–80 (2000)
Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Logic in Computer Science, pp. 280–291. IEEE, Computer Science Press, Los Alamitos (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hasuo, I., Jacobs, B., Sokolova, A. (2008). The Microcosm Principle and Concurrency in Coalgebra. In: Amadio, R. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2008. Lecture Notes in Computer Science, vol 4962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78499-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-78499-9_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78497-5
Online ISBN: 978-3-540-78499-9
eBook Packages: Computer ScienceComputer Science (R0)