Abstract
Simulations are a very natural way of relating concurrent systems, which are mathematically modeled by Kripke structures. The range of available notions of simulations makes it very natural to adopt a categorical viewpoint in which Kripke structures become the objects of several categories while the morphisms are obtained from the corresponding notion of simulation. Here we define in detail several of those categories, collect them together in various institutions, and study their most interesting properties.
Research supported by ONR Grant N00014-02-1-0715, NSF Grant CCR-0234524, by DARPA through Air Force Research Laboratory Contract F30602-02-C-0130, and by the Spanish CICYT projects MELODIAS TIC 2002-01167 and MIDAS TIC 2003–0100.
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.
References
Arrais, M., Fiadeiro, J.L.: Unifying theories in different institutions. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 81–101. Springer, Heidelberg (1996)
Barr, M., Wells, C.: Category Theory for Computing Science. 3rd edn. Centre de Recherches Mathématiques (1999)
Browne, M.C., Clarke, E.M., Grümberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science 59, 115–131 (1988)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)
Herrlich, H., Strecker, G.E.: Category Theory: An Introduction. Advanced Mathematics. Allyn and Bacon, Boston (1973)
Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North-Holland, Amsterdam (1999)
Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Springer, Heidelberg (1998)
Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, University of Texas at Austin (Aug. 2001)
Martí-Oliet, N., Meseguer, J., Palomino, M.: Theoroidal maps as algebraic simulations. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 126–143. Springer, Heidelberg (2005)
Martí-Oliet, N., Meseguer, J., Palomino, M.: Algebraic simulations. Submitted (2005), http://maude.sip.ucm.es/~miguelpt/bibliography
Meseguer, J., Martí-Oliet, N., Palomino, M.: Equational abstractions. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 2–16. Springer, Heidelberg (2003)
Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, pp. 284–296. Springer, Heidelberg (1997)
Tarlecki, A., Burstall, R.M., Goguen, J.A.: Some fundamental algebraic tools for the semantics of computation. Part 3: Indexed categories. Theoretical Computer Science 91(2), 239–264 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Palomino, M., Meseguer, J., Martí-Oliet, N. (2005). A Categorical Approach to Simulations. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds) Algebra and Coalgebra in Computer Science. CALCO 2005. Lecture Notes in Computer Science, vol 3629. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11548133_20
Download citation
DOI: https://doi.org/10.1007/11548133_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28620-2
Online ISBN: 978-3-540-31876-7
eBook Packages: Computer ScienceComputer Science (R0)