The set of regions of a transition system, ordered by set inclusion, is an orthomodular poset, often referred to as quantum logic, here called regional logic. Regional logics, which result to be also regular and rich, are the main subject of investigation in this work. Given a regular, rich logic L, one can build a condition/event transition system A, such that L embeds into the regional logic of A. Call stable a logic if the embedding is an isomorphism. We give some necessary conditions for a logic to be stable, and show that under these, the embedding presents some stronger property. The full characterization of the class of stable logics is still an open problem. In particular, we show that any {0, 1}-pasting of n Boolean logics is stable, and that, whenever L contains n maximal Boolean sublogics sharing exactly one atom, L is stable.
Regions of transition systems have been introduced by Ehrenfeucht and
Rozenberg [
We are interested in the order structure of regions both in case they are seen
concretely as sets ordered by set inclusion and in case they are seen abstracly
as quantum logics. While quantum logics [
In more detail, we exploit a duality between condition/event transition
systems and rich and regular quantum logics presented in [
The special cases analyzed in this paper exploit the fact that any quantum
logic can be seen as a family of partially overlapping Boolean algebras. In
particular, we show that any {0, 1}-pasting ([
The rest of the paper is structured as follows. In section 2, after preliminary definitions on transition systems, condition event transition systems (CETS) and regions, we present in section 2.2 basic notions on quantum logics, in particular on rich and regular logics, as well as the notion of two-value state. In section 3 we show that to any CETS it is possible to associate the quantum logic of its regions, and we show a synthesis procedure to associate a CETS to any rich and regular logic. Sections 4 and 5 constitute the original part of the paper: the first deals with some results towards the characterization of stable logics, the second considers some particular subclass of logics, and shows that they are stable. Section 6 concludes the paper with some remarks. 2 2.1
Transition systems are a class of automata representing the global behaviour of
a system in opposition to the representation via local states or local properties.
The relation between these two ways of representation is extensively reported
in the literature, see [
Definition 1. A transition system is a triple 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. We assume that the following conditions are respected: 1. the underlying graph of the 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 .
In some cases, we will drop axiom 1, which imposes connection.
A region of a transition system is a set of its states such that the occurrence of one of its events has the same crossing relation, namely entering, leaving the region itself, or otherwise neither of the two. This is formalised as follows. Definition 2. A region of a transition system A = (Q, E, T ) is a subset r of Q such that ∀e ∈ E, ∀(q1, e, q2), (q3, e, q4) ∈ T : 1. (q1 ∈ r and q2 6∈ r) ⇒ (q3 ∈ r and q4 6∈ r); and 2. (q1 6∈ r and q2 ∈ r) ⇒ (q3 6∈ 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 that originates the regions 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. 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 6∈ 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}.
Condition/event transition systems have been introduced as the class of
transition systems isomorphic to the sequential case graphs of condition/event net
systems [
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: (q1, e, q2) ∈ T ; 3. ∀ q1 ∈ Q, ∀ e ∈ E e• ⊆ Rq1 ⇒ ∃ q2 ∈ Q: (q1, e, q2) ∈ T .
Basic facts concerning regions of CETS [
We consider R(A) as enriched with the usual concrete structure. Elements, seen as subsets of A, are ordered by inclusion. Set union and intersection are here partial operations; R(A) is closed by set complement. 2.2
We will follow the notation and definitions given in [
This latter condition is sometimes referred to as orthomodular law. Let x, y ∈ L be such that x ≤ y0, then we say that they are orthogonal, denoted x ⊥ y.
A sublogic of L is a subset Lˆ of L that is itself a logic with respect to the restrictions of the operation (.)0 and the relation ≤ to Lˆ. In particular, x ∈ Lˆ ⇒ x0 ∈ Lˆ and, ∀x, y ∈ Lˆ x ≤ y0 ⇒ x ∨ y ∈ Lˆ. A sublogic is Boolean if it is a Boolean algebra.
An element a of a logic is an atom if, for any element b of L such that b ≤ a either b = a or b = 0. Atoms are the least elements in the logic except for the bottom element. A logic is said to be atomic if any element, except the bottom, is greater or equal to some atom. Finite logics are atomic. Atomic logics present the practical advantage to be determined by the relations among their atoms, and thus allow for a concise representation.
We say that two elements x and y in L are compatible, denoted x $ y if,
and only if, there exist three mutually orthogonal elements xˆ, yˆ and z in L such
that x = xˆ ∨ z and y = yˆ ∨ z. Intuitively, we can see maximal sets of mutually
compatible elements in L as maximal Boolean sublogics of L. The following
definition is taken from [
Definition 6. A logic L is called regular if, for any set {x, y, z} ⊆ L of pairwise compatible elements, we have that x $ (y ∨ z).
The relation between compatible subsets of a logic L and Boolean sublogics of
L is put in evidence by the following proposition, to be found in [
Proposition 2. A logic L is regular if and only if every subset of pairwise compatible elements of L admits an enlargement to a Boolean sublogic of L. Example 1. The poset shown in figure 1 is a regular quantum logic. The set of its atoms is v, w, x, y, z. Examples of orthogonal pairs of elements are: x ⊥ y, x ⊥ w, v ⊥ w. It contains two maximal Boolean sublogics: {0, v, w, x, v0, w0, x0, 1} and {0, x, y, z, x0, y0, z0, 1}, which intersect in the (non-maximal) Boolean sublogic {0, x, x0, 1}.
Morphisms of logics are defined in such a way that they preserve order (and
consequently orthogonality) and compatibility. The formal definition is borrowed
from [
Fig. 1. A regular quantum logic.
Definition 7. Let L1 and L2 be logics. A mapping f : L1 → L2 is a morphism of logics if the following conditions are satisfied: 1. f (0) = 0; 2. ∀x ∈ L1 f (x0) = f (x)0; 3. ∀x, y ∈ L1 x ⊥ y ⇒ f (x ∨ y) = f (x) ∨ f (y).
A morphism f : L1 → L2 is an isomorphism if f is bijective, and f −1 is a morphism. Moreover, f is an embedding if f (L1) is a sublogic of L2 and f : L1 → f (L1) is an isomorphism.
A crucial notion in the following is the concept of two-valued state which, in
the case of regional logics, will allow to identify subsets of regions
corresponding to states of the related condition/event transition systems. The following
definition can be found in [
Definition 8. A two-valued state on a quantum logic L is a mapping s : L → {0, 1} such that: 1. s(1) = 1; 2. ∀x, y ∈ L x ⊥ y
⇒ s(x ∨ y) = s(x) + s(y) An immediate consequence of the definition is that a state s preserves order.
In [
If L is atomic, then every state will assign 1 to exactly one atom per maximal Boolean sublogic.
Given a logic L, we denote by S(L) the set of all states on L and by Sx the set {s ∈ S(L) | s(x) = 1}.
Definition 9. Let L be a logic, and X ⊆ L, then the up-closure of X, denoted
↑X, is the set of all elements in L greater or equal to some element in X.
Formally:
↑X := {a ∈ L | ∃x ∈ X : x ≤ a}
This definition is particularly useful, for it allows to represent states in a concise
way. This representation relies on a result from [
Proposition 3. Any state s of a finite logic L is the characteristic function of a set ↑X, where X is a maximal set of pairwise incompatible atoms, such that it intersects each maximal set of mutually orthogonal atoms.
Example 2. Consider the logic shown in figure 1. v 6 $ y, v 6 $ z, w 6 $ y and w 6 $ z, and indeed its states are: ↑{v, y}, ↑{v, z}, ↑{w, y}, ↑{w, z} as well as ↑{x}. Sv = {↑{v, y}, ↑{v, z}}, Sx = {↑{x}}.
Logics which have “enough” states, in such a way that the order relation can be re-constructed by the evaluation of the states, are called rich.
Definition 10. Let L be a logic and x, y ∈ L. L is rich if:
Sx ⊆ Sy ⇒ x ≤ y.
Sa ∩ Sb 6= ∅.
The converse property: x ≤ y ⇒ Sx ⊆ Sy is a consequence of condition 2.
in Def. 8 above. A characterisation of rich logics, which will be of use in the
contributions of the present work, is provided by the following theorem ([
Theorem 1. Let L be a logic. Then L is rich if and only if ∀a, b ∈ L a 6 $ b ⇒ Example 3. Consider again the logic shown in figure 1. It is rich, in fact, for example, v 6 $ y and Sv ∩ Sy = {↑{v, y}} since Sv = {↑{v, y}, ↑{v, z}} and Sy = {↑{v, y}, ↑{w, y}}.
A particular type of logic is known as concrete logic. A logic is called concrete if it can be represented as a collection of subsets of a given set Ω. In this case, the order relation is the set inclusion between subsets of Ω while the orthocomplement ( . )0 is the set complement in Ω.
Definition 11. The tuple (Δ, ⊆, ∅, Ω, (.)0), where Δ is a collection of subsets of a given set Ω and A ∈ Δ ⇒ (A)0 = Ω \ A, is a concrete logic if and only if the following conditions are satisfied:
Note that in this concrete representation of a logic, orthogonality is equivalent
to being pairwise disjoint, and two elements A1, A2 ∈ Δ will be compatible if
and only if A1 ∩ A2 ∈ Δ. A more detailed presentation of concrete logics and the
discussion on the satisfaction by concrete logics of properties 1-4 in definition 5
can be found in [
As shown in section 3 below, the set of regions R(A) of a CETS A is a
concrete logic. This is the reason why we are interested in concrete logics and in
the following theorem (due to Stanley Gudder and reported in [
The proof of this theorem uses a property of duality between L and the set of its states S(L): each element in x ∈ L can be represented by the set Sx of the s ∈ S(L) such that s(x) = 1. Conversely, we note that states are in fact characteristic functions, and can therefore be interpreted as subsets of L. We will use the same duality in the next sections.
Remark. In the present paper, we have partly changed notation and terminology
with respect to [
In the following, we recall how to associate to any CETS a concrete regular logic, and how to construct a CETS starting from a rich and regular logic; afterwards, we discuss the relations between these two transformations.
Let us consider the properties of regions recalled in proposition 1. By using
these properties, it is possible to construct a logic starting from the regions of a
transition system. More precisely, if A = (Q, E, T ) is a finite CETS and R(A) is
its set of regions then R(A) = (R(A), ⊆, ∅, Q, (.)0) (where r ∈ R(A) ⇒ (r)0 =
Q \ r) is a rich and regular quantum logic as proved in [
In [
In the following, besides illustrating the synthesis procedure, we show by means of examples that in general in both cases there is no isomorphism between L and R(A(L)) as well as between A and A(R(A)).
The core of the synthesis procedure is in interpreting the states of S(L) as the states of a transition system. A state of the transition system can be identified with the set of all regions containing it, and, by proposition 3, it coincides with the state of a logic, as in definition 8. In fact, the transition system associated to a logic L is constructed by taking S(L) as the set of states, and symmetric differences between states as events. Formally we have the following.
E(L) = {hs1 \ s2, s2 \ s1i | s1, s2 ∈ S(L), s1 6= s2}. (1) The set of transitions is now naturally defined as the set of all pairs of distinct states, each labelled by the corresponding ordered symmetric difference. In the
T (L) = {(s1, [s1, s2], s2) | s1, s2 ∈ S(L), s1 6= s2} Of course, the same label can have several occurrences. We can now define the transition system
A(L) = (S(L), E(L), T (L)).
(2)
(3)
The transition system A(L) includes a transition for each ordered pair of states;
hence we call it saturated of transitions. A(L) is a CETS, as shown in [
At this point, two natural questions arise about the two opposite transformations and the possibility that they are inverse of each other:
1. Given a rich and regular logic L, build the CETS A(L) and consider its regional logic R(A(L)). Is R(A(L)) isomorphic to L?.
2. Given a CETS A0, construct the CETS associated to its regional logic A(R(A0)). Is A(R(A0)) isomorphic to A0?
In the general case, L embeds into R(A(L)). In fact, for each x ∈ L, Sx is a set of regions of A(L) and the embedding is given by φ(x) = Sx ⊆ S(L).
The fact that φ( . ) is an embedding of logics will be formally proved in the next section in proposition 4. However, φ( . ) is not always an isomorphism, and this can be clarified by the following example.
Example 4. Consider the set Ω = {1, 2, . . . , 6} and define Δ as the collection of the X ∈ P(Ω) such that |X| is an even number. Then L = (Δ, ⊆, ∅, Ω, (.)0) is a regular concrete logic in which, for x, y ∈ Δ, x $ y ⇔ x ∩ y ∈ Δ. All the states of L are represented by the sets δi = {x ∈ Δ | i ∈ x} for i = {1, 2, . . . , 6}. The CETS associated to L, A(L) has then six states and a set of transitions, computed as in eq. 2 above, whose labels are all distinct. This means that the regions of the CETS A(L), defined as in eq. 3 above, are isomorphic to the power set P(Ω) that strictly contains Δ.
Viceversa, by assuming as given a CETS A = (Q, E, T ), the general case shows that S(R(A)), and then also A(R(A)), can contain states which do not correspond to any state in Q. This means that, in general, A is not isomorphic to A(R(A)), as for example in the following.
Example 5. Consider the CETS A = (Q, E, T ) shown in figure 2. Its regions are the trivial ones, ∅ and Q, plus x = {1, 2, 5}, y = {1, 2, 6}, z = {1, 3, 5}, w = {1, 3, 6} and the respective complements {3, 4, 6} = ({1, 2, 5})0, {3, 4, 5} = ({1, 2, 6})0, {2, 4, 6} = ({1, 3, 5})0 and {2, 4, 5} = ({1, 3, 6})0. The corresponding concrete logic is represented in figure 3 and its states are formed by choosing exactly one element from each complementary pair of disjoint non-trivial regions. Hence, there are sixteen states. By applying the synthesis procedure above to the logic R(A) = (R(A), ⊆, ∅, Q, (.)0), we find that six out of the sixteen states in S(R(A)) correspond to the original states of A.
Concerning the relation between regions and events, we note that pre- and post-regions of an event e ∈ E can be retrieved in R(A) as set differences between states of the logic. Remember that Rq1 is the set of regions containing q1 and Rq2 is the set of regions containing q2. If (q1, e, q2) is a transition in A, then Rq1 \Rq2 gives the set of regions from which e exits, namely the set of pre-regions of e; the difference in the other direction gives the set of post-regions. By definition of region, these differences are independent of the individual occurrence of e in A: let (q1, e, q2), (q3, e, q4) ∈ T . Then Rq1 \ Rq2 = Rq3 \ Rq4 = •e and Rq2 \ Rq1 = Rq4 \ Rq3 = e•. Hence, these set differences allow us to identify different occurrences as corresponding to the same event, in other words, that two transitions carry the same label.
Example 6. For the CETS A in figure 2, the case can be exemplified by considering the two events labelled a, leading from state 1 to state 3 and from state 2 to state 4, respectively. In this case, R1 is the set composed by {1, 2, 5}, {1, 2, 6}, {1, 3, 5}, {1, 3, 6} and R3 is composed by {3, 4, 6}, {3, 4, 5}, {1, 3, 5}, {1, 3, 6}. By computing the set differences as above, we find that: R1 \ R3 = R2 \ R4, the set of regions from which a exits. The symmetric case leads to R3 \ R1 = R4 \ R2. x x0 y y0 z z0 w
w0
With reference to the logic R(A) of the CETS A in figure 2 as represented in figure 3, we can compute, in terms of symmetric differences, the transitions between any couple of the sixteen states of the logic R(A) as in equation 2 above. We find, among many others, the transitions corresponding to the identical labels of A. For example, by considering the states in Sx and in Sy, we have that Sx \ Sy = Sy0 \ Sx0 . 4
In the previous section, we have considered two cases: the first one deals with the construction of a logic R(A) starting from a CETS A and the second one deals with the construction, or synthesis, of a CETS A(L) starting from a regular and rich logic L. In both cases, by applying again the process and computing A(R(A)) and R(A(L)) we obtain two embeddings. The original CETS A embeds in terms of both states and transitions into the CETS resulting from the synthesis procedure applied to R(A), and the original logic L embeds into the concrete logic formed by taking Ω as the states of A(L) and Δ as the set of regions of A(L), as asserted by theorem 2. We say that the logic L is stable if this embedding is an isomorphism of logics.
Definition 12. A quantum logic L is stable if there is an isomorphism of logics from L onto R(A(L)).
Our aim is to characterize the class of stable regional logics. In what follows, we present some new results towards such a goal. First we discuss two necessary conditions for a logic to be regional, and then we prove that one implies the other. Afterwards, in subsection 4.2, we prove that there is an embedding of logics from L to R(A(L)), and that, under the same condition, this embedding is strong in the sense that it preserve also incompatibility. 4.1
In [
The property tip results from the translation in the abstract setting of
quantum logic of a property of regions of transition systems, which we call triple
intersection property and which is expressed by the following lemma, the proof
of which can be found in [
Lemma 1. Let A be a CETS, and let a, b, c ∈ R(A) be such that: a ∩ b = b ∩ c = c ∩ a, then z = a ∩ b ∩ c ∈ R(A).
The triple intersection property (tip) for a logic L is then obtained by considering for any element in L the set of two-valued states selecting that element and from the fact that this set identifies a region of the CETS A(L) synthesised from L.
∀a, b, c ∈ L : Sa ∩ Sb = Sb ∩ Sc = Sc ∩ Sa ⇒
∃z ∈ L : Sz = Sa ∩ Sb ∩ Sc As well as tip, also eti is inspired by a property of regions. If (q1, e, q2), (q3, e, q4), with q1 6= q3 and q2 6= q4, are two distinct transitions in a CETS A = (Q, E, T ), then R(A) must contain two incompatible regions, one containing q1 and q2 but not q3, the other containing q1 and q3 but not q2. Hence, events with multiple occurrences and pairs of incompatible regions are related. In this sense, we say that the events of an abstract logic L testify incompatibility ; L is said to be eti if, for any pair of incompatible regions, the set E(L) contains an element witnessing this incompatibility.
∀a, b ∈ L :
a 6 $ b ⇒
∃s1 ∈ Sa ∩ Sb, sa ∈ Sa ∩ Sb0 , sb ∈ Sb ∩ Sa0 , s0 ∈ Sa0 ∩ Sb0 : sa \ s1 = s0 \ sb
Example 7. An example of a concrete logic which is neither tip nor eti is the
logic of the subsets of even cardinality of {1, 2, 3, 4, 5, 6}, already seen in example
4. This logic is regular and rich, but not regional as discussed in [
Any regional logic is tip, as shown in [
Theorem 3. Let L be a eti logic. Then L is tip.
Sa ∩ Sb = Sb ∩ Sc = Sc ∩ Sa.
Proof. By contradiction, let L be eti and not tip. Not tip means: ∃a, b, c ∈ L : Sa ∩ Sb = Sb ∩ Sc = Sc ∩ Sa 6= ∅ and ∀z ∈ L : Sz 6= Sa ∩ Sb ∩ Sc. We have two cases.
First case: a $ b. Then since Sa ∩ Sb 6= ∅, a 6⊥ b and then there exist three mutually orthogonal elements aˆ, ˆb and x in L such that a = aˆ ∨ x and b = ˆb ∨ x. This implies Sa to be the disjoint union of Saˆ and Sx, and Sb to be the disjoint union of Sˆb and Sx, then we get the contradiction: ∃x : Sx = Sa ∩ Sb = Sc ∩ Sa.
Second case: a 6 $ b. Then, since L is eti, there are four states: s1 ∈ Sa ∩ Sb, sa ∈ Sa ∩ Sb0 , sb ∈ Sb ∩ Sa0 , s0 ∈ Sa0 ∩ Sb0 such that: sa \ s1 = s0 \ sb. Then s1 ∈ Sa ∩ Sb implies s1 ∈ Sc. Since Sc is a region in R(A(L)), then either sa ∈ Sc and sb ∈/ Sc, or sb ∈ Sc and sa ∈/ Sc. In any case this contradicts the hypothesis tu 4.2
Strong embedding of L into R(A(L)) At this point, we stress the fact that given a regular, and rich logic L, and its synthesised CETS A(L), the injection defined by φ(x) = Sx is a morphism of logics. Furthermore, we show that φ : L → R(A(L)) is an embedding of logics. To check that φ is a morphism, we verify the three properties in Def. 7. First note that S0 = ∅ is the bottom element in R(A(L)). Second, since any x ∈ L is orthogonal to its complement x0, from point 2. in Def 8, it stands that Sx ∩ Sx0 = ∅, and furthermore, ∀x ∈ L : Sx ∪ Sx0 = S(L), so Sx0 = S(L) \ Sx. The third point is a direct consequence of proposition 1.
On the other hand, put Sx = Sy, then L being rich, it holds from Def. 10 that x ≤ y and y ≤ x, so φ is injective. We see in the following proposition, that φ is even an embedding.
Proposition 4. Let L be a rich and regular logic, and φ : L → R(A(L)) be defined by φ(x) = Sx for all x ∈ L. Then ψ ≡ φ−1|φ(L) is a logic morphism. Proof. Clearly, ∀x ∈ L : ψ(Sx) = x. Now, since L is rich, the only element whose associated set of states is the bottom element, hence ψ(∅) = 0. Also, ψ(S(L) \ Sx) = ψ(Sx0 ) = x0, so it preserves orthocomplements. Finally, consider two disjoint Sx, Sy. Then Sx ⊆ S(L) \ Sy = Sy0 , and since L is rich, x ⊥ y. From point 2. in Def. 8 it stands that {s ∈ S(L) | s(x ∨ y) = 1} = {s ∈ S(L) | s(x) = 1} ∪ {s ∈ S(L) | s(y) = 1} = Sx ∪ Sy. Hence ψ(Sx ∪ Sy) = x ∨ y. tu Now, φ being an embedding means that L and R(A(L)) would be isomorphic if φ was surjective. We have also seen in the previous section that L being eti is a necessary condition for that. We shall now see that if L is eti, the embedding verifies a stronger property, required (but not sufficient) for φ to be an isomorphism.
We remind the reader that logic morphisms preserve order, orthogonality and compatibility. Since φ is an embedding it shall also reflect these relations. However, in general this is only true when considering them restricted to the image φ(L). Indeed, if φ is an embedding then L is isomorphic to φ(L), but the lack of surjectivity might, in the general case, allow the images of two incompatible elements to be compatible. We shall explain this notion through an example. Example 8. Consider the logic L = {0, u, u0, v, v0, 1}, and the Boolean logic B whose atoms are {a1, a2, a3, a4}. Then the mapping given by φ(u) = a1 ∨ a2, φ(u0) = a3 ∨ a4, φ(v) = a1 ∨ a3, φ(v0) = a2 ∨ a4 is indeed an embedding. Since (a1 ∨ a2)0 = a3 ∨ a4 and (a1 ∨ a3)0 = a2 ∨ a4, the sublogic L1 = {0, a1 ∨ a2, a3 ∨ a4, a1 ∨ a3, a2 ∨ a4, 1} of B is isomorphic to L. However, when considered in the whole of B, we see that a1 is both a1 ≤ a1 ∨ a2 and a1 ≤ a1 ∨ a3, with {a1, a2, a3} mutually orthogonal in B. Thus φ(u) $ φ(v), whereas u 6 $ v. This does not prevent φ from being an embedding because, in fact a1, a2, a3 ∈/ L1.
This example should justify the following definition (see [
Definition 15. Let φ : L1 → L2 be an embedding between logics. Then φ is said to be a strong embedding if ∀a, b ∈ L1 : a $ b ⇔ φ(a) $ φ(b) For instance, a logic with incompatible elements cannot embed strongly into a Boolean logic.
We shall now prove that a logic L being eti is a sufficient condition for φ : L → R(A(L)) to be a strong embedding.
Theorem 4. Let L be a rich and regular logic. If L is eti, then the embedding φ : L → R(A(L)) defined as φ(x) = Sx is strong.
Proof. We have already shown that φ preserves compatibility, it will therefore be sufficient to prove that it also preserves incompatibility. So let a, b ∈ L verify a 6 $ b. Since L is eti, ∃s1 ∈ Sa ∩ Sb, sa ∈ Sa ∩ Sb0 , sb ∈ Sb ∩ Sa0 , s0 ∈ Sa0 ∩ Sb0 : sa \ s1 = s0 \ sb. Then e = [s1, sa] ∈ E(L) will be a label in the saturated transition system A(L), and the transitions (s1, e, sa), (sb, e, s0) ∈ T (L) will prevent Sa ∩ Sb from being a region. Indeed, (s1, e, sa) crosses the border of Sa ∩ Sb, whereas (sb, e, s0) does not. Since R(A(L)) is a concrete logic, we have that Sa = φ(a) 6 $ φ(b) = Sb. tu This result implies, in particular, that if new regions are produced by the synthesis procedure, these cannot be contained in the image by φ of an atom. Orthocomplementation implies therefore that they cannot contain the images of coatoms (maximal elements except for the top). Thus, the possible lack of surjectivity of φ is narrowed down. 5
In this section we look at a few subclasses of concrete logics, and show that they are stable.
To start with the simplest example, let L be a finite Boolean logic with k atoms. Then L is a regular rich logic, isomorphic to the power set of {1, · · · , k}, in which singletons correspond to atoms. L has exactly k states, each corresponding to ↑{x}, where x is an atom of L.
This implies that all the ordered symmetric differences between states differ in at least one atom, so that each transition in A(L) carries a unique label, and all subsets of states are regions. Hence, L and R(A(L)) are isomorphic, and L is stable.
In the next cases, we will use the notion of restriction of a transition system to a subset of events. We will say that A1 = (S, E1, T1) is a restriction of A = (S, E, T ) if they have the same set of states, E1 ⊆ E, and T1 is obtained by removing from T all the transitions labelled by events in E \ E1. From the definition of regions, it follows immediately that R(A) ⊆ R(A1).
The next case we consider is that of a logic obtained as the so-called {0, 1}pasting of two (or more) logics. This construction is strictly related to a construction on transition systems, so we briefly deviate from the main route, in order to clarify the correspondence.
Given two transition systems, A1 and A2, with disjoint sets of events, we can build a new one by putting them side-by-side and letting them work in parallel. Definition 16. Let Ai = (Qi, Ei, Ti) be a CETS for i = 1, 2, with E1 ∩ E2 = ∅. Define
A1 || A2 = (Q1 × Q2, E1 ∪ E2, T ) where
T ={((q1, q2), e, (q10, q2)) | (q1, e, q10) ∈ T1} ∪ {((q1, q2), e, (q1, q20)) | (q2, e, q20) ∈ T2} By construction, for each region r of A1, the set r × Q2 is a region of A1 || A2, and, for each region r of A2, the same holds for the set Q1 ×r. For any region r of A1 || A2, the projection of its states on the first component must be a region of A1 (and symmetrically for the projection on the second component), because in any transition only one of the two components of a state will change; hence, the full set of non-trivial regions of A1 || A2 is given by {r × Q2 | r ∈ R(A1)} ∪ {Q1 × r | r ∈ R(A2)}. We now introduce the corresponding operation on logics, found as {0-1}-pasting in the literature. We use the same symbol as for the operation on transition systems. It will always be clear by the context which is being applied. Definition 17. Let L1 and L2 be two logics with 0i, 1i for i = 1, 2 the respective least and greatest elements. Define on L1 ∪ L2 the equivalence relation ∼:= {(a, a) | a ∈ L1 ∪ L2} ∪ {(01, 02), (11, 12)}.
Then L1 || L2 = (L1 ∪L2)/∼ is the {0-1}-pasting of L1 and L2. It is their disjoint union but for identification of 01 with 02, and 11 with 12.
The {0-1}-pasting of L1 and L2, L1 || L2, is again a logic.
Without loss of generality, in what follows we will simplify the notation concerning the {0-1}-pasting of L1 and L2 by indicating by the same element 0 and, respectively, 1 the bottom and top elements in both L1 and L2. As a useful consequence, the set of states S(L1 || L2) of L1 || L2, seen as membership functions, will simply be composed by the union s1 ∪ s2 for any pair of states s1 ∈ S(L1) and s2 ∈ S(L2).
The next lemma shows that the parallel product of transition systems and the {0, 1}-pasting of logics are strictly related. The lemma follows from the characterization of regions of A1 || A2 discussed above.
Lemma 2. Let Ai = (Qi, Ei, Ti) be a CETS for i = 1, 2, with E1 ∩ E2 = ∅. Then R(A1 || A2) and R(A1) || R(A2) are isomorphic logics.
Proposition 5. Let L1 and L2 be stable regional logics. Then L = L1 || L2 is a stable regional logic.
Proof. Consider A(L) = (S(L), E(L), T (L)), the synthesis as defined in section 3. Every state in L is obtained by taking the union of a state of L1 and a state L2, and every such union is a state in L:
S(L) = {s1 ∪ s2 | s1 ∈ S(L1), s2 ∈ S(L2)}. All these unions are distinct, so we can represent S(L) as S(L1) × S(L2).
We will now define a transition system on S(L), by taking a subset of the events and transitions of the saturated transition system. Define EM ={[(s1, s2), (s01, s2)] | s1, s01 ∈ S(L1), s2 ∈ S(L2)} ∪
{[(s1, s2), (s1, s02)] | s1 ∈ S(L1), s2, s02 ∈ S(L2)} We must now take all the transitions corresponding to labels in E.
TM ={((s1, s2), [(s1, s2), (s01, s2)], (s01, s2)} ∪
{((s1, s2), [(s1, s2), (s1, s02)], (s1, s02)}.
The transition system AM (L) = (S(L), EM , TM ) is a restriction of A(L), such that EM ⊆ E, hence, its set of regions is a superset of R(A(L)). On the other hand, each region of AM (L) is either of the form S(L1) × r, for r ∈ L2, or of the form r × S(L2), for r ∈ L1. Hence, after theorem 2, there is an isomorphism between L and R(AM (L)), and since R(A(L)) ⊆ R(AM (L)) ' R(A(L1)) ∪ R(A(L2) ⊆ R(A(L)), there is a bijection between L and R(A(L)), and L is stable. tu The construction and the argument above can be easily generalised to the case of the {0, 1}-pasting of K logics.
Let us now suppose that L is a rich, regular quantum logic with exactly
two maximal Boolean sublogics, B1 and B2, such that B1 ∩ B2 = B, with
B = {0, x, x0, 1}, and x is an atom of L (hence x0 is a co-atom). Note that B
is a Boolean logic (it corresponds to what is called the centre of L in [
Proposition 6. Let L be a logic such that L = B1 ∪ B2, B1, B2 are Boolean sublogics, and B = B1 ∩ B2 = {0, x, x0, 1}. Then L is stable.
Proof. There are two kinds of states of L. States of the first kind are built by choosing one atom a of L in B1 \ B2, one atom b of L in B2 \ B1, and the upclosure of {a, b} in L. The only state of the second kind is the up-closure of {x}. We will now define a generalised transition system, so that it is a restriction of A(L), by selecting a subset of events, and the corresponding transitions.
Let us denote each state in A(L) of the first kind by the ordered pair (a, b), with a and b atoms of L. Let x, y, w, and z be variables ranging on the atoms of L. Then we select the events associated to transitions from, say, (x, y) to (w, y), and those associated to transitions from (x, y) to (x, z).
Let EM (L) be this set of events, and define T M (L) as the set of all transitions in A(L) with labels in EM (L). Finally, define AM (L) = (S(L), EM (L), T M (L)). Clearly, AM (L) is a generalised transition system, which is a restriction of A(L).
AM (L) is not connected because the state ↑{x}, with x the atom of L common to B1 and B2, is isolated.
Each transition in A(L) starting from, or leading to, ↑{x} carries a unique label, which has no other occurrence. Hence, the singleton formed by this state is a region in A(L), as it is in AM (L).
The rest of AM (L) can be seen as the parallel product of A(B1), without the states corresponding to atoms shared with B2, and the analogous substructure of A(B2). We can then apply the same argument as in the case of the {0, 1}-pasting given in proposition 5 above.
The construction can be generalised to the case of a family of K Boolean logics, such that their pairwise intersections coincide, and consist in a Boolean logic B = {0, x, x0, 1}, and x is an atom of L. A state of A(L) is either the up-closure of {x} or the up-closure of a set built by choosing exactly one atom from each Bi. 6
With the results presented in this paper we have done a further step towards the characterization of the rich and regular quantum logics, which result to be isomorphic to the orthomodular posets of the regions of the CETSs synthesised starting from the logics themself.
We are particularly interested in such a characterization because it is the basis for founding a logic of distributed systems. While the regions of a single sequential component constitute a Boolean logic, the presence of concurrency leads to a family of partially overlapping Boolean sublogics, each one corresponding to a sequential component.
This work is partially supported by MIUR.