Paper: A Sheaf-Theoretic Model of Concurrency (at LICS 1986)

Authors: Luís F. Monteiro Fernando C. N. Pereira

Abstract

We develop here a structural theory of concurrency in which the locality of interaction between subsystems is described with the mathematical tools of the theory of sheaves. This theory allows us to model precisely processes that interact through common behavior at shared locations. In contrast to behavioral models, ours keeps track of the individual contributions of subsystems to overall system behavior, allowing a finer-grained analysis of subsystem interactions.
From event signatures that specify relations of independence and exclusivity between events, we construct spaces of locations where activity may occur. Behaviors are then modeled as elements of sheaves of monoids over those spaces and processes as certain sets of behaviors. The construction of the model, and in particular ist avoidance of interleaving, gives it very convenient mathematical properties - sheaves of behavior monoids are to event signatures what free monoids are to alphabets. The theory also allows us to identify on purely structural grounds event signatures with a potential for deadlock.
We conclude with a discussion of the solution of process equations in our model, with an example from CSP.

BibTeX

  @InProceedings{MonteiroPereira-ASheafTheoreticMode,
    author = 	 {Luís F. Monteiro and Fernando C. N. Pereira},
    title = 	 {A Sheaf-Theoretic Model of Concurrency},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {66--76},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }