Bisimulations and Unfolding in P-Accessible Categorical Models

Authors Jérémy Dubut, Eric Goubault, Jean Goubault-Larrecq



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.25.pdf
  • Filesize: 437 kB
  • 14 pages

Document Identifiers

Author Details

Jérémy Dubut
Eric Goubault
Jean Goubault-Larrecq

Cite AsGet BibTex

Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. Bisimulations and Unfolding in P-Accessible Categorical Models. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 25:1-25:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.25

Abstract

In this paper, we propose a categorical framework for bisimulations and unfoldings that unifies the classical approach from Joyal and al. via open maps and unfoldings. This is based on a notion of categories accessible with respect to a subcategory of path shapes, i.e., for which one can define a nice notion of trees as glueing of paths. We prove that transitions systems and pre sheaf models are a particular case of our framework. We also prove that in our framework, several characterizations of bisimulation coincide, in particular an "operational one" akin to the standard definition in transition systems. Also, accessibility is preserved by coreflexions. We then design a notion of unfolding, which has good properties in the accessible case: its is a right adjoint and is a universal covering, i.e., initial among the morphisms that have the unique lifting property with respect to path shapes. As an application, we prove that the universal covering of a groupoid, a standard construction in algebraic topology, coincides with an unfolding, when the category of path shapes is well chosen.
Keywords
  • categorical models
  • bisimulation
  • coreflexions
  • unfolding
  • universal covering

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. F. Borceux. Handbook of Categorical Algebra 2 : Categories and Structures. Cambridge University Press, 1994. Google Scholar
  2. J. Esparza and K. Heljanko. Unfoldings: A Partial-Order Approach to Model Checking. Monographs in Theoretical Computer Science. An EATCS Series. Springer Publishing Company, Incorporated, 2008. Google Scholar
  3. A. Girard, A. A. Julius, and G. J. Pappas. Approximate bisimulation for a class of stochastic hybrid systems. In 2006 American Control Conference, June 2006. Google Scholar
  4. A. Hatcher. Algebraic Topology. Cambridge University Press, 2002. Google Scholar
  5. A. Joyal and I. Moerdijk. A completeness theorem for open maps. Annals of Pure and Applied Logic, 70:51-86, 1994. Google Scholar
  6. A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from Open Maps. Information and Computation, 127(2):164-185, 1996. Google Scholar
  7. G. Lafferriere, G. J. Pappas, and S. Sastry. Hybrid Systems V, chapter Hybrid Systems with Finite Bisimulations, pages 186-203. Springer Berlin Heidelberg, 1999. Google Scholar
  8. M. Makkai and R. Paré. Accessible categories: The foundations of categorical model theory Contemporary Mathematics. 104. American Mathematical Society, 1989. Google Scholar
  9. J. P. May. A Concise Course in Algebraic Topology. Chicago Lectures in Mathematics. University of Chicago Press, 1999. Google Scholar
  10. M. Nielsen, G. Plotkin, and G. Winskel. Petri Nets, Event Structures and Domains, Part I. Theor. Comput. Sci., 13:85-108, 1981. Google Scholar
  11. M. Nielsen and G. Winskel. Models for Concurrency. Oxford University Press, 1995. Google Scholar
  12. D. Park. Concurrency and Automata on Infinite Sequences. Lecture Notes in Computer Science, 154:167-183, 1981. Google Scholar
  13. G. Winskel. A New Definition of Morphism on Petri Nets. In STACS 84, Symposium of Theoretical Aspects of Computer Science, Paris, France, 11-13 April, 1984, Proceedings, pages 140-150, 1984. Google Scholar
  14. G. Winskel. Event structures. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986, pages 325-392, 1986. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail