Using Category Theory to Explore and Model Label Event Structures

Ming Zhu, Jing Li

College of Computer Science and Technology, Shandong University of Technology, Zibo, China.

DOI: 10.4236/jcc.2019.71005                

Abstract

The development of a concurrent system poses unique challenges, especially those related to correctness and consistency, as such a system usually involves several interactive processes executing simultaneously. To deal with some of these challenges, we resorted to Labeled Event Structures (LES) and category theory as the formal methods to model concurrent systems. Specifically, in this paper, we proposed an idea to define categories and corresponding constructs, such as product and sum, to model events and relationships among events represented by LES. To explain the idea, several examples are developed. Though a mathematical proof, the proposed idea helped to build a correct-by-construction approach for formalizing LES models of concurrent systems.

Keywords

Concurrent System, LES, Formalization, Category Theory

1. Introduction

A concurrent system that consists of several simultaneously executing components allows carrying out multiple tasks at the same time, which can accelerate the computational work of software substantially. To model concurrent system, Labeled Event Structures (LES) were proposed and evolved in research [1] [2] . However, a concurrent system usually involves many concurrently interactive components; the exhibition of a large number of different behaviors typically occurs, which may introduce difficulties to the development of concurrent systems [3] . In particular, the notable difficulties include the state-space explosion, unpredictable composition, and others [4] . To tackle this kind of challenge, the formal method is considered to be a way, which can provide systems with known safety properties [5] . Usually, a formal specification can be used to check for particular types of errors and as inputs for model checking. Category theory is a formal method, which has been used to model and verify concurrent systems. Category theory has been proposed as a framework to offer specification structure. It has a rich body of theory to reason objects and their relations. Moreover, category theory adopts a correct-by-construction approach by which components can be specified, proved and composed in the way of preserving their properties.

Researches [6] [7] used category theory to model concurrent systems. As a continuation, we propose to use category theory to explore and model LES for concurrent systems in this paper. Specifically, we propose an approach to construct categorical object, morphism, product, and sum for LES. To explain our work, a vending machine example is designed by LES, and modeled by category theory. The rest of this paper is organized as follows. Section 2 introduces related work to this paper. Section 3 introduces background knowledge required to understand the remaining content of the paper. Section 4 provides a vending machine example modeled by LES, which is used for the explanation of the proposed categorical modeling. Section 5 shows how to construct categorical structures from LES. Section 6 illustrates how to use the proposed categorical approach to model the vending machine example. Section 7 concludes this paper.

2. Related Work

2.1. Labeled Event Structure

LES is a mathematical model with true concurrency that describes a process in terms of relations between sets of events it generates. Loogen and Goltz used LES to analyze and model nondeterministic concurrent processes [8] . de León, Haar and Longuet proposed a theoretical framework based on LES for testing and verifying observable behaviors of concurrent systems from true concurrency models like Petri nets or networks of automata [9] . Castellan, Clairambault, Rideau and Winskel introduced a detailed, self-contained update to concurrent games on event structures which were preserved by composition with a copycat strategy, and the construction of a bicategory of these strategies [10] . Bruni, Melgratti and Montanari proposed a definition of a particular class of graph grammars that are expressive enough to model name passing calculi while simplifying the denotational domain construction, and applied this technique to derive event structure semantic [11] .

2.2. Category Theory

For modeling concurrency, category theory is used to model, analyze, and compare Transition System, Trace Language, Event Structure, Petri nets, and other classical models of concurrency [12] [13] [14] . Sisiaridis, Kuchta and Markowitch proposed a framework for implementing Godement calculus and cartesian closed comma categories for information security management in the detection of threats and attacks in communication systems [15] . Paper [16] introduces a formal language model which formalized agent-environment interaction in a multi-agent framework called Conversational Grammar Systems (CGS). This system provided a model with a high degree of flexibility. Based on eco-grammar systems, the formal model used in this paper can be defined as an evolutionary multi-agent system. Category theory is applied to study relationships between geometrical models for concurrency and classical models [17] . Abdel Gawad outlined and summarized four new potential applications of category theory to OOP research are presented the use of operads to model Java sub-typing [18] .

3. Background

In this section, background and work related to our research are introduced.

3.1. Labeled Event Structure

An event structure expresses how these events are related to each other. In general event structures that are widely used, a concurrent system or a process can be represented as tuples $\left(E;Con;⊢\right)$ .

Definition 1. An event structure is a tuple $\left(E;Con;⊢\right)$ consisting of

・ a set of events E,

・ the consistency predicate $Con\subseteq {\text{2}}^E$ , the set of conflict-free finite subsets of E, and

・ the enabling relation $⊢\subseteq Con\times E$

which satisfies the following properties:

・ consistency of Con: $\forall X,Y\subseteq E\wedge X\subseteq Y\Rightarrow Y\in Con$ and

・ $\forall e\in E$ . $\forall X,Y\subseteq E$ . $X⊢e\wedge X\subseteq Y\in Con\Rightarrow Y⊢e$ , that is, if X enables e so does any conflict-free superset Y of X.

Example 1. There is a transition system with states $S=\left\{S_0,S_{\text{1}},S_{\text{2}},S_{\text{3}},S_{\text{4}}\right\}$ , where S₀ is the initial state, and transitions $T=\left\{a,b,c,d\right\}$ . The graphical representation of the transition system is show in Figure 1.

This transition system can be represented by LES as follows:

$E=\left\{a;b;c;d\right\}$

$Con=\left\{\varnothing ,\left\{a\right\},\left\{b\right\},\left\{c\right\},\left\{d\right\},\left\{a,b\right\},\left\{a,d\right\},\left\{a,c\right\},\left\{b,c\right\},\left\{a,b,c\right\}\right\}$

$⊢:\varnothing ⊢a,\left\{a\right\}⊢b,\left\{a\right\}⊢d,\left\{a,b\right\}⊢c$

Figure 1. A transition system.

3.2. Category Theory

Category theory focuses on the relationships (morphisms) between objects instead of their representations; the morphisms can determine the nature of interactions established between the objects.

Definition 2. A category consists of the following data:

・ Objects: A, B, C, etc.

・ Arrows (Morphisms): f, g, h, etc.

・ For each arrow f, there are given objects: dom(f), cod(f) called domain as well as codomain of f, and f: A → B indicates that A = dom(f), B = cod(f).

・ Given arrows f: A → B and g: B → C with cod(f) = dom(g), there is an given arrow:

$g\circ f:A\to C$ called composite of f and g.

・ For each object A, there is an given arrow: 1_A: A → A called identity arrow of A.

These data need to satisfy the following laws:

・ Associativity: $h\circ \left(g\circ f\right)=\left(h\circ g\right)\circ f$ for all f: A → B, g: B → C, h: C → D.

・ Unit: $f\circ {\text{1}}_A=f={\text{1}}_B\circ f$ for all f: A → B.

Example 2. Let (S; ≤) be a partially-ordered set (poset). Define the category C in which: each member x of S is an object of C; and each relation x ≤ y of (S; ≤) is a morphism x → y of C.

We can verify that C is a category as follows:

・ For every object x, there is an identity morphism x → x, corresponding to reflexivity, x ≤ x, in the poset.

・ The morphisms (x → y) and (y → z) form a composition pair: $\left(y\to z\right)\circ \left(x\to y\right)=\left(x\to z\right)$ ; corresponding to transitivity, x ≤ y, y ≤ z, and x ≤ z, in the poset.

・ Composition is associative:

$\left(\left(x\to y\right)\circ \left(v\to x\right)\right)\circ \left(u\to v\right)=\left(v\to y\right)\circ \left(u\to v\right)=u\to y$

and

$\left(x\to y\right)\circ \left(\left(v\to x\right)\circ \left(u\to v\right)\right)=\left(x\to y\right)\circ \left(u\to x\right)=\left(u\to y\right)$ ,

because of

$\begin{array}{l}\left(\left(x\le y\right)\circ \left(v\le x\right)\right)\circ \left(u\le v\right)\\ =\left(x\le y\right)\circ \left(\left(v\le x\right)\circ \left(u\le v\right)\right)\\ =\left(x\le y\right)\circ \left(u\le x\right)\\ =\left(v\le y\right)\circ \left(u\le v\right)=\left(u\le y\right)\end{array}$

Definition 3. Let A and B be objects in a category Cat. Then a product of A and B consists of:

・ an object, A × B,

・ morphisms, often called projections, $A\times B\stackrel{{\pi }_a}{\to }A$ and $A\times B\stackrel{{\pi }_b}{\to }B$ , and

・ the property that, for any object C and morphisms $C\stackrel{f_a}{\to }A$ , $C\stackrel{f_b}{\to }B$ , there is a unique morphism $C\stackrel{g}{\to }A\times B$ such that Figure 2 commutes. That is ${\pi }_a\circ g=f_a$ and _{${\pi }_b\circ g=f_b$} .

Definition 4. Let A and B be objects in a category Cat. Then a sum (or coproduct) of A and B consists of:

・ an object, A + B,

・ morphisms, often called inclusions or canonical projections, $A\stackrel{i_a}{\to }A+B$ and $B\stackrel{i_b}{\to }A+B$ , and

・ the property that, for any object C and morphisms $C\stackrel{f_a}{\to }A$ and $C\stackrel{f_b}{\to }B$ , there is a unique morphism $A+B\stackrel{\langle f_a;f_b\rangle }{\to }C$ such that Figure 3 commutes. That is $\langle f_a;f_b\rangle \circ i_a=f_a$ and $\langle f_a;f_b\rangle \circ i_b=f_b$ .

4. An Overview of a Vending Machine Example

In this paper, we use a vending machine example to illustrate how to construct categories and the corresponding structures for models specified by LES which is defined and specified in section 3.

Example 3. There is a vending machine and a person. The vending machine can offer coke and pepsi. Each time, the vending machine accepts a coin first, then dispenses a bottle of coke or pepsi according to the person’s choice.

In this example, the vending machine and the person are modeled as two processes. When the person inserts a coin and vending machine accepts the coin, this interaction can be represented by the shared event coin in person and vending machine. When person chooses coke or pepsi and vending machine accepts it, this interaction can be represented by the shared event coke or pepsi in person and vending machine. After that, the communications between person and vending machine terminate.

By using LES, the communications between person and vending machine in the example can be modeled as follows:

Figure 2. Product.

Figure 3. Sum (coproduct).

$VMP=\left(E;Con;⊢\right)$

$E=\left\{coin;coke;pepsi;stop\right\}$

$\begin{array}{l}Con=\{\varnothing ,\left\{coin\right\},\left\{coke\right\},\left\{pepsi\right\},\left\{coin,coke\right\},\left\{coin,pepsi\right\},\\ \left\{coin,pepsi,stop\right\},\left\{coin,coke,stop\right\}\}\end{array}$

$⊢:\varnothing ⊢coin,\left\{coin\right\}⊢coke,\left\{coin\right\}⊢pepsi,\left\{coin,coke\right\}⊢stop,\left\{coin,pepsi\right\}⊢stop$

5. Construct Categorical Structures for LES Models

In this section, we use category theory to construct structures for LES models. We first define categorical object and morphism for constructing categories for LES models, then we construct product and sum based on the categories, and we use the vending machine example in Section 3 to explain the categorical structures.

5.1. Object

An object is like an event structure, but simpler. Formally, an object (E, R) consists of a set of events, E, and an ordering relation $R\subseteq E\times E$ . If events e₁ and e₂ are related by R (that is, $\left(e_{\text{1}},e_{\text{2}}\right)\in R$ ), $\left\{e_{\text{1}}\right\}⊢e_{\text{2}}$ that indicates “e₁ precedes e₂” or “e₁ happens before e₂”.

The relation R is a partial order: reflexive, antisymmetric, and transitive. If $e_{\text{1}}\ne e_{\text{2}}$ , it is not possible to have both $e_{\text{1}}⊢e_{\text{2}}$ and $e_2⊢e_1$ , but it is possible that neither is true.

An object can be represented by a forest diagram such as Figure 4. For example:

For this object,

$E=\left\{a,b,c,d,e\right\}$ ,

$R=\left\{\varnothing ⊢a,\varnothing ⊢c,\left\{a\right\}⊢b,\left\{c\right\}⊢d,\left\{c\right\}⊢e\right\}$

R is reflexive, transitive. In Figure 3, we omit reflexive and transitive arrows. Note that some pairs of events, e.g., a and c, are unrelated: this means simply that there are no constraints on their order of occurrence.

5.2. Morphism

Let $O_{\text{1}}=\left(E_{\text{1}},R_{\text{1}}\right)$ and $O_{\text{2}}=\left(E_{\text{2}},R_{\text{2}}\right)$ be objects. There is a morphism $O_{\text{1}}\stackrel{m}{\to }{O}_{\text{2}}$ if and only if $E_{\text{1}}\subseteq E_{\text{2}}$ and $O_{\text{1}}\subseteq O_{\text{2}}$ . In words:

・ Every event e that belongs to E₁ also belongs to E₂.

・ Every ordered pair $\left\{e_{\text{1}}\right\}⊢e_{\text{2}}$ in O₁ also belongs to O₂.

There is an identity morphism for every object (E, R) because $E\subseteq E$ and $R\subseteq R$ . Similarly, compositions of morphism exist by transitivity of $\subseteq$ . Consequently, the objects and morphisms combined forma category CP.

If there is a morphism $O_{\text{1}}\stackrel{m}{\to }{O}_{\text{2}}$ , which indicates O₁ is contained by O₂ or simply O₂ contains O₁. This terminology is consistent with a set “containing” its subsets.

Figure 4. Graphical representation of object.

Also, if there is a morphism $O_{\text{1}}\stackrel{m}{\to }{O}_{\text{2}}$ , then it must be unique, because there is only one way that a set can be a subset of another set.

There exist some special cases:

・ Traces are objects: the trace $\left\{a\right\}⊢b$ , $\left\{a,b\right\}⊢c$ can be represented as object a → b→ c.

・ If trace t₁ is a prefix of trace t₂, there is a morphism $t_{\text{1}}\stackrel{m}{\to }{t}_{\text{2}}$ .

・ Event trees are objects: the object shown above in Figure 3 has a tree with c as root.

・ There is a morphism from any path in a tree to the tree itself.

5.3. Sum (Coproduct)

If S and T are objects, we define their sum(coproduct) S + T to be the smallest object that contains both S and T. The sum can be defined by set union as follows:

Definition 5. Let $S=\left(E_{\text{1}},R_{\text{1}}\right)$ and $T=\left(E_{\text{2}},R_{\text{2}}\right)$ , then

$S+T=\left(E_1,R_1\right)+\left(E_2,R_2\right)=\left(E_1\cup E_2,R_1\cup R_2\right).$

・ By definition, S + T contains S. Consequently, there is a morphism $S\stackrel{i_s}{\to }S+T$ . Similarly, there is a morphism $T\stackrel{i_t}{\to }S+T$ .

・ Let X be another object and suppose there is a morphism $S\stackrel{s}{\to }X$ , then X contains S. Similarly, if there is a morphism $T\stackrel{t}{\to }X$ , then X contains T. Thus X contains both S and T. Since S + T is the smallest object containing both S and T, it follows that X must contain S + T and therefore there is a morphism $S+T\stackrel{h}{\to }X$ . The morphism h is unique.

To illustrate the sum S + T, Figure 5 describes the sum and it commutes.

We can use sum to build branching structures, which can be explained by using Example 4 as follows:

Example 4. Given (E₁, R₁) and (E₂, R₂), where

・ $E_1=\left\{a,b\right\}$ , $R_{\text{1}}=\left\{\varnothing ⊢a,\left\{a\right\}⊢b\right\}$ .

・ $E_{\text{2}}=\left\{a,c\right\}$ , $R_{\text{2}}=\left\{\varnothing ⊢a,\left\{a\right\}⊢c\right\}$ .

Then, there is a sum $\left(E_{\text{1}}\cup E_{\text{2}},R_{\text{1}}\cup R_{\text{2}}\right)=\left(\left\{a,b,c\right\},\left\{\varnothing ⊢a,\left\{a\right\}⊢b,\left\{a\right\}⊢c\right\}\right)$ which can be represented by Figure 6.

In general, when S + T is formed, we assume that the event structures S and T belong to the same process. If e occurs in both structures, it refers to the same event.

Figure 5. The sum S + T.

Figure 6. The sum $\left(E_{\text{1}}\cup E_{\text{2}},R_{\text{1}}\cup R_{\text{2}}\right)$ .

5.4. Product

The purpose of the product is to combine concurrent processes, each defined by an object, i.e., event structure. To do this, two kinds of event must be distinguished:

Let $P_{\text{1}}=\left(E_{\text{1}},R_{\text{1}}\right)$ and $P_{\text{2}}=\left(E_{\text{2}},R_{\text{2}}\right)$ be objects corresponding to concurrent processes and let $e\in E_{\text{1}}$ . Then:

・ If $e\in E_{\text{2}}$ , it indicates that e is a communication event and e must occur simultaneously in both processes.

・ Otherwise, $e\notin E_{\text{2}}$ , and e belongs to process P only. In this case, e is an independent event.

Product of P₁ and P₂ can be constructed as follows:

・ Let $E^{\times }=E_1\cap E_2$ be the set of events that communicate, namely the communication set. The communication set is as large as possible, which means that the only events that cannot be added to it are not communication events.

・ The ordering relation R ^× is the union $R_1\cup R_2$ restricted to elements of E ^×. Formally,

$R^{\times }=\left\{\left(e_1,e_2\right)|e_1\in E^{\times }\text{and}{e}_2\in E^{\times }\text{and}\left(e_1,e_2\right)\in R_1\cup R_2\right\}$

So, the definition of product is provided as follows:

Definition 6. Let $S=\left(E_{\text{1}},R_{\text{1}}\right)$ and $T=\left(E_{\text{2}},R_{\text{2}}\right)$ , then

$\begin{array}{c}S\times T=\left(E_1,R_1\right)\times \left(E_2,R_2\right)\\ =\left(E_1\cap E_2,\left\{\left(e_1,e_2\right)|e_1\in E^{\times }\text{and}{e}_2\in E^{\times }\text{and}\left(e_1,e_2\right)\in R_1\cup R_2\right\}\right)\end{array}$

・ By construction, S × T contains only events that occur in S and T and is therefore contained in both of them. Thus the projections $S\times T\stackrel{{\pi }_s}{\to }S$ and $S\times T\stackrel{{\pi }_t}{\to }T$ are well-defined.

・ Assuming that there is an object X and morphisms $X\stackrel{s}{\to }S$ and $X\stackrel{t}{\to }T$ . Then X must be contained in both S and T. Therefore it must also be contained in S × T which is the largest object contained in both S and T. Hence the morphism $X\stackrel{h}{\to }S\times T$ exists and is unique.

To illustrate the sum S × T, Figure 7 describes the product and it commutes.

We can use product to build largest communication structures, which can be explained by using Example 5 as follows:

Example 5. Let $P=\left(E_P,R_P\right)$ and $Q=\left(E_Q,R_Q\right)$ defined as in Figure 8, in which the c’s are communicating events and the e’s are independent events:

Then the product P × Q has the events $E_P\cap E_Q=\left\{c_{\text{1}},c_{\text{2}}\right\}$ and the ordering is just $\left\{c_{\text{1}}\right\}⊢c_{\text{2}}$ . The processes execute as shown, with time increasing from left to right, synchronizing at c₁ and c₂. The execution independent events, such as e₃, are ignored, as they don’t affect the communications. So, independent events are abstracted out of the system.

6. Use Categorical Structures to Model the Vending Machine

In Section 4, this paper provided a vending machine in Example 3 which is modeled by LES. In this section, we use categorical structures defined in Section 5 to model the vending machine example.

The objects of the vending machine are listed as follows:

$A=\left(\left\{\right\},\left\{\right\}\right),$

$B=\left(\left\{coin\right\},\left\{\varnothing ⊢coin\right\}\right),$

$C=\left(\left\{coin,coke\right\},\left\{\varnothing ⊢coin,\left\{coin\right\}⊢coke\right\}\right),$

$D=\left(\left\{coin,pepsi\right\},\left\{\varnothing ⊢coin,\left\{coin\right\}⊢pepsi\right\}\right),$

$E=\left(\left\{coin,coke\right\},\left\{\varnothing ⊢coin,\left\{coin\right\}⊢coke,\left\{coke\right\}⊢stop\right\}\right),$

$F=\left(\left\{coin,pepsi\right\},\left\{\varnothing ⊢coin,\left\{coin\right\}⊢pepsi,\left\{pepsi\right\}⊢stop\right\}\right),$

$G=\left(\left\{coin,coke\right\},\left\{\varnothing ⊢coin,\left\{coin\right\}⊢coke,\left\{coin\right\}⊢pepsi\right\}\right),$

$H=\left(\left\{coin,coke\right\},\left\{\varnothing ⊢coin,\left\{coin\right\}⊢coke,\left\{coin\right\}⊢pepsi,\left\{coke\right\}⊢stop\right\}\right)$ ,

$I=\left(\left\{coin,coke\right\},\left\{\varnothing ⊢coin,\left\{coin\right\}⊢coke,\left\{coin\right\}⊢pepsi,\left\{pepsi\right\}⊢stop\right\}\right)$ ,

$\begin{array}{l}J=(\left\{coin,coke\right\},\{\varnothing ⊢coin,\left\{coin\right\}⊢coke,\left\{coin\right\}⊢pepsi,\\ \left\{coke\right\}⊢stop,\left\{pepsi\right\}⊢stop\}),\end{array}$

The morphisms between objects are listed as follows, where identities and composites are ignored:

$\begin{array}{l}A\to B,B\to C,B\to D,C\to E,D\to F,C\to G,D\to G,\\ E\to H,F\to I,G\to H,G\to I,H\to J,I\to J\end{array}$

The diagram of the category of the vending machine is illustrated in Figure 9.

In Figure 9, there exist some products and sums, where a product represents the largest communication structure of two objects and a sum represents the branching structure of two objects.

Figure 7. The sum S × T.

Figure 8. Communication events.

Figure 9. Category of the vending machine.

・ Products of the category of the vending machine are listed as follows:

$G\times F=D,H\times F=D,H\times I=G,E\times G=C,H\times F=D,E\times F=B$

The above-mentioned products are just some in the category, while there are other products that are not listed specifically in above.

・ Sums of the category of the vending machine are listed as follows:

$C+D=G,E+G=H,G+F=I,H+I=J,E+D=H,E+F=J,C+F=I$

The above-mentioned sums are just some in the category, while there are other sums that are not listed specifically in above.

7. Conclusion

In view of the difficulties in the development of concurrent systems, the present work proposes a new approach to model LES based on the category theory, which helps to explore the communication events and relationship among them. Specifically, categorical object, morphism, product, and sum are constructed for events and relationships. To explain the work, a vending machine example is designed by LES, and the communications between vending machines and persons are modeled by category theory. By adopting the categorical approach, we can explore and model concurrent systems designed by LES with categorical structures, which can be specified, proved and composed formally with preserving their properties. In Future, we will explore the usage of more categorical structures, such as limit/colimit and natural transformation in LES which may be useful for the formalization and verification of communications.

Acknowledgements

We thank the editor and the referee for their comments. Research of M. Zhu and J. Li is funded by the Shandong University of Technology grants 4041-416069 and 4041-417010. The support is greatly appreciated.

Conflicts of Interest

The authors declare no conflicts of interest regarding the publication of this paper.

References

[1]	Winskel, G. (1989) An Introduction to Event Structures. Proceeding of Linear, Time, Branching Time and Partial Order in Logics and Models for Concurrency, Berlin, 30 May-3 June 1989, 364-397.
[2]	Baldan, P., Busi, N., Corradini, A. and Pinna, G.M. (2000) Domain and Event Structure Semantics for Petri Nets with Read and Inhibitor Arcs. Theoretical Computer Science, 323, 129-189. https://doi.org/10.1016/j.tcs.2004.04.001
[3]	Kuang, H. (2013) Towards a Formal Reactive Autonomic Systems Framework Using Category Theory. Ph.D. Thesis, Concordia University, Montreal.
[4]	Sampson, A.T. (2008) Process-Oriented Patterns for Concurrent Software Engineering. Ph.D. Thesis, University of Kent, Kent.
[5]	Hinchey, M.G., Rouff, C.A., Rash, J.L. and Truszkowski, W.F. (2005) Requirements of an Integrated Formal Method for Intelligent Swarms. Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, Lisbon, 5-6 September 2005, 125-133. https://doi.org/10.1145/1081180.1081196
[6]	Zhu, M., Grogono, P. and Ormandjieva, O. (2017) Exploring Relationships between Syntax and Semantics of a Process-Oriented Language by Category Theory. Proceedings of the 8th International Conference on Ambient Systems, Networks and Technologies, Madeira, 16-19 May 2017, 241-248. https://doi.org/10.1016/j.procs.2017.05.342
[7]	Zhu, M., Grogono, P., Ormandjieva, O. and Kuang H. (2016) Using Failures and Category Theory to Verify Process Communications between Design and Implementation of Concurrent Systems. Proceedings of the 7th International Conference on Ambient Systems, Networks and Technologies, Madrid, 23-26 May 2016, 700-704. https://doi.org/10.1016/j.procs.2016.04.155
[8]	Loogen, R. and Goltz, U. (1991) Modelling Nondeterministic Concurrent Processes with Event Structures. Fundamenta Informaticae, 14, 39-73.
[9]	León, H.P.D., Haar, S. and Longuet, D. (2012) Conformance Relations for Labeled Event Structures. Proceedings of the 6th International Conference on Tests and Proofs, Prague, 31 May-1 June 2012, 83-98. https://doi.org/10.1007/978-3-642-30473-6_8
[10]	Castellan, S. and Clairambault, P., Rideau, S. and Winskel, G. (2016) Concurrent Games. Logical Methods in Computer Science, 13, 1-51.
[11]	Bruni, R., Melgratti, H. and Montanari, U. (2006) Event Structure Semantics for Nominal Calculi. Proceedings of 17th International Conference on Concurrency Theory, Bonn, 27-30 August 2006, 295-309.
[12]	Winskel, G. and Nielsen, M. (1995) Models for Concurrency. Handbook of Logic in Computer Science, Vol. 4, 1-148.
[13]	Nielsen, M., Sassone, V. and Winskel, G. (1996) Models for Concurrency: Towards a Classification. Theoretical Computer Science, 170, 297-348. https://doi.org/10.1016/S0304-3975(96)80710-9
[14]	Hildebrandt, T.T. (2000) Categorical Models for Fairness: Completion vs. Delay. Proceedings of the First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, Cork, 20-21 July 2000, 188.
[15]	Sisiaridis, D., Kuchta, V. and Markowitch, O. (2016) A Categorical Approach in Handling Event-Ordering in Distributed Systems. Proceedings of IEEE 22nd International Conference on Parallel and Distributed Systems, Wuhan, 13-16 December 2016, 1145-1150. https://doi.org/10.1109/ICPADS.2016.0150
[16]	Enguix, G.B. and Lopez, M.D.J. (2007) Agent-Environment Interaction in a Multi-Agent System: A Formal Model. Proceedings of the GECCO Conference on Genetic and Evolutionary Computation, London, 7-11 July 2007, 2607-2612.
[17]	Goubault, E. and Mimram, S. (2010) Formal Relationships between Geometrical and Classical Models for Concurrency. Proceedings of the Workshop on Geometric and Topological Methods in Computer Science, Denmark, 11-15 January 2010, 77-109.
[18]	Abdel Gawad, M.A. (2017) Novel Uses of Category Theory in Modeling OOP. CoRR, abs/1709.08056, 1-8.