Modeling interaction by sheaves and geometric logic

  • Viorica Sofronie-Stokkermans
  • Karel Stokkermans
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)


In this paper we show that, given a family of interacting systems, many notions which are important for expressing properties of systems can be modeled as sheaves over a suitable topological space. In such contexts, geometric logic can be used to test whether “local” properties can be lifted to a global level. We develop a way to use this method in the study of interacting systems, illustrated by examples.


Model Check Atomic Formula Parallel Action Relation Symbol Computation Tree Logic 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AT90]
    J. Adámek and V. Trnková. Automata and Algebras in Categories. Kluwer Academic Publishers, 1990.Google Scholar
  2. [CGL96]
    E.M. Clarke, O. Grumberg, and D.E. Long. Model checking. In Nato ASI Series F, volume 152, New York, Heidelberg, Berlin, 1996. Springer-Verlag.Google Scholar
  3. [CK90]
    C.C. Chang and H.J. Keisler. Model Theory. North-Holland, Amsterdam, 3rd edition, 1990.zbMATHCrossRefGoogle Scholar
  4. [CW96]
    G.L. Cattani and G. Winskel. Presheaf models for concurrency. In D. van Dalen and M. Bezem, editors, Proceedings of Computer Science Logic’ 96, LNCS 1258, pages 58-75. Springer Verlag, Berlin, 1996.Google Scholar
  5. [Die90]
    V. Diekert. Combinatorics on Traces. In LNCS 454. Springer Verlag, 1990.zbMATHGoogle Scholar
  6. [Gog92]
    J.A. Goguen. Sheaf semantics for concurrent interacting objects. Mathematical Structures in Computer Science, 11:159–191, 1992.MathSciNetCrossRefGoogle Scholar
  7. [Joh82]
    P. Johnstone. Stone Spaces. Cambridge Studies in Advanced Mathematics 3. Cambridge University Press, 1982.Google Scholar
  8. [Krö87]
    F. Kröger. Temporal Logic of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer Verlag, 1987.Google Scholar
  9. [Lil93]
    J. Lilius. A sheaf semantics for Petri nets. Technical Report A23, Dept. of Computer Science, Helsinki University of Technology, 1993.Google Scholar
  10. [Mal94]
    G. Malcolm. Interconnections of object specifications. In R. Wieringa and R. Feenstra, editors, Working Papers of the International Workshop on Information Systems — Correctness and Reusability, 1994. Appeared as internal report IR-357 of the Vrije Universiteit Amsterdam.Google Scholar
  11. [MLM92]
    S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic. Universitext. Springer Verlag, 1992.Google Scholar
  12. [MP86]
    L. Monteiro and F. Pereira. A sheaf theoretic model for concurrency. Proc. Logic in Computer Science (LICS’86), 1986.Google Scholar
  13. [Pfa91]
    J. Pfalzgraf. Logical fiberings and polycontextural systems. In P. Jorrand and J. Kelemen, editors, Proc. Fundamentals of Artificial Intelligence Research, volume 535 of LNCS (subseries LNAI), pages 170–184. Springer Verlag, 1991.Google Scholar
  14. [Sof96]
    V. Sofronie. Towards a sheaf theoretic approach to cooperating agents scenarios. In J. Calmet, J.A. Campbell, and J. Pfalzgraf, editors, Proceedings of Artificial Intelligence and Symbolic Mathematical Computation, International Conference, AISMC-3, Steyr, LNCS 1138, pages 289–304. Springer-Verlag, 1996.Google Scholar
  15. [SS97]
    V. Sofronie-Stokkermans. Fibered Structures and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems. PhD thesis, RISC-Linz, J. Kepler University Linz, 1997.Google Scholar
  16. [Win96]
    G. Winskel. A presheaf semantics of value-passing proceses. In Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR’ 96 Proceedings, LNCS 1119, pages 98–114, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Viorica Sofronie-Stokkermans
    • 1
  • Karel Stokkermans
    • 2
  1. 1.Max-Planck Institut für InformatikSaarbrückenGermany
  2. 2.Institut für ComputerwissenschaftenSalzburgAustria

Personalised recommendations