We study the relation between labelled transition systems and the corresponding partial orders of regions. In particular, we focus on the sets of their potential events, or labels on the transitions, providing them with a structure so as to reason about concurrency from the perspective of the observable properties of these systems. This is achieved by introducing the notion of minimal events, as the generators of such a structure of labels. We show that these events are sufficient to synthesize a transition system, such that its Regional Partial Order is isomorphic to the one obtained with the full set of events.
Elementary Net Systems [
ENS are formalized as bipartite directed graphs, the nodes of which belong
in one of the following classes. A condition, or local state, can take the values
true or false. An event can dynamically alter the values of the conditions which
are connected to it by an edge. This change in the values is guided by the firing
rule [
In this model, the labeling function induces an equivalence relation on the
transitions. Such a relation, and the corresponding equivalence classes, were
studied in the frame of 2-Structures [
Regions, as subsets of global states, can be ordered by inclusion. The set of
regions of an ETS is closed under set complement, and union of disjoint elements.
Such structures, orthomodular partial orders, were well studied in the first
attempts to axiomatize quantum mechanics [
By identifying regions and conditions, we stress the duality between global
states, seen as subsets of conditions, and regions, seen as subsets of global states.
This duality was exploited in [
In this work, we continue that study by selecting a specific subclass of the
events of the synthesized system that guarantees both connectedness and
preservation of the regional structure: one can consider the regions of the canonical
CETS obtained from a logic. The canonical CETS, and the alternative CETS
we here propose will carry the same set of regions. The main contribution of this
work relies on the properties of the regions which are minimal for the partial
order defining the logic [
This rather technical result will allow us to develop on the relation between
the logic of regions, and the associated canonical CETS. It was already pointed
out, as a remark in [
Definition 1. A labelled 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 such that: 1. the underlying graph of the labelled transition system is connected; 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 .
We will write s [ei to mean that there is s0 such that (s, e, s0) ∈ T , in this case we may also write s [ei s0. Transition system will mean labelled transition system in what follows.
Note: we will always use finite structures in this contribution.
Regions were introduced in [
Definition 2. A region of a transition system A = (Q, E, T ) is a subset r of Q such that every event crosses r uniformly, namely: ∀e ∈ E, ∀(q1, e, q2), (q3, e, q4) ∈ T : 1. (q1 ∈ r and q2 ∈/ r) implies (q3 ∈ r and q4 ∈/ r) and 2. (q1 ∈/ r and q2 ∈ r) implies (q3 ∈/ r and q4 ∈ r).
Given a transition system A, its set of regions will be denoted by R(A); given a state q ∈ Q, the set of regions containing q will be denoted by Rq(A) and, when the transition system is clear from the context, simply by Rq. Note that the set of regions R(A) of a transition system A = (Q, E, T ) cannot be empty since at least the whole set of states Q is a region. We say an event e ∈ E is orthogonal to a region r ∈ R(A), whenever ∀(q1, e, q2) ∈ T : q1 ∈ r ⇔ q2 ∈ r. Definition 3. Let A = (Q, E, T ) be a transition system. The pre-set and postset operations, denoted respectively by the operators •( . ) and ( . )•, applied to regions r ∈ R(A) and events e ∈ E are defined by: 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 ∈/ r}; 3. •e = {r ∈ R(A) | e ∈ r•}; 4. e• = {r ∈ R(A) | e ∈ •r}.
Elementary systems require an initial global state. In this work, deal with a
similar class of systems, in which only simple connectedness of the underlying graph
is required. Condition/Event transition systems, in the context of the synthesis
problem, have been introduced as the class of transition systems representing the
behaviour of Condition/Event Net Systems, one of the basic classes of Petri nets
[
Definition 4. A Condition/Event Transition System — CETS — is a transition system such that the following conditions are satisfied: 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 . 1 3 γ α α e 5 We will use the following basic properties of regions of CETS: α 2 γ 4 β 7 e 6 f
α
Proposition 1. [
Using the basic properties of regions recalled in Proposition 1, the set R(A)
can be endowed with an algebraic structure: it can be partially ordered by set
inclusion, and a complement can be defined as set-complement operation. More
precisely, if A = (Q, E, T ) is a CETS, then the logic L(A) = hR(A), ⊆, (.)0, ∅, Qi,
where (r)0 = Q \ r, can be defined. We will call the logic L(A) regional logic.
This logic has been shown to be a quantum logic [
Wi∈I xi exists in L; 5. ∀ x, y ∈ L x ≤ y ⇒ y = x ∨ (x0 ∧ y).
This latter condition is sometimes referred to as orthomodular law. The symbols ∧ and ∨ refer, when defined, to the ordinary meet and join operations. We say that two elements x and y in a logic are orthogonal, and write x ⊥ y, if x ≤ y0. Hence, Proposition 1 implies that two regions are orthogonal whenever they are disjoint subsets of states.
Partial orders of regions are a subclass of quantum logics: they have been shown verify a set of properties which may not hold in an arbitrary quantum logic. One of them involves the notion of state.
Definition 6. ([
Note: a two-valued state s, seen as a characteristic set function, always selects either an element x ∈ L or its orthocomplement x0: ∀x ∈ L, s(x) = 1 ⇔ s(x0) = 0. An immediate consequence is that, if s1 and s2 are distinct states, then s1 \ s2, seen as a set, is not empty. In this work, we will refer to two-valued states simply as states, and mainly consider them as the subsets they are formally characteristic functions of.
Given a logic L, we denote by S(L) the set of all (two-valued) states on L and
by Sx the set {s ∈ S(L) | s(x) = 1}. In general, logics could, by their structure,
admit no state at all. Logics having “enough” states in such a way that the order
relation can be re-constructed by their states are called rich:
Definition 7. ([
Sx ⊆ Sy ⇒ x ≤ y.
Intuitively, a rich logic is faithfully represented by its set of states. A theorem
due to Stanley Gudder ([
It is well known [
The relation of compatibility between a and b is noted as a $ b. Its opposite relation is noted by x 6 $ y. Note that two ordered or orthogonal elements are always compatible. A maximal subset of pairwise compatible elements in L, with the partial order on L, is a sublogic of L. It is also a Boolean algebra: it is closed under complement (·)0, meet (∧), and join (∨), and the last two distribute over each other. We may refer to these as maximal Boolean sublogics or blocks of L.
Intuitively, the blocks of L will correspond to the sequential components in the net system view. This motivates the idea that there should be some consistency among compatible elements of the logic. The well studied property of regularity, accurately translates this notion.
Definition 9. ([
The main consequence of regularity is precisely that it will allow us to
interpret compatibility of two elements as their belonging to the same sequential
component.
Proposition 2. ([
Indeed, it has been shown [
The dual notion, that incompatibility of two regions should translate their
belonging to different sequential components, was studied in [
Given a regional logic L(A) = hR(A), ⊆, (.)0, ∅, Qi for some CETS A, we can construct a new transition system from L = L(A). The transition system defined by L is constructed with S(L) as its set of states. Its events are pairs of symmetric differences between states.
Definition 10. Let e = [s1, s2] denote the pair of set differences hs1 \ s2, s2 \ s1i. Define •e = s1 \ s2, and e• = s2 \ s1, so that e = h•e, e•i. Let
E = {[s1, s2] = hs1 \ s2, s2 \ s1i | s1, s2 ∈ S(L), s1 6= s2}.
T = {(s1, [s1, s2], s2) | s1, s2 ∈ S(L), s1 6= s2}.
We can now define the transition system A(L) = (S(L), E, T ). In this frame,
s1 [ei s2 ⇒ s2 = (s1 \ •e) ∪ e•. We will refer to this binding as firing rule.
It was shown in [
Note that the regions of A(L) form again a regional logic, R(A(L)). In
general, we know [
A compact graphical representation of finite logics can be obtained with a
technique due to Richard Greechie and reported in [
The block diagram of a logic exploits this fact, and depicts only the atoms of the logic. Instead of representing all orthogonality dependencies, maximal cliques of ⊥ are represented by straight lines. In this way, the block diagram of a Boolean algebra will be composed only by one maximal clique of ⊥ while at least two blocks are needed for the representation of a non-Boolean logic L. In Figure 2, a simple non-Boolean logic L is represented. The two blocks of atoms in A(L) composing its block diagram are drawn on the right.
c0 c 1 0 a0 a b0 b d0 d e0 e a
e b c d
We will now present a result that will allow us to characterize the states of the logic on its block diagram. Informally, this result states that a state must contain exactly one atom per maximal Boolean sublogic. In order to formalize this, we shall define some notation. Definition 11. Let C⊥(A(L)) be the set of maximal cliques of the ⊥ relation. Let Cnc(A(L)) be the set of maximal cliques of 6 $. By CL(A(L)) we denote the set of elements α ∈ Cnc(A(L)) such that ∀β ∈ C⊥(A(L)), |α ∩ β| = 1. Finally, for any subset S ⊆ A(L), the up-closure of S is defined as ↑S := {s0 ∈ L | ∃s ∈ S : s ≤ s0}.
In [
Theorem 1. Let hL, ≤, (.)0, 0, 1i be a regular logic, A(L) its set of atoms, s ∈ S(L) and CL(A(L)) as in definition 11 above, then (s ∩ A(L)) ∈ CL(A(L)). Moreover, if α ∈ CL(A(L)) then ↑α is a state in L.
Example 1. With reference to Figure 2 the states of L are: ↑{a, d}, ↑{a, e}, ↑{b, d}, ↑{b, e}, ↑{c}. A maximal clique of 6 $ is not, in general, sufficient for the definition of a state. The requirement, as in definition 11, that each maximal clique of 6 $ meets each maximal clique of ⊥ is essential. With reference to Figure 3, the up-closure of the maximal clique {a1, b2, g1} of 6 $, ↑{a1, b2, g1} is not a state since an element from the block {c1, c2, c3} is missing.
Example 2. The regional logic L of the transition system in Figure 1 is represented, as block diagram of its atoms, in Figure 3. The minimal regions in L, corresponding to the atoms, are: a2 = {2, 4, 6, 8}, a1 = {1, 3, 5, 7}, g1 = {1, 2, 9, 11}, g2 = {3, 4, 10, 12}, b2 = {7, 8, 11, 12}, b1 = {5, 6, 9, 10}, c1 = {9, 10, 11, 12}, c2 = {1, 2, 3, 4} and c3 = {5, 6, 7, 8}. Its representation as Net System is in Figure 4 where only one representative of the class of markings is drawn. This marking is composed by the regions c2 = {1, 2, 3, 4}, a1 = {1, 3, 5, 7} and g1 = {1, 2, 9, 11}.
c1 c2 c3 a1 b1 g1 a2 b2 g2
f g1 γ a2 g2 α c1 e c3 c2 a1 b1 d b2 β We now show that the events of a logic are fully characterized by the atoms in their neighbourhoods. This allows us to characterize events on the block diagram of L.
Definition 12. For each e ∈ E, the neighbourhood of e is ν(e) = •e ∪ e•; the atomic neighbourhood is νA(e) = (•e ∩ A(L)) ∪ (e• ∩ A(L)) Lemma 1. Let e1, e2 ∈ E. If νA(e1) = νA(e2), then e1 = e2.
Proof. Let e1 = hs1 \ s2, s2 \ s1i. Choose x ∈ s1 \ s2, and suppose that x is not an atom of L. Then there is at least one atom a of L in s1, with a < x. From x ∈/ s2, it follows that a ∈/ s2. A symmetric argument applies to s2 \ s1, hence e1 cannot be distinguished from e2 because of a non-atomic element in their neighbourhoods. tu 3
The synthesis of the saturated transition system from a given logic, allows one to identify sets of transitions according to the modifications they apply on states, when these are seen as subsets of regions. These modifications, or symmetric differences of regions, are then taken as the set of labels of the transition system. 3.1
In this section, we exploit this fact to endow the set of events with a richer structure. We define a composition operation with inverse, and neutral element. The neutral element will just be e∅ := h∅, ∅i the empty event. This event should be considered only for structural purposes. Intuitively, it would just leave any state unchanged; hence no transition carries it as a label.
We first define the operation of sequential composition of two events. The resulting event will correspond to the consecutive occurrence of its operands. The existence of this new event will depend, however, on the existence of a state binding the operands in sequence. In our setting, events are defined over a fixed structure of states, making the following a partial operation.
Let L be a regional logic.
Definition 13. We say that two events e1, e2 ∈ E are sequentiable iff ∃s ∈ S(L) : e1• ⊆ s ∧ •e2 ⊆ s (1) If two events are sequentiable, we define their sequential composition as: e1 ⊕ e2 = h(•e1 \ e2•) ∪ (•e2 \ e1•), (e2• \ •e1) ∪ (e1• \ •e2)i
= h(•e1 ∪ •e2) \ (e1• ∪ e2•), (e1• ∪ e2•) \ (•e1 ∪ •e2)i The definition does not depend on the choice of s. Condition 1 requires an occurrence of e1 to bring the system to a state which enables e2. The following result exemplifies why this is required, and shows that e1 ⊕ e2 belongs to E. Proposition 3. Let s0, s, s1 ∈ S(L) be three distinct states, and e1, e2 ∈ E be events such that s0 [e1i s [e2i s1. Then s0 [e1 ⊕ e2i s1 Proof. By definition of E, e1 = hs0 \ s, s \ s0i, and e2 = hs \ s1, s1 \ si. Then by definition of ⊕, e1 ⊕ e2 = h((s0 \ s) ∪ (s \ s1)) \ ((s \ s0) ∪ (s1 \ s)), ((s \ s0) ∪ (s1 \ s)) \ ((s0 \ s) ∪ (s \ s1))i. Straightforward set operations then lead to e1 ⊕ e2 = hs0 \ s1, s1 \ s0i. tu Associativity of the composition comes as a consequence of this last result. We now define the inverse of an event.
Definition 14. Let e ∈ E : e = h•e, e•i. Then e−1 = he•, •ei is the inverse of e. The transition system synthesized from a logic is saturated with events. For any ordered pair of states, E contains an event which labels the corresponding transition. Hence, as stated in the following proposition, any event has an inverse. Proposition 4. Let e ∈ E then e−1 ∈ E.
Proof. e ∈ E ⇒ ∃s, s0 ∈ SL : s [ei s0. By definition, it holds that e = hs\s0, s0\si. Now, ∃t ∈ T : t = (s0, [s0, s], s), and clearly, it will carry as a label hs0 \ s, s \ s0i = e−1 ∈ E. tu The inverse is well defined for all event, and so is the composition e ⊕ e−1 = e−1 ⊕ e = e∅.
Whenever composition of two events is well defined, inversion behaves accordingly, in the sense that (e1 ⊕ e2)−1 = e2−1 ⊕ e1−1 whenever they are defined.
The sequential composition operation is, of course, not commutative in general. We can formalise concurrency of two events as the commutativity of their sequential composition: the occurrence of any of them does not disable the other. Definition 15. We say two events e1, e2 ∈ E are independent iff νA(e1) ∩ νA(e2) = ∅ Note that this condition holds iff (•e1 ∪ e1•) ∩ (•e2 ∪ e2•) = ∅
We say they are concurrent if they are independent, and there exists a state that enables both of them:
∃s ∈ S(L) : •e1 ∪ •e2 ⊆ s ∧ (e1• ∪ e2•) ∩ s = ∅ It follows from independence that, when two events are concurrent, their composition becomes simply e1 ⊕ e2 = h•e1 ∪ •e2, e1• ∪ e2•i.
We show that two events are concurrent if and only if their composition is commutative and some state enables both of them. This correspondence between concurrency among two events, and commutativity of their composition accurately translates the idea that concurrent events form diamonds in the saturated transition system. We exploit this fact to prove the following result. Proposition 5. Let e1, e2 ∈ E; then they are concurrent iff e1 ⊕ e2 and e2 ⊕ e1 are well defined and equal, and there exists a state which enables both. Proof. We first prove that if e1 and e2 are concurrent, then their composition is commutative. So let s, s1, s2, s0 ∈ S(L) : s [e1i s1 ∧ s1 [e2i s0 ∧ s [e2i s2. The firing rule yields s1 = (s \ •e1) ∪ e1•, and s0 = (s1 \ •e2) ∪ e2•, and it follows from independence of e1 and e2 that s0 = (s\(•e1 ∪•e2))∪(e1• ∪e2•) = (s2 \•e1)∪e1•. Hence s2 [e1i s0.
For the converse, suppose s, s1, s2, s0 ∈ S(L) : s [e1i s1 ∧ s1 [e2i s0∧ s [e2i s2 ∧ s2 [e1i s0. Assume, as a contradiction hypothesis that ∃a ∈ νA(e1) ∩ νA(e2) 6= ∅. We distinguish four cases. If a ∈ •e1 ∩ •e2 then a ∈/ s1 and so s1[e2i. If a ∈ •e1 ∩ e2• then a ∈ s2, and so s[e2is2. Analogously a ∈ •e2 ∩ e1• implies that s[e1is1. Finally, If a ∈ e1• ∩ e2• then s1[e2i. tu The following example should clarify the last proof. The composition of two concurrent events is a diagonal of the diamond they form. In the net system interpretation, this corresponds to an event which has the same effect as firing the operands simultaneously. This view justifies the term of step. Example 3. In Figure 5 we can see that s1 [e1i s5 [e2i s2, and s1 [e2i s6 [e1i s2. The fact that from s1 the system reaches s2 after firing e1 and e2 regardless of the order of firing, implies that e1 ⊕ e2 = e2 ⊕ e1 = d.
e2 s1 s6 e1 d e1 s5 s2 e2 e2 s3 s8 e1 d e1
s7 e2
s4 We say that an event is a step if it is the diagonal of some diamond. Whenever e1, e2 are concurrent events, we may write e = e1 ⊕ e2 = e1 step e2, and say that e is the step {e1, e2}.
There is an essential difference between the non-commutative and the commutative composition of events. Indeed, commutative composition provides the diagonal of a diamond. Such a diagonal event should, in our view, be distinguished from other events. Provided that a system already depicts two concurrent events, their step provides no additional information regarding concurrency, or connectedness of the system. This section will be devoted to formalising, and proving this last statement.
In order to do so, we study the structure of diamonds as seen in the Greechie
representation of the logic. In the following, we will consider states of the logic
as the cliques of incompatibility of the atoms which intersect every block of the
logic as in theorem 1. We will therefore see events as the symmetric differences
of these. For the basic notions on graph theory, see [
Definition 16. Let G⊥(L) = (A(L), ⊥|A(L)×A(L)) be the Orthogonality Graph of a Regional Logic L. Given a subset of atoms A ⊆ A(L), we will call (A, ⊥ |A2 ) the subgraph of G⊥(L) induced by A.
Recall that each maximal clique of G⊥(L) corresponds to the set of atoms of a block (maximal Boolean sublogic) of L.
A bipartite graph is a graph whose set of vertices can be partitioned in two
classes, such that no two vertices in the same class are bound by an edge (see
[
Proposition 6. Let e ∈ E, and G⊥(L) as in Definition 16. Then (•e∩A(L), e•∩ A(L)) is a bipartition of (νA(e), ⊥ |νA(e)2 ).
Proof. e ∈ E implies ∃s, s0 ∈ S(L) : s [ei s0. Then •e ⊆ s and e• ⊆ s0. •e ⊆ s ⇒ ∀a1, a2 ∈ •e : a1, a2 ∈ s. From Theorem 1, it follows that a16 $ a2, so in particular (a1, a2) ∈/⊥. The result is analogous for e• and s0. tu The converse, however, is not always the case. We here provide an example of a logic, in which there is a bipartite subgraph of G⊥(L) which does not correspond to an event.
Example 4. In Figure 3, we can consider ({a1, b1, g1, a2, b2, g2}) as an induced subgraph. In this case, ({a1, b1, g1}, {a2, b2, g2}) forms a bipartition, but there is no event e = h{a1, b1, g1}, {a2, b2, g2}i, since no state enables it. Such a state would be a maximal clique of 6 $, but as seen in Example 2, {a1, b1, g1} does not intersect every block of L, and is therefore not a state.
We wish to study the properties of diamonds, as seen on G⊥(L). The next result will exhibit a property that any pair of concurrent events must verify. Proposition 7. Let e1 and e2 be two concurrent events. Then ∀a1 ∈ •e1, ∀a2 ∈ e2• : a1 6 $ a2, and symmetrically ∀a3 ∈ e1•, ∀a4 ∈ •e2 : a3 6 $ a4.
Proof. Since e1 and e2 are concurrent, they must form a diamond. Namely, ∃s, s1, s2, s0 ∈ S(L) : s [e1i s1 [e2i s0 ∧ s [e2i s2 [e1i s0. Hence, e1• ∪ •e2 ⊆ s1, and e2• ∪ •e1 ⊆ s2. Theorem 1 then yields the result. tu This last result might become clearer when looking at a Greechie diagram. Example 5. Consider the events e1 = h{a1}, {a2}i, and e2 = h{b1}, {b2}i from Figure 3. They are both enabled at state s = {a1, b1, c3}. The existence of the state s1 = {a2, b1, c3} implies that a2 ∈ e1•, and b1 ∈ •e2 verify a2 6 $ b1. Symmetrically, the state s2 = {a1, b2, c3} provides a1 6 $ b2. We shall now prove the much stronger converse result. Namely, we show that given an event, seen as the bipartite induced subgraph of G⊥(L), we can determine whether it is the step of two concurrent events, and if so, actually reconstruct the corresponding diamond.
Lemma 2. Connected components of the subgraph of G⊥(L) induced by an event e, form a set of pairwise concurrent events, the step of which is e. Proof. Let e ∈ E, and suppose that there is a partition {ai}i≤n of •e, and a partition {bi}i≤n of e• such that ai ∪ bi are the connected components of (νA(e), ⊥ |νA(e)2 ), for i ≤ n. We proceed by induction over the states. For the base case, consider s, s0 ∈ S(L) : s [ei s0. Now, let j ≤ n, then (s \ aj) ∪ bj must be a clique of 6 $, since otherwise there would be an r1 ∈ Si6=j ai and an r2 ∈ bj such that r1 ⊥ r2, contradicting that aj ∪ bj is a connected component for ⊥.
Now suppose (s \ aj) ∪ bj is not a state. Then there must be a block B of G⊥(L) such that ((s \ aj) ∪ bj) ∩ B = ∅. s ∈ S(L) implies that ∃r ∈ s ∩ B, so it must be r ∈ aj. Analogously, s0 ∈ S(L) implies that ∃r0 ∈ s0 ∩ B, so it must be r0 ∈ Si6=j bi. Clearly, r, r0 ∈ B → r $ r0, and •e ∩ e• = ∅ → r 6= r0, so r ⊥ r0. This contradicts the fact that aj ∪ bj is a connected component. Then sj = (s \ aj) ∪ bj must be a state, and there must be an ej = haj, bji ∈ E such that s [eji sj.
The induction step is absolutely analogous. One only needs to consider the event e0j = hSi6=j ai, Si6=j bji, noting that sj [e0ji s0.
The result holds for any choice of j ≤ n at any induction step, hence all permutations of n provide a sequential decomposition of the event e. Note that, by construction, and for any j ≤ n, the events ej are pairwise independent, and the existence of the state s provides that they must be concurrent. It should be clear that ∀j1 6= j2 : ej1 ⊕ ej2 = ej2 ⊕ ej1 ∈ E. It follows from associativity of ⊕ that Li≤n ei = e. tu This Lemma represents the main technical contribution of this work, and most of the results we henceforth present are consequences of it. Indeed, it is a powerful tool which will allow us to decompose events, as the step of a family of pairwise concurrent events.
In order to formalise the notion of minimality of the events which are no further decomposable in this way, we introduce the following partial order of events. We shall not extend our discourse on this last construction in this paper, but we find it justifies the intuitive idea that such events are in some sense minimal.
Definition 17. Let E be a set of events. We define <⊆ E2 as ∀e1, e ∈ E : e1 < e iff ∃e2 ∈ E : e1 ⊕ e2 = e2 ⊕ e1 = e.
Proof. < is irreflexive since, by convention, we do not consider e∅ ∈ E. < is transitive, as a consequence of Proposition 7, and independence of concurrent events. < is antisymmetric, since e1 ⊕ e2 = e2 ⊕ e1 = e, and e3 ⊕ e = e ⊕ e3 = e1 imply that e1 ⊕ e2 ⊕ e3 = e1, and so e3 = e2−1. Hence s [ei implies that s [e2i and s [e2−1i, but then there must be an s0 ∈ S(L) : s0 [e2i s [e2i, which contradicts the separation axioms in Definition 4. tu We will say that an event is minimal if it is minimal with respect to this partial order. From Lemma 2, it should be clear that an event is minimal if and only if it is connected, as a bipartite induced subgraph of G⊥(L). The main result that we present here is that it is sufficient to consider minimal events when synthesizing a transition system, in order for it to be connected, but also to depict all the concurrency encoded in the logic. This last notion will be formalized by comparing the set of regions of such a transition system, and that of the canonical synthesized system, which is saturated with events. Definition 18. We call M ⊆ E the set of events which are minimal in (E, <). We will start showing that M is sufficient to generate the regions of the transition system synthesized from L. The idea is rather simple. When two concurrent events are in E, then the separation axioms (see Definition 4) corresponding to their step are redundant.
Definition 19. Let A = (Q, E, T ) be a transition system, and G ⊆ E be a subset of events of A. Define TG as the set of all transitions of A labelled by some element of G. Then
A \ G = (Q, E \ G, T \ TG) Clearly, A \ G is a, possibly non-connected, transition system.
Lemma 3. Let A = (Q, E, T ) be a CETS, s0, s1, s2, s3 ∈ Q, and e1, e2, d ∈ E, such that s0 [e1i s1 [e2i s3, s0 [e2i s2 [e1i s3, and s0 [di s3. Then A and A \ {d} have the same set of regions.
Proof. Any region of A is also a region of A \ {d}, since the latter has been obtained by removing an event. Suppose now that r is a region of A \ { } d , but not of A. This implies that there are two transitions in A, say (s1, d, s2) and (s3, d, s4), with different crossing relations with respect to r. Suppose that s1 ∈ r, s2, s3, s4 ∈/ r (all other combinations can be dealt with in a similar way). By hypothesis, •d = •e1 ∪ •e2, and d• = e1• ∪ e2•. Hence, e1 and e2 are enabled at s1 and at s3, and form two diamonds, as shown in Figure 5.
Suppose that s5 is in r. Then, e1 is orthogonal to r, and e2 ∈ •r; but this leads to a contradiction, since s7 ∈/ r, and (s7, e2, s4) does not cross the border of r. On the other hand, e5 ∈/ r contradicts the hypothesis that s3 ∈/ r, because in this case e1 should leave r. tu This last result implies, in particular, that minimal events convey all the information regarding concurrency, all other events being steps of these. This is formalized in the following theorem. Theorem 2. Let L be a rich, and regular logic. Let A = (S(L), E, T ) be the saturated transition system synthesized from L. Let M be the set of minimal events in (E, <). Then the Regional logic R(A) is isomorphic to R((S(L), M, TM )). Proof. We reason by induction over the set of states. Starting from A, we apply Lemma 3 to show that for any diagonal d, R(A) ' R(A \ {d}). In the inductive step, the hypothesis will be that R(A \ D) ' R(A), then for any step d in E \ D, Lemma 3 provides R(A \ (D ∪ {d})) ' R(A). Clearly, when D contains all the steps of E, then E \ D = M . tu Theorem 3. Let M be a set of minimal events in (E, <), and let TM be the set of all transitions carrying some label in M , then the graph representation of the transition system (S(L), M, TM ) is connected.
Proof. By construction, the graph associated to the saturated synthesized transition system (S(L), E, T ) is a complete graph. It is therefore connected. Now let s, s0 ∈ S(L). We proceed again by induction. Suppose [s, s0] is not a minimal event. Then Lemma 2 shows that ∃s1/2 ∈ S(L) : s [[s, s1/2]i s1/2 [[s1/2, s0]i s0. For the inductive step, assume there is a path s [e1i s1 [e2i . . . [eii si [ei+1i s0. Now, from Lemma 2 it holds that ∀ej+1 ∈/ M : ∃sj1/2 such that sj [[sj , sj1/2]i sj1/2 [[sj1/2, sj+1]i sj+1. Clearly,s [e1i s1 [e2i . . . sj [[sj , sj1/2]i sj1/2 [[sj1/2, sj+1]i sj+1 . . . [eii si [ei+1i s0 is a path connecting s and s0. The induction will then end with a path connecting s and s0 where all arcs correspond to minimal events. tu A direct consequence of this last theorem, is that the transition system depicting only minimal events verifies the first axiom of Definition 1. 4
In the synthesis of a transition system from a quantum logic, the state of the art provides a canonical system which is saturated with events. All possible events are considered. In this work, we have endowed this set of events with a structure, so as to provide an alternative canonical system with less events, by considering only the ones which do not correspond to the step firing of any other two. We have shown that they then have the same set of regions. Together with the connectedness of the underlying graph in the new canonical system, we have gathered technical results which seem promising towards the main aim in this line of research. Our goal is to show that, under suitable conditions, the regional logic of the synthesized transition system is isomorphic to the original one.
This work has been partially supported by MIUR.