The set of regions of a condition/event transition system represents all the possible local states of a net system the behaviour of which is specified by the transition system. This set can be endowed with a structure, so as to form an orthomodular partial order. Given such a structure, one can then define another condition/event transition system. We study cases in which this second transition system has the same collection of regions as the first one. When it is so, the structure of regions is called stable. We propose, to this aim, a composition operation, and a refinement operation for stable orthomodular partial orders, the results of which are stable.
This work studies the interrelations between local states, locally observable
properties, and events of distributed systems. To this aim, its framework is set in the
relation between elementary Petri net systems, and the labelled transition
systems expressing their behaviour, their case graphs. Indeed, labelled transition
systems are commonly used models for verification of properties of the specified
system [
We focus on the particular case in which local states act like Boolean
variables, forbidding executions by carrying true or false values. Thus, the framework
is narrowed down to elementary and condition/event models, and their close
relation to the theory of regions. In [
Regions, as subsets of global states of a system, carry an algebraic structure
[
Orthomodular partial orders typically represent, in an algebraic fashion,
systems about which the acquisition of information depends on the point of view,
or experiment. They were first introduced by Birkhoff and Von Neumann [
In the view that omp’s are a suitable specification for the observable
properties of a system, we are concerned with a second synthesis problem: Given an
omp determine whether it is the regional structure of some elementary transition
system. This problem was first posed in [
Not every omp is stable, and the full characterization of the class of stable
omp’s is an open problem which represents a long term objective. It is
conjectured that every regional omp, the structured collection of regions of some
elementary transition system, is stable. The present work includes itself in a
series of papers [
The present work extends [
This work implicitly deals with elementary net systems (ENS for short) [
Condition/Event net systems (CENS for short) are structurally identical to ENS with the addition of a backward firing rule which provides symmetry to the reachability relation amongst markings; reachability becomes an equivalence relation, and reachability classes substitute the initial marking required for ENS. b1 e1 b2 b3 e4 e3 b4 e2 b5
e4 e2 e1 q2 q5 q3
e3 e2 e1 q1 q4 The behaviour of CENS can be expressed by means of a labelled transition system. In such a model, states correspond to the reachable markings of the net system. A marking enabling an event will correspond to a state from which an arrow, labelled with this event, points to the state which is reached when the event is fired. Such a labelled transition system is the sequential case graph of the underlying net system.
Definition 1 (Transition System). A transition system is a structure A = (Q, E, T ), where Q is a set of states, E is a set of events and T ⊆ Q × E × Q is a set of transitions carrying labels in E, such that:
2. ∀(q1, e, q2) ∈ T q1 6= q2; 3. ∀(q, e1, q1)(q, e2, q2) ∈ T q1 = q2 ⇒ e1 = e2; 4. ∀e ∈ E ∃ (q1, e, q2) ∈ T .
All the structures we consider are finite. A fundamental notion used in this
contribution is the one of region. Regions were introduced in [
Regions are subsets of states which have a consistent orientation with the labelling of transitions. As such, they can be assigned an incidence with respect to each event, and interpreted as Boolean conditions which hold at the states composing them.
Example 1. With reference to Figure 1, the extension of b1 is a region. As a subset of states, all occurrences of e1 exit it and e4 enters it. All occurrences of the remaining events do not cross the border of b1.
The set of regions of a transition system A will be denoted by R(A) and, given a state q of A, Rq will denote the subset of the regions in R(A) which contains the state q. Given a transition system A and its set of regions R(A), the pre-set and post-set operators can be defined: Definition 3 (Pre- and Post-sets). •( . ), the pre-set operator, and ( . )•, the post-set operator, are defined on the events E and on the regions R(A) of the transition system A as follows. Let r be a region in R(A) 1. •r = {e ∈ E | ∃ (q1, e, q2) ∈ T such that q1 ∈/ r and q2 ∈ r}; 2. r• = {e ∈ E | ∃ (q1, e, q2) ∈ T such that q1 ∈ r and q2 6∈ r}; 3. •e = {r ∈ R(A) | e ∈ r•}; 4. e• = {r ∈ R(A) | e ∈ •r}.
We are concerned with a specific class of transition systems, the condition/event
transition systems (cets for short). cets can be defined as those labelled
transition systems which are the sequential case graph of some CENS. An alternative
definition, in terms of regions and the separation axioms, follows from the results
of [
a transition system in which the following conditions hold: 1. ∀ q1, q2 ∈ Q Rq1 = Rq2 ⇒ q1 = q2; 2. ∀ q1 ∈ Q ∀ e ∈ E •e ⊆ Rq1 ⇒ ∃ q2 ∈ Q such that (q1, e, q2) ∈ T ; 3. ∀ q1 ∈ Q ∀ e ∈ E e• ⊆ Rq1 ⇒ ∃ q2 ∈ Q such that (q2, e, q1) ∈ T .
This definition requires of a transition system, that its set of regions is
sufficient to fully determine the incidence of each event with respect to each state.
Under these conditions, a CENS can be constructed, which has the set of
regions for conditions, and the transition labels as events, and such that its case
graph is isomorphic to the given transition system. This tight relation between
CENS and cets was thoroughly formalised in [
The following basic properties of the regions R(A) of a cets A are proven
in [
Orthomodular partially ordered sets, indicated as omp in what follows, are well
known algebraic structures in the literature on Quantum Logics. The following
definition can be found as the finite version of Definition 1.1.1 in [
We will often denote hL, ≤, (.)0, 0, 1i simply by L, and assume that an omp Li has underlying structure hLi, ≤i, (.)0, 0i, 1ii.
In general, ∧ and ∨ operations can be undefined for some pairs of elements of L. Two elements x and y in L are said to be orthogonal, noted by x ⊥ y, when x ≤ y0. As a consequence of their basic properties, as listed at the end of Section 2.1 above, the set of regions of a cets is an omp. 0 and 1 are, respectively, ∅ and Q, the order is given by set containment and orthocomplement by set complement; moreover, two regions are orthogonal whenever their intersection is empty.
Since all the structures we consider are finite, an omp can be equivalently
specified by its collection of atoms A(L) := {x ∈ L \ {0} | ∀y ∈ L : (y ≤ x) →
(y = x or y = 0)} together with their orthogonality relation. Each element of L
can then be retrieved as the join of a collection of pairwise orthogonal atoms. The
reader is referred to [
Definition 6 (OMP-morphism). ([
i∈I A morphism f : L1 → L2 is an isomorphism if f is injective, maps L1 onto L2 and f −1 is a morphism. An isomorphism f : L1 → M , when M is a sub-omp of
Morphisms of omp’s preserve compatibility, order and orthogonality [
A two-valued state of an omp is a well-known concept in the literature on
Quantum Logics ([
Since states of L are uniquely defined by means of up-closures of maximal cliques of 6 $, we will frequently refer to these maximal cliques as the states of the omp L when clear from the context.
The collection of all states of an omp L will be denoted by S(L). It will also be useful to consider the collection of states which contain a given element. Given an element x ∈ L, let us define the notation Sx := {s ∈ S(L) | x ∈ s}.
The following section is concerned with the representation of an omp as a collection of subsets of its states. The order in L will then be set inclusion, and the orthocomplement will simply be given by set complement. When this is the case, the omp is said to admit a concrete representation. 2.3
As explained in more detail in section 2.4 below, omps can be constructed from
the regions of a cets. These omps will, from now on, be referred to as regional
omps. They have been shown, in [
– Regularity: L is regular whenever every set of pairwise compatible elements
is a compatible set [
There is some inconsistency in the terminology referring to these concepts
in the literature, and it has led to some confusion in the axiomatic definition of
these properties. Indeed regularity is the term used in [
Richness is axiomatically defined in [
An omp L is called unital when for every element x ∈ L \ {0} there is a state s ∈ S(L) such that x ∈ s.
∀x, y ∈ L : Sx ⊆ Sy ⇒ x ≤ y
In Chapter 2 of [
∀x, y ∈ L : x 6 $ y ⇒ ∃s ∈ S(L) : x ∈ s and y ∈ s
Rich omp’s where shown in Chapter 2 of [
∀x, y ∈ L : x 6= y ⇒ ∃s ∈ S(L) : x ∈ s ⇔ y ∈/ s
We now prove two lemmas that will be used in the proof of Theorem 2 below:
∀x, y ∈ L : x 6 $ y ⇒ ∃s ∈ S(L) : x ∈/ s and y ∈/ s if and only if: ∀x, y ∈ L : x 6 $ y ⇒ ∃s ∈ S(L) : x ∈ s and y ∈ s Proof. Suppose that L is an omp such that ∀x, y ∈ L : x 6 $ y ⇒ ∃s ∈ S(L) : x ∈ s and y ∈ s and consider two elements x, y ∈ L : x 6 $ y; then it is also true that x0 6 $ y0. By hypothesis we have that ∃s ∈ S(L) : x0 ∈ s and y0 ∈ s and neither x nor y belong to s, which means that ∃s ∈ S(L) : x ∈/ s and y ∈/ s for every pair of incompatible elements in L.
Conversely, suppose that L is an omp such that ∀x, y ∈ L : x 6 $ y ⇒ ∃s ∈ S(L) : x ∈/ s and y ∈/ s and consider two elements x, y ∈ L : x 6 $ y; again it is true that x0 6 $ y0. By hypothesis we have that ∃s ∈ S(L) : x0 ∈/ s and y0 ∈/ s and both x and y belong to s, which means that ∃s ∈ S(L) : x ∈ s and y ∈ s for every pair of incompatible elements in L.
Proof. For every element x ∈ L distinct from 0 we have that ∃s ∈ S(L) : x ∈ s ⇔ 0 ∈/ s and since 0 doesn’t belong to any state of L then x belongs to s.
Proof. Suppose that L is rich and consider two elements x, y ∈ L : x 6= y. There are two cases:
x $ y : in this case there exists a Boolean subalgebra of L that contains both x and y. For both of them we calculate the set of atoms below them, A↓(x) = {a ∈ A(L) | a ≤ x} and A↓(y) = {a ∈ A(L) | a ≤ y}. Such sets differs in at least an element z, because otherwise it would mean, out of Axiom 4 in Definition 5, that x = y. If we consider a state s ∈ S(L) such that z ∈ s then s will contain only one element between x and y because z belongs to to only one of the two sets A↓(x) and A↓(y). The existence of s is ensured by the fact that L is unital, which means that ∃s ∈ S(L) : x ∈ s ⇔ y ∈/ s.
x 6 $ y : if x 6 $ y then we also have that x 6 $ y0. From the hypothesis we have that ∃s ∈ S(L) : x ∈ s and y0 ∈ s which means that ∃s ∈ S(L) : x ∈ s ⇔ y ∈/ s.
Now, suppose that L is prime, for Lemma 2 L is also unital. Consider two elements x, y ∈ L : x 6 $ y. That means that x 6 $ y0 and in particular x 6= y0. By Definition 9 of prime omp we have that ∃s ∈ S(L) : x ∈ s ⇔ y0 ∈/ s which means that ∃s ∈ S(L) : x ∈ s ⇔ y ∈ s. Again, we consider two cases: x ∈ s : then ∃s ∈ S(L) : x ∈ s and y ∈ s x ∈/ s : then ∃s ∈ S(L) : x ∈/ s and y ∈/ s which, as shown in Lemma 1, is equivalent to ∃s0 ∈ S(L) : x ∈ s0 and y ∈ s0. tu 2.4
As anticipated in section 2.3 above, we know that, given a cets A = (S, E, T ), H(A) = (R(A), ⊆, ∅, S, ( . )0) with ( . )0 the set complement operation, is an omp. Moreover, this regional omp is regular and rich.
We know as well that, given a regular and rich omp L, J (L) = (S(L), E(L),
T (L)) is a cets; where E(L) and T (L), the sets of, respectively, events and
transitions, are constructed by exploiting symmetric differences between states
as defined in [
In [
It is our long-term goal to fully characterise the class of stable omp’s, and it is conjectured that it coincides with the class of regional omp’s. In the next section, we will present a compositional approach which will allow us to prove the stability of a wide class of regional omps. 3
This section will start introducing a rather general composition operation for omp’s. The result of this composition will not always be an omp but we show that it is the case in particular instances. 3.1
We here present a composition operation for omp’s, in the fashion of those
presented in [
(I, L1, L2, φ1, φ2), such that I, L1, and L2 are omp’s, and φi : I → Li(i = 1, 2) are morphisms of omp’s.
A V-formation serves as specification for composing L1 and L2 on the common interface I. In categorical terms, it is simply a diagram in the category of omp’s. Strictly speaking, the interface would only be φ1−1(L1) ∩ φ2−1(L2), so in order to simplify notation, we here consider V-formations in which φi(i = 1, 2) are embeddings, and so for each i = 1, 2, φi(I) is a sub-omp of Li isomorphic to I.
L1 a01 a1 11 = φ1(1I )
Given a V-formation of omp’embeddingss, we propose a straightforward
composition operation. This construction is inspired by co-equalisers [
Let V = (I, L1, L2, φ1, φ2) be a V-formation of omp’s. Consider L˜, the disjoint union of L1 and L2 such that φi : I → L˜ (i = 1, 2), with φ1(I) ∩ φ2(I) = ∅. The equivalence relation induced by V is the binary relation ∼V := {(x, x) ∈ L˜2 | x ∈ L} ∪ {(φ1(x), φ2(x)) ∈ L˜2 | x ∈ I} ∪ {(φ2(x), φ1(x)) ∈ L˜2 | x ∈ I}. ˜
It is straightforward to verify that ∼V is an equivalence relation. It is
reflexive, and symmetric by construction. If x, y, z ∈ L˜ are such that x ∼V y and
y ∼V z then it must be either z = x or z = y, so ∼V is transitive. We will
denote the equivalence class of an element x ∈ L˜ by [x]. This equivalence relation
satisfies these additional properties:
Proposition 1. Let V = (I, L1, L2, φ1, φ2) be a V-formation of omp’s, and ∼V
as in Definition 11. Then:
1. ∀i ∈ {1, 2} : ∀x ∈ Li : [x] ∩ Li = {x}
2. ∀x, y ∈ L˜ : x ∼v y ⇔ x0 ∼V y0
3. [01] = [02] = {01, 02} and [
Proof. 1. By construction. 2. Let x, y ∈ L˜ be two distinct elements such that x ∼ y. From the definition of ∼V , it follows that ∃z ∈ I : φ1(z) = x and φ2(z) = y (up to swapping of x and y). Since φ1 and φ2 are omp-morphisms, it follows that φ1(z0) = x0 and φ2(z0) = y0, hence x0 ∼ y0. 3. It is a direct consequence of Axioms 1 and 2 in Definition 6. 4. Let x ≤ y then ∃i ∈ {1, 2} : x, y ∈ Li, and x ≤i y. Analogously, ∃j ∈ {1, 2} : x˜, y˜ ∈ Lj , and y˜ <j x˜. Clearly it must be that i 6= j. Now, x ∼V x˜, and y ∼V y˜ ⇒ ∃a, b ∈ I : φi(a) = x, φj (a) = x˜, φi(a) = y, and φj (b) = y˜. Since φi is an omp-embedding, it must reflect the order, yielding a ≤ b, but φj preserves the order, and so x˜ ≤ y˜.
These results allow for endowing the quotient L˜/ ∼V with a structure.
Definition 12 (I-pasting of OMP’s). Consider the setting of Definition 11,
and define:
tu
1. L = L˜/ ∼V ,
2. 0 = [01] = [02] and 1 = [
Then the I-pasting of L1 and L2 induced by V is the structure L1|I|L2 = hL, ≤ , (·)0, 0, 1i.
It follows immediately from Proposition 1 (4.) that ≤ is an order relation.
Proposition 1 (2.), states that ∼V is congruence for complementation, and so
(·)0 is well-defined on L. It is furthermore trivial to verify that 0 and 1 are
respectively the minimal and maximal elements in L. Note that whenever x ⊥ y,
then [x] ⊥ [y]. So defined, the composition of two omp’s over an interface is
simply obtained by identifying the elements whose pre-images through φ1 and
φ2 coincide. In general, such an I-pasting will be an orthocomplemented partial
order [
Example 2. With reference to Figure 3. Let I = {0, 1, x, x0} be an omp with 0 ≤ x, x0 ≤ 1. For i = 1, 2, let Li be Boolean algebras with three atoms each {ai, bi, ci}. Since φi are omp-morphisms, φi(0) = 0i, and φi(1) = 1i. Now let φ1(x) = c1, so that φ1(x0) = c01 = a1 ∨ b1; and φ2(x0) = c2 so that φ2(x) = c02 = a2 ∨ b2. In this case, ∼ is the reflexive and symmetric closure of {(01, 02), (11, 12), (c1, c02), (c01, c2)}, let [x] denote its equivalence classes. In L1|I|L2, we have that [a1] ≤ [c01] = [c2] ≤ [a02]. Hence, [a1] and [a2] are orthogonal, but they have no least upper bound. Indeed, [a1], [a2] ≤ [b01], [b02] and [b01] ∧ [b02] = [0].
In what follows, we will study cases in which this composition is actually an omp.
It is a known result [
We consider now the case in which the interface is a non-trivial Boolean
algebra I = {0, 1, y, y0} whose atoms are: A(I) = {y, y0}. With such an
interface, we impose that the corresponding saturated transition systems synchronise
according to the specified embeddings. One of the components will be a finite
Boolean algebra, and will be denoted B. Boolean algebras considered as omp’s
were shown to be stable in [
Example 3. With reference to Figure 2, b1, b2, b4, b5 and b3 are all atoms, however b1, b2, b4, b5 are free, but b3 is not. Indeed, b3 belongs to two maximal Boolean algebras.
The considered embeddings will then identify a free atom of an omp with an atom of B.
Theorem 3. Let L be an omp, and x ∈ A(L) be an atom. Let B be a finite Boolean algebra, and a ∈ A(B). Let I = {0, 1, y, y0}, and define φL : I → L, and φB : I → B such that φL(y) = x, and φB(y) = a. Then L|I|B induced by the
Proof. After Proposition 1, it suffices to show that orthogonal joins are well
defined, and that the orthomodular law holds. First note that in this case, the
only identifications are [0] = {0L, 0B}, [
On the other hand, since L0 is an omp, then c ≤ f implies that f = c∨(f ∧c0), hence [f ] = [c] ∨ ([f ] ∧ [c]0). tu In the following, L I B will refer to this particular construction, and L will be | | assumed to be stable. Furthermore, we will suppose that φL(y) = x is a free atom, and show that L I B is stable whenever L is.
| | We start defining J 0(L) = (Q0L, EL0, T L0) in the following way:
Q0L = Sy ∪ {s ∪ {vi}|s ∈ Sy0 , φB(y) 6= vi ∈ A(B)} EL0 = {[s, s0]|s, s0 ∈ Q0L, s 6= s0}
T L0 = {(s, [s, s0], s0)|s, s0 ∈ Q0L, [s, s0] ∈ EL0, s 6= s0}. s0 s3
s2 J (L) s1 s4 φL(y) s1 s4 [φL(y)] sv2 2 sv2 0 sv2 3
Lemma 3. J 0(L) is isomorphic to J (L|I|B). Furthermore, for every vi ∈ A(B) such that φB(y) 6= vi, the subgraph of J 0(L) induced by S(y)∪S(vi) is isomorphic to J (L).
Proof. Every state q ∈ Q0L contains one, and only one, atom of B and since φL(y) is a free atom, it has one, and only one, atom for every Boolean algebra of L. Hence the elements of Q0L coincide with the elements of S(L|I|B). Since the construction of J 0(L) is completely determined by the set of states as in the construction of J (L|I|B), the two transition systems J (L|I|B) and J 0(L) are isomorphic.
We also observe that for every atom vi ∈ A(B) distinct from φB(y) the elements in S(y) ∪ S(vi) coincide with the elements of S(y) ∪ S(y0), which is the set of states of J (L). From this observation it is easy to see that there is an isomorphism between J (L) and any subgraph of J 0(L) induced by a set of states in the form S(y) ∪ S(vi). tu This last lemma will permit to consider J 0(L) instead of J (L|I|B). Lemma 4. If a region H ∈ R(J 0(L)) contains a state s∪{vi} ∈ Q0L and Svi 6⊆ H then ∀s ∪ {vj } ∈ Q0L : s ∪ {vj } ∈ H.
Proof. Since Svi 6⊆ H there must be a state s0 ∪ {vi} ∈/ H, which means that the event [s, s0] is an event labeling a transition exiting H. Now suppose that there is a state s ∪ {vj } ∈ Q0L that doesn’t belong to H. This means that the transition from s ∪ {vj } to s0 ∪ {vj } ∈ Q0L does not exit H, but such a transition is also labeled [s, s0], which is not possible since that would mean that H is not a region. tu Lemma 5. Every atomic region of J 0(L) is in the form Sx for x ∈ A(L|I|B). Proof. Assume that there is an atomic region H 6∈ {Sx | x ∈ A(L|I|B)}. Consider the subgraphs induced by Sy ∪ Svi for all the φB(y) 6= vi ∈ B and call Hvi ⊂ H the sets H ∩(Sy ∪Svi ). All the Hvi are atomic regions in every subgraph of J 0(L) induced by Sy ∪ Svi , since they are all isomorphic to J (L). The regions Hvi can be atomic or not. If they are atomic, then they must coincide with an atomic region Sx, with y 6= x ∈ Ln. Hence, after Lemma 4, H ∈ {Sx}x∈Ln+1 . If they are not atomic, then there are Hv01 ⊂ Hv1 ,...,Hv0k ⊂ Hvk from which we can make the region Si∈{1,..,k} Hv0i ⊂ H, hence H is not atomic. tu Theorem 4. Let L be a stable omp, and x ∈ A(L) be a free atom. Let B be a finite Boolean algebra, and a ∈ A(B). Let I = {0, 1, y, y0}, and define φL : I → L, and φB : I → B such that φL(y) = x, and φB(y) = a. Then L|I|B induced by the V-formation (I, L, B, φL, φB) is stable.
Proof. We wish to show that H(J (L|I|B)) ' L|I|B. With Lemma 3, we reduce
it to showing that H(J 0(L)) ' L|I|B. Since H(J 0(L)) is a finite omp, it is
characterised by the orthogonality relation among its atoms. Now, Lemma 5
states that each atom of H(J 0(L)) corresponds to an atom of L|I|B, and it was
shown in [
For each pair of elements x ∈ A(L), y ∈ A(B), there is a state in s ∈ J (L|I|B)
such that [x] ∈ s and [y] ∈ s. Hence, the pasting must preserve
incompatibility. Since the pasting also preserves orthogonality, we have that L|I|B, and
H(J (L|I|B)) have same collection of atoms, with identical orthogonality
relations. As it was shown in [
The operation of refining an atom of an omp into two new atoms preserves stability.
Theorem 5. Let L be a stable omp. Let x ∈ A(L). Consider Ma = (A(L) \ {x}) ∪ {y, z}, in which all orthogonal atoms of L remain orthogonal in Ma, and all atoms orthogonal to x in L are orthogonal to both y and z in Ma. Then the omp M generated by Ma is stable.
Proof. We will consider only the atoms of L and M , and states as represented by maximal cliques of 6 $ as in Definition 7. Let Sx0 be the set of states of L not containing x. By construction of Ma, for each state s ∈ Sx of L there are two states of M , in Sy and Sz respectively. Furthermore, the states of Sx0 all contain an atom orthogonal to x in L, and it will be orthogonal to both y and z in M . Thus, Sx0 , Sy and Sz constitute a partition of the states of M .
Starting from the states of M as partitioned above, it is possible to define the following sets of events: Ex0 = {[s, s0] | s, s0 ∈ Sx0 , s 6= s0}, Ey,z = {[s, s0]|s ∈ Sy, s0 ∈ Sz}, Ey = {[s, s0]|s, s0 ∈ Sy}, Ez = {[s, s0]|s, s0 ∈ Sz}, Ex0,y = {[s, s0] | s ∈ Sx0 , s0 ∈ Sy} and Ex0,z = {[s, s0] | s ∈ Sx0 , s0 ∈ Sz}.
Let Ay be the transition system with the following sets of states and events: Sx0 ∪Sy and Ex0 ∪Ey∪Ex0,y, let, symmetrically, Az be the transition system whose states are Sx0 ∪Sz and whose events are Ex0 ∪Ez ∪Ex0,z. We note that both R(Ay) and R(Az) are isomorphic to the regions of the saturated system J (L) since in both cases of R(Ay) and R(Az), atoms y and z replace uniformly x. Moreover, since states Sy and Sz are disjoint, it is possible to construct the cets A = Ay ∪ Az endowed by all the new events in Ey,z. We note that R(A) must contain R(J (M )) since cets A, having less events than J (M ), can have less constraints in the construction of its regions. We want to show that R(A) = R(J (M )). Let, by contradiction, r be a region in R(A) not belonging to R(J (M )).
If r ⊆ Sx0 , then r ∈ R(J (M )) since all the labels in Ex0 belong to both cets A and J (M ) and the new events in Ex0,y and Ex0,z are distinct copies of the original events Ex0,x in J (L), so they do not create new regions. If r ⊆ Sy and, symmetrically, for r ⊆ Sz then r must be a region in R(J (M )) since all the labels in Ey and Ex0,y, and symmetrically Ez and Ex0,z are, by construction, isomorphic to the labels Ex0,x in J (L) and all the new labels Ey,z are exiting from or, respectively, entering in r. The only remaining case could be for r being a minimal region in R(A) and a non minimal region in R(J (M )) but this would be in contradiction with y and z being atoms in M . tu Example 4. Consider three Boolean algebras B1, B2 and B3 with three atoms each, A(Bi) = {ai, bi, ci} for i = 1, 2, 3. Let I = {0, x, x0, 1} and consider the two omp-morphisms φi : I → Bi (i = 1, 2), such that φi(x) = ci. B1 is a stable logic, and c1 is clearly a free atom, so after Theorem 4, L = B1|I|B2 is a stable omp. L is isomorphic to the omp in Figure 2, by considering b3 = [φ1(x)] = [φ2(x)]. Since L is stable, and b5 is a free atom, we can compose it with B3, by means of the morphisms φL and φ3, provided by φL(x) = b5 and φ3(x) = c3. The Greechie diagram of L|I|B3 is depicted at the top of Figure 5. Thanks to Theorem 5, we can now split any atom of L|I|B3, obtaining, for example, the stable omp depicted at the bottom of Figure 5. [b4] [b3] [b4] [b5] Fig. 5. Greechie diagrams of two omps. The omp depicted below, is obtained from the one depicted above, by refining the atoms as shown. Since the omp above is stable, so is the one below.
A free atom of the operands can be refined both after and before the composition operation, in this second way, only one of the two refining atoms will be used as interface with the appended sequential component, the other one remaining free for further composition. With this method, one can iterate the composition operation without worrying about exhaustion of available free atoms of the original system.
Example 5. Consider a system made of two sequential components each of which can get to a state for which they require the same resource. If each of these components can be in two additional states, the regional omp for this system is represented as L1 in Figure 6. B1 and B2 represent the two sequential components, and x1, x2 correspond to their mutually exclusive states. Bc represents the state of the resource c, it can be in state xi, indicating that Bi holds c, or in state y1, indicating that c is available. When c is available, no other component is involved in the coresponding local state of Bc, and so y1 is a free atom. L1 is isomorphic to the omp at the top of Figure 5, and was shown to be stable in Example 4. We may want to make the resource c available for a third sequential component B3, so we can use Theorem 4 to compose L1 and B3 on y1, obtaining the stable L2 = L1|I|B3 a shown in Figure 6. However, in this new compound system, the resource must be held by one of the three components Bi, as Bc has no more free atoms. No additional component can be added to the system, to compete for c. Instead of performing the composition L1|I|B3 directly, we can first make use of Theorem 5, and refine y1 in L1 into two new free atoms x3, y2, thus obtaining the omp L3 of Figure 6. We can now compose it with B3 on x3, thus obtaining L4 = L3|I|B3, which is stable. One can see that y2 remains a free atom, a local state representing that the resource is available. This process can be iterated, to obtain a system with n sequential components competing for the same resource.
L1 L3
B1 x1 B1 x1
B2 x2 B2 x2 y1
Bc y1 x3 y2
Bc
L2 L4
B1 x1 B1 x1
B2 x2 B2 x2
B3 y1 B3 x3
Bc y2
Bc
In [
However, not every regional omp can be obtained with the defined operations. For instance, a strong limitation is the restriction of the composition operation to interfacing on free atoms. Another limitation of this operation is that it does not allow for extending a system with a sequential component that would synchronise with the system at more than one state. A clear goal in our approach is to extend the composition operation so as to generate every regional omp. In this way, by showing that we can generate all regional omps with stability preserving operations, we would prove the conjecture that all regional omps are stable.
We wish to thank Lucia Pomello, and Luca Bernardinello for the fruitful discussions. Thanks to the three anonymous reviewers for the useful remarks and suggestions. This work is partially supported by MIUR.