# Unified Mathematical Framework for Slicing and Symmetry Reduction over Event Structures

Authors: Xinyan Gao; Yingcai Ding; Wenbo Liu; Kaidi Zheng; Siyu Huang; Ning Zhou; Dakui Li
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

Nonclassical slicing and symmetry reduction can act as efficient structural abstract methods for pruning state space when dealing with verification problems. In this paper, we mainly address theoretical and algorithmic aspects for nonclassical slicing and symmetry reduction over prime event structures. We propose sliced and symmetric quotient reduction models of event structures and present their corresponding algorithms. To construct the underlying foundation of the proposed methodologies, we introduce strong and weak conflict concepts and a pair of mutually inverse operators and extend permutation group based symmetry notion of event structures. We have established a unified mathematical framework for slicing and symmetry reduction, and further investigated the translation, isomorphism, and equivalence relationship and other related basic facts from a theoretical point of view. The framework may provide useful guidance and theoretical exploration for overcoming verification challenges. This paper also demonstrates their practical applications by two cases.


---

## Body

## 1. Introduction

Generally, to detect whether a finite execution trace of a distributed program satisfies a given predicate, namely, predicate detection (a kind of verification problems), is a fundamental problem in asynchronous distributed systems. It has applications in many domains such as testing, debugging, and monitoring of distributed programs and it is also a powerful runtime verification method.Unfortunately, predicate detection is NP complete [1] and suffers from the excessive size of the state space and the state explosion problem—the number of possible global states of the program increases exponentially owing to simple combination.To deal with this problem, several useful reduction techniques have been suggested in succession for reducing the state space in recent years, such as partial order reduction and symmetric reduction methods [2–4].On the one hand, the basic observation is that many distributed or concurrent systems exhibit a certain degree of symmetry, for example, a system composed of identical or isomorphic components whose identities are interchangeable from a verification point of view. This kind of structural symmetry in the system is also reflected in the full state space of the system. The main idea behind the symmetry reduction method is to figure out this symmetry and obtain a condensed state space which is typically much smaller than the full state space, but from which the same kind of properties of the system can be derived without unfolding the condensed state space to the full state space. Thus, it can be used to verify any property of the original model.On the other hand, a slice of a system with respect to a criterion is a subsystem that only contains all the states of the original system that satisfy this specification. The advantage of this technique lies in the fact that the detection is performed only on the small part of the global state space which is of interest. In many cases, the slice is exponentially smaller than the original. In order to tangle predicate detection problem, nonclassical slicing technique, named computation slicing, as an abstraction mechanism, inspired by the classical program slicing of Weiser [5, 6], was first proposed by Garg and Mittal [7].For the majority predicate classes, the computation slicing algorithm has polynomial-time complexity and gains exponential reduction of state spaces. Computation slicing has been proved to be an efficient technique for pruning state space of predicate detection in distributed computation. Moreover, it has also been successfully applied to solve the problems of temporal properties verification in transaction level hardware descriptions such as PCI local bus protocol and the MSI (modified shared invalid) cache coherence protocol [6] in SoC (system on chip) systems and so forth.Due to the restriction of partial order execution trace model [5, 8], this approach has some limitations. Firstly, it is a runtime checking method and only checks a single partial execution trace once. It is not easy to obtain 100% path coverage even though this detection is performed multiple times. Thus, it is not suitable for exhaustive analysis by reasoning about all possible execution of the system model. Secondly, its underlying model is partially ordered set and it is not expressive enough to handle these models with explicit choice structures or conflicts. Because all the runtime traces do not contain any conflict information, it is not convenient to analyze the system under construction statically.In this paper, we extend the notion of computation slicing from partial order traces to prime event structures with conflict. We propose a more general event structure slicing notion and a complete mathematical theoretical framework for computing the event structure slices.The main idea is that a prime event structure can be viewed as such a system model consisting of several conflict-free substructures. These substructures themselves are in mutual weak conflict. Any of such conflict-free event substructures of a prime event structure acts as a partial order execution trace which can be sliced by traditional computation slicing algorithm. Based on this idea, we propose a partition approach to decompose a prime event structure into a group of conflict-free substructures equivalently. Each of these substructures can be sliced with respect to a given slicing criterion by the existing slicing algorithm and we can get a set of the sliced substructures. We have proved that these sliced results can be composed together and yield a new prime event structure by a so-called weak choice composition operation. We have shown that the newly generated prime event structure is the slicing result of the original prime event structure. Meanwhile, based on above partition, we can detect structural symmetry property and make symmetric reduction on each substructure of the original system. In additional, we also investigate the relationship between the symmetric reduction model and the original one.The main contribution of our work can be summarized as follows. We introduced the slicing notion into the area of event structure and extended nonclassical computation slicing with conflict. We also proposed a unified mathematical framework as a common theory basis for event structure slicing and symmetry reduction. We also made a comparison between our event structure slicing and the traditional computation slicing and demonstrated the mathematical aspects of this framework.The rest of this paper is structured as follows. Related work is discussed in Section2. Section 3 introduces the notion of event structure and other basic definitions. Section 4 describes two core operators over event strictures. Slicing reduction derived from computation slicing will be discussed in Section 5. Symmetry reduction theory based on permutation group is reported in Section 6. The overall mathematical framework for event structure slicing and symmetry reduction will be provided in Section 7. In the last section, we make a short summary of our work.


## 2. Related Work

Regarding the slicing technique, the work in [5, 6] proposed classical program slice idea firstly by Weiser. Given a program and a set of variables, a program slice consists of all statements in the program that may affect the value of the variables in the set at some given point.During years after the program slice notion was proposed, a lot of work based on this notion had been performed. For example, in 1992, the notion of a slice has been also extended to distributed programs [9]. In 2000, the notion of a nonclassical computation slice, which is very similar to the concept of a program slice, has been proposed. In work [7, 10], computation slice over partial order traces was firstly investigated by Garg and Mittal, de Bakker et al. This computation slice notion is based on partial order traces model, which is a special case of event structure without conflict.Event structure, as an true concurrency model [11–16], can be taken as an extension of partial order model. In concurrency theory, event structures constitute a major branch of concurrent models. These were initially developed as a link between Petri nets and Scott domain theory [17] and have since been extensively applied as a semantic model for process algebras, for example [18].All the previous work [7, 8, 19, 20] does not consider the case with conflict. Compared with them, our work is aimed to extend this slicing notion to the area of event structure.On the other hand, as for symmetry reduction, the use of symmetry to reduce state space has been investigated widely by researchers. Technically speaking, symmetry in event structures [3, 4] is similar to symmetry in model checking [2, 21, 22]. In work [23], a category of event structures with symmetry was introduced and its categorical properties were investigated, while our work is relevant to the structural reduction via symmetry property over event structure model.In our previous work [24], we have extended this technique to event structure area. In this paper, we will further investigate the common basis for both slicing and symmetry reduction over event structures and provide a unified framework.


## 3. Event Structure and Basic Definitions

In this section, we will introduce the notion of prime event structure [11, 17, 25, 26] and the basic definitions we use throughout the paper. The prime event structure is firstly defined and other related key notions are introduced. Moreover, we focus on finite prime event structures only.Definition 1 (prime event structure).
Aprime event structure (over an alphabet A, a set of actions) is a 4-tuple structure (
E
,
⪯
,
♯
,
l
) with (i)
E, a finite set of events;
(ii)
⪯
⊆
E
×
E, a partial order, the causality relation, satisfying the principle of finite causes: for all e
∈
E
:
{
e
′
∈
E
∣
e
′
⪯
e
} is finite and the inverse of ⪯ is denoted by ⪯
-
1;
(iii)
♯
⊆
E
×
E, the (irreflexive and symmetric) conflict relation, satisfying the principle of conflict inheritance: ∀
d
,
e
,
f
∈
E
:
d
⪯
e
∧
d
♯
f
⇒
e
♯
f;
(iv)
l
:
E
→
A, the action-labelling function.A prime event structure (for short, an event structure) represents a system in the following way: the action names are activities which the system may perform, an event labelleda
∈
A stands for a particular occurrence of an action, e
a
⪯
e
b indicates that a cannot occur before b has, and e
c
♯
e
d indicates that actions c and d can never occur together in one run.The conflict inheritance property states that if an evente is in conflict with some event f, then it is in conflict with all causal successors of f.From the causality relation, it is not difficult to derive a notion ofcausal independence:
(1)
e
cod
⟺
¬
(
e
=
d
∨
e
⪯
d
∨
e
⪯
-
1
d
∨
e
♯
d
)
.LetE denote the domain of prime event structures labelled over A and ∅
=
(
∅
,
∅
,
∅
,
∅
) stand for the empty event structure. Generally, the components of an event structure E will be denoted by E
E
,
⪯
E
,
♯
E, and l
E, respectively. More specifically, E
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
). If clear from the context, the index will be omitted; that is, E
=
(
E
,
⪯
,
♯
,
l
) is also a valid form.Additionally, forX
⊆
E
E, the restriction of E to X can be defined as E
|
X
=
(
X
,
⪯
E
∩
(
X
×
X
)
,
♯
E
∩
(
X
×
X
)
,
l
E
|
X
). Let Succ
(
e
) denote all causal successors of an event e; that is, Succ
(
e
)
=
{
a
∈
E
E
∣
e
⪯
E
a
,
e
∈
E
E
}.Definition 2 (event substructure).
LetE
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E and E
'
=
(
E
E
'
,
⪯
E
′
,
♯
E
′
,
l
E
′
)
∈
E be event structures; E
' is called asubstructure of E (denoted by E
'
⊲
E) if and only if (i)
E
E
′
⊆
E
E;
(ii)
for alle
,
e
′
∈
E
E
,
e
♯
E
'
e
′
⇔
e
,
e
′
∈
E
E
'
∧
e
♯
E
e
′;
(iii)
for alle
,
e
′
∈
E
E
,
e
⪯
E
′
e
′
⇔
e
,
e
′
∈
E
E
′
∧
e
⪯
E
e
′.Definition 3 (conflict-free event structure).
An event structureE
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E is calledconflict-free event structure (denoted by c
f
E
S, for short) if and only if its conflict relation is empty; that is, ♯
E
=
∅.LetF denote the domain of conflict-free prime event structures.In order to characterize the conflict relationship between two conflict-free event structures (or substructures of a prime event structure), we introduce the following basic definitions: strong conflict, weak conflict, and weak conflict event structure set (for short, weak conflict set).Definition 4 (strong conflict).
LetF
1
=
(
E
F
1
,
⪯
F
1
,
∅
,
l
F
1
)
∈
F and F
2
=
(
E
F
2
,
⪯
F
2
,
∅
,
l
F
2
)
∈
F. The conflict relation between E
1
(
E
1
⊆
E
F
1 and  E
1
≠
∅
) and E
2
(
E
2
⊆
E
F
2 and  E
2
≠
∅
) is calledstrong conflictif and only if for all e
∈
E
1, f
∈
E
2
:
e
♯
f, denoted by E
1
♯
s
E
2. F
1 and F
2 are calledstrong conflict if and only if their event sets are in mutually strong conflict, that is, for all F
1
,
F
2
∈
F
:
F
1
♯
s
F
2
⇔
E
F
1
♯
s
E
F
2, denoted by F
1
♯
s
F
2.More generally, for anyE
1
∈
E and E
2
∈
E, the relation between nonempty E
1
′
(
∅
≠
E
1
′
⊆
E
E
1
) and E
2
′
(
∅
≠
E
2
′
⊆
E
E
2
) is calledextended strong conflict if and only if for all e
∈
E
1
′, f
∈
E
2
′
:
e
♯
f, denoted by E
1
′
♯
x
s
E
2
′. That is, each of E
1
′ is in conflict with each of E
2
′ and the existence of conflict relation in E
1
′ or E
2
′ is allowed.Definition 5 (weak conflict).
LetF
1
=
(
E
F
1
,
⪯
F
1
,
∅
,
l
F
1
)
∈
F and F
2
=
(
E
F
2
,
⪯
F
2
,
∅
,
l
F
2
)
∈
F. The conflict relation between event sets E
1
(
E
1
⊆
E
F
1 and  E
1
≠
∅
) and E
2
(
E
2
⊆
E
F
2 and  E
2
≠
∅
) is calledweak conflict if and only if ∃
e
∈
E
1
,
∃
f
∈
E
2
:
e
♯
f, denoted by E
1
♯
w
E
2. The conflict-free event structures, F
1 and F
2, are calledweak conflict if and only if their event sets are in weak conflict; that is, for all F
1
,
F
2
∈
F
:
F
1
♯
w
F
2
⇔
E
F
1
♯
w
E
F
2, denoted by F
1
♯
w
F
2.Stated in words, it is not that each event ofE
F
1 is in conflict with each event of E
F
2, but there exists at least one conflicting event pair between E
F
1 and E
F
2.Basically, according to the previous definitions, strong conflict relation is a special case of weak conflict relation.Definition 6 (weak conflict set).
LetW
F
n
c
f
w
=
{
F
i
∈
F
∣
i
,
n
∈
N
,
1
≤
i
≤
n
} over event set E
W
F, W
F
n
c
f
w is called aweak conflict set if and only if E
W
F
=
⋃
i
=
1
n
E
F
i and for all F
i
,
F
j
∈
W
F
n
c
f
w
:
i
≠
j
⇒
F
i
♯
w
F
j
(
i
,
j
∈
N
,
1
≤
i
≤
n
).For convenience, letw
f
s
e
t
F
(
W
F
n
c
f
w
)
=
{
E
F
i
∣
i
∈
N
,
1
≤
i
≤
n
} denote the family of weak conflict event sets.Definition 7 (maximal conflict-free event substructure).
LetE
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E be an event structure; any event subset E
′
⊆
E
E is called amaximal conflict-free event subset (for short, mcfset) of E
E if and only if it satisfies the following: (1)
for alle
,
f
∈
E
′
:
¬
(
e
♯
f
);
(2)
for allc
∈
(
E
E
-
E
′
)
:
∃
d
∈
E
′
⇒
c
♯
d.Its corresponding substructureE
' is calledmaximal conflict-free event substructure of E; that is, E
'
=
(
E
′
,
≤
E
∩
(
E
′
×
E
′
)
,
∅
,
l
E
′
).


## 4. Operators over Event Structure

In this section, a pair of mutually inverse operators,c
f
p (conflict-free partition) and w
c
c (weak conflict composition), will be introduced and discussed. For any prime event structure E, partition and composition operation over it can be associated via its family of configurations.


### 4.1. Maximal Conflict-Free Partition

In fact, a prime event structure can be viewed as a system consisting of several substructures, which are conflict-free themselves. Such a conflict-free event substructure of a prime event structure represents a specific possible partial order execution trace via branching or nondeterministic choices. For any prime event structure, it is a certainty that we can get its maximal conflict-free substructures by some kind of conflict-free partition operation according to the characteristics of its conflict relation.First of all, we give the definition of maximal conflict pattern for an event structure. The notion of maximal conflict pattern can make great contributions to accelerate the process of partition by avoiding unnecessary partition steps. We then provide the key partition algorithm for a prime event structure.Definition 8 (maximal conflict pattern).
LetE
=
(
E
E
,
≤
E
,
♯
E
,
l
E
)
∈
E; for any A
⊆
E
E and B
⊆
E
E, A
♯
x
s
B is called amaximal conflict patternif and only if for all A
′
⊆
E
E, for all B
′
⊆
E
E
:
(
A
⊂
A
′
∧
B
⊂
B
′
)
⇒
¬
(
A
′
♯
x
s
B
′
).For any prime event structure, we can get these maximal conflict patterns by the following two steps:(1)
casual successors expanding;
(2)
conflict pairs merging.Firstly, due to the conflict inheritance property, we know that if evente is in conflict with event f then their casual successors are also in mutual conflict; that is, ∀
c
∈
Succ
(
e
)
,
∀
d
∈
Succ
(
f
)
:
e
♯
f
⇒
c
♯
d.Let{
e
}
♯
=
{
e
}
∪
Succ
(
e
) and {
f
}
♯
=
{
f
}
∪
Succ
(
f
); we have that {
e
}
♯ and {
f
}
♯ are in strong conflict if e
♯
E
f; namely, ∀
e
,
f
∈
E
E
:
e
♯
E
f
⇒
{
e
}
♯
♯
s
{
f
}
♯.For example, for a prime event structureE, if c
♯
E
d and casual relations are c
⪯
E
e
1
,
c
⪯
E
e
2,d
⪯
E
f
1
,
f
1
⪯
E
f
2, and d
⪯
E
f
3, we then have {
c
,
e
1
,
e
2
,
}
♯
s
{
d
,
f
1
,
f
2
,
f
3
}.We also have that any nonempty subset of{
e
}
♯ and any nonempty subset of {
e
}
♯ are also in strong conflict.Consider a prime event structureE
∈
E whose conflict relation has l
(
l
∈
N
) conflict pairs. Expand each conflict relation with its successors according to the conflict inheritance property and we can get full conflict relation pairs: {
e
1
}
♯
♯
s
{
f
1
}
♯
,
…
,
{
e
l
}
♯
♯
s
{
f
l
}
♯; here, e
i
♯
E
f
i
,
e
i
∈
E
E
,
f
i
∈
E
E
(
i
∈
N
,
1
≤
i
≤
l
).Secondly, for such a group of full conflict relation pairs obtained by the above steps, there may exist common elements among some pairs that can be merged together and form a maximal conflict pattern. For example, eventse
1
,
e
2
,
e
3, and e
4 are mutually in conflict; we have six immediate conflict relation pairs: {
e
1
}
♯
s
{
e
2
}, {
e
1
}
♯
s
{
e
3
}, {
e
1
}
♯
s
{
e
4
}, {
e
2
}
♯
s
{
e
3
}, {
e
2
}
♯
s
{
e
4
}, and {
e
3
}
♯
s
{
e
4
}.From the principle of permutation, we then have three maximal conflict patterns by merging conflict pairs:{
e
1
}
♯
x
s
{
e
2
,
e
3
,
e
4
}, {
e
2
}
♯
x
s
{
e
3
,
e
4
}, and {
e
3
}
♯
x
s
{
e
4
}. Equivalently, {
e
4
}
♯
x
s
{
e
1
,
e
2
,
e
3
}, {
e
3
}
♯
x
s
{
e
1
,
e
2
}, and {
e
2
}
♯
x
s
{
e
1
} are also the valid maximal conflict patterns.Assume that there arem
∈
N maximal conflict patterns after expanding and merging which are I
♯
E
1
:
A
1
♯
x
s
B
1
,
…
,
I
♯
E
m
:
A
m
♯
x
s
B
m, respectively.Here,I
♯
E
i
:
A
i
♯
x
s
B
i denotes the ith pattern, and ∀
e
∈
A
i
⊆
E
E
,
∀
f
∈
B
i
⊆
E
E
:
e
♯
E
f
(
i
∈
N
,
1
≤
i
≤
m
).IfA
i
♯
x
s
B
i, then any nonempty subset of A
i and any nonempty subset of B
i are also in extended strong conflict.For any event setD, let D
^ denote any nonempty subset of D
(
∅
≠
D
^
⊆
D
); correspondingly, I
♯
E
i
^
:
A
i
^
♯
x
s
B
i
^ denotes a conflict subpattern of I
♯
E
i
(
i
∈
N
,
1
≤
i
≤
m
).Formally,I
'
:
A
′
♯
x
s
B
′ is called aconflict subpattern of I
:
A
♯
x
s
B if and only if (
∅
≠
A
′
⊆
A
)
∧
(
∅
≠
B
′
⊆
B
), denoted by I
'
⊆
pattern
I (or I
⊇
pattern
I
'). Otherwise, I
'
⊈
pattern
I (or I
⊉
pattern
I
').LetP
E
=
{
I
♯
E
i
:
A
i
♯
x
s
B
i
∣
i
∈
N
,
1
≤
i
≤
m
} denote the maximal conflict pattern set of an event structure E.For any prime event structure, it is a certainty that we can get its maximal conflict-free substructures by some kind of conflict-free partition operation according to its conflict relation characteristics:maximal  conflict  patterns. Thus, we have the following theorem for partition.Theorem 9.
For any prime event structure, its maximal conflict-free partition exists and the partition result is unique.Proof. (1) Existence. The proof is constructive.If there is no conflict inE
E, then E
E itself is the maximal conflict-free event subset of E. Otherwise, for any nonempty event subset E
(
E
⊆
E
E
∧
E
≠
∅
), and there exists such maximal conflict pattern I
♯
E
i
:
A
i
♯
x
s
B
i
(
i
∈
N
,
1
≤
i
≤
m
) that (
A
i
^
∪
B
i
^
)
⊆
E.In order to make a subsetE
′ of E
(
E
′
⊆
E
) become conflict-free with respect to the conflict relation: A
i
♯
x
s
B
i, that is, eliminate this conflict relation from its all subsets, we have known that if A
i
^
⊆
E
′ (or B
i
^
⊆
E
′), then there should be B
i
⊈
E
′(or A
i
⊈
E
′); otherwise, the I
♯
E
i conflict pattern will still exist in its subsets.By greedy policy, letA
i
′ and B
i
′ be both maximal inclusion subsets with respect to E calculated by A
i
′
=
maxincl
(
A
i
,
E
) and B
i
′
=
maxincl
(
B
i
,
E
), respectively. This means the current event set E will be partitioned into two parts by this maximal conflict subpattern: one part is (
E
-
A
i
′
), and the other is (
E
-
B
i
′
). Certainly, there exists no I
♯
E
i conflict relation between (
E
-
A
i
′
) and (
E
-
B
i
′
) any more. If there does not exist any conflict in (
E
-
B
i
′
) (or (
E
-
A
i
′
)), then (
E
-
B
i
′
) (or (
E
-
A
i
′
)) is one conflict-free event subset of E
E.Otherwise, apply the next maximal conflict patternI
♯
E
i
+
1
(
i
∈
N
,
1
≤
i
≤
m
) to all the previously obtained event subsets in the same manner. This partition process is continued until no conflict exists.As we know, if each pattern of the maximal conflict patterns set has been applied just once by the above manner, then any consequent subset will be conflict-free and the partition process will stop. Meanwhile, there are2
m conflict-free subsets at most.Because intersection ofx
i and y
i
(
x
,
y
∈
{
A
,
B
}
,
i
≠
j
,
1
≤
i
,
j
≤
m
) can be nonempty, thus the partition tree is not yet a full binary tree and set inclusion among these solution nodes is allowed. If some subsets are included by others, then they will be removed until every result subset cannot be included by others. It is not difficult to verify that every consequent subset is maximal and conflict-free. Exploiting these expanded fully conflict patterns to partition the event set E
E step by step, we will eventually get all maximal conflict-free event subsets. That is, there exists a practical algorithm to implement the partition operation. Without loss of generality, let ⊘
A denote such partition for the time being.(2) Uniqueness. Assume we have m
c
f
s
e
t
N
A
(
E
) distinct maximal conflict-free event subsets in total by partition ⊘
A. These subsets form a set of m
c
f
s
e
t
s, denoted by R
A
=
{
A
1
,
A
2
,
…
,
A
n
∣
n
=
m
c
f
s
e
t
N
A
(
E
)
}.We might as well assume there is another partition⊘
B that generates the result set R
B
=
{
B
1
,
B
2
,
…
,
B
m
∣
m
=
m
c
f
s
e
t
N
B
(
E
)
} which is also a set of m
c
f
sets.Consider any element ofR
B; let B
i
(
1
≤
i
≤
m
,
i
∈
N
) denote it. The relationship between an element A
j
(
1
≤
j
,
k
≤
m
c
f
s
e
t
N
A
(
E
)
,
j
,
k
∈
N
) in R
A and B
i satisfies the following.(1)
∃
A
j
∈
R
A
:
A
j
⊂
B
i
⊆
E
E.
Since∀
A
k
∈
R
A
,
k
≠
j
:
A
j
♯
w
A
k, then ∀
A
k
∈
R
A
,
k
≠
j
:
B
i
♯
w
A
k. We have known that A
j
∈
R
A is maximal, and now event subset B
i is also a subset of E
E and is in weak conflict with other event subsets except A
i. Moreover, B
i includes A
i. This case leads to a contradiction.
(2)
∃
A
j
∈
R
A
:
B
i
⊂
A
j
⊆
E
E.
The proof is similar to the above case (1). This case also leads to a contradiction.
(3)
∀
A
j
∈
R
A
:
A
j
≠
B
i.
(3.1)
∀
A
j
∈
R
A
:
A
j
♯
w
B
i.
SinceB
i is also a subset of E
E, thus, R
A
′
=
{
A
1
,
A
2
,
…
,
A
n
,
B
i
∣
n
=
m
c
f
s
e
t
N
A
(
E
)
} is a valid set of m
c
f
s
e
t
s. There are n
+
1 subsets in this partition ⊘
A. This is in contradiction with that there are n
(
n
=
m
c
f
s
e
t
N
A
(
E
)
) subsets in R
A.
(3.2)
∃
A
j
∈
R
A
:
¬
(
A
j
♯
w
B
i
).
Since∀
A
k
∈
R
A
,
k
≠
j
:
A
j
♯
w
A
k, then ∀
A
k
∈
R
A
,
k
≠
j
:
(
A
j
∪
B
i
)
♯
w
A
k; that is, R
A
′′
=
{
A
1
,
A
2
,
…
,
{
A
j
∪
B
i
}
,
…
,
A
n
,
∣
n
=
m
c
f
s
e
t
N
A
(
E
)
} is a valid set of m
c
f
s
e
t
s. A
j
(
A
j
∈
R
A
) is maximal; moreover, A
j
⊂
(
A
j
∪
B
i
)
∈
R
A
′′ is maximal too. This leads to a contradiction.
(3.3)
∀
A
j
∈
R
A
:
¬
(
A
j
♯
w
B
i
).
The proof is similar to the above case (3.2). This case also leads to a contradiction.Therefore, we are forced to have only∃
A
j
∈
R
A
:
A
j
=
B
i; that is, any element in R
B is also an element in R
A; we get R
B
⊆
R
A; in the same manner, we will get R
A
⊆
R
B. Thus, we have R
B
=
R
A.This establishes the uniqueness and also implies the partition result is independent of partition order or conflict pattern.Therefore, we have the conclusion.AssumeE
∈
E has m
c
f
s
e
t
N
(
E
)
∈
N
m
c
f
E
S
s in total. Here, let N
E
=
m
c
f
s
e
t
N
(
E
) (N
E, for short) denote total amount of m
c
f
E
S
s, E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) denote the ith maximal conflict-free event substructure, and E
E
i
max
⁡ denote the event set of E
i
max
⁡.Then the result set can be represented asB
m
c
f
E
S
(
E
)
=
{
E
i
max
⁡
∣
i
∈
N
,
1
≤
i
≤
N
E
}.In fact, everyE
i
max
⁡
(
i
∈
,
1
≤
i
≤
m
c
f
s
e
t
N
(
E
)
) of the original prime event structure represents a specific possible execution choice in a system run. We might as well let c
f
p denote such an operator. Then, we have the following definition of this partition operator.Definition 10 (conflict-free partition).
An operatorc
f
p is calledconflict-free partition operator for E
∈
E if and only if B
m
c
f
E
S
(
E
)
=
c
f
p
(
E
).According to our previous discussion, we have C-like pseudocode descriptions: Algorithm1 for c
f
p.Algorithm 1:Conflict-free partition: c
f
p.
Input: a prime event structure: E;
Output: the set of m
c
f
E
S
s: B
m
c
f
E
S
(
E
);
BEGIN
(1)
C
=
∅
;
i
n
t
i
=
1
;
i
n
t
n
=
0
;
R
=
∅;
(2)
S
Q
=
E
n
t
e
r
Q
u
e
u
e
(
E
E
,
1
);
/* Initialize the Queue */
(3)if (I
s
C
o
n
f
l
i
c
t
F
r
e
e
(
E
E
)){
(5)C
=
∪
{
E
};
(6)  GotoBUILDES;
(7)} /* end if; */
/* Expand and merge each conflict pair and build maximal conflict patterns:
{
I
#
E
i
:
A
i
#
x
s
B
i
∣
i
∈
,
1
≤
i
≤
m
}; */
(8)for (i
=
1
;
i
≤
m
;
i++) { /* do */
(9)  Select a partition pattern:I
#
E
i
:
A
i
#
x
s
B
i;
(10) /* Current level isi, apply I
#
E
i, otherwise, skip while loop to the next one: i++; */
(11)while (!
E
m
p
t
y
Q
u
e
u
e
(
S
Q
)  &
&
i
=
=
V
a
r
Q
u
e
u
e
(
S
Q
,
L
E
V
E
L
)) {
/* Get the head of the Queue: event set */
(12)E
=
O
u
t
Q
u
e
u
e
(
S
Q
,
E
V
E
N
T
);
(13)A
i
′
=
m
a
x
i
n
c
l
(
A
i
,
E
);
(14)B
i
′
=
m
a
x
i
n
c
l
(
B
i
,
E
);
(15)E
1
=
(
E
-
A
i
′
);
(16)E
2
=
(
E
-
B
i
′
);
/*E
1 is a conflict-free subset; */
(17)if (I
s
C
o
n
f
l
i
c
t
F
r
e
e
(
E
1
)) {
(18)
C
=
C
∪
{
E
1
};
/* Remove these elements included in others; */
(19)R
e
m
o
v
e
I
n
c
l
u
d
e
d
E
l
e
m
e
n
t
(
C
);
(20)  }else{
/* Continue next partition by the conflict pattern: I
#
E
i
+
1; */
(21)  S
Q
=
E
n
t
e
r
Q
u
e
u
e
(
E
1
,
i
+
1
);
(22)  } /* end if */
(23)  if (I
s
C
o
n
f
l
i
c
t
F
r
e
e
(
E
2
)) {
(24)C
=
C
∪
{
E
2
};
(25)R
e
m
o
v
e
I
n
c
l
u
d
e
d
E
l
e
m
e
n
t
(
C
);
(26)  }else{
(27)S
Q
=
E
n
t
e
r
Q
u
e
u
e
(
E
2
,
i
+
1
);
(28)  } /* end if */
(29)  } /* end while */
(30) } /* end for */
(31)BUILDES: /* Build the sub-structure: F
=
(
E
F
,
⪯
F
,
#
F
,
l
F
)  */
(32)  while (¬
I
s
E
m
p
t
y
(
C
)) {
(33) Select a conflict-free event subset A
!
# from C;
(34) E
F
=
A
!
#;
(35) #
F
=
∅;
(36) ⪯
F
=
⪯
E
∩
(
A
!
#
×
A
!
#
);
(37) l
F
=
l
|
A
!
#;
(38) C
=
C
-
{
A
!
#
};
(39) R
=
R
∪
F; n++;
(40) } /* end while */
(41)m
c
f
s
e
t
N
(
E
)
=
n;
(42) returnR;
END;


### 4.2. Family of Configurations

In general, the behavior of an event structure is described by its configurations which are sets of events with certain properties. In other words, a configuration is a set of events that have happened during a specific run of the event structure.We will review the basic definition of configuration in the following section. More detailed information can be found in [26].Definition 11 (configuration).
LetX be a subset of X
⊆
E
E of a prime event structure E
∈
E; then X is called aconfiguration of E if and only if (1)
X is left-closed if and only if ∀
c
,
d
∈
E
,
d
∈
X
∧
c
≤
d
⇒
c
∈
X.
(2)
X is conflict-free if and only if ∀
e
,
f
∈
X
:
¬
(
e
♯
E
f
).A configuration can also be viewed as a global state where all events in the configuration have occurred. The configuration of the event structure should be conflict-free because conflicting events can never happen in a system run. In addition, all casual predecessors of an event in a configuration should be contained in this configuration too; that is, configuration should be downwards closed; otherwise this event could not have happened at all.That is, a subsetX is a (finite) configuration of E if and only if it is finite, left-closed, and conflict-free.The semantics of a prime event structure is defined as the family of its configurations ordered by set inclusion. LetC
o
n
f
F
(
E
) denote the family of all configurations of event structure E, which forms an ordered set (called prime algebraic coherent partial order; see [16]) by inclusion; that is, (
C
o
n
f
F
(
E
)
,
⊆
) is partial order.Definition 12.
A configurationX
∈
Conf
F
(
E
) is calledcomplete or (successfully)terminated if and only if ∀
d
∈
E
:
d
∉
X
⇒
∃
e
∈
X
:
e
♯
d. A configuration X
∈
C
o
n
f
F
(
E
) is calledmaximal if and only if ∀
Y
∈
Conf
F
(
E
)
:
X
⊄
Y.For any prime event structureE, a configuration of E is maximal if and only if it is complete. Obviously, for any maximal configuration of a prime event structure, there exists a corresponding maximal conflict-free substructure set. An empty or initial configuration, denoted by ∅
Conf
F
∈
Conf
F
(
E
), represents the initial state in which there is no event happened.In general, initial configuration and complete configuration are also called trivial configurations, while others are called nontrivial configurations.Similarly, we have the following configuration definition for conflict-free event structure.Definition 13 (configuration ofc
f
E
S).
LetF
=
(
E
F
,
⪯
F
,
∅
,
l
F
) be a c
f
E
S and let Z be a subset of E
F
(
Z
⊆
E
F
); then Z is called a configuration of F if and only if Z is left-closed; that is, ∀
c
,
d
∈
E
F
,
d
∈
Z
∧
c
⪯
d
⇒
c
∈
Z.SinceF
∈
F, its event subset is evidently conflict-free.Letc
f
Conf
F
(
F
) denote the family of all configurations of conflict-free event structure F. Clearly, when F is the ith m
c
f
E
S: E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of prime event structure E
∈
E, its family of all configurations is denoted by m
c
f
Conf
F
(
E
i
max
⁡
).Definition 14 (subfamily of configurations).
LetF
∈ be a c
f
E
S and let Ω
(
∅
≠
Ω
⊆
E
F
) be a nonempty event subset; a subfamily of configurations of F with respect to event subset Ω is the family of configurations of its event substructure F
|
Ω
=
(
Ω
,
≤
F
∩
(
Ω
×
Ω
)
,
∅
,
l
Ω
) restricted by event subset Ω; that is, c
f
subConf
F
(
F
,
Ω
)
≜
c
f
Conf
F
(
(
Ω
,
≤
F
∩
(
Ω
×
Ω
)
,
∅
,
l
Ω
)
).Clearly, for anym
c
f
E
S
E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of event structure E
∈
E, its subfamily of configurations with respect to event subset Ω
(
∅
≠
Ω
⊆
E
E
,
i
max
⁡
) is denoted by m
c
f
subConf
F
(
E
i
max
⁡
,
Ω
)
≜
m
c
f
Conf
F
(
(
Ω
,
≤
E
i
max
⁡
∩
(
Ω
×
Ω
)
,
∅
,
l
Ω
)
) for convenience.Lemma 15.
The relation between the family of configurations of a prime event structure and that of itsm
c
f
E
S
s can be described by C
o
n
f
F
(
E
)
=
⋃
1
≤
i
≤
N
E
(
m
c
f
C
o
n
f
F
(
E
i
max
⁡
).Proof. To prove the result of this lemma, we will show that
(2)
⋃
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
)
⊆
Conf
F
(
E
)
,
Conf
F
(
E
)
⊆
⋃
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
)
both hold.(1)“⊆”. For any configuration X
∈
Conf
F
(
E
), since X is a configuration, by definition, X should be conflict-free. Thus X should be the subset of one of the maximal configurations. Otherwise, if X is greater than any maximal configuration, then X must contain mutual conflicting events; that is impossible.Therefore, we have that there must exist a maximal configuration which containsX. Such a maximal configuration corresponds to a maximal conflict-free event subset: E
E
i
max
⁡
∈
(
i
∈
N
,
1
≤
i
≤
N
E
); that is, X must be the element of m
c
f
Conf
F
(
E
i
max
⁡
); that is, X
∈
m
c
f
Conf
F
(
E
i
max
⁡
). We have Conf
F
(
E
)
⊆
⋃
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
).(2)“⊇”. For any configuration X
∈
m
c
f
Conf
F
(
E
i
max
⁡
)
(
i
∈
N
,
1
≤
i
≤
N
E
), of course, X
∈
⋃
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
); this implies X
⊆
E
E
i
max
⁡ and E
E
i
max
⁡
⊆
E
E; therefore, we get X
⊆
E
E. Since X is a configuration, it is also a configuration of E; that is, X
∈
C
o
n
f
F
(
E
).We have∪
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
)
⊆
Conf
F
(
E
).Therefore, from (1) and (2), we have the result.


### 4.3. Domains of Configurations

In this section, we will discuss the concept of domain from the point of view that computation states are taken as such subsets and progress in a computation is measured by the occurrence of more events.Firstly, we will recall some related conceptions regarding domain [16, 27]. Then, some important facts will be discussed.Definition 16 (least upper bound).
LetD
=
(
D
,
⊑
) be a partial order; an element d
∈
D is calledleast upper bound of subset X (X
⊆
D), denoted by d
=
⊔
X, if and only if (
∀
x
∈
X
:
x
⊑
d
)
∧
(
∀
d
′
∈
D
:
(
∀
x
∈
X
:
x
⊑
d
′
)
⇒
d
⊑
d
′
).Definition 17 (coherent).
LetD
=
(
D
,
⊑
) be a partial order; two elements x
,
y
∈
D are calledconsistent (denoted by x
↑
y) if and only if ∃
z
∈
D
:
x
⊑
z
∧
y
⊑
z; a subset X
⊆
D ispairwise consistent if and only if any two of its element have an upper bound in D; that is, ∀
x
,
y
∈
X
:
x
↑
y; (
D
,
⊑
) is calledcoherent if and only if every pairwise consistent subset X (X
⊆
D) has a least upper bound ⊔
X.
Theconsistency relation of x and y is denoted by x
↑
y; conversely,inconsistency is denoted by x
↑
y.Definition 18 (complete prime).
A partial orderD
=
(
D
,
⊑
); an element is acomplete prime if and only if for every finite subset X
⊆
D, if ⊔
X exists and p
⊆
⊔
X then there exists an x
∈
X such that p
⊑
x (i.e., p
⊑
⊔
X
⇒
∃
x
∈
X
.
p
⊑
x
).LetP
(
D
) denote the set of complete prime of (
D
,
⊑
).Definition 19 (prime algebraic).
A partial orderD
=
(
D
,
⊑
) is calledfinitary if and only if ∀
p
,
d
∈
P
(
D
)
:
{
d
∈
D
∣
d
⊑
p
} is finite. (
D
,
⊑
) is calledprime algebraic if and only if P
(
D
) is countable and ∀
d
∈
D
:
d
=
⊔
{
p
∈
P
(
D
)
∣
p
⊑
d
}.
Namely,D is calledprime algebraic if and only if, for every element d
∈
D, ⊔
D
d exists (define ⊔
D
d
=
{
p
⊑
d
∣
p
is
a
complete
prime
}
), and d
=
⊔
D
d.Definition 20 (domain).
A coherent, prime algebraic, and finitary partial order is called aScott domain (or simply adomain).Definition 21.
LetD
=
(
D
,
⊑
) be acoherent, finitary prime algebraic domain. Define P
r
[
D
]
=
(
P
(
D
)
,
⪯
,
♯
), where P
(
D
) consists of the complete primes of D:(1)
∀
p
,
p
′
∈
P
(
D
)
:
p
⪯
p
′
⇔
p
⊑
p
′;
(2)
∀
p
,
p
′
∈
P
(
D
)
:
p
♯
p
′
⇔
p
↑
p
′.Definition 22.
LetD
=
(
D
,
⊑
) be aprime algebraic complete lattice. Define P
r
[
D
]
=
(
P
(
D
)
,
⪯
), where P
(
D
) consists of the complete primes of D, ∀
p
,
p
′
∈
P
(
D
)
:
p
⪯
p
′
⇔
p
⊑
p
′.Theorem 23.
LetE
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E; then (
C
o
n
f
F
(
E
)
,
⊆
) is a finitary coherent prime algebraic domain; the complete primes are the set {
a
∈
E
E
∣
a
⪯
e
,
e
∈
E
E
} (see [25]).Theorem 24.
Let(
D
,
⊑
) be a finitary coherent prime algebraic domain. Then, P
r
[
D
]
=
(
P
(
D
)
,
⪯
,
♯
) is a prime event structure, with φ
:
(
D
,
⊑
)
≅
(
C
o
n
f
F
(
P
r
[
D
]
)
,
⊆
) giving an isomorphism of partial orders where φ
(
d
)
=
{
p
⊑
d
∣
p
is
a
complete
prime
} with inverse λ
:
C
o
n
f
F
(
P
r
[
D
]
)
→
(
D
,
⊑
) given by λ
(
x
)
=
⊔
x (see [16]).Evidently, event structures and coherent, finitary prime algebraic domains are equivalent; one can be used to represent the other.The following theorem describes the important property of family of configurations of a prime event structure.Theorem 25.
For any nonemptym
c
f
E
S: E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of event structure E
∈
E, its family of configurations (
m
c
f
C
o
n
f
F
(
E
i
max
⁡
)
,
⊆
) is prime algebraic complete lattice. Its complete primes are those elements of the form {
a
∈
E
E
i
max
⁡
∣
a
⪯
e
,
e
∈
E
E
i
max
⁡
}.Proof. The proof is straightforward.Thus prime event structure and finitary coherent prime algebraic domain are equivalent; this implies that there is a one-to-one correspondence between a prime event structure and its family of configurations; one can be used to represent the other.


### 4.4. Weak Choice Composition

Theorem23 describes an important property between the domains of configurations of prime event structures and the prime event structures themselves.We can obtain a full set ofm
c
f
E
S
s from a prime event structure by applying c
f
p operator over it. Conversely, given a full set of m
c
f
E
S
s of an event structure, we can certainly recover the original event structure that generates this set of m
c
f
E
S
s by some kind of composition operation.Further, for any weak conflict set, we give the constraint conditions, under which this weak conflict set can be composed together and form a prime event structure that can generate this set by conflict-free partition operation.The following theorem discusses the constraint conditions for composition.Theorem 26 (necessary and sufficient condition for composition).
For any weak conflict setW
F
n
c
f
w
=
{
F
i
∈
F
∣
i
,
n
∈
N
,
1
≤
i
≤
n
}, if it satisfies the following conditions: (1) and (2), then there exists a unique prime event structure E
∈
E
prime that can generate this set by c
f
p partition operation; that is, W
F
n
c
f
w
=
c
f
p
(
E
).(1)
∀
F
i
,
F
j
∈
W
F
n
c
f
w
:
Ω
=
(
E
F
i
∩
E
F
j
)
∧
(
Ω
≠
∅
)
⇒
c
f
subConf
F
(
F
i
,
Ω
)
=
c
f
subConf
F
(
F
j
,
Ω
)  (
i
,
j
∈
N
,
i
≠
j
,
1
≤
i
≤
n
).
(2)
(
⋃
i
=
1
n
c
f
Conf
F
(
F
i
)
,
⊆
)
is a finitary coherent prime algebraic domain.Proof. On one hand, the intersection of event sets of any two c
f
E
S
s is nonempty meaning that common events have happened from both event structures. By definition, if these events represent common global states in runs of a system described by the same prime event structure with multiple choices, they should behave identically. That is, their configurations with respect to the intersection of event set should be identical.In addition, from Theorems23 and 24, the family of configurations of a prime event structure ordered by set inclusion should be a finitary coherent prime algebraic domain.Thus, we have the necessary condition for composition.On the other hand, from Theorems23 and 24, we have that there is a one-to-one correspondence between a prime event structure and its family of configurations. Given a valid family of configurations for prime event structure, then there should exist a corresponding prime event structure.For any weak conflict set:W
F
n
c
f
w
=
{
F
i
∈
F
∣
i
,
n
∈
,
1
≤
i
≤
n
}, if all c
f
C
o
n
f
F
(
F
i
) by joining can form a valid family of configurations for a prime event structure, that is, ⋃
1
≤
i
≤
n
c
f
C
o
n
f
F
(
F
i
) forms a ordered by set inclusion, then there should exist such a unique prime event structure E that C
o
n
f
F
(
E
)
=
⋃
1
≤
i
≤
n
c
f
C
o
n
f
F
(
F
i
).Therefore, we get the necessary and sufficient condition for composition.Obviously, the setB
m
c
f
E
S
(
E
) of a prime event structure satisfies the above condition. Clearly, this implies that there must exists a composition operation which can construct the target event structure E from a weak conflict set that satisfies the constraint conditions. We may as well let w
c
c denote the operator. Thus, we have the following definition.Definition 27 (weak choice composition (w
c
c operator)).
LetW
F
n
c
f
w be a weak conflict set, which satisfies necessary and sufficient conditions for composition; an operator w
c
c is calledweak choice composition operator if and only if the result event structure R
=
w
c
c
(
W
F
n
c
f
w
) and R satisfies the following: (1)
Conf
F
(
R
)
=
(
⋃
i
=
1
n
c
f
Conf
F
(
F
i
)
,
⊆
);
(2)
W
F
n
c
f
w
=
c
f
p
(
R
).The following theorem states that the operatorw
c
c and c
f
p are mutually inverse for a prime event structure.Theorem 28.
For anyE
∈
E
,
E
=
w
c
c
(
c
f
p
(
E
)
) holds.Proof. The proof is straightforward.Obviously, it is not difficult to derive an algorithm for weak conflict composition operator from Definition27 and Theorem 28.


## 4.1. Maximal Conflict-Free Partition

In fact, a prime event structure can be viewed as a system consisting of several substructures, which are conflict-free themselves. Such a conflict-free event substructure of a prime event structure represents a specific possible partial order execution trace via branching or nondeterministic choices. For any prime event structure, it is a certainty that we can get its maximal conflict-free substructures by some kind of conflict-free partition operation according to the characteristics of its conflict relation.First of all, we give the definition of maximal conflict pattern for an event structure. The notion of maximal conflict pattern can make great contributions to accelerate the process of partition by avoiding unnecessary partition steps. We then provide the key partition algorithm for a prime event structure.Definition 8 (maximal conflict pattern).
LetE
=
(
E
E
,
≤
E
,
♯
E
,
l
E
)
∈
E; for any A
⊆
E
E and B
⊆
E
E, A
♯
x
s
B is called amaximal conflict patternif and only if for all A
′
⊆
E
E, for all B
′
⊆
E
E
:
(
A
⊂
A
′
∧
B
⊂
B
′
)
⇒
¬
(
A
′
♯
x
s
B
′
).For any prime event structure, we can get these maximal conflict patterns by the following two steps:(1)
casual successors expanding;
(2)
conflict pairs merging.Firstly, due to the conflict inheritance property, we know that if evente is in conflict with event f then their casual successors are also in mutual conflict; that is, ∀
c
∈
Succ
(
e
)
,
∀
d
∈
Succ
(
f
)
:
e
♯
f
⇒
c
♯
d.Let{
e
}
♯
=
{
e
}
∪
Succ
(
e
) and {
f
}
♯
=
{
f
}
∪
Succ
(
f
); we have that {
e
}
♯ and {
f
}
♯ are in strong conflict if e
♯
E
f; namely, ∀
e
,
f
∈
E
E
:
e
♯
E
f
⇒
{
e
}
♯
♯
s
{
f
}
♯.For example, for a prime event structureE, if c
♯
E
d and casual relations are c
⪯
E
e
1
,
c
⪯
E
e
2,d
⪯
E
f
1
,
f
1
⪯
E
f
2, and d
⪯
E
f
3, we then have {
c
,
e
1
,
e
2
,
}
♯
s
{
d
,
f
1
,
f
2
,
f
3
}.We also have that any nonempty subset of{
e
}
♯ and any nonempty subset of {
e
}
♯ are also in strong conflict.Consider a prime event structureE
∈
E whose conflict relation has l
(
l
∈
N
) conflict pairs. Expand each conflict relation with its successors according to the conflict inheritance property and we can get full conflict relation pairs: {
e
1
}
♯
♯
s
{
f
1
}
♯
,
…
,
{
e
l
}
♯
♯
s
{
f
l
}
♯; here, e
i
♯
E
f
i
,
e
i
∈
E
E
,
f
i
∈
E
E
(
i
∈
N
,
1
≤
i
≤
l
).Secondly, for such a group of full conflict relation pairs obtained by the above steps, there may exist common elements among some pairs that can be merged together and form a maximal conflict pattern. For example, eventse
1
,
e
2
,
e
3, and e
4 are mutually in conflict; we have six immediate conflict relation pairs: {
e
1
}
♯
s
{
e
2
}, {
e
1
}
♯
s
{
e
3
}, {
e
1
}
♯
s
{
e
4
}, {
e
2
}
♯
s
{
e
3
}, {
e
2
}
♯
s
{
e
4
}, and {
e
3
}
♯
s
{
e
4
}.From the principle of permutation, we then have three maximal conflict patterns by merging conflict pairs:{
e
1
}
♯
x
s
{
e
2
,
e
3
,
e
4
}, {
e
2
}
♯
x
s
{
e
3
,
e
4
}, and {
e
3
}
♯
x
s
{
e
4
}. Equivalently, {
e
4
}
♯
x
s
{
e
1
,
e
2
,
e
3
}, {
e
3
}
♯
x
s
{
e
1
,
e
2
}, and {
e
2
}
♯
x
s
{
e
1
} are also the valid maximal conflict patterns.Assume that there arem
∈
N maximal conflict patterns after expanding and merging which are I
♯
E
1
:
A
1
♯
x
s
B
1
,
…
,
I
♯
E
m
:
A
m
♯
x
s
B
m, respectively.Here,I
♯
E
i
:
A
i
♯
x
s
B
i denotes the ith pattern, and ∀
e
∈
A
i
⊆
E
E
,
∀
f
∈
B
i
⊆
E
E
:
e
♯
E
f
(
i
∈
N
,
1
≤
i
≤
m
).IfA
i
♯
x
s
B
i, then any nonempty subset of A
i and any nonempty subset of B
i are also in extended strong conflict.For any event setD, let D
^ denote any nonempty subset of D
(
∅
≠
D
^
⊆
D
); correspondingly, I
♯
E
i
^
:
A
i
^
♯
x
s
B
i
^ denotes a conflict subpattern of I
♯
E
i
(
i
∈
N
,
1
≤
i
≤
m
).Formally,I
'
:
A
′
♯
x
s
B
′ is called aconflict subpattern of I
:
A
♯
x
s
B if and only if (
∅
≠
A
′
⊆
A
)
∧
(
∅
≠
B
′
⊆
B
), denoted by I
'
⊆
pattern
I (or I
⊇
pattern
I
'). Otherwise, I
'
⊈
pattern
I (or I
⊉
pattern
I
').LetP
E
=
{
I
♯
E
i
:
A
i
♯
x
s
B
i
∣
i
∈
N
,
1
≤
i
≤
m
} denote the maximal conflict pattern set of an event structure E.For any prime event structure, it is a certainty that we can get its maximal conflict-free substructures by some kind of conflict-free partition operation according to its conflict relation characteristics:maximal  conflict  patterns. Thus, we have the following theorem for partition.Theorem 9.
For any prime event structure, its maximal conflict-free partition exists and the partition result is unique.Proof. (1) Existence. The proof is constructive.If there is no conflict inE
E, then E
E itself is the maximal conflict-free event subset of E. Otherwise, for any nonempty event subset E
(
E
⊆
E
E
∧
E
≠
∅
), and there exists such maximal conflict pattern I
♯
E
i
:
A
i
♯
x
s
B
i
(
i
∈
N
,
1
≤
i
≤
m
) that (
A
i
^
∪
B
i
^
)
⊆
E.In order to make a subsetE
′ of E
(
E
′
⊆
E
) become conflict-free with respect to the conflict relation: A
i
♯
x
s
B
i, that is, eliminate this conflict relation from its all subsets, we have known that if A
i
^
⊆
E
′ (or B
i
^
⊆
E
′), then there should be B
i
⊈
E
′(or A
i
⊈
E
′); otherwise, the I
♯
E
i conflict pattern will still exist in its subsets.By greedy policy, letA
i
′ and B
i
′ be both maximal inclusion subsets with respect to E calculated by A
i
′
=
maxincl
(
A
i
,
E
) and B
i
′
=
maxincl
(
B
i
,
E
), respectively. This means the current event set E will be partitioned into two parts by this maximal conflict subpattern: one part is (
E
-
A
i
′
), and the other is (
E
-
B
i
′
). Certainly, there exists no I
♯
E
i conflict relation between (
E
-
A
i
′
) and (
E
-
B
i
′
) any more. If there does not exist any conflict in (
E
-
B
i
′
) (or (
E
-
A
i
′
)), then (
E
-
B
i
′
) (or (
E
-
A
i
′
)) is one conflict-free event subset of E
E.Otherwise, apply the next maximal conflict patternI
♯
E
i
+
1
(
i
∈
N
,
1
≤
i
≤
m
) to all the previously obtained event subsets in the same manner. This partition process is continued until no conflict exists.As we know, if each pattern of the maximal conflict patterns set has been applied just once by the above manner, then any consequent subset will be conflict-free and the partition process will stop. Meanwhile, there are2
m conflict-free subsets at most.Because intersection ofx
i and y
i
(
x
,
y
∈
{
A
,
B
}
,
i
≠
j
,
1
≤
i
,
j
≤
m
) can be nonempty, thus the partition tree is not yet a full binary tree and set inclusion among these solution nodes is allowed. If some subsets are included by others, then they will be removed until every result subset cannot be included by others. It is not difficult to verify that every consequent subset is maximal and conflict-free. Exploiting these expanded fully conflict patterns to partition the event set E
E step by step, we will eventually get all maximal conflict-free event subsets. That is, there exists a practical algorithm to implement the partition operation. Without loss of generality, let ⊘
A denote such partition for the time being.(2) Uniqueness. Assume we have m
c
f
s
e
t
N
A
(
E
) distinct maximal conflict-free event subsets in total by partition ⊘
A. These subsets form a set of m
c
f
s
e
t
s, denoted by R
A
=
{
A
1
,
A
2
,
…
,
A
n
∣
n
=
m
c
f
s
e
t
N
A
(
E
)
}.We might as well assume there is another partition⊘
B that generates the result set R
B
=
{
B
1
,
B
2
,
…
,
B
m
∣
m
=
m
c
f
s
e
t
N
B
(
E
)
} which is also a set of m
c
f
sets.Consider any element ofR
B; let B
i
(
1
≤
i
≤
m
,
i
∈
N
) denote it. The relationship between an element A
j
(
1
≤
j
,
k
≤
m
c
f
s
e
t
N
A
(
E
)
,
j
,
k
∈
N
) in R
A and B
i satisfies the following.(1)
∃
A
j
∈
R
A
:
A
j
⊂
B
i
⊆
E
E.
Since∀
A
k
∈
R
A
,
k
≠
j
:
A
j
♯
w
A
k, then ∀
A
k
∈
R
A
,
k
≠
j
:
B
i
♯
w
A
k. We have known that A
j
∈
R
A is maximal, and now event subset B
i is also a subset of E
E and is in weak conflict with other event subsets except A
i. Moreover, B
i includes A
i. This case leads to a contradiction.
(2)
∃
A
j
∈
R
A
:
B
i
⊂
A
j
⊆
E
E.
The proof is similar to the above case (1). This case also leads to a contradiction.
(3)
∀
A
j
∈
R
A
:
A
j
≠
B
i.
(3.1)
∀
A
j
∈
R
A
:
A
j
♯
w
B
i.
SinceB
i is also a subset of E
E, thus, R
A
′
=
{
A
1
,
A
2
,
…
,
A
n
,
B
i
∣
n
=
m
c
f
s
e
t
N
A
(
E
)
} is a valid set of m
c
f
s
e
t
s. There are n
+
1 subsets in this partition ⊘
A. This is in contradiction with that there are n
(
n
=
m
c
f
s
e
t
N
A
(
E
)
) subsets in R
A.
(3.2)
∃
A
j
∈
R
A
:
¬
(
A
j
♯
w
B
i
).
Since∀
A
k
∈
R
A
,
k
≠
j
:
A
j
♯
w
A
k, then ∀
A
k
∈
R
A
,
k
≠
j
:
(
A
j
∪
B
i
)
♯
w
A
k; that is, R
A
′′
=
{
A
1
,
A
2
,
…
,
{
A
j
∪
B
i
}
,
…
,
A
n
,
∣
n
=
m
c
f
s
e
t
N
A
(
E
)
} is a valid set of m
c
f
s
e
t
s. A
j
(
A
j
∈
R
A
) is maximal; moreover, A
j
⊂
(
A
j
∪
B
i
)
∈
R
A
′′ is maximal too. This leads to a contradiction.
(3.3)
∀
A
j
∈
R
A
:
¬
(
A
j
♯
w
B
i
).
The proof is similar to the above case (3.2). This case also leads to a contradiction.Therefore, we are forced to have only∃
A
j
∈
R
A
:
A
j
=
B
i; that is, any element in R
B is also an element in R
A; we get R
B
⊆
R
A; in the same manner, we will get R
A
⊆
R
B. Thus, we have R
B
=
R
A.This establishes the uniqueness and also implies the partition result is independent of partition order or conflict pattern.Therefore, we have the conclusion.AssumeE
∈
E has m
c
f
s
e
t
N
(
E
)
∈
N
m
c
f
E
S
s in total. Here, let N
E
=
m
c
f
s
e
t
N
(
E
) (N
E, for short) denote total amount of m
c
f
E
S
s, E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) denote the ith maximal conflict-free event substructure, and E
E
i
max
⁡ denote the event set of E
i
max
⁡.Then the result set can be represented asB
m
c
f
E
S
(
E
)
=
{
E
i
max
⁡
∣
i
∈
N
,
1
≤
i
≤
N
E
}.In fact, everyE
i
max
⁡
(
i
∈
,
1
≤
i
≤
m
c
f
s
e
t
N
(
E
)
) of the original prime event structure represents a specific possible execution choice in a system run. We might as well let c
f
p denote such an operator. Then, we have the following definition of this partition operator.Definition 10 (conflict-free partition).
An operatorc
f
p is calledconflict-free partition operator for E
∈
E if and only if B
m
c
f
E
S
(
E
)
=
c
f
p
(
E
).According to our previous discussion, we have C-like pseudocode descriptions: Algorithm1 for c
f
p.Algorithm 1:Conflict-free partition: c
f
p.
Input: a prime event structure: E;
Output: the set of m
c
f
E
S
s: B
m
c
f
E
S
(
E
);
BEGIN
(1)
C
=
∅
;
i
n
t
i
=
1
;
i
n
t
n
=
0
;
R
=
∅;
(2)
S
Q
=
E
n
t
e
r
Q
u
e
u
e
(
E
E
,
1
);
/* Initialize the Queue */
(3)if (I
s
C
o
n
f
l
i
c
t
F
r
e
e
(
E
E
)){
(5)C
=
∪
{
E
};
(6)  GotoBUILDES;
(7)} /* end if; */
/* Expand and merge each conflict pair and build maximal conflict patterns:
{
I
#
E
i
:
A
i
#
x
s
B
i
∣
i
∈
,
1
≤
i
≤
m
}; */
(8)for (i
=
1
;
i
≤
m
;
i++) { /* do */
(9)  Select a partition pattern:I
#
E
i
:
A
i
#
x
s
B
i;
(10) /* Current level isi, apply I
#
E
i, otherwise, skip while loop to the next one: i++; */
(11)while (!
E
m
p
t
y
Q
u
e
u
e
(
S
Q
)  &
&
i
=
=
V
a
r
Q
u
e
u
e
(
S
Q
,
L
E
V
E
L
)) {
/* Get the head of the Queue: event set */
(12)E
=
O
u
t
Q
u
e
u
e
(
S
Q
,
E
V
E
N
T
);
(13)A
i
′
=
m
a
x
i
n
c
l
(
A
i
,
E
);
(14)B
i
′
=
m
a
x
i
n
c
l
(
B
i
,
E
);
(15)E
1
=
(
E
-
A
i
′
);
(16)E
2
=
(
E
-
B
i
′
);
/*E
1 is a conflict-free subset; */
(17)if (I
s
C
o
n
f
l
i
c
t
F
r
e
e
(
E
1
)) {
(18)
C
=
C
∪
{
E
1
};
/* Remove these elements included in others; */
(19)R
e
m
o
v
e
I
n
c
l
u
d
e
d
E
l
e
m
e
n
t
(
C
);
(20)  }else{
/* Continue next partition by the conflict pattern: I
#
E
i
+
1; */
(21)  S
Q
=
E
n
t
e
r
Q
u
e
u
e
(
E
1
,
i
+
1
);
(22)  } /* end if */
(23)  if (I
s
C
o
n
f
l
i
c
t
F
r
e
e
(
E
2
)) {
(24)C
=
C
∪
{
E
2
};
(25)R
e
m
o
v
e
I
n
c
l
u
d
e
d
E
l
e
m
e
n
t
(
C
);
(26)  }else{
(27)S
Q
=
E
n
t
e
r
Q
u
e
u
e
(
E
2
,
i
+
1
);
(28)  } /* end if */
(29)  } /* end while */
(30) } /* end for */
(31)BUILDES: /* Build the sub-structure: F
=
(
E
F
,
⪯
F
,
#
F
,
l
F
)  */
(32)  while (¬
I
s
E
m
p
t
y
(
C
)) {
(33) Select a conflict-free event subset A
!
# from C;
(34) E
F
=
A
!
#;
(35) #
F
=
∅;
(36) ⪯
F
=
⪯
E
∩
(
A
!
#
×
A
!
#
);
(37) l
F
=
l
|
A
!
#;
(38) C
=
C
-
{
A
!
#
};
(39) R
=
R
∪
F; n++;
(40) } /* end while */
(41)m
c
f
s
e
t
N
(
E
)
=
n;
(42) returnR;
END;


## 4.2. Family of Configurations

In general, the behavior of an event structure is described by its configurations which are sets of events with certain properties. In other words, a configuration is a set of events that have happened during a specific run of the event structure.We will review the basic definition of configuration in the following section. More detailed information can be found in [26].Definition 11 (configuration).
LetX be a subset of X
⊆
E
E of a prime event structure E
∈
E; then X is called aconfiguration of E if and only if (1)
X is left-closed if and only if ∀
c
,
d
∈
E
,
d
∈
X
∧
c
≤
d
⇒
c
∈
X.
(2)
X is conflict-free if and only if ∀
e
,
f
∈
X
:
¬
(
e
♯
E
f
).A configuration can also be viewed as a global state where all events in the configuration have occurred. The configuration of the event structure should be conflict-free because conflicting events can never happen in a system run. In addition, all casual predecessors of an event in a configuration should be contained in this configuration too; that is, configuration should be downwards closed; otherwise this event could not have happened at all.That is, a subsetX is a (finite) configuration of E if and only if it is finite, left-closed, and conflict-free.The semantics of a prime event structure is defined as the family of its configurations ordered by set inclusion. LetC
o
n
f
F
(
E
) denote the family of all configurations of event structure E, which forms an ordered set (called prime algebraic coherent partial order; see [16]) by inclusion; that is, (
C
o
n
f
F
(
E
)
,
⊆
) is partial order.Definition 12.
A configurationX
∈
Conf
F
(
E
) is calledcomplete or (successfully)terminated if and only if ∀
d
∈
E
:
d
∉
X
⇒
∃
e
∈
X
:
e
♯
d. A configuration X
∈
C
o
n
f
F
(
E
) is calledmaximal if and only if ∀
Y
∈
Conf
F
(
E
)
:
X
⊄
Y.For any prime event structureE, a configuration of E is maximal if and only if it is complete. Obviously, for any maximal configuration of a prime event structure, there exists a corresponding maximal conflict-free substructure set. An empty or initial configuration, denoted by ∅
Conf
F
∈
Conf
F
(
E
), represents the initial state in which there is no event happened.In general, initial configuration and complete configuration are also called trivial configurations, while others are called nontrivial configurations.Similarly, we have the following configuration definition for conflict-free event structure.Definition 13 (configuration ofc
f
E
S).
LetF
=
(
E
F
,
⪯
F
,
∅
,
l
F
) be a c
f
E
S and let Z be a subset of E
F
(
Z
⊆
E
F
); then Z is called a configuration of F if and only if Z is left-closed; that is, ∀
c
,
d
∈
E
F
,
d
∈
Z
∧
c
⪯
d
⇒
c
∈
Z.SinceF
∈
F, its event subset is evidently conflict-free.Letc
f
Conf
F
(
F
) denote the family of all configurations of conflict-free event structure F. Clearly, when F is the ith m
c
f
E
S: E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of prime event structure E
∈
E, its family of all configurations is denoted by m
c
f
Conf
F
(
E
i
max
⁡
).Definition 14 (subfamily of configurations).
LetF
∈ be a c
f
E
S and let Ω
(
∅
≠
Ω
⊆
E
F
) be a nonempty event subset; a subfamily of configurations of F with respect to event subset Ω is the family of configurations of its event substructure F
|
Ω
=
(
Ω
,
≤
F
∩
(
Ω
×
Ω
)
,
∅
,
l
Ω
) restricted by event subset Ω; that is, c
f
subConf
F
(
F
,
Ω
)
≜
c
f
Conf
F
(
(
Ω
,
≤
F
∩
(
Ω
×
Ω
)
,
∅
,
l
Ω
)
).Clearly, for anym
c
f
E
S
E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of event structure E
∈
E, its subfamily of configurations with respect to event subset Ω
(
∅
≠
Ω
⊆
E
E
,
i
max
⁡
) is denoted by m
c
f
subConf
F
(
E
i
max
⁡
,
Ω
)
≜
m
c
f
Conf
F
(
(
Ω
,
≤
E
i
max
⁡
∩
(
Ω
×
Ω
)
,
∅
,
l
Ω
)
) for convenience.Lemma 15.
The relation between the family of configurations of a prime event structure and that of itsm
c
f
E
S
s can be described by C
o
n
f
F
(
E
)
=
⋃
1
≤
i
≤
N
E
(
m
c
f
C
o
n
f
F
(
E
i
max
⁡
).Proof. To prove the result of this lemma, we will show that
(2)
⋃
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
)
⊆
Conf
F
(
E
)
,
Conf
F
(
E
)
⊆
⋃
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
)
both hold.(1)“⊆”. For any configuration X
∈
Conf
F
(
E
), since X is a configuration, by definition, X should be conflict-free. Thus X should be the subset of one of the maximal configurations. Otherwise, if X is greater than any maximal configuration, then X must contain mutual conflicting events; that is impossible.Therefore, we have that there must exist a maximal configuration which containsX. Such a maximal configuration corresponds to a maximal conflict-free event subset: E
E
i
max
⁡
∈
(
i
∈
N
,
1
≤
i
≤
N
E
); that is, X must be the element of m
c
f
Conf
F
(
E
i
max
⁡
); that is, X
∈
m
c
f
Conf
F
(
E
i
max
⁡
). We have Conf
F
(
E
)
⊆
⋃
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
).(2)“⊇”. For any configuration X
∈
m
c
f
Conf
F
(
E
i
max
⁡
)
(
i
∈
N
,
1
≤
i
≤
N
E
), of course, X
∈
⋃
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
); this implies X
⊆
E
E
i
max
⁡ and E
E
i
max
⁡
⊆
E
E; therefore, we get X
⊆
E
E. Since X is a configuration, it is also a configuration of E; that is, X
∈
C
o
n
f
F
(
E
).We have∪
1
≤
i
≤
N
E
(
m
c
f
Conf
F
(
E
i
max
⁡
)
)
⊆
Conf
F
(
E
).Therefore, from (1) and (2), we have the result.


## 4.3. Domains of Configurations

In this section, we will discuss the concept of domain from the point of view that computation states are taken as such subsets and progress in a computation is measured by the occurrence of more events.Firstly, we will recall some related conceptions regarding domain [16, 27]. Then, some important facts will be discussed.Definition 16 (least upper bound).
LetD
=
(
D
,
⊑
) be a partial order; an element d
∈
D is calledleast upper bound of subset X (X
⊆
D), denoted by d
=
⊔
X, if and only if (
∀
x
∈
X
:
x
⊑
d
)
∧
(
∀
d
′
∈
D
:
(
∀
x
∈
X
:
x
⊑
d
′
)
⇒
d
⊑
d
′
).Definition 17 (coherent).
LetD
=
(
D
,
⊑
) be a partial order; two elements x
,
y
∈
D are calledconsistent (denoted by x
↑
y) if and only if ∃
z
∈
D
:
x
⊑
z
∧
y
⊑
z; a subset X
⊆
D ispairwise consistent if and only if any two of its element have an upper bound in D; that is, ∀
x
,
y
∈
X
:
x
↑
y; (
D
,
⊑
) is calledcoherent if and only if every pairwise consistent subset X (X
⊆
D) has a least upper bound ⊔
X.
Theconsistency relation of x and y is denoted by x
↑
y; conversely,inconsistency is denoted by x
↑
y.Definition 18 (complete prime).
A partial orderD
=
(
D
,
⊑
); an element is acomplete prime if and only if for every finite subset X
⊆
D, if ⊔
X exists and p
⊆
⊔
X then there exists an x
∈
X such that p
⊑
x (i.e., p
⊑
⊔
X
⇒
∃
x
∈
X
.
p
⊑
x
).LetP
(
D
) denote the set of complete prime of (
D
,
⊑
).Definition 19 (prime algebraic).
A partial orderD
=
(
D
,
⊑
) is calledfinitary if and only if ∀
p
,
d
∈
P
(
D
)
:
{
d
∈
D
∣
d
⊑
p
} is finite. (
D
,
⊑
) is calledprime algebraic if and only if P
(
D
) is countable and ∀
d
∈
D
:
d
=
⊔
{
p
∈
P
(
D
)
∣
p
⊑
d
}.
Namely,D is calledprime algebraic if and only if, for every element d
∈
D, ⊔
D
d exists (define ⊔
D
d
=
{
p
⊑
d
∣
p
is
a
complete
prime
}
), and d
=
⊔
D
d.Definition 20 (domain).
A coherent, prime algebraic, and finitary partial order is called aScott domain (or simply adomain).Definition 21.
LetD
=
(
D
,
⊑
) be acoherent, finitary prime algebraic domain. Define P
r
[
D
]
=
(
P
(
D
)
,
⪯
,
♯
), where P
(
D
) consists of the complete primes of D:(1)
∀
p
,
p
′
∈
P
(
D
)
:
p
⪯
p
′
⇔
p
⊑
p
′;
(2)
∀
p
,
p
′
∈
P
(
D
)
:
p
♯
p
′
⇔
p
↑
p
′.Definition 22.
LetD
=
(
D
,
⊑
) be aprime algebraic complete lattice. Define P
r
[
D
]
=
(
P
(
D
)
,
⪯
), where P
(
D
) consists of the complete primes of D, ∀
p
,
p
′
∈
P
(
D
)
:
p
⪯
p
′
⇔
p
⊑
p
′.Theorem 23.
LetE
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E; then (
C
o
n
f
F
(
E
)
,
⊆
) is a finitary coherent prime algebraic domain; the complete primes are the set {
a
∈
E
E
∣
a
⪯
e
,
e
∈
E
E
} (see [25]).Theorem 24.
Let(
D
,
⊑
) be a finitary coherent prime algebraic domain. Then, P
r
[
D
]
=
(
P
(
D
)
,
⪯
,
♯
) is a prime event structure, with φ
:
(
D
,
⊑
)
≅
(
C
o
n
f
F
(
P
r
[
D
]
)
,
⊆
) giving an isomorphism of partial orders where φ
(
d
)
=
{
p
⊑
d
∣
p
is
a
complete
prime
} with inverse λ
:
C
o
n
f
F
(
P
r
[
D
]
)
→
(
D
,
⊑
) given by λ
(
x
)
=
⊔
x (see [16]).Evidently, event structures and coherent, finitary prime algebraic domains are equivalent; one can be used to represent the other.The following theorem describes the important property of family of configurations of a prime event structure.Theorem 25.
For any nonemptym
c
f
E
S: E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of event structure E
∈
E, its family of configurations (
m
c
f
C
o
n
f
F
(
E
i
max
⁡
)
,
⊆
) is prime algebraic complete lattice. Its complete primes are those elements of the form {
a
∈
E
E
i
max
⁡
∣
a
⪯
e
,
e
∈
E
E
i
max
⁡
}.Proof. The proof is straightforward.Thus prime event structure and finitary coherent prime algebraic domain are equivalent; this implies that there is a one-to-one correspondence between a prime event structure and its family of configurations; one can be used to represent the other.


## 4.4. Weak Choice Composition

Theorem23 describes an important property between the domains of configurations of prime event structures and the prime event structures themselves.We can obtain a full set ofm
c
f
E
S
s from a prime event structure by applying c
f
p operator over it. Conversely, given a full set of m
c
f
E
S
s of an event structure, we can certainly recover the original event structure that generates this set of m
c
f
E
S
s by some kind of composition operation.Further, for any weak conflict set, we give the constraint conditions, under which this weak conflict set can be composed together and form a prime event structure that can generate this set by conflict-free partition operation.The following theorem discusses the constraint conditions for composition.Theorem 26 (necessary and sufficient condition for composition).
For any weak conflict setW
F
n
c
f
w
=
{
F
i
∈
F
∣
i
,
n
∈
N
,
1
≤
i
≤
n
}, if it satisfies the following conditions: (1) and (2), then there exists a unique prime event structure E
∈
E
prime that can generate this set by c
f
p partition operation; that is, W
F
n
c
f
w
=
c
f
p
(
E
).(1)
∀
F
i
,
F
j
∈
W
F
n
c
f
w
:
Ω
=
(
E
F
i
∩
E
F
j
)
∧
(
Ω
≠
∅
)
⇒
c
f
subConf
F
(
F
i
,
Ω
)
=
c
f
subConf
F
(
F
j
,
Ω
)  (
i
,
j
∈
N
,
i
≠
j
,
1
≤
i
≤
n
).
(2)
(
⋃
i
=
1
n
c
f
Conf
F
(
F
i
)
,
⊆
)
is a finitary coherent prime algebraic domain.Proof. On one hand, the intersection of event sets of any two c
f
E
S
s is nonempty meaning that common events have happened from both event structures. By definition, if these events represent common global states in runs of a system described by the same prime event structure with multiple choices, they should behave identically. That is, their configurations with respect to the intersection of event set should be identical.In addition, from Theorems23 and 24, the family of configurations of a prime event structure ordered by set inclusion should be a finitary coherent prime algebraic domain.Thus, we have the necessary condition for composition.On the other hand, from Theorems23 and 24, we have that there is a one-to-one correspondence between a prime event structure and its family of configurations. Given a valid family of configurations for prime event structure, then there should exist a corresponding prime event structure.For any weak conflict set:W
F
n
c
f
w
=
{
F
i
∈
F
∣
i
,
n
∈
,
1
≤
i
≤
n
}, if all c
f
C
o
n
f
F
(
F
i
) by joining can form a valid family of configurations for a prime event structure, that is, ⋃
1
≤
i
≤
n
c
f
C
o
n
f
F
(
F
i
) forms a ordered by set inclusion, then there should exist such a unique prime event structure E that C
o
n
f
F
(
E
)
=
⋃
1
≤
i
≤
n
c
f
C
o
n
f
F
(
F
i
).Therefore, we get the necessary and sufficient condition for composition.Obviously, the setB
m
c
f
E
S
(
E
) of a prime event structure satisfies the above condition. Clearly, this implies that there must exists a composition operation which can construct the target event structure E from a weak conflict set that satisfies the constraint conditions. We may as well let w
c
c denote the operator. Thus, we have the following definition.Definition 27 (weak choice composition (w
c
c operator)).
LetW
F
n
c
f
w be a weak conflict set, which satisfies necessary and sufficient conditions for composition; an operator w
c
c is calledweak choice composition operator if and only if the result event structure R
=
w
c
c
(
W
F
n
c
f
w
) and R satisfies the following: (1)
Conf
F
(
R
)
=
(
⋃
i
=
1
n
c
f
Conf
F
(
F
i
)
,
⊆
);
(2)
W
F
n
c
f
w
=
c
f
p
(
R
).The following theorem states that the operatorw
c
c and c
f
p are mutually inverse for a prime event structure.Theorem 28.
For anyE
∈
E
,
E
=
w
c
c
(
c
f
p
(
E
)
) holds.Proof. The proof is straightforward.Obviously, it is not difficult to derive an algorithm for weak conflict composition operator from Definition27 and Theorem 28.


## 5. Slicing Reduction

In this section, we will discuss slicing reduction technique for partial order trace or prime event structure. Slicing is often taken as an effective abstract technique to combat the state explosion problem. A slicing algorithm for event structure with respect to predicates in a subset of temporal logic formulas is studied. Specially, we focus on statically analyzing rather than online detecting over event structure model.First of all, we will retrospect the classical notion of computation slicing for partial order traces. Then, we will extend the idea from partial order traces to prime event structures with conflict relations. Additionally, all related definitions and theorems [18, 19, 28] for our theory will be discussed.


### 5.1. Partial Order Trace Slicing

Computation slicing was introduced in [7] as an abstraction technique for analyzing partial order traces of distributed programs or distributed computations.Generally, for classical program slicing, programs are sliced with respect to a slicing criterion that is an interested point for analyzing. In static program slicing, for example, “a program line number” can be taken as a valid slicing criterion. Thus, in order to compute a slice, we need to firstly define the slicing criterion.Intuitively, a slice of a trace with respect to a temporal logic specification or a predicate (slicing criterion)φ is a subtrace that contains all the states of the trace that satisfy φ. A slice contains all the states that satisfy φ such that it can be computed efficiently and is often much smaller than the original model.We can use directed graphs to model partial order (execution) traces (POTs, for short) as well as slices. Thus, a notion namedgraph ideal (ororder ideal) of directed graph [29] is introduced to specify partial order traces and slices pictorially. Formally, its definition is given as follows.Definition 29 (order ideal).
Given a poset(
X
,
≤
), (
≤ denotes an order relation) a subset S of X is anorder ideal if it satisfies ∀
x
,
y
:
x
,
y
∈
X
:
(
x
∈
S
)
∧
(
y
≤
x
)
⇒
(
y
∈
S
).Definition 30 (graph ideal).
Given a directed graphG
=
(
V
,
Γ
), let V
(
G
) and Γ
(
G
) denote the set of vertices with event labels and directed edges, respectively. A subgraph H of G is agraph ideal if it satisfies ∀
u
,
v
∈
V
(
G
)
,
H
⊆
V
(
G
)
,
v
∈
H
∧
(
u
,
v
)
∈
Γ
(
G
)
⇒
u
∈
H.It is more convenient to use directed graphs to represent partially ordered sets and prime event structures for slicing computation. It satisfies the following.(1)
For any evente and f of E, if e
⪯
f, then there is directed edge from the vertex v
e labelled with e to the vertex v
f labelled with f.
(2)
For any evente and f of E, if e
♯
f, then there is dash line between the vertex v
e labelled with e to the vertex v
f labelled with f.For example, as shown in Figure1, a partial order trace or a m
c
f
E
S is demonstrated pictorially. The corresponding event structure for Figure 1 is as follows.(i)
E
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
,
(
A
c
t
=
{
a
,
b
,
c
,
d
}
).
(1)
E
E
=
{
e
1
,
e
2
,
e
3
,
e
4
}.
(2)
⪯
E
=
{
e
1
⪯
e
2
,
e
1
⪯
e
4
,
e
3
⪯
e
4
}.
(3)
l
(
e
1
)
=
a
,
l
(
e
2
)
=
b
,
l
(
e
3
)
=
c
,
l
(
e
4
)
=
d.
(4)
♯
E
=
∅.Figure 1
Partial order trace and its directed graph representation.In addition, when attempting to construct the graph representation ofm
c
f
E
S, as Figure 1 shows, two specific vertexes ⊤ and ⊥ will be added as initial state and terminal state corresponding to initial configuration and maximal configuration, respectively.A subset of elements forms an order ideal if whenever an element is contained in the subset then all its preceding elements are also contained in the subset. Intuitively, order ideals or left-closed subsets can be graphically represented by graph ideals. Generally, independency relation will not be represented explicitly. It is not difficult to have that partial order trace is only a special case of prime event structure with no conflict relations. Here, graph ideal is a notion equivalent to the configuration of an event structure. Empty set and the set of all vertices are called trivial ideal. Similarly, initial configuration and complete configuration are also called trivial configurations.Definition 31 (predicate on configuration).
Intuitively, a logic formula or predicate is a Boolean-valued function defined on the set of configurations:φ
:
Conf
F
(
E
)
→
{
0,1
}. It actually represents a subset of configurations in which the Boolean function evaluates to 1.The predicate detection problem is to decide whether the initial configuration of an event structure satisfies a predicate. More formally, we have the following definition.Definition 32 (predicate detection).
For any prime event structureE and any predicate φ, predicate detection is to decide whether Conf
F
(
E
)
,
{
⊥
}
⊨
φ holds or not.Predicates are used to specify system behaviors and properties such as safety and liveness. Properties expressed by a CTL (computational tree logic, introduced in [30]) formula are beyond the scope of this paper. For evaluating the value of a predicate efficiently, various predicate classes [28] such as conjunctive, stable, observer-independent, linear, relational, and nontemporal regular [7] predicates have been defined.Generally, predicate on configurations will act as the slicing criterion for POTs slicing.Definition 33 (slice ofm
c
f
E
S(POTs)).
Aslice of a m
c
f
E
S(POTs): E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of prime event structure E with respect to a formula φ, denoted by m
c
f
E
S
slice
(
E
i
max
⁡
,
φ
), is such an event structure that satisfies the following. (i)
Its family of configurations contains all the configurations that satisfyφ.
(ii)
Its family of configurations has the least number of configurations and still forms a sublattice.This formal definition is derived from computation slice notion [7] given by Garg and Mittal. Meanwhile, existence and uniqueness of the m
c
f
E
S slice have also been discussed; that is, the following theorem holds.Theorem 34.
For anyE
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of a prime event structure and any predicate φ, the slice of with respect to predicate φ, that is, m
c
f
E
S
slice
(
E
i
max
⁡
,
φ
) exists and is unique.Proof. The proof is straightforward; see [8, 20, 31].In general, the family of configurations for am
c
f
E
S forms a distributed lattice, and its slice with respect to a predicate is a sublattice. Sometimes a slice may contain those configurations that do not satisfy the predicate for completing sublattice.In the next section, we will discuss the slicing definition and model for prime event structure.


### 5.2.  Sliced Model over Event Structure

Generally, predicate on configurations acts as the slicing criterion for prime event structure slicing. Temporal regular predicate, such as a regular subset of CTL called RCTL [7, 8, 29], which contains four temporal operators EF, AG, EG, and EX[j], and nontemporal regular predicates both can also be taken as the slicing criterions.Compared with the definition of slice ofm
c
f
E
S, we have a similar case for prime event structure.Definition 35 (slice of prime event structure).
A slice of a prime event structure with respect to a formulaφ, denoted by S
l
i
c
e
E
S
(
E
,
φ
), is such an event structure that satisfies the following. (i)
Its family of configurations contains all the configurations that satisfyφ.
(ii)
Its family of configurations has the least number of configurations.Generally, a slice may contain configurations that do not satisfy the given predicate. The slice of an event structure with respect to a predicate is calledlean [32] if every configuration of the slice satisfies the predicate.Theorem 36.
For anyE
∈
E and any predicate φ, S
l
i
c
e
E
S
(
E
,
φ
) exists and is unique, and S
l
i
c
e
E
S
(
E
,
φ
)
=
w
c
c
(
m
c
f
E
S
s
l
i
c
e
(
c
f
p
(
E
)
,
φ
)
) holds.Proof. (1) Existence and Uniqueness. From Theorem 34, we have that, for any E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of a prime event structure E and any predicate φ, its slice with respect to predicate φ exists and is unique.For anym
c
f
E
S, the family of configuration of m
c
f
E
S
slice
(
E
i
max
⁡
,
φ
) is a distributed lattice and is unique.Further, let⋃
E
C
=
⋃
1
≤
i
≤
N
E
(
m
c
f
C
o
n
f
(
m
c
f
E
S
s
l
i
c
e
)
(
(
E
i
max
⁡
,
φ
)
)
); ⋃
E
C is also unique and (
⋃
E
C
,
⊆
) is a finitary coherent prime algebraic domain.Next, we show that the slicing operation will keep the second part of necessary and sufficient condition for composition.For anyE
i
max
⁡ and E
j
max
⁡
(
j
≠
i
), if E
E
i
max
⁡
∩
E
E
j
max
⁡
=
D and D
≠
∅, we then have that c
f
subConf
F
(
E
i
max
⁡
,
D
)
=
c
f
subConf
F
(
E
j
max
⁡
,
D
); that is, for any nonempty event subset D
′
(
D
′
⊆
D
) and any predicate φ, if any configuration of D
′ satisfies φ, that is, D
′ is the common part of both slices of E
i
max
⁡ and E
j
max
⁡. We still get that c
f
subConf
F
(
E
i
max
⁡
,
D
′
)
=
c
f
subConf
F
(
E
j
max
⁡
,
D
′
).This means that, for any twom
c
f
E
S
s, if their intersection is nonempty, no matter which part of the intersection belongs to the slice, after slicing, the necessary and sufficient condition for composition will be still satisfied.Thus, we get that⋃
E
C is a valid family of configurations for prime event structures; there should exist such a unique prime event structure R
∈
E that satisfies Conf
F
(
R
)
=
⋃
E
C. We can get R by applying w
c
c to the corresponding event structures of ⋃
E
C.Therefore, the existence and uniqueness for event structure slicing have been established. We will then prove that the prime event structureR is the ultimate result of slicing.(2) Satisfactoriness and Minimality. On the one hand, for any configuration X of event structure E that makes predicate φ hold, that is, X
∈
Conf
F
(
Slice
E
S
(
E
,
φ
)
), there must be a m
c
f
E
S: E
i
max
⁡ so that X
∈
Conf
F
(
Slice
E
S
(
E
,
φ
)
); let C
i
=
m
c
f
Conf
F
(
m
c
f
E
S
slice
(
E
j
max
⁡
,
φ
)
), because C
i contains all the configurations of event structure E
j
max
⁡ that make predicate φ hold. We have that X must be contained by C
i; that is, X
∈
C
i.We getX
∈
Conf
F
(
Slice
E
S
(
E
,
φ
)
)
⇒
X
∈
⋃
E
C.Further, we getConf
F
(
Slice
E
S
(
E
,
φ
)
)
⊆
⋃
E
C.On the other hand, for any configurationX
∈
⋃
E
C, we get X
∈
Conf
F
(
E
) and X can make predicate φ hold; then X
∈
Conf
F
(
Slice
E
S
(
E
)
) must hold. Thus, we get X
∈
⋃
E
C
⇒
X
∈
Conf
F
(
Slice
E
S
(
E
,
φ
)
).That is,⋃
E
C
⊆
Conf
F
(
Slice
E
S
(
E
,
φ
)
).Therefore, we have⋃
E
C
=
Conf
F
(
Slice
E
S
(
E
,
φ
)
).Thus, we get thatSlice
E
S
(
E
,
φ
)
=
R.Moreover, by the definition of slice of maximal conflict-free event substructure, we have that, for anyE
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
), the corresponding m
c
f
E
S
slice
(
E
i
max
⁡
,
φ
) contains the least number of configurations that satisfy the given predicate φ; we then have that ⋃
E
C
=
Conf
F
(
Slice
E
S
(
E
,
φ
)
) also contains the least number of configurations satisfying this specification. Thus, satisfactoriness and minimality both hold.Consequently, from both(
1
) and (
2
), we conclude that the theorem holds.


### 5.3. Slicing Reduction Algorithm

In this section, we will present an approach for event structure slice computing. The slicing algorithm for a prime event structure or itsm
c
f
E
S
s with respect to regular predicates is based on theAdding Edges Theorem (see [8, 20, 31, 33]).In fact, by the following theorem, these lattices will never be actually constructed in the slicing process for efficiency.The configurations do not satisfy the predicate but still can be included to complete the sublattice.Given a distributive latticeL generated by a graph G, every sublattice of L can be generated by a graph obtained by adding edges to G. The following theorem holds.Theorem 37 (Adding Edges Theorem).
LetL
′ be any sublattice of a finite distributive lattice L generated by the directed graph G. Then, there exists a graph G
′ that can be obtained by adding edges to (removing vertices from)  G that generates L
′.For any prime event structure, we can get the slices of itsm
c
f
E
S
s by applying the Adding Edges Theorem. These slices can be composed by w
c
c to form a new prime event structure which is the target slice of the original event structure. This approach is less general but results in more efficient detection algorithms for a special class of predicates. Note that we will never actually construct the lattice or family of configurations of the event structure due to efficiency.Garg and Mittal have presented an efficient algorithmslice
(
G
,
φ
) [8, 28] based on graphical representation G to compute the slice of POTs (or conflict-free event structures) with respect to a predicate φ. The algorithm adopts the principle of the Adding Edges Theorem and can produce a sliced graph representation. Especially, we have G
=
slice
(
G
,
true
) for predicate φ
=
true itself.We extend the idea and algorithm to more general models and provide an algorithm for slicing them
c
f
E
S
s and the original prime event structure. Thus, we have Algorithm 2 to compute the slice of conflict-free event structure.Algorithm 2:Slicing algorithm: m
c
f
E
S
s
l
i
c
e
(
m
c
f
E
S
(
E
)
,
φ
).
Input:
(1) a conflict-free event structure:m
c
f
E
S
(
E
),
(2) a regular predicate:φ
Output: the slice of m
c
f
E
S: E
i
max
⁡
s
l
i
c
e
BEGIN
(1)K
=
∅;
(2) generate graph representationG for E
i
max
⁡;
(3) computing slice:K
=
s
l
i
c
e
(
G
,
φ
);
(4) generate event structureE
i
max
⁡
s
l
i
c
e from graph representation K;
(5) returnE
i
max
⁡
s
l
i
c
e;
ENDFor a prime event structure with conflict relations, we have to applyc
f
p operator to get m
c
f
s
e
t
N
(
E
) maximal conflict-free event substructures and each of them can be sliced by m
c
f
E
S
slice. Then, the set consisting of each sliced result can be composed together by w
c
c to construct a new event structure. This new event structure will be the sliced result.Thus, we can derive Algorithm3 to compute the slice of a prime event structure.Algorithm 3:Slicing algorithm: s
l
i
c
e
E
S
(
E
,
φ
).
Input:
(1) an event structure:E
(2) a regular predicate:φ
Output: the slice: E
s
l
i
c
e
BEGIN
(1)
i
n
t  n
=
0, C
=
∅;
(2)
R
=
∅;
(3)
B
m
c
f
E
S
(
E
)
=
c
f
p
(
E
)
(4)
n
=
m
c
f
s
e
t
N
(
E
);
(5)for (i
n
t
i
=
0
;
i
<
n
;
i++) {
(6)  get theith  m
c
f
E
S: E
i
max
⁡ from B
m
c
f
E
S;
(7)C
=
C
∪
m
c
f
E
S
s
l
i
c
e
(
E
i
max
⁡
,
φ
);
(8)}
(9)if (C
≠
∅){
(10)
R
=
w
c
c
(
C
);
(11)  }
(12)  returnR;
ENDBecause the set of the slices ofm
c
f
E
S
s may no longer keep the weak conflict relation which exists in the original m
c
f
E
S
s.Therefore, afterm
c
f
E
S
slice
(
m
c
f
E
S
(
E
)
,
φ
) operation is performed, the relation among these slices can be one of the following cases:(1)
strong conflict;
(2)
conflict-free;
(3)
weak conflict;
(4)
hybrid of weak conflict and conflict-free;
(5)
hybrid of weak conflict and strong conflict;
(6)
hybrid of strong conflict, weak conflict, and conflict-free.In case of (1), (3), and (5), the operationw
c
c can be performed directly. But in case of (2), (4), and (6), we have to add some events in order to make the result set of slices still be able to form a valid weak conflict set at the end of process.For temporal predicates [8], such as E
F, E
G and A
G can be computed by slice
(
G
,
E
F
(
φ
)
), slice
(
G
,
E
G
(
φ
)
), and slice
(
G
,
A
G
(
φ
)
), respectively. From the definition of a slice, we know that every configuration of a slice slice
E
S
(
E
,
φ
) is also a configuration of E.Clearly, the following two corollaries hold.Corollary 38.
(1) For any prime event structureE
∈
E, Conf
F
(
slice
E
S
(
E
,
E
G
(
φ
)
)
)
⊆
Conf
F
(
slice
E
S
(
E
,
φ
)
)
⊆
Conf
F
(
E
).
Similarly forA
G, the following holds.
(2) For any prime event structureE
∈
E, Conf
F
(
slice
E
S
(
E
,
A
G
(
φ
)
)
)
⊆
Conf
F
(
slice
E
S
(
E
,
φ
)
)
⊆
Conf
F
(
E
).Corollary 39.
For any prime event structureE
∈
E, Conf
F
(
slice
E
S
(
E
,
E
F
(
φ
)
)
)
⊆
Conf
F
(
E
).


### 5.4. Case Study for Slicing Reduction

In this section, we will give an example to illustrate the prime event structure slice notion and its computing process.Consider a prime event structure:E
=
(
E
E
,
≤
E
,
♯
E
,
l
E
), as shown in Figure 2. The components are described as follows:(1)
event set:E
E
=
{
e
a
,
e
b
,
e
c
,
e
1
,
e
2
,
e
3
,
e
4
};
(2)
conflict relation:#
E
=
{
e
b
#
e
1
};
(3)
casual relation:⪯
E
=
{
e
b
⪯
e
a
,
e
c
⪯
e
a
,
e
1
⪯
e
2
,
e
1
⪯
e
4
,
e
3
⪯
e
4
,
e
c
⪯
e
3
};
(4)
action labels:l
E
(
e
a
)
=
a
,
l
E
(
e
b
)
=
b
,
l
E
(
e
c
)
=
c,l
E
(
e
1
)
=
a
1
,
l
E
(
e
2
)
=
a
2
,
l
E
(
e
3
)
=
a
3
,
l
E
(
e
4
)
=
a
4;
(5)
action functions:
(i)
action
(
a
1
)
:
{
x
=
x
+
1
}
;
(ii)
action
(
a
2
)
:
{
x
=
x
+
3
};
(iii)
action
(
a
3
)
:
{
y
=
y
+
3
};
(iv)
action
(
a
4
)
:
{
y
=
y
+
2
};
(v)
action
(
a
)
:
{
z
=
z
+
2
};
(vi)
action
(
b
)
:
{
z
=
z
+
1
};
(vii)
action
(
c
)
:
{
y
=
y
-
1
};
(viii)
initValue
:
{
x
=
1
;
y
=
1
;
z
=
0
};
(6)
slice criterion:{
φ
=
-
2
≤
(
y
-
x
+
z
)
<
2
}.Figure 2
A Prime event structureE.In this example, the system global states will be updated after an action function executes. Figure2 depicts all the events conflict (for simplicity, only immediate conflict relation is shown) and casual relation. Figure 3 shows its corresponding family of configurations.Figure 3
Family of configurations ofE.There is one conflict relation between eventb and e
1; due to the conflict inheritance property of prime event structures, we have e
b
♯
e
1
,
e
b
♯
e
2
,
e
b
♯
e
4 and e
a
♯
e
1
,
e
a
♯
e
2
,
e
a
♯
e
4; that is, each of {
e
a
,
e
b
} is in conflict with each of {
e
1
,
e
2
,
e
4
}. Obviously, according to this conflict relation, apply c
f
p operation to the prime event structure E and we get that this event structure has only two m
c
f
E
S
s: they are E
1
=
(
{
e
a
,
e
b
,
e
c
,
e
3
}
,
≤
E
1
,
∅
,
l
E
1
) and E
2
=
(
{
e
1
,
e
2
,
e
3
,
e
4
,
e
c
}
,
≤
E
2
,
∅
,
l
E
2
) depicted by Figures 4(1) and 4(2), respectively, and Figures 5(1) and 5(2) show their corresponding families of configurations.Figure 4
m
c
f
E
S
s of E: E
1 and E
2.Figure 5
Families of configurations ofm
c
f
E
S
s(E
1 and E
2).The configurations that satisfy the predicate are labelled with frames. In fact, these configurations are only used to describe relationship between original event structure and its slice graphically; in general, they will never be actually constructed in the slicing algorithm for efficiency.The families of configurations of the slices ofE
1 and E
2 with respect to the predicate {
φ
=
-
2
≤
(
y
-
x
+
z
)
<
2
} are shown in Figures 6(1) and 6(2), respectively. It can be verified that both m
c
f
Conf
(
E
1
) and m
c
f
Conf
(
E
2
) form distributed lattices.Figure 6
Subfamilies of configurations of the slices.These configurations of the slices are exactly the ones that satisfy the given predicate in the family of configurations of the original event structure. Figure7 shows the family of configurations constructed by applying ∪ operation to the families of configurations of all slices.Figure 7
Subfamily of configurations of the slice.Finally, in Figure8, the slice of E
1 and the slice of E
2 are combined into the slice of E by w
c
c operator, as expected.Figure 8
Slice model with respect toφ.To illustrate the benefit of predicate detection by using slicing reduction as shown in above example, consider the states in Figure3 again.Let{
φ
=
-
2
≤
(
y
-
x
+
z
)
<
2
} be the predicate to be checked, and suppose we want to detect whether E
F
(
φ
) holds or not; that is, there exists a global state that satisfies φ. Without slicing reduction applied, we are forced to examine all global states, 15 states in total as shown in Figure 3, to decide whether the traces satisfy the predicate.Alternatively, we can compute the slice via slicing reduction technique with respect to the regular temporal predicate and use this slice for predicate detection.For this purpose, firstly, we compute the slice with respect toφ and the slice is shown in Figure 7.Finally, we check whether the initial state is the same as the initial state of the slice and decide whether the predicate is satisfied or not.The slice contains only 9 states and has much fewer states than the original traces itself. Generally, it is exponentially smaller in many cases and this can result in substantial savings.


## 5.1. Partial Order Trace Slicing

Computation slicing was introduced in [7] as an abstraction technique for analyzing partial order traces of distributed programs or distributed computations.Generally, for classical program slicing, programs are sliced with respect to a slicing criterion that is an interested point for analyzing. In static program slicing, for example, “a program line number” can be taken as a valid slicing criterion. Thus, in order to compute a slice, we need to firstly define the slicing criterion.Intuitively, a slice of a trace with respect to a temporal logic specification or a predicate (slicing criterion)φ is a subtrace that contains all the states of the trace that satisfy φ. A slice contains all the states that satisfy φ such that it can be computed efficiently and is often much smaller than the original model.We can use directed graphs to model partial order (execution) traces (POTs, for short) as well as slices. Thus, a notion namedgraph ideal (ororder ideal) of directed graph [29] is introduced to specify partial order traces and slices pictorially. Formally, its definition is given as follows.Definition 29 (order ideal).
Given a poset(
X
,
≤
), (
≤ denotes an order relation) a subset S of X is anorder ideal if it satisfies ∀
x
,
y
:
x
,
y
∈
X
:
(
x
∈
S
)
∧
(
y
≤
x
)
⇒
(
y
∈
S
).Definition 30 (graph ideal).
Given a directed graphG
=
(
V
,
Γ
), let V
(
G
) and Γ
(
G
) denote the set of vertices with event labels and directed edges, respectively. A subgraph H of G is agraph ideal if it satisfies ∀
u
,
v
∈
V
(
G
)
,
H
⊆
V
(
G
)
,
v
∈
H
∧
(
u
,
v
)
∈
Γ
(
G
)
⇒
u
∈
H.It is more convenient to use directed graphs to represent partially ordered sets and prime event structures for slicing computation. It satisfies the following.(1)
For any evente and f of E, if e
⪯
f, then there is directed edge from the vertex v
e labelled with e to the vertex v
f labelled with f.
(2)
For any evente and f of E, if e
♯
f, then there is dash line between the vertex v
e labelled with e to the vertex v
f labelled with f.For example, as shown in Figure1, a partial order trace or a m
c
f
E
S is demonstrated pictorially. The corresponding event structure for Figure 1 is as follows.(i)
E
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
,
(
A
c
t
=
{
a
,
b
,
c
,
d
}
).
(1)
E
E
=
{
e
1
,
e
2
,
e
3
,
e
4
}.
(2)
⪯
E
=
{
e
1
⪯
e
2
,
e
1
⪯
e
4
,
e
3
⪯
e
4
}.
(3)
l
(
e
1
)
=
a
,
l
(
e
2
)
=
b
,
l
(
e
3
)
=
c
,
l
(
e
4
)
=
d.
(4)
♯
E
=
∅.Figure 1
Partial order trace and its directed graph representation.In addition, when attempting to construct the graph representation ofm
c
f
E
S, as Figure 1 shows, two specific vertexes ⊤ and ⊥ will be added as initial state and terminal state corresponding to initial configuration and maximal configuration, respectively.A subset of elements forms an order ideal if whenever an element is contained in the subset then all its preceding elements are also contained in the subset. Intuitively, order ideals or left-closed subsets can be graphically represented by graph ideals. Generally, independency relation will not be represented explicitly. It is not difficult to have that partial order trace is only a special case of prime event structure with no conflict relations. Here, graph ideal is a notion equivalent to the configuration of an event structure. Empty set and the set of all vertices are called trivial ideal. Similarly, initial configuration and complete configuration are also called trivial configurations.Definition 31 (predicate on configuration).
Intuitively, a logic formula or predicate is a Boolean-valued function defined on the set of configurations:φ
:
Conf
F
(
E
)
→
{
0,1
}. It actually represents a subset of configurations in which the Boolean function evaluates to 1.The predicate detection problem is to decide whether the initial configuration of an event structure satisfies a predicate. More formally, we have the following definition.Definition 32 (predicate detection).
For any prime event structureE and any predicate φ, predicate detection is to decide whether Conf
F
(
E
)
,
{
⊥
}
⊨
φ holds or not.Predicates are used to specify system behaviors and properties such as safety and liveness. Properties expressed by a CTL (computational tree logic, introduced in [30]) formula are beyond the scope of this paper. For evaluating the value of a predicate efficiently, various predicate classes [28] such as conjunctive, stable, observer-independent, linear, relational, and nontemporal regular [7] predicates have been defined.Generally, predicate on configurations will act as the slicing criterion for POTs slicing.Definition 33 (slice ofm
c
f
E
S(POTs)).
Aslice of a m
c
f
E
S(POTs): E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of prime event structure E with respect to a formula φ, denoted by m
c
f
E
S
slice
(
E
i
max
⁡
,
φ
), is such an event structure that satisfies the following. (i)
Its family of configurations contains all the configurations that satisfyφ.
(ii)
Its family of configurations has the least number of configurations and still forms a sublattice.This formal definition is derived from computation slice notion [7] given by Garg and Mittal. Meanwhile, existence and uniqueness of the m
c
f
E
S slice have also been discussed; that is, the following theorem holds.Theorem 34.
For anyE
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of a prime event structure and any predicate φ, the slice of with respect to predicate φ, that is, m
c
f
E
S
slice
(
E
i
max
⁡
,
φ
) exists and is unique.Proof. The proof is straightforward; see [8, 20, 31].In general, the family of configurations for am
c
f
E
S forms a distributed lattice, and its slice with respect to a predicate is a sublattice. Sometimes a slice may contain those configurations that do not satisfy the predicate for completing sublattice.In the next section, we will discuss the slicing definition and model for prime event structure.


## 5.2.  Sliced Model over Event Structure

Generally, predicate on configurations acts as the slicing criterion for prime event structure slicing. Temporal regular predicate, such as a regular subset of CTL called RCTL [7, 8, 29], which contains four temporal operators EF, AG, EG, and EX[j], and nontemporal regular predicates both can also be taken as the slicing criterions.Compared with the definition of slice ofm
c
f
E
S, we have a similar case for prime event structure.Definition 35 (slice of prime event structure).
A slice of a prime event structure with respect to a formulaφ, denoted by S
l
i
c
e
E
S
(
E
,
φ
), is such an event structure that satisfies the following. (i)
Its family of configurations contains all the configurations that satisfyφ.
(ii)
Its family of configurations has the least number of configurations.Generally, a slice may contain configurations that do not satisfy the given predicate. The slice of an event structure with respect to a predicate is calledlean [32] if every configuration of the slice satisfies the predicate.Theorem 36.
For anyE
∈
E and any predicate φ, S
l
i
c
e
E
S
(
E
,
φ
) exists and is unique, and S
l
i
c
e
E
S
(
E
,
φ
)
=
w
c
c
(
m
c
f
E
S
s
l
i
c
e
(
c
f
p
(
E
)
,
φ
)
) holds.Proof. (1) Existence and Uniqueness. From Theorem 34, we have that, for any E
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
) of a prime event structure E and any predicate φ, its slice with respect to predicate φ exists and is unique.For anym
c
f
E
S, the family of configuration of m
c
f
E
S
slice
(
E
i
max
⁡
,
φ
) is a distributed lattice and is unique.Further, let⋃
E
C
=
⋃
1
≤
i
≤
N
E
(
m
c
f
C
o
n
f
(
m
c
f
E
S
s
l
i
c
e
)
(
(
E
i
max
⁡
,
φ
)
)
); ⋃
E
C is also unique and (
⋃
E
C
,
⊆
) is a finitary coherent prime algebraic domain.Next, we show that the slicing operation will keep the second part of necessary and sufficient condition for composition.For anyE
i
max
⁡ and E
j
max
⁡
(
j
≠
i
), if E
E
i
max
⁡
∩
E
E
j
max
⁡
=
D and D
≠
∅, we then have that c
f
subConf
F
(
E
i
max
⁡
,
D
)
=
c
f
subConf
F
(
E
j
max
⁡
,
D
); that is, for any nonempty event subset D
′
(
D
′
⊆
D
) and any predicate φ, if any configuration of D
′ satisfies φ, that is, D
′ is the common part of both slices of E
i
max
⁡ and E
j
max
⁡. We still get that c
f
subConf
F
(
E
i
max
⁡
,
D
′
)
=
c
f
subConf
F
(
E
j
max
⁡
,
D
′
).This means that, for any twom
c
f
E
S
s, if their intersection is nonempty, no matter which part of the intersection belongs to the slice, after slicing, the necessary and sufficient condition for composition will be still satisfied.Thus, we get that⋃
E
C is a valid family of configurations for prime event structures; there should exist such a unique prime event structure R
∈
E that satisfies Conf
F
(
R
)
=
⋃
E
C. We can get R by applying w
c
c to the corresponding event structures of ⋃
E
C.Therefore, the existence and uniqueness for event structure slicing have been established. We will then prove that the prime event structureR is the ultimate result of slicing.(2) Satisfactoriness and Minimality. On the one hand, for any configuration X of event structure E that makes predicate φ hold, that is, X
∈
Conf
F
(
Slice
E
S
(
E
,
φ
)
), there must be a m
c
f
E
S: E
i
max
⁡ so that X
∈
Conf
F
(
Slice
E
S
(
E
,
φ
)
); let C
i
=
m
c
f
Conf
F
(
m
c
f
E
S
slice
(
E
j
max
⁡
,
φ
)
), because C
i contains all the configurations of event structure E
j
max
⁡ that make predicate φ hold. We have that X must be contained by C
i; that is, X
∈
C
i.We getX
∈
Conf
F
(
Slice
E
S
(
E
,
φ
)
)
⇒
X
∈
⋃
E
C.Further, we getConf
F
(
Slice
E
S
(
E
,
φ
)
)
⊆
⋃
E
C.On the other hand, for any configurationX
∈
⋃
E
C, we get X
∈
Conf
F
(
E
) and X can make predicate φ hold; then X
∈
Conf
F
(
Slice
E
S
(
E
)
) must hold. Thus, we get X
∈
⋃
E
C
⇒
X
∈
Conf
F
(
Slice
E
S
(
E
,
φ
)
).That is,⋃
E
C
⊆
Conf
F
(
Slice
E
S
(
E
,
φ
)
).Therefore, we have⋃
E
C
=
Conf
F
(
Slice
E
S
(
E
,
φ
)
).Thus, we get thatSlice
E
S
(
E
,
φ
)
=
R.Moreover, by the definition of slice of maximal conflict-free event substructure, we have that, for anyE
i
max
⁡
(
i
∈
N
,
1
≤
i
≤
N
E
), the corresponding m
c
f
E
S
slice
(
E
i
max
⁡
,
φ
) contains the least number of configurations that satisfy the given predicate φ; we then have that ⋃
E
C
=
Conf
F
(
Slice
E
S
(
E
,
φ
)
) also contains the least number of configurations satisfying this specification. Thus, satisfactoriness and minimality both hold.Consequently, from both(
1
) and (
2
), we conclude that the theorem holds.


## 5.3. Slicing Reduction Algorithm

In this section, we will present an approach for event structure slice computing. The slicing algorithm for a prime event structure or itsm
c
f
E
S
s with respect to regular predicates is based on theAdding Edges Theorem (see [8, 20, 31, 33]).In fact, by the following theorem, these lattices will never be actually constructed in the slicing process for efficiency.The configurations do not satisfy the predicate but still can be included to complete the sublattice.Given a distributive latticeL generated by a graph G, every sublattice of L can be generated by a graph obtained by adding edges to G. The following theorem holds.Theorem 37 (Adding Edges Theorem).
LetL
′ be any sublattice of a finite distributive lattice L generated by the directed graph G. Then, there exists a graph G
′ that can be obtained by adding edges to (removing vertices from)  G that generates L
′.For any prime event structure, we can get the slices of itsm
c
f
E
S
s by applying the Adding Edges Theorem. These slices can be composed by w
c
c to form a new prime event structure which is the target slice of the original event structure. This approach is less general but results in more efficient detection algorithms for a special class of predicates. Note that we will never actually construct the lattice or family of configurations of the event structure due to efficiency.Garg and Mittal have presented an efficient algorithmslice
(
G
,
φ
) [8, 28] based on graphical representation G to compute the slice of POTs (or conflict-free event structures) with respect to a predicate φ. The algorithm adopts the principle of the Adding Edges Theorem and can produce a sliced graph representation. Especially, we have G
=
slice
(
G
,
true
) for predicate φ
=
true itself.We extend the idea and algorithm to more general models and provide an algorithm for slicing them
c
f
E
S
s and the original prime event structure. Thus, we have Algorithm 2 to compute the slice of conflict-free event structure.Algorithm 2:Slicing algorithm: m
c
f
E
S
s
l
i
c
e
(
m
c
f
E
S
(
E
)
,
φ
).
Input:
(1) a conflict-free event structure:m
c
f
E
S
(
E
),
(2) a regular predicate:φ
Output: the slice of m
c
f
E
S: E
i
max
⁡
s
l
i
c
e
BEGIN
(1)K
=
∅;
(2) generate graph representationG for E
i
max
⁡;
(3) computing slice:K
=
s
l
i
c
e
(
G
,
φ
);
(4) generate event structureE
i
max
⁡
s
l
i
c
e from graph representation K;
(5) returnE
i
max
⁡
s
l
i
c
e;
ENDFor a prime event structure with conflict relations, we have to applyc
f
p operator to get m
c
f
s
e
t
N
(
E
) maximal conflict-free event substructures and each of them can be sliced by m
c
f
E
S
slice. Then, the set consisting of each sliced result can be composed together by w
c
c to construct a new event structure. This new event structure will be the sliced result.Thus, we can derive Algorithm3 to compute the slice of a prime event structure.Algorithm 3:Slicing algorithm: s
l
i
c
e
E
S
(
E
,
φ
).
Input:
(1) an event structure:E
(2) a regular predicate:φ
Output: the slice: E
s
l
i
c
e
BEGIN
(1)
i
n
t  n
=
0, C
=
∅;
(2)
R
=
∅;
(3)
B
m
c
f
E
S
(
E
)
=
c
f
p
(
E
)
(4)
n
=
m
c
f
s
e
t
N
(
E
);
(5)for (i
n
t
i
=
0
;
i
<
n
;
i++) {
(6)  get theith  m
c
f
E
S: E
i
max
⁡ from B
m
c
f
E
S;
(7)C
=
C
∪
m
c
f
E
S
s
l
i
c
e
(
E
i
max
⁡
,
φ
);
(8)}
(9)if (C
≠
∅){
(10)
R
=
w
c
c
(
C
);
(11)  }
(12)  returnR;
ENDBecause the set of the slices ofm
c
f
E
S
s may no longer keep the weak conflict relation which exists in the original m
c
f
E
S
s.Therefore, afterm
c
f
E
S
slice
(
m
c
f
E
S
(
E
)
,
φ
) operation is performed, the relation among these slices can be one of the following cases:(1)
strong conflict;
(2)
conflict-free;
(3)
weak conflict;
(4)
hybrid of weak conflict and conflict-free;
(5)
hybrid of weak conflict and strong conflict;
(6)
hybrid of strong conflict, weak conflict, and conflict-free.In case of (1), (3), and (5), the operationw
c
c can be performed directly. But in case of (2), (4), and (6), we have to add some events in order to make the result set of slices still be able to form a valid weak conflict set at the end of process.For temporal predicates [8], such as E
F, E
G and A
G can be computed by slice
(
G
,
E
F
(
φ
)
), slice
(
G
,
E
G
(
φ
)
), and slice
(
G
,
A
G
(
φ
)
), respectively. From the definition of a slice, we know that every configuration of a slice slice
E
S
(
E
,
φ
) is also a configuration of E.Clearly, the following two corollaries hold.Corollary 38.
(1) For any prime event structureE
∈
E, Conf
F
(
slice
E
S
(
E
,
E
G
(
φ
)
)
)
⊆
Conf
F
(
slice
E
S
(
E
,
φ
)
)
⊆
Conf
F
(
E
).
Similarly forA
G, the following holds.
(2) For any prime event structureE
∈
E, Conf
F
(
slice
E
S
(
E
,
A
G
(
φ
)
)
)
⊆
Conf
F
(
slice
E
S
(
E
,
φ
)
)
⊆
Conf
F
(
E
).Corollary 39.
For any prime event structureE
∈
E, Conf
F
(
slice
E
S
(
E
,
E
F
(
φ
)
)
)
⊆
Conf
F
(
E
).


## 5.4. Case Study for Slicing Reduction

In this section, we will give an example to illustrate the prime event structure slice notion and its computing process.Consider a prime event structure:E
=
(
E
E
,
≤
E
,
♯
E
,
l
E
), as shown in Figure 2. The components are described as follows:(1)
event set:E
E
=
{
e
a
,
e
b
,
e
c
,
e
1
,
e
2
,
e
3
,
e
4
};
(2)
conflict relation:#
E
=
{
e
b
#
e
1
};
(3)
casual relation:⪯
E
=
{
e
b
⪯
e
a
,
e
c
⪯
e
a
,
e
1
⪯
e
2
,
e
1
⪯
e
4
,
e
3
⪯
e
4
,
e
c
⪯
e
3
};
(4)
action labels:l
E
(
e
a
)
=
a
,
l
E
(
e
b
)
=
b
,
l
E
(
e
c
)
=
c,l
E
(
e
1
)
=
a
1
,
l
E
(
e
2
)
=
a
2
,
l
E
(
e
3
)
=
a
3
,
l
E
(
e
4
)
=
a
4;
(5)
action functions:
(i)
action
(
a
1
)
:
{
x
=
x
+
1
}
;
(ii)
action
(
a
2
)
:
{
x
=
x
+
3
};
(iii)
action
(
a
3
)
:
{
y
=
y
+
3
};
(iv)
action
(
a
4
)
:
{
y
=
y
+
2
};
(v)
action
(
a
)
:
{
z
=
z
+
2
};
(vi)
action
(
b
)
:
{
z
=
z
+
1
};
(vii)
action
(
c
)
:
{
y
=
y
-
1
};
(viii)
initValue
:
{
x
=
1
;
y
=
1
;
z
=
0
};
(6)
slice criterion:{
φ
=
-
2
≤
(
y
-
x
+
z
)
<
2
}.Figure 2
A Prime event structureE.In this example, the system global states will be updated after an action function executes. Figure2 depicts all the events conflict (for simplicity, only immediate conflict relation is shown) and casual relation. Figure 3 shows its corresponding family of configurations.Figure 3
Family of configurations ofE.There is one conflict relation between eventb and e
1; due to the conflict inheritance property of prime event structures, we have e
b
♯
e
1
,
e
b
♯
e
2
,
e
b
♯
e
4 and e
a
♯
e
1
,
e
a
♯
e
2
,
e
a
♯
e
4; that is, each of {
e
a
,
e
b
} is in conflict with each of {
e
1
,
e
2
,
e
4
}. Obviously, according to this conflict relation, apply c
f
p operation to the prime event structure E and we get that this event structure has only two m
c
f
E
S
s: they are E
1
=
(
{
e
a
,
e
b
,
e
c
,
e
3
}
,
≤
E
1
,
∅
,
l
E
1
) and E
2
=
(
{
e
1
,
e
2
,
e
3
,
e
4
,
e
c
}
,
≤
E
2
,
∅
,
l
E
2
) depicted by Figures 4(1) and 4(2), respectively, and Figures 5(1) and 5(2) show their corresponding families of configurations.Figure 4
m
c
f
E
S
s of E: E
1 and E
2.Figure 5
Families of configurations ofm
c
f
E
S
s(E
1 and E
2).The configurations that satisfy the predicate are labelled with frames. In fact, these configurations are only used to describe relationship between original event structure and its slice graphically; in general, they will never be actually constructed in the slicing algorithm for efficiency.The families of configurations of the slices ofE
1 and E
2 with respect to the predicate {
φ
=
-
2
≤
(
y
-
x
+
z
)
<
2
} are shown in Figures 6(1) and 6(2), respectively. It can be verified that both m
c
f
Conf
(
E
1
) and m
c
f
Conf
(
E
2
) form distributed lattices.Figure 6
Subfamilies of configurations of the slices.These configurations of the slices are exactly the ones that satisfy the given predicate in the family of configurations of the original event structure. Figure7 shows the family of configurations constructed by applying ∪ operation to the families of configurations of all slices.Figure 7
Subfamily of configurations of the slice.Finally, in Figure8, the slice of E
1 and the slice of E
2 are combined into the slice of E by w
c
c operator, as expected.Figure 8
Slice model with respect toφ.To illustrate the benefit of predicate detection by using slicing reduction as shown in above example, consider the states in Figure3 again.Let{
φ
=
-
2
≤
(
y
-
x
+
z
)
<
2
} be the predicate to be checked, and suppose we want to detect whether E
F
(
φ
) holds or not; that is, there exists a global state that satisfies φ. Without slicing reduction applied, we are forced to examine all global states, 15 states in total as shown in Figure 3, to decide whether the traces satisfy the predicate.Alternatively, we can compute the slice via slicing reduction technique with respect to the regular temporal predicate and use this slice for predicate detection.For this purpose, firstly, we compute the slice with respect toφ and the slice is shown in Figure 7.Finally, we check whether the initial state is the same as the initial state of the slice and decide whether the predicate is satisfied or not.The slice contains only 9 states and has much fewer states than the original traces itself. Generally, it is exponentially smaller in many cases and this can result in substantial savings.


## 6. Symmetry Reduction

Finite state systems frequently exhibit symmetry which can be found in memories, caches, register files, bus protocols, and anything that has a lot of replicated structures. The use of symmetry to reduce state space has been investigated widely by researchers [2, 3, 15, 22, 23].In this section, we will discuss symmetry properties over prime event structures. Symmetry in an event structure implies the existence of nontrivial permutation groups that preserve both the events labelling and all relations of causal dependence and independence that exist between events. We start by introducing some notions of group theory.


### 6.1. Automorphism Groups

We know that the set of all permutation on a set forms a permutation group under functional composition. A permutation group over a finite setX consists of bijections, X
→
X, and their compositions as the binary operations.Definition 40 (permutation group).
LetX be a finite set; apermutation of X is a bijection from X to itself. Then, S
X
:
=
{
f
:
X
→
X
∣
f
i
s
a
b
i
j
e
c
t
i
o
n
}; that is, the family of all the permutations of the set X, denoted by S
X, forms a group called thesymmetric group on X. For any bijection f
∈
S
X is called apermutation. Any subgroup of is called a permutation group on X.Obviously, a symmetric group is a special permutation group. A permutation group over a set has good properties; specially, it can induce an equivalence relation. The equivalence classes of an equivalence relation on a set can form a partition of this set. Thus, for a setX, if there exists a permutation group on the set X, the permutation group can induce a partition of the set X. We can easily check this property.In this paper, permutation groups are used to partition the set of events in an event structure so that we use equivalence classes (orbits) of events to investigate symmetry in this event structure.Definition 41 (automorphism).
LetE
=
(
E
,
⪯
,
♯
,
l
)
∈
E and let G be a permutation group on the event set E of E. A permutation f
∈
G is said to be anautomorphism of E if and only if f satisfies the following conditions: (1)
∀
e
1
,
e
2
∈
E
:
e
1
⪯
e
2
⇒
f
(
e
1
)
⪯
f
(
e
2
)
,
e
1
♯
e
2
⇒
f
(
e
1
)
♯
f
(
e
2
);
(2)
l
(
e
1
)
=
l
(
f
(
e
2
)
).Definition 42 (automorphism group).
A permutation groupG is called anautomorphism group for the event structure E  (
E
=
(
E
,
⪯
,
♯
,
l
)
∈
E
) if and only if every permutation f
∈
G is an automorphism of E.Notice that everyf
∈
G has an inverse, which is also an automorphism; our definition of an automorphism group can prove that f
∈
G is an automorphism for an event structure E if and only if f satisfies the following condition: ∀
e
1
,
e
2
∈
E
:
e
1
⪯
e
2
⇔
f
(
e
1
)
⪯
f
(
e
2
)
;
e
1
♯
e
2
⇔
f
(
e
1
)
♯
f
(
e
2
)
;
and
l
(
e
1
)
=
l
(
f
(
e
2
)
).


### 6.2. Quotient Model of an Event Structure

The symmetric quotient model for an event structure is a structural reduced model.LetG be a permutation group acting on the set E and e
∈
E; then the orbit of e is the set θ
(
e
)
=
{
d
∣
∃
g
∈
G
:
f
(
e
)
=
d
}. From each orbit θ
(
e
) we pick a representative that is called rep
(
θ
(
e
)
). Intuitively, the quotient model can be obtained by collapsing all the events to orbits.Definition 43 (symmetric quotient model).
LetE
=
(
E
,
⪯
,
♯
,
l
)
∈
E and let G be an automorphism group on the event set E of the event structure E. Thesymmetric quotient model
E
G
=
(
E
G
,
⪯
G
,
♯
G
,
l
G
) is defined as follows. (1)
The event set isE
G
=
{
θ
(
e
)
∣
e
∈
E
}, the set of orbits of the events in E.
(2)
The causality relation⪯
G is given by ⪯
G
=
{
(
θ
(
e
1
)
,
θ
(
e
2
)
)
∣
(
e
1
,
e
2
)
∈
⪯
} and the inverse of ⪯
G is denoted by ⪰
G.
(3)
The conflict relation♯
G is given by ♯
G
=
E
G
×
E
G
∖
(
≺
G
∪
≻
G
∪
c
o
G
∪
{
(
e
′′
,
e
′′
)
∣
e
′′
∈
E
G
}
), where c
o
G
=
{
(
θ
(
e
1
)
,
θ
(
e
2
)
)
∣
co
⁡
=
E
×
E
(
⪯
∪
⪰
∪
♯
∪
(
e
′
,
e
′
)
∣
e
′
∈
E
)
,
(
e
1
,
e
2
)
∈
E
}.
(4)
The labelling functionl
G is given by l
G
(
θ
(
e
)
)
=
l
(
rep
(
θ
(
e
)
)
).An automorphism groupG of an event structure E
=
(
E
,
⪯
,
♯
,
l
) is an invariance group for an action a
∈
A
c
t if and only if the following condition holds: ∀
f
∈
G
,
e
∈
E
:
l
(
θ
)
=
a
⇔
l
(
f
(
θ
)
)
=
a.We then say thata is an invariant under G. Thus, if G is an invariance group for all actions in the action set Act of E and E
G is the symmetric quotient model for E; we can directly have ∀
a
∈
Act
,
e
∈
E
:
l
(
θ
)
⇔
l
G
(
θ
(
e
)
)
=
l
(
rep
(
θ
(
e
)
)
=
a.From the above definition, we have that the symmetric quotient model is still a prime event structure and preserves all the causal dependence and independence relations of the original, but the conflict relations are reduced. Note that every two different events in an orbit are exactly in conflict with each other. The quotient model can preserve all the behavior of the original one.


### 6.3. Symmetry Reduction Algorithm

Based on previous discussion, we have Algorithm4 for symmetry reduction. In this algorithm, replicated substructure will be removed and only one copy will be kept.Algorithm 4:Symmetry reduction: s
r
(
E
).
Input: a prime event structure E;
Output: the reduced model of the event structure: E
s
r;
BEGIN
(1)
C
=
∅
;
i
=
1
;
n
=
0
;
B
=
∅
;
B
=
∅;
/*  Step  One: partition via c
f
p operator, we will get all maximal conflict-free sub-structure of an event structure */
(2)
B
=
B
m
c
f
E
S
(
E
)
=
c
f
p
(
E
);
(3)
n
=
m
c
f
s
e
t
N
(
E
);
/*  Step  Two: automorphism checking for sub-structure */
(4) for (i
=
0
;
i
≤
n
;
i++) {
(5)    for (j
=
0
;
i
≤
i
;
j++) {
/*  Step  Two-1: get action set of each maximal conflict-free sub-structure from B  */
(6)L
A
c
t
(
E
i
)
=
{
a
∈
A
c
t
∣
∃
e
∈
E
i
:
l
(
e
)
=
a
}
(7)L
A
c
t
(
E
j
)
=
{
a
∈
A
c
t
∣
∃
e
∈
E
j
:
l
(
e
)
=
a
}
/*  I
s
N
o
t
I
d
e
n
t
i
c
a
l: checking two sets are are identical or not*/
/*  |
S
|: the element amount of the set S  */
/*  Step  Two-2: checking their action sets are identical or not */
(8)  if ((|
L
A
c
t
(
E
i
|
≠
|
L
A
c
t
(
E
j
)
|) ∥
I
s
N
o
t
I
d
e
n
t
i
c
a
l
(
L
A
c
t
(
E
i
)
,
L
A
c
t
(
E
j
)) {
(9)  break; }
/*  Step  Two-3: checking their causal relations are identical or not */
(10)  if ((|
⪯
E
i
max
⁡
|
≠
|
⪯
E
j
max
⁡
|) ∥
I
s
N
o
t
I
d
e
n
t
i
c
a
l
(
⪯
E
i
max
⁡
,
⪯
E
j
max
⁡) {
(11)  break; }
/*  Step  Two-4: checking their conflict relations are identical or not */
(12)  if ((|
#
E
i
max
⁡
|
≠
|
#
E
j
max
⁡
|) ∥
I
s
N
o
t
I
d
e
n
t
i
c
a
l
(
#
E
i
max
⁡
,
#
E
j
max
⁡) {
(13)  break; }
/*  Step  Three: automorphism exists, remove the duplicated one and merge for reduction */
(14)B
=
B
-
E
j
max
⁡;
(15)n
=
n
-
1;
(16)  } /* end forj  */
(17)  } /* end fori  */
(18) returnE
s
r
=
w
c
c
(
B
);
END;Firstly,c
f
p operator will be applied on a given event structure to get a set of conflict-free substructures.Then, for any two elements of them, a checking procedure will be performed to remove the redundant one.Finally,w
c
c will be applied on the substructure set to get the reduced model. Detailed pseudocode description is shown  in Algorithm 4.


### 6.4. An Example for Symmetry Reduction

In this section, an example will be discussed to demonstrate the reduction process based on Algorithm4.The example of a prime event structureE with five events (e
1, e
2, e
3, e
4, and e
5) and its semantics in terms of families of configurations is given in Figures 9(1) and 9(2), respectively.Figure 9
An event structure and its family of configurations.The action-labelling (action set:A
c
t
=
{
a
,
b
,
c
,
d
}) function is defined as follows: l
(
e
1
)
=
a, l
(
e
2
)
=
b, l
(
e
3
)
=
c, l
(
e
4
)
=
b, and l
(
e
5
)
=
d.In this structure, we havee
3
⪯
e
5, e
2
♯
e
4, e
3
♯
e
2, and e
3
♯
e
4. We also have e
5
♯
e
2, e
5
♯
e
1, and e
5
♯
e
4(due to conflict inheritance).Then event set isE
G
=
{
e
1
,
e
2
,
e
3
,
e
4
,
e
5
} and we can construct a permutation group G on the set E
G where two permutations are as follows:
(3)
(
e
1
e
2
e
3
e
4
e
5
e
1
e
2
e
3
e
4
e
5
)
(
e
1
e
2
e
3
e
4
e
5
e
1
e
4
e
3
e
2
e
5
)Obviously, the groupG is an invariance group for all actions in A
c
t
=
{
a
,
b
,
c
,
d
}. We then have the orbits of events in being θ
(
e
2
)
=
θ
(
e
4
)
=
{
e
2
,
e
4
}, θ
(
e
1
)
=
{
e
1
}, θ
(
e
3
)
=
{
e
3
}, and θ
(
e
5
)
=
{
e
5
}. Thus, the symmetric quotient model can be described as shown in Figure 10.Figure 10
Symmetric quotient model ofE: E
G.We can get weak conflict set of the event structureE by c
f
p operator as follows: c
f
p
(
E
)
=
{
E
1
,
E
2
,
E
3
}, where
(4)
E
1
=
(
E
1
,
⪯
1
,
♯
1
,
l
1
)
,
E
2
=
(
E
2
,
⪯
2
,
♯
2
,
l
2
)
,
E
3
=
(
E
3
,
⪯
3
,
♯
3
,
l
3
)
,
E
1
=
{
e
1
,
e
2
}
,
E
2
=
{
e
1
,
e
4
}
,
E
3
=
{
e
1
,
e
3
,
e
5
}
.Thus, we haveE
1
♯
w
E
2, E
1
♯
w
E
3, and E
3
♯
w
E
2 (or, E
1
♯
w
E
2, E
1
♯
w
E
3, and E
3
♯
w
E
2).By definition, we have thatE
1 and E
2 are symmetric. According to the symmetry reduction algorithm, we will remove replicated events but keep the common or representation ones. The substructure E
2 is removed. The resulted substructure set consists of two elements: E
1 and E
3, because E
1 and E
3 are weak conflict sets of E and w
c
c operator can be applied on them to construct a new event structure: E
'
=
w
c
c
(
E
1
,
E
3
). Thus, the symmetric reduced event structure can be described by Figure 11.Figure 11
Reduced model:E
'.To illustrate the advantage for properties checking by using symmetry reduction as shown in the above example, consider the states in Figure9, 9 states in total.Suppose we want to check whether a propertyE
F
(
p
) holds or not; that is, there exists a global state that satisfies φ. Without symmetry reduction applied, we have to examine all global states, 9 states in total. But with symmetry reduction, as shown in Figure 11 or Figure 10 to decide whether the property holds, only 7 states should be checked and a considerable saving can be achieved.


## 6.1. Automorphism Groups

We know that the set of all permutation on a set forms a permutation group under functional composition. A permutation group over a finite setX consists of bijections, X
→
X, and their compositions as the binary operations.Definition 40 (permutation group).
LetX be a finite set; apermutation of X is a bijection from X to itself. Then, S
X
:
=
{
f
:
X
→
X
∣
f
i
s
a
b
i
j
e
c
t
i
o
n
}; that is, the family of all the permutations of the set X, denoted by S
X, forms a group called thesymmetric group on X. For any bijection f
∈
S
X is called apermutation. Any subgroup of is called a permutation group on X.Obviously, a symmetric group is a special permutation group. A permutation group over a set has good properties; specially, it can induce an equivalence relation. The equivalence classes of an equivalence relation on a set can form a partition of this set. Thus, for a setX, if there exists a permutation group on the set X, the permutation group can induce a partition of the set X. We can easily check this property.In this paper, permutation groups are used to partition the set of events in an event structure so that we use equivalence classes (orbits) of events to investigate symmetry in this event structure.Definition 41 (automorphism).
LetE
=
(
E
,
⪯
,
♯
,
l
)
∈
E and let G be a permutation group on the event set E of E. A permutation f
∈
G is said to be anautomorphism of E if and only if f satisfies the following conditions: (1)
∀
e
1
,
e
2
∈
E
:
e
1
⪯
e
2
⇒
f
(
e
1
)
⪯
f
(
e
2
)
,
e
1
♯
e
2
⇒
f
(
e
1
)
♯
f
(
e
2
);
(2)
l
(
e
1
)
=
l
(
f
(
e
2
)
).Definition 42 (automorphism group).
A permutation groupG is called anautomorphism group for the event structure E  (
E
=
(
E
,
⪯
,
♯
,
l
)
∈
E
) if and only if every permutation f
∈
G is an automorphism of E.Notice that everyf
∈
G has an inverse, which is also an automorphism; our definition of an automorphism group can prove that f
∈
G is an automorphism for an event structure E if and only if f satisfies the following condition: ∀
e
1
,
e
2
∈
E
:
e
1
⪯
e
2
⇔
f
(
e
1
)
⪯
f
(
e
2
)
;
e
1
♯
e
2
⇔
f
(
e
1
)
♯
f
(
e
2
)
;
and
l
(
e
1
)
=
l
(
f
(
e
2
)
).


## 6.2. Quotient Model of an Event Structure

The symmetric quotient model for an event structure is a structural reduced model.LetG be a permutation group acting on the set E and e
∈
E; then the orbit of e is the set θ
(
e
)
=
{
d
∣
∃
g
∈
G
:
f
(
e
)
=
d
}. From each orbit θ
(
e
) we pick a representative that is called rep
(
θ
(
e
)
). Intuitively, the quotient model can be obtained by collapsing all the events to orbits.Definition 43 (symmetric quotient model).
LetE
=
(
E
,
⪯
,
♯
,
l
)
∈
E and let G be an automorphism group on the event set E of the event structure E. Thesymmetric quotient model
E
G
=
(
E
G
,
⪯
G
,
♯
G
,
l
G
) is defined as follows. (1)
The event set isE
G
=
{
θ
(
e
)
∣
e
∈
E
}, the set of orbits of the events in E.
(2)
The causality relation⪯
G is given by ⪯
G
=
{
(
θ
(
e
1
)
,
θ
(
e
2
)
)
∣
(
e
1
,
e
2
)
∈
⪯
} and the inverse of ⪯
G is denoted by ⪰
G.
(3)
The conflict relation♯
G is given by ♯
G
=
E
G
×
E
G
∖
(
≺
G
∪
≻
G
∪
c
o
G
∪
{
(
e
′′
,
e
′′
)
∣
e
′′
∈
E
G
}
), where c
o
G
=
{
(
θ
(
e
1
)
,
θ
(
e
2
)
)
∣
co
⁡
=
E
×
E
(
⪯
∪
⪰
∪
♯
∪
(
e
′
,
e
′
)
∣
e
′
∈
E
)
,
(
e
1
,
e
2
)
∈
E
}.
(4)
The labelling functionl
G is given by l
G
(
θ
(
e
)
)
=
l
(
rep
(
θ
(
e
)
)
).An automorphism groupG of an event structure E
=
(
E
,
⪯
,
♯
,
l
) is an invariance group for an action a
∈
A
c
t if and only if the following condition holds: ∀
f
∈
G
,
e
∈
E
:
l
(
θ
)
=
a
⇔
l
(
f
(
θ
)
)
=
a.We then say thata is an invariant under G. Thus, if G is an invariance group for all actions in the action set Act of E and E
G is the symmetric quotient model for E; we can directly have ∀
a
∈
Act
,
e
∈
E
:
l
(
θ
)
⇔
l
G
(
θ
(
e
)
)
=
l
(
rep
(
θ
(
e
)
)
=
a.From the above definition, we have that the symmetric quotient model is still a prime event structure and preserves all the causal dependence and independence relations of the original, but the conflict relations are reduced. Note that every two different events in an orbit are exactly in conflict with each other. The quotient model can preserve all the behavior of the original one.


## 6.3. Symmetry Reduction Algorithm

Based on previous discussion, we have Algorithm4 for symmetry reduction. In this algorithm, replicated substructure will be removed and only one copy will be kept.Algorithm 4:Symmetry reduction: s
r
(
E
).
Input: a prime event structure E;
Output: the reduced model of the event structure: E
s
r;
BEGIN
(1)
C
=
∅
;
i
=
1
;
n
=
0
;
B
=
∅
;
B
=
∅;
/*  Step  One: partition via c
f
p operator, we will get all maximal conflict-free sub-structure of an event structure */
(2)
B
=
B
m
c
f
E
S
(
E
)
=
c
f
p
(
E
);
(3)
n
=
m
c
f
s
e
t
N
(
E
);
/*  Step  Two: automorphism checking for sub-structure */
(4) for (i
=
0
;
i
≤
n
;
i++) {
(5)    for (j
=
0
;
i
≤
i
;
j++) {
/*  Step  Two-1: get action set of each maximal conflict-free sub-structure from B  */
(6)L
A
c
t
(
E
i
)
=
{
a
∈
A
c
t
∣
∃
e
∈
E
i
:
l
(
e
)
=
a
}
(7)L
A
c
t
(
E
j
)
=
{
a
∈
A
c
t
∣
∃
e
∈
E
j
:
l
(
e
)
=
a
}
/*  I
s
N
o
t
I
d
e
n
t
i
c
a
l: checking two sets are are identical or not*/
/*  |
S
|: the element amount of the set S  */
/*  Step  Two-2: checking their action sets are identical or not */
(8)  if ((|
L
A
c
t
(
E
i
|
≠
|
L
A
c
t
(
E
j
)
|) ∥
I
s
N
o
t
I
d
e
n
t
i
c
a
l
(
L
A
c
t
(
E
i
)
,
L
A
c
t
(
E
j
)) {
(9)  break; }
/*  Step  Two-3: checking their causal relations are identical or not */
(10)  if ((|
⪯
E
i
max
⁡
|
≠
|
⪯
E
j
max
⁡
|) ∥
I
s
N
o
t
I
d
e
n
t
i
c
a
l
(
⪯
E
i
max
⁡
,
⪯
E
j
max
⁡) {
(11)  break; }
/*  Step  Two-4: checking their conflict relations are identical or not */
(12)  if ((|
#
E
i
max
⁡
|
≠
|
#
E
j
max
⁡
|) ∥
I
s
N
o
t
I
d
e
n
t
i
c
a
l
(
#
E
i
max
⁡
,
#
E
j
max
⁡) {
(13)  break; }
/*  Step  Three: automorphism exists, remove the duplicated one and merge for reduction */
(14)B
=
B
-
E
j
max
⁡;
(15)n
=
n
-
1;
(16)  } /* end forj  */
(17)  } /* end fori  */
(18) returnE
s
r
=
w
c
c
(
B
);
END;Firstly,c
f
p operator will be applied on a given event structure to get a set of conflict-free substructures.Then, for any two elements of them, a checking procedure will be performed to remove the redundant one.Finally,w
c
c will be applied on the substructure set to get the reduced model. Detailed pseudocode description is shown  in Algorithm 4.


## 6.4. An Example for Symmetry Reduction

In this section, an example will be discussed to demonstrate the reduction process based on Algorithm4.The example of a prime event structureE with five events (e
1, e
2, e
3, e
4, and e
5) and its semantics in terms of families of configurations is given in Figures 9(1) and 9(2), respectively.Figure 9
An event structure and its family of configurations.The action-labelling (action set:A
c
t
=
{
a
,
b
,
c
,
d
}) function is defined as follows: l
(
e
1
)
=
a, l
(
e
2
)
=
b, l
(
e
3
)
=
c, l
(
e
4
)
=
b, and l
(
e
5
)
=
d.In this structure, we havee
3
⪯
e
5, e
2
♯
e
4, e
3
♯
e
2, and e
3
♯
e
4. We also have e
5
♯
e
2, e
5
♯
e
1, and e
5
♯
e
4(due to conflict inheritance).Then event set isE
G
=
{
e
1
,
e
2
,
e
3
,
e
4
,
e
5
} and we can construct a permutation group G on the set E
G where two permutations are as follows:
(3)
(
e
1
e
2
e
3
e
4
e
5
e
1
e
2
e
3
e
4
e
5
)
(
e
1
e
2
e
3
e
4
e
5
e
1
e
4
e
3
e
2
e
5
)Obviously, the groupG is an invariance group for all actions in A
c
t
=
{
a
,
b
,
c
,
d
}. We then have the orbits of events in being θ
(
e
2
)
=
θ
(
e
4
)
=
{
e
2
,
e
4
}, θ
(
e
1
)
=
{
e
1
}, θ
(
e
3
)
=
{
e
3
}, and θ
(
e
5
)
=
{
e
5
}. Thus, the symmetric quotient model can be described as shown in Figure 10.Figure 10
Symmetric quotient model ofE: E
G.We can get weak conflict set of the event structureE by c
f
p operator as follows: c
f
p
(
E
)
=
{
E
1
,
E
2
,
E
3
}, where
(4)
E
1
=
(
E
1
,
⪯
1
,
♯
1
,
l
1
)
,
E
2
=
(
E
2
,
⪯
2
,
♯
2
,
l
2
)
,
E
3
=
(
E
3
,
⪯
3
,
♯
3
,
l
3
)
,
E
1
=
{
e
1
,
e
2
}
,
E
2
=
{
e
1
,
e
4
}
,
E
3
=
{
e
1
,
e
3
,
e
5
}
.Thus, we haveE
1
♯
w
E
2, E
1
♯
w
E
3, and E
3
♯
w
E
2 (or, E
1
♯
w
E
2, E
1
♯
w
E
3, and E
3
♯
w
E
2).By definition, we have thatE
1 and E
2 are symmetric. According to the symmetry reduction algorithm, we will remove replicated events but keep the common or representation ones. The substructure E
2 is removed. The resulted substructure set consists of two elements: E
1 and E
3, because E
1 and E
3 are weak conflict sets of E and w
c
c operator can be applied on them to construct a new event structure: E
'
=
w
c
c
(
E
1
,
E
3
). Thus, the symmetric reduced event structure can be described by Figure 11.Figure 11
Reduced model:E
'.To illustrate the advantage for properties checking by using symmetry reduction as shown in the above example, consider the states in Figure9, 9 states in total.Suppose we want to check whether a propertyE
F
(
p
) holds or not; that is, there exists a global state that satisfies φ. Without symmetry reduction applied, we have to examine all global states, 9 states in total. But with symmetry reduction, as shown in Figure 11 or Figure 10 to decide whether the property holds, only 7 states should be checked and a considerable saving can be achieved.


## 7. Mathematical Framework

In this section, we will provide a unified mathematical framework for slicing and symmetry reduction based onc
f
p and w
c
c operators.Firstly, we will review some basic definitions in this section. Here, we refer the reader to [14] for details. Next, we will introduce the single action transitions [3] for event structures. Finally, we will discuss the related theories for slicing and symmetric reduction and establish the unified framework.


### 7.1. Basic Definitions

Definition 44.
For any event structureE
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E, define L
[
E
]
=
(
Conf
F
(
E
)
,
⊆
). Especially, for any conflict-free event structure F
=
(
E
F
,
⪯
F
,
∅
,
l
F
)
∈
F, define L
[
F
]
=
(
Conf
F
(
F
)
,
⊆
).In fact,L
[
F
] is the partial order of left-closed and conflict-free subsets of E
E ordered by set inclusion.L
[
E
] is the partial order of left-closed subsets of E
F ordered by set inclusion.Definition 45 (single action transition).
LetE
∈
E. A transition X
→
a
E
X
′ is called asingle action transition if and only if a
∈
A
c
t
,
X
,
X
′
∈
Conf
F
(
E
)
,
X
⊆
X
′ and there exists an event e such that X
′
-
X
=
e with l
E
(
e
)
=
a.Here,X
→
a
E
X
′ indicates that in the event structure the state represented by the configuration X may evolve into a state represented by the configuration by performing the action a. This transition relation associates a labelled system based on single action transitions with each event structure.Definition 46 (trace).
LetE
∈
E. A word w
=
a
1
…
a
n
∈
A
c
t
* is calledtrace of E if and only if ∃
X
0
,
…
,
X
n
∈
C
o
n
f
F
(
E
)
:
X
0
=
∅ and X
i
-
1
→
a
i
X
i
,
i
=
1
,
…
,
n.Here, letTrs
(
E
) denote the set of all traces of E.Definition 47 (interleave trace equivalence).
LetE
1
,
E
2
∈
E. E
1 and E
2 are calledinterleave trace equivalence
(
E
1
≈
i
t
E
2
) if and only if Trs
(
E
1
)
=
Trs
(
E
2
).Definition 48 (interleaving bisimulation).
LetE
1
,
E
2
∈
E. A relation R
⊆
C
(
E
1
)
×
C
(
E
2
) is called interleaving bisimulation between E
1 and E
2 if and only if (
∅
,
∅
)
∈
R and (
X
,
Y
)
∈
R; then (1)
X
→
a
E
1
X
′
,
a
∈
A
c
t
⇒
∃
Y
′
:
Y
→
a
E
2
Y
′
∧
(
X
′
,
Y
′
)
∈
R;
(2)
Y
→
a
E
2
Y
′
,
a
∈
A
c
t
⇒
∃
X
′
:
X
→
a
E
1
X
′
∧
(
X
′
,
Y
′
)
∈
R.Definition 49 (interleaving bisimulation equivalent).
LetE
1
,
E
2
∈
E. E
1 and E
2 are called interleaving bisimulation equivalent
(
E
1
≈
i
b
E
2
) if and only if there exists an interleaving bisimulation between E
1 and E
2.


### 7.2. Unified Framework

The unified framework for slicing and symmetry reduction we have set up can be pictured as in Figure12.Figure 12
Unified mathematical framework.(1) Isomorphism and Equivalence. We are concerned with the translation of concepts and ideas from one side to the other. The following theorems hold.Theorem 50.
LetF be a conflict-free event structure, F
=
(
E
F
,
⪯
F
,
∅
,
l
F
)
∈
F; then F
≅
℘
[
L
[
F
]
]. Similarly, let P
=
(
D
,
⊑
) be a prime algebraic complete lattice; then P
≅
L
[
℘
[
P
]
].Theorem 51.
LetE be a prime event structure, E
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E; then E
≅
℘
[
L
[
E
]
]. Similarly, let P
=
(
D
,
⊑
) be a prime algebraic coherent domain; then P
≅
L
[
℘
[
P
]
].Clearly, from Theorems50 and 51, we have the following.(1)
For any prime event structureE, we have that E
≅
℘
[
L
[
E
]
].
(2)
Similarly, for any partial orderP
=
(
D
,
⊑
), P is a prime algebraic complete lattice or a finitary coherent prime algebraic domain; we have that P
≅
L
[
℘
[
P
]
].From Theorems23, 24, and 25, we have that conflict-free event structures and prime algebraic complete lattices are equivalent; this implies that there is a one-to-one correspondence between a prime event structure and its family of configurations. Similarly, prime event structures and finitary coherent prime algebraic domains are also equivalent; one can be used to represent the other.(2) Mutual Inverse Operation. For any prime event structure, c
f
p and w
c
c are mutually inverse operators.We can get the full set of maximal conflict-free substructures of a prime event structure byc
f
p operator.Conversely, given the full set of maximal conflict-free substructures of the prime event structure, we can recover the original prime event structure byw
c
c operator.(3) Slicing Reduction. Firstly, compared with traditional computation slicing, Figure 12 demonstrates the translation between a conflict-free event structure (or its slice) and prime algebraic complete lattice. This forms the theoretical basis of computation slicing technique proposed by Garg and Mittal, Sen [7, 20].Secondly, Figure12 also demonstrates the translation between a prime event structure (or its slice) and finitary coherent prime algebraic domain, which serves as the theoretical basis of our event structure slicing with conflict. A pair of mutually inverse operators, c
f
p and w
c
c, act as a link between the two parts.Thirdly, the slice of a prime event structure can be computed by the following steps:(1)
applyingc
f
p operator to partition the original prime event structure into a full set of maximal conflict-free substructures;
(2)
for each maximal conflict-free substructure, applying traditional computation slicing algorithm based on Adding Edges Theorem [7, 8, 20] over its directed graph representation to compute the slice with respect to the given predicate;
(3)
applyingw
c
c operator to compose the resulted slices in above step (2) and form a new prime event structure, while the generated event structure is the slice of the original prime event structure.(4) Symmetry Reduction. Operators c
f
p and w
c
c can also play an important role in symmetry reduction.Symmetry reduction of a prime event structure can be performed by the following steps:(1)
applyingc
f
p operator to partition the original prime event structure into a full set of maximal conflict-free substructures;
(2)
checking automorphism among the produced substructures and checking causal relation and action set;
(3)
removing duplicated substructure and applyingw
c
c operator to compose the resulted structure to form a newly generated prime event structure, which will be symmetry reduced prime event structure.(5) Trace Equivalence. The relation between original event structure and its quotient model can be specified by Theorems 52 and 53 (See [3]).Theorem 52.
LetE
∈
E and E
G be quotient structure of E; then E
G
≈
i
t
E.Theorem 53.
LetE
∈
E and let E
G be the symmetric quotient model for E. Then E
≃
i
b
E
G.Generally, given an event structureE, in fact, its behavior is exhibited by the labelled transition system (LTS, for short) LT
S
E
=
{
Conf
F
(
E
), A
c
t
E
,
T
E
,
∅
}, where(1)
the configurationsConf
F
(
E
) are states;
(2)
the set of labels is the set of actionsA
c
t
E;
(3)
the transitionsT
E are single action transitions between every two configurations of E; namely, T
E
⊆
C
o
n
f
F
(
E
)
×
A
c
t
E
×
C
o
n
f
F
(
E
);
(4)
the initial configuration (the empty set∅) is the initial state.The above equivalence is based on labelled transition systems whose transitions are single action transitions. As shown in Figure12, we construct labelled transition system for prime event structure and its quotient model, we will have that their LTSs are interleaving bisimulation and interleave trace equivalence also. Therefore, the following corollary holds.Corollary 54.
LetE
∈
E and E
G let be the symmetric quotient model for E. If L
T
S
=
(
Conf
F
(
E
)
,
A
c
t
,
→
E
,
∅
)  and L
T
S
G
=
(
Conf
F
(
E
G
)
,
A
c
t
,
→
E
G
,
∅
) are induced from E and E
G, respectively, then L
T
S
≈
i
t
L
T
S
G and L
T
S
≈
i
b
L
T
S
G hold.Evidently, we have the following theorems.Theorem 55.
For anyE
∈
E, its symmetric quotient model E
G and symmetric reduced model E
' are isomorphism; that is, E
G
≅
E
'.Proof. It is not difficult to prove it by constructing a bijection between the events and their orbits.Theorem 56.
For anyE
∈
E, its symmetric reduced model E
' is a substructure of E; that is, E
'
⊲
E.Proof. The proof is straightforward.(6) Technique Combination. Symmetry reduction technique is orthogonal to slicing reduction and can be used in conjunction with slicing. Thus, it is easy to have the following result.Theorem 57.
For anyE
∈
E, let φ be a regular predicate; then the following statements hold: s
r
(
S
l
i
c
e
E
S
(
E
,
φ
)
)
=
w
c
c
(
m
c
f
E
S
slice
(
c
f
p
(
s
r
(
E
)
)
,
φ
)
) and s
r
(
S
l
i
c
e
E
S
(
E
,
φ
)
)
=
S
l
i
c
e
E
S
(
s
r
(
E
)
,
φ
).Proof. The proof is straightforward.


## 7.1. Basic Definitions

Definition 44.
For any event structureE
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E, define L
[
E
]
=
(
Conf
F
(
E
)
,
⊆
). Especially, for any conflict-free event structure F
=
(
E
F
,
⪯
F
,
∅
,
l
F
)
∈
F, define L
[
F
]
=
(
Conf
F
(
F
)
,
⊆
).In fact,L
[
F
] is the partial order of left-closed and conflict-free subsets of E
E ordered by set inclusion.L
[
E
] is the partial order of left-closed subsets of E
F ordered by set inclusion.Definition 45 (single action transition).
LetE
∈
E. A transition X
→
a
E
X
′ is called asingle action transition if and only if a
∈
A
c
t
,
X
,
X
′
∈
Conf
F
(
E
)
,
X
⊆
X
′ and there exists an event e such that X
′
-
X
=
e with l
E
(
e
)
=
a.Here,X
→
a
E
X
′ indicates that in the event structure the state represented by the configuration X may evolve into a state represented by the configuration by performing the action a. This transition relation associates a labelled system based on single action transitions with each event structure.Definition 46 (trace).
LetE
∈
E. A word w
=
a
1
…
a
n
∈
A
c
t
* is calledtrace of E if and only if ∃
X
0
,
…
,
X
n
∈
C
o
n
f
F
(
E
)
:
X
0
=
∅ and X
i
-
1
→
a
i
X
i
,
i
=
1
,
…
,
n.Here, letTrs
(
E
) denote the set of all traces of E.Definition 47 (interleave trace equivalence).
LetE
1
,
E
2
∈
E. E
1 and E
2 are calledinterleave trace equivalence
(
E
1
≈
i
t
E
2
) if and only if Trs
(
E
1
)
=
Trs
(
E
2
).Definition 48 (interleaving bisimulation).
LetE
1
,
E
2
∈
E. A relation R
⊆
C
(
E
1
)
×
C
(
E
2
) is called interleaving bisimulation between E
1 and E
2 if and only if (
∅
,
∅
)
∈
R and (
X
,
Y
)
∈
R; then (1)
X
→
a
E
1
X
′
,
a
∈
A
c
t
⇒
∃
Y
′
:
Y
→
a
E
2
Y
′
∧
(
X
′
,
Y
′
)
∈
R;
(2)
Y
→
a
E
2
Y
′
,
a
∈
A
c
t
⇒
∃
X
′
:
X
→
a
E
1
X
′
∧
(
X
′
,
Y
′
)
∈
R.Definition 49 (interleaving bisimulation equivalent).
LetE
1
,
E
2
∈
E. E
1 and E
2 are called interleaving bisimulation equivalent
(
E
1
≈
i
b
E
2
) if and only if there exists an interleaving bisimulation between E
1 and E
2.


## 7.2. Unified Framework

The unified framework for slicing and symmetry reduction we have set up can be pictured as in Figure12.Figure 12
Unified mathematical framework.(1) Isomorphism and Equivalence. We are concerned with the translation of concepts and ideas from one side to the other. The following theorems hold.Theorem 50.
LetF be a conflict-free event structure, F
=
(
E
F
,
⪯
F
,
∅
,
l
F
)
∈
F; then F
≅
℘
[
L
[
F
]
]. Similarly, let P
=
(
D
,
⊑
) be a prime algebraic complete lattice; then P
≅
L
[
℘
[
P
]
].Theorem 51.
LetE be a prime event structure, E
=
(
E
E
,
⪯
E
,
♯
E
,
l
E
)
∈
E; then E
≅
℘
[
L
[
E
]
]. Similarly, let P
=
(
D
,
⊑
) be a prime algebraic coherent domain; then P
≅
L
[
℘
[
P
]
].Clearly, from Theorems50 and 51, we have the following.(1)
For any prime event structureE, we have that E
≅
℘
[
L
[
E
]
].
(2)
Similarly, for any partial orderP
=
(
D
,
⊑
), P is a prime algebraic complete lattice or a finitary coherent prime algebraic domain; we have that P
≅
L
[
℘
[
P
]
].From Theorems23, 24, and 25, we have that conflict-free event structures and prime algebraic complete lattices are equivalent; this implies that there is a one-to-one correspondence between a prime event structure and its family of configurations. Similarly, prime event structures and finitary coherent prime algebraic domains are also equivalent; one can be used to represent the other.(2) Mutual Inverse Operation. For any prime event structure, c
f
p and w
c
c are mutually inverse operators.We can get the full set of maximal conflict-free substructures of a prime event structure byc
f
p operator.Conversely, given the full set of maximal conflict-free substructures of the prime event structure, we can recover the original prime event structure byw
c
c operator.(3) Slicing Reduction. Firstly, compared with traditional computation slicing, Figure 12 demonstrates the translation between a conflict-free event structure (or its slice) and prime algebraic complete lattice. This forms the theoretical basis of computation slicing technique proposed by Garg and Mittal, Sen [7, 20].Secondly, Figure12 also demonstrates the translation between a prime event structure (or its slice) and finitary coherent prime algebraic domain, which serves as the theoretical basis of our event structure slicing with conflict. A pair of mutually inverse operators, c
f
p and w
c
c, act as a link between the two parts.Thirdly, the slice of a prime event structure can be computed by the following steps:(1)
applyingc
f
p operator to partition the original prime event structure into a full set of maximal conflict-free substructures;
(2)
for each maximal conflict-free substructure, applying traditional computation slicing algorithm based on Adding Edges Theorem [7, 8, 20] over its directed graph representation to compute the slice with respect to the given predicate;
(3)
applyingw
c
c operator to compose the resulted slices in above step (2) and form a new prime event structure, while the generated event structure is the slice of the original prime event structure.(4) Symmetry Reduction. Operators c
f
p and w
c
c can also play an important role in symmetry reduction.Symmetry reduction of a prime event structure can be performed by the following steps:(1)
applyingc
f
p operator to partition the original prime event structure into a full set of maximal conflict-free substructures;
(2)
checking automorphism among the produced substructures and checking causal relation and action set;
(3)
removing duplicated substructure and applyingw
c
c operator to compose the resulted structure to form a newly generated prime event structure, which will be symmetry reduced prime event structure.(5) Trace Equivalence. The relation between original event structure and its quotient model can be specified by Theorems 52 and 53 (See [3]).Theorem 52.
LetE
∈
E and E
G be quotient structure of E; then E
G
≈
i
t
E.Theorem 53.
LetE
∈
E and let E
G be the symmetric quotient model for E. Then E
≃
i
b
E
G.Generally, given an event structureE, in fact, its behavior is exhibited by the labelled transition system (LTS, for short) LT
S
E
=
{
Conf
F
(
E
), A
c
t
E
,
T
E
,
∅
}, where(1)
the configurationsConf
F
(
E
) are states;
(2)
the set of labels is the set of actionsA
c
t
E;
(3)
the transitionsT
E are single action transitions between every two configurations of E; namely, T
E
⊆
C
o
n
f
F
(
E
)
×
A
c
t
E
×
C
o
n
f
F
(
E
);
(4)
the initial configuration (the empty set∅) is the initial state.The above equivalence is based on labelled transition systems whose transitions are single action transitions. As shown in Figure12, we construct labelled transition system for prime event structure and its quotient model, we will have that their LTSs are interleaving bisimulation and interleave trace equivalence also. Therefore, the following corollary holds.Corollary 54.
LetE
∈
E and E
G let be the symmetric quotient model for E. If L
T
S
=
(
Conf
F
(
E
)
,
A
c
t
,
→
E
,
∅
)  and L
T
S
G
=
(
Conf
F
(
E
G
)
,
A
c
t
,
→
E
G
,
∅
) are induced from E and E
G, respectively, then L
T
S
≈
i
t
L
T
S
G and L
T
S
≈
i
b
L
T
S
G hold.Evidently, we have the following theorems.Theorem 55.
For anyE
∈
E, its symmetric quotient model E
G and symmetric reduced model E
' are isomorphism; that is, E
G
≅
E
'.Proof. It is not difficult to prove it by constructing a bijection between the events and their orbits.Theorem 56.
For anyE
∈
E, its symmetric reduced model E
' is a substructure of E; that is, E
'
⊲
E.Proof. The proof is straightforward.(6) Technique Combination. Symmetry reduction technique is orthogonal to slicing reduction and can be used in conjunction with slicing. Thus, it is easy to have the following result.Theorem 57.
For anyE
∈
E, let φ be a regular predicate; then the following statements hold: s
r
(
S
l
i
c
e
E
S
(
E
,
φ
)
)
=
w
c
c
(
m
c
f
E
S
slice
(
c
f
p
(
s
r
(
E
)
)
,
φ
)
) and s
r
(
S
l
i
c
e
E
S
(
E
,
φ
)
)
=
S
l
i
c
e
E
S
(
s
r
(
E
)
,
φ
).Proof. The proof is straightforward.


## 8. Conclusion

In this paper, we presented a unified mathematical framework for event structure slicing and symmetric reduction. We described the equivalent relationship between original event structure and its maximal conflict-free event substructures. We proposed two mutually inverse operators: conflict-free partition operator and weak choice composition operator. Both symmetry reduction and slicing reduction can be performed by this pair of operators. We also investigated the related properties, translations, and correspondences between event structures and domains. Essentially, slicing over event structure is a high level extension to the traditional computation slicing based on the model with conflict.Slicing technique can make the verification of program behavior easier by reducing the size of the state space to be analyzed. Symmetry reduce is another powerful structural reduction technique that can also be applied to narrow down state space. Both quotient model and sliced model produced by reduction are often much smaller than the original model. The consequential model can be used to significantly improve the effectiveness of property verification of the original model.In future work, on the one hand, we will extend our work to other more complicated event structure models, such as flow event structure [34] and bundle event structure [35, 36]. On the other hand, we hope to implement and test our approach on various verification tools in practice. In addition, we would like to exploit more possible applications and theories.



---

*Source: 352152-2014-06-12.xml*