Higher Dimensional Modal Logic

Higher dimensional automata (HDA) are a model of concurrency that can express most of the traditional partial order models like Mazurkiewicz traces, pomsets, event structures, or Petri nets. Modal logics, interpreted over Kripke structures, are the logics for reasoning about sequential behavior and interleaved concurrency. Modal logic is a well behaved subset of first-order logic; many variants of modal logic are decidable. However, there are no modal-like logics for the more expressive HDA models. In this paper we introduce and investigate a modal logic over HDAs which incorporates two modalities for reasoning about"during"and"after". We prove that this general higher dimensional modal logic (HDML) is decidable and we define an axiomatic system for it. We also show how, when the HDA model is restricted to Kripke structures, a syntactic restriction of HDML becomes the standard modal logic. Then we isolate the class of HDAs that encode Mazurkiewicz traces and show how HDML, with natural definitions of corresponding Until operators, can be restricted to LTrL (the linear time temporal logic over Mazurkiewicz traces) or the branching time ISTL. We also study the expressiveness of the basic HDML language wrt. bisimulations and conclude that HDML captures the split-bisimulation.


Introduction
This paper extends [1] by adding all the proofs and some more explanations. Moreover, it corrects some essential errors that appeared in the proofs of soundness and completeness of the axiomatic system of [1]. The present paper also adds new results that steam from two comments that this work attracted. We discuss the expressive power of the basic logic wrt. bisimulations, concluding that it captures the split-bisimulation. We investigate more carefully the extension of the basic language with the Until operator; we define precisely two kinds of Until, and we use the LTL-like to encode the LTrL logic and the CTL-like to encode the ISTL logic.
Higher dimensional automata (HDAs) are a general formalism for modeling concurrent systems [2,3]. In this formalism concurrent systems can be modeled at different levels of abstraction, not only as all possible interleavings of their concurrent actions. HDAs can model concurrent systems at any granularity level and make no assumptions about the durations of the actions, i.e., refinement of actions [4] is well accommodated by HDAs. Moreover, HDAs are not constrained to only before-after modeling and expose explicitly the choices in the system. It is a known issue in concurrency models that the combination of causality, concurrency, and choice is difficult; in this respect, HDAs and Chu spaces [5] do a fairly good job [6].
Higher dimensional automata are more expressive than most of the models based on partial orders or on interleavings (e.g., Petri nets and the related Mazurkiewicz traces, or the more general partial order models like pomsets or event structures). Therefore, one only needs to find the right class of HDAs in order to get the desired models of concurrency.
Work has been done on defining temporal logics over Mazurkiewicz traces [7] and strong results like decidability and expressive completeness are known [8,9]. For more general partial orders some temporal logics become undecidable [10]. For the more expressive event structures there are fewer works; a modal logic is investigated in [11].
There is hardly any work on logics for higher dimensional automata [6] and, as far as we know, there is no work on modal logics for HDAs. In practice, one is more comfortable with modal logics, like temporal logics or dynamic logics, because these are generally decidable (as opposed to full first-order logic, which is undecidable).
That is why in this paper we introduce and develop a logic in the style of standard modal logic. This logic has HDAs as models, hence, the name higher dimensional modal logic (HDML). This is our basic language to talk about general models of concurrent systems. For this basic logic we prove decidability using a form of filtration argument, and we show how compactness fails. Also, we provide an axiomatic system and prove it is sound and complete for the higher dimensional automata. HDML in its basic variant is shown to become standard modal logic when the language and the higher dimensional models are restricted in a certain way.
HDML contrasts with standard temporal/modal logics in the fact that HDML can reason about what holds "during" some concurrent events are executing. The close related logic for distributed transition systems of [12] is in the same style of reasoning only about what holds "after" some concurrent events have finished executing. As we show in the examples section, the "after" logics can be encoded in HDML, hence also the logic of [12].
The other purpose of this work is to provide a general framework for reasoning about concurrent systems at any level of abstraction and granularity, accounting also for choices and independence of actions. Thus, the purpose of the examples in Section 3 is to show that studying HDML, and particular variants of it, is fruitful for analyzing concurrent systems and their logics. In this respect we study variants of higher dimensional modal logic inspired by temporal logic and dynamic logic. Already in Section 3.2 we add to the basic language two kinds of Until operator, in the style of linear and branching time temporal logics. We show how this variant of HDML, when interpreted over the class of HDAs corresponding to Kripke structures, can be particularized just by syntactic restrictions to CTL [13]. A second variant, in Section 3.3, decorates the HDML modalities with labels. This multi-modal variant of HDML together with the LTL-like Until operator, when interpreted over the class of HDAs that encodes Mazurkiewicz traces, becomes LTrL [9] (the linear time temporal logic over Mazurkiewicz traces).

Modal Logic over Higher Dimensional Automata
In this section we define a higher dimensional automaton (HDA) following the definition and terminology of [3,6]. Afterwards we propose higher dimensional modal logic (HDML) for reasoning about concurrent systems modeled as HDAs. The semantic interpretation of the language is defined in terms of HDAs (i.e., the HDAs, with a valuation function attached, are the models we propose for HDML).
For an intuitive understanding of the HDA model consider the standard example [6,3] pictured in Figure 1. It represents a HDA that models two concurrent events which are labeled by a and b (one might have the same label a for both events). The HDA has four states, q 1 0 to q 4 0 , and four transitions between them. This would be the standard picture for interleaving, but in the case of HDA there is also a square q 2 . Traversing through the interior of the square means that both events are executing. When traversing on the lower transition means that event one is executing but event two has not started yet, whereas, when traversing through the upper transition it means that event one is executing and event two has finished already. In the states there is no event executing, in particular, in state q 3 0 both events have finished, whereas in state q 1 0 no event has started yet. In the same manner, HDAs allow to represent three concurrent events through a cube, or more events through hypercubes. Causality of events is modeled by sticking such hypercubes one after the other. For our example, if we omit the interior of the square (i.e., the grey q 2 is removed) we are left with a description of a system where there is the choice between two sequences of two events, i.e., a; b + b; a. Definition 2.1 (higher dimensional automata). A cubical set H = (Q, s,t) is formed of a family of sets Q = ∞ n=0 Q n with all sets Q n disjoint, and for each n, a family of maps s i ,t i : Q n → Q n−1 with 1 ≤ i ≤ n which respect the following cubical laws: α i • β j = β j−1 • α i , 1 ≤ i < j ≤ n and α, β ∈ {s,t}.
In H, the s and t denote the collection of all the maps from all the families (i.e., for all n). A higher dimensional structure (Q, s,t, l) over an alphabet Σ is a cubical set together with a labeling function l : Q 1 → Σ which respects l(s i (q)) = l(t i (q)) for all q ∈ Q 2 and i ∈ {1, 2}. 1 A higher dimensional automaton (Q, s,t, l, I, F) is a higher dimensional structure with two designated sets of initial and final cells I ⊆ Q 0 and F ⊆ Q 0 .
We call the elements of Q 0 , Q 1 , Q 2 , Q 3 respectively states, transitions, squares, and cubes, whereas the general elements of Q n are called n-dimensional cubes (or hypercubes). We call generically an element of Q a cell (also known as n-cell). For a transition q ∈ Q 1 the s 1 (q) and t 1 (q) represent respectively its source and its target cells (which are states from Q 0 in this case). Similarly for a general cell q ∈ Q n there are n source cells and n target cells all of dimension n − 1. Intuitively, an n-dimensional cell q represents a snapshot of a concurrent system in which n events are performed at the same time, i.e., concurrently. A source cell s i (q) represents the snapshot of the system before the starting of the i th event, whereas the target cell t i (q) represents the snapshot of the system immediately after the termination of the i th event. A transition of Q 1 represents a snapshot of the system in which a single event is performed.
The cubical laws account for the geometry (concurrency) of the HDAs; there are four kinds of cubical laws depending on the instantiation of α and β . For the example of Figure 1 consider the cubical law where α is instantiated to t and β to s, and i = 1 and j = 2: t 1 (s 2 (q 2 )) = s 1 (t 1 (q 2 )). In the left hand side, the second source cell of q 2 is, in this case, the transition s 2 (q 2 ) = q 1 1 = (q 1 0 , q 2 0 ) and the first target cell of q 1 1 is q 2 0 (the only target cell because s 2 (q 2 ) ∈ Q 1 ); this must be the same cell when taking the right hand side of the cubical law, i.e., the first target cell is t 1 (q 2 ) = q 2 1 = (q 2 0 , q 3 0 ) and the first source of q 2 1 is q 2 0 . We propose the language of higher dimensional modal logic for talking about concurrent systems. HDML follows the tradition and style of standard modal languages [14].

Decidability of HDML
The filtration for the states is the same as in the standard modal logic, but for cells of dimension 1 or higher we need to take care that the maps t and s in the filtration model remain maps and that they respect the cubical laws so that the filtration is still a HDML model. This can be done, but the filtration model is bigger than what is obtained in the case of standard modal logic. On top, the proof of the small model property (Theorem 2.13) is more involved due to the complexities of the definition of filtration given in Definition 2.6. Definition 2.4 (subformula closure). The subformula closure of a formula ϕ is the set of formulas C (ϕ) defined recursively as: The size of a formula (denoted |ϕ|) is calculated by summing the number of Boolean and modal symbols with the number of atomic propositions and ⊥ symbols that appear in the formula. (All instances of a symbol are counted.) Proposition 2.5 (size of the closure). The size of the subformula closure of a formula ϕ is linear in the size of the formula; i.e., |C (ϕ)| ≤ |ϕ|.
Proof. The proof is easy, using structural induction and observing that for the atomic formulas the size of the closure is exactly 1, the size of the formula. For a compound formula like {}ϕ the induction hypothesis says that |C (ϕ)| ≤ |ϕ| which means 1 + |C (ϕ)| ≤ 1 + |ϕ|. Definition 2.6 (filtration). Given a formula ϕ, we define below a relation ≡ (which is easily proven to be an equivalence relation) over the cells of a higher dimensional structure H , where q, q ′ ∈ Q i , for some i ∈ N: Lemma 2.7. Any two sets [p], [q] ∈ Q f n , for some n ∈ N, are disjoint.
Proof. By induction on n. The base case for n = 0 is easy as the definition of Q f 0 results in the equivalence classes on Q 0 generated by the equivalence relation ≡, which are disjoint.
Inductive step: Consider [p], [q] ∈ Q f n , for which we assume that ∃r ∈ Q n with r ∈ [p] and r ∈ [q]. From the definition we get (1) q ≡ r ≡ p and, (2) ). (Note that t f i on the left side is different than the t f i on the right side, as the left one is applied to elements of Q f n−1 whereas the right one is applied to elements of Q f n .) The other three kinds of cubical laws are treated analogous only that one needs to reason with the s i maps too.
Assume, wlog. because the opposite assumption would follow analogous reasoning, that t f . From the definition we have both: Therefore, from the two we have that , because by the Definition 2.6 (of the t i maps) it means that ∀p ∈ [q ′ n−1 ] it holds that t j−1 (p) ∈ [q n−2 ], i.e., our desired result.
From the assumption we have that ∀q ∈ [q] : t i (q) ∈ [q ′ n−1 ]. Pick one of these t i (q) and claim this to be the p ∈ [q ′ n−1 ] we are looking for. From the cubical laws for the initial H model we know that for any q ∈ [q], t i (t j (q)) = t j−1 (t i (q)) = t j−1 (p). Because of (3) we have that t j−1 (p) ∈ [q n−2 ], and thus our claim is proven; i.e, t j−1 applied to the element t i (q) that we picked from [q ′ n−1 ], is in [q n−2 ]. Corollary 2.9 (filtration is a model).
The filtration H f of a model H through a closure set C (ϕ) is a higher dimensional structure (i.e., is still a HDML model).
Proof. Essentially, the proof amounts to showing that the definitions of s f i and t f i are that of maps and that they respect the cubical laws which were done in Lemma 2.8.

Lemma 2.10 (sizes of filtration sets).
Each set Q f n of the filtration H f obtained in Definition 2.6 has finite size which depends on the size of the formula ϕ used in the filtration; more precisely each Q f n is bounded from above by Proof. The case for 0 is simple as the number of equivalence classes of Q 0 can be maximum the number of subsets of the subformula closure C (ϕ) which is 2 |ϕ| .
The case for n = 1 is based on the size of Q f 0 . Each of the 2 |ϕ| equivalence classes in which Q f 1 can be divided may have infinitely many cells. Any such equivalence class can still be broken into smaller subsets depending on the maps t 1 and s 1 . Because t 1 can have outcome in any of the [q 0 ] ∈ Q f 0 , we get a first split into 2 |ϕ| subdivisions. For each of these we can still split it into 2 |ϕ| more subdivisions because of s 1 . We thus get a maximum of 2 |ϕ| · (2 |ϕ| ) 2·1 for Q f 1 . For the general case of n we need to consider all maps t i , s i , that means 2 · n maps. For each of these maps we split the 2 |ϕ| possible initial equivalence classes according to the size of O f n−1 . Thus we get a maximum of 2 |ϕ| · (|Q f n−1 |) 2·n subdivisions. Calculating this series gives the bound on the size of Q f n as being 2 |ϕ|·N where As a side remark, the size of O f n is more than double exponential in the dimension n, but is less than triple exponential. More precisely, for N, the sum is bounded from above by (n + 1) · 2 n which makes N the order of n! · (n + 1) · 2 n . We know that n! grows faster than exponential, but not too fast; more precisely, using Stirling's approximation of n! we have that lg(n!) = Θ(n · lg(n)) making n! · (n + 1) · 2 n = (n + 1) · 2 n+lg(n!) of order (n + 1) · 2 Θ(n·(lg(n)+1)) . Therefore, |O f n | is bounded by 2 |ϕ|·(n+1)·2 Θ(n·(lg(n)+1)) (where we consider |ϕ| to be a constant, and hence, not contributing to the bound). 2

Lemma 2.11 (filtration lemma)
. Let H f be the filtration of H through the closure set C (ϕ), as in Definition 2.6. For any formula ψ ∈ C (ϕ) and any cell q ∈ H , we have H , q |= ψ iff H f , [q] |= ψ.
Proof. By induction on the structure of the formula ψ.
Base case:

Inductive step:
The case for → is straightforward making use of the induction hypothesis because the set C (ϕ) is closed under subformulas.
Take now ψ = ψ ′ and we prove that Considering the only if implication we assume that (cf. definition of satisfiability from Table 1 When we take ψ = {}ψ ′ we use analogous arguments as in the proof of ψ ′ . In this case we work with the definition of s f i and we look for cells of higher dimension (instead of lower dimension).
We define two degrees of concurrency of a formula ϕ: the upwards concurrency (denoted |ϕ| uc ) and downwards concurrency (denoted |ϕ| dc ). The degree of upwards concurrency counts the maximum number of nestings of the during modality {} that are not compensated by a modality. (E.g., the formula {}{}φ ∨ {}φ ′ has the degree of upwards concurrency equal to 2, the same as {} {}{}φ .) The formal definition of | | uc is: The definition of the degree of downwards concurrency | | dc is symmetric to the one above in the two modalities; i.e., interchange the modalities in the last two lines. Note that |ϕ| uc + |ϕ| dc ≤ |ϕ|. The next result offers a safe reduction of a model where we remove all cells which have dimension greater than some constant depending on the formula of interest. Lemma 2.12 (concurrency boundedness). If a HDML formula ϕ is satisfiable, H , q |= ϕ with q ∈ Q k , then it exists a model with all the sets Q m , with m > |ϕ| uc + k, empty, which satisfies the formula.
Proof. By induction on the structure of the formula ϕ.
Base case: For φ ∈ Φ B and ⊥ the evaluation is in the same cell q and thus all the cells of dimension higher than k are not important and can be empty.
Inductive step: For ϕ 1 → ϕ 2 the semantics says that whenever H , q |= ϕ 1 then H , q |= ϕ 2 . From the induction hypothesis we have that all cells of dimension greater than k + |ϕ 1 | uc (respectively k + |ϕ 2 | uc ) are not important for checking ϕ 1 (respectively ϕ 2 ). Thus it is a safe approximation to consider all the cells of at most dimension max(k + |ϕ 1 | uc , k + |ϕ 2 | uc ) = k + |ϕ 1 → ϕ 2 | uc and all sets Q m of greater dimension can be empty.
For {}ϕ the semantics says that we need to check the formula ϕ in cells of dimension one greater, i.e., q k+1 |= ϕ. From the induction hypothesis we know that for checking q k+1 |= ϕ it is enough to have only cells of most dimension k + 1 + |ϕ| uc = k + |{}ϕ| uc (where all other cells can be removed).
For ϕ the semantics says that we need to check q k−1 |= ϕ, that is, in cells of immediately lower dimension. For this, the induction hypothesis says that we need to consider cells of dimension at most k − 1 + |ϕ| uc which is the same as k + (|ϕ| uc − 1). When |ϕ| uc = 0 then k is a safe approximation and from the definition of the | | uc it is the same as k + | ϕ| uc . Otherwise, when |ϕ| uc > 0, the definition of | | uc tells us that k + (|ϕ| uc − 1) is exactly k + | ϕ| uc .

Notation:
The formula φ ∧ ¬φ expresses that there can be terminated at least two different events (in other words, the cell in which the formula is evaluated to true has dimension at least two). Similarly the formula (φ ∧ ¬φ ′ ) ∧ (¬φ ∧ ¬φ ′ ) ∧ (¬φ ∧ φ ′ ) says that there are at least three events that can be terminated. For each i ∈ N * one can write such a formula to say that there are at least i events that can be terminated. Denote such a formula by i. Also define i ϕ as i applications of the modality to ϕ (i.e., . . . ϕ where appears i times). Similar, for the during modality denote {}i the formula that can start i different events, and by {} i ϕ the i applications of {} to ϕ. Proof. Assume that there exists a model H and a cell q l ∈ Q l in this model for which H , q l |= ϕ. We can prove that there exists a (maybe different) model H ′ and a cell q ′ l that satisfy ϕ but which l < |ϕ| − |ϕ| uc . We do this by induction on the structure of ϕ.
Base case: when ϕ = φ ∈ Φ B . The semantics needs to look only at the valuations, and by the assumption, the valuation of q l in H satisfies ϕ. Hence we can just use one cell model where we attach this satisfying valuation to it. Therefore level Q 0 is enough; hence l = 0 < |φ | − |φ | uc = 1 − 0.
When ϕ = {}ϕ 1 the semantics says that exists q l+1 ∈ Q l+1 where ϕ 1 holds. The inductive hypothesis says that l + 1 < |ϕ 1 | − |ϕ 1 | uc . This means that l < |ϕ 1 When ϕ = ϕ 1 the semantics says that exists q n−1 ∈ Q l−1 where ϕ 1 holds. From the inductive hypothesis we have l −1 < |ϕ 1 |−|ϕ 1 | uc . This means that l < |ϕ 1 |+1−|ϕ 1 From the above we can safely assume l = |ϕ| − |ϕ| uc . From Lemma 2.12 we know that we need to consider only the sets Q n for n ≤ l + |ϕ| uc = |ϕ|, and all other sets of Q are empty. From Lemma 2.11 we know that we can build a filtration model H f s.t. the formula ϕ is still satisfiable and, by Lemma 2.10, we know that all the sets Q f n have a finite number of cells. Thus we are safe if we sum up all the cells in all the Q f n , with n ≤ |ϕ|.
Corollary 2.14 (decidability). Deciding the satisfiability of a HDML formula ϕ is done in space at most ∑ |ϕ| n=0 2 |ϕ|·N where N is defined in Theorem 2.13.

Axiomatic system for HDML
In the following we give an axiomatic system for HDML and prove it to be sound. This system corrects the one in [1]. In Table 2 we give a set of axioms and rules of inference for HDML. If a formula is derivable in this axiomatic system we write ⊢ ϕ. We say that a formula ϕ is derivable from a set of formulas S iff ⊢ ψ 1 ∧ · · · ∧ ψ n → ϕ for some ψ 1 , . . . , ψ n ∈ S (we write equivalently S ⊢ ϕ). A set of formulas S is said to be consistent if S ⊢⊥, otherwise it is said to be inconsistent. A consistent set S is called maximal iff all sets S ′ , with S ⊂ S ′ , are inconsistent. Proposition 2.15 (theorems). The following are derivable in the axiomatic system of Table 2: Axiom schemes: (A1) All instances of propositional tautologies.
Inference rules: Moreover, one can use the following derived rules: Proof. The first two theorems are derivable as in standard modal logic only using the standard axioms (A2)-(A3'). The derived rules are also as in standard modal logic. The theorem (3) is a consequence of (A6): 2 The theorem (4) uses axiom (A6). The theorem (6) is a consequence of (A7): from propositional reasoning we have ⊤ → (7) is derivable in an analogous way as the one above only that we use axiom (A7'). The theorem (8) is just the instantiation of axiom (A9) when i = 0 (i.e., 0 ⊤ △ = ⊤). The theorem (9) is a consequence of (A7'): The theorem (10) is a consequence of the theorem (9) by contraposition. The theorem (11) is derivable from theorem (8). The theorem (12) is derivable from theorem (11). The theorem (13) is derivable from theorem (11) after using axiom (A5) and axiom (A9') instantiate to i = 1: (14) follows either from axiom (A10) by the D' rule or from axiom (A10') by the D rule. Theorem (16) is an instantiation of axiom (A10). Theorem (15) needs twice the application of axiom (A10) and the D rule. We need here the application of the axiom two times because we move the modality two times over {}, whereas for the other theorems we move the modality only once. The theorems (17) and (18) are just the contrapositives of axioms (A10) respectively (A10').

Exercise 2.1.
A challenge is to prove the validity of: Before proving soundness we should have some intuition about the non-standard axioms (A5) to (A10'). First consider the axioms (A6) to (A7') which relate to the cubical laws.
• Axiom (A6) embodies the cubical law t i (t j (q)) = t j−1 (t i (q)) (i.e., the cubical law where α is instantiated to t and β to t). This axiom is to be checked only for cell of dimension 2 or higher (i.e., 2 ⊤ holds).
• The two axioms (A7) and (A7') relate to the cubical laws where α and β are instantiated differently, one to s and the other to t; e.g., s i (t j (q)) = t j−1 (s i (q)). We included both axioms (A7) and (A7') for symmetry reasons, but it is clear that one can be obtained from the other by contraposition.
The other axioms talk about the dimensions of the cells and about the division of the cells into layers Q n .
• Axiom (A5) i → i ⊤ says that if in a cell there can be terminated at least i different events then this means that this cell has dimension at least i (i.e., one can go i levels down by i ⊤). This is natural because the dimension of a cell is given by the number of events that are currently executing concurrently.
i ⊤ has two purposes. In the basic variant (for i = 0 it becomes [ {}] ⊤) it says that in any cell, however one starts an event then one can also terminate an event. In the general form the axiom says that from some level i when going one level up (by starting an event) and then one level down (by terminating an event) we always end up on the same level i; i.e., we end in a cell of the same dimension like the cell that it started in. Axiom (A9') intuitively finds out the level of the current cell. If one can start and then can terminate an event in a cell of at least dimension i then the current cell also has dimension at least i.
• Axiom (A8) intuitively says that if from a cell we can start an event and reach a cell of some concurrency complexity (given by the i ⊤) then any way of starting an event from this cell ends up in cells of the same complexity. Though similar in nature, axiom (A8') can be seen intuitively as saying that if one t map of the current cell ends up in a cell of dimension at least i then all the t maps end up in the same dimension. These two axioms relate with the part of the definition of the HDA where all the s i and t i maps for some n are defined on the same domain and codomain.
• Axioms (A10) and (A10') are somehow related to the notion of homotopy (see eg. [3, ch.7.4]) or to the ways one can walk (i.e., the paths on a HDA, to be defined later) on the HDAs using the HDML modalities (or in other terms, these axioms are related to the histories of an event). One may reach a cell from another cell in a HDA in different ways and the notion of homotopy says that all these ways are considered equivalent. Take the example of the square (cell of dimension 2) from Figure 1 where the state in the upper-right corner can be reached from the cell in the lower-left corner in more than one way. In this setting axioms (A10) and (A10') basically say that instead of going through the inside of a square one can go on one of it sides. In other words, instead of going through a cell of higher dimension one can go only through cells of lowed dimensions. Particular to our example from Figure 1 the axiom (A10) says that when going from the lower-left corner through the inside of the square one can instead go through one of the lower or left sides and reach the same place. The other axiom (A10') says that for reaching the upper-right corner, instead of going through its inside one can just take one of its upper or right sides. Note also the theorems (14)-(16) which involve four HDML modalities stacked one on top of the other. These are theorems of the two axioms (A10) and (A10') which involve only three modalities. In particular note the converse implication of (14) which is not a theorem. This says intuitively that one cannot infer from just being able to walk on the edges of a square that the square is filled in, i.e., that true concurrency is present. This makes HDML powerful enough for the distinction between true concurrency and interleaving.
Remark that a natural counterpart (using the {} modality in place of ) of the axiom (A6) is {}ϕ (which appeared in the short paper version [1]). But this "axiom" is broken by the fact that HDAs allow choices. This formula would be valid only when working inside a single full cube (i.e., no choices, just concurrency), as would be the case when representing Mazurkiewicz traces as HDAs. Theorem 2.16 (soundness). The axiomatic system of Table 2 is sound; i.e., ∀ϕ : ⊢ ϕ ⇒ |= ϕ.
Proof. For soundness of the axiomatic system it is enough to prove that the axioms (A5) to (A10') are valid.
We start with axiom (A6) and assume H , q n |= [ ]ϕ for some q n ∈ Q n and n ≥ 2 because of the assumption 2 ⊤. This means that exists some q n−1 ∈ Q n−1 s.t. t k (q n ) = q n−1 for some 1 ≤ k ≤ n with H , q n−1 |= [ ]ϕ, and from this it means that for any 1 ≤ l ≤ n − 1, H ,t l (q n−1 ) |= ϕ. We need to show that H , q n |= [ ] ϕ. This means that for any m = k we have to find a 1 ≤ m ′ ≤ n − 1 s.t. H ,t m ′ (t m (q n )) |= ϕ. 3 This is easy by applying the cubical law, considering wlog. m < k, t m (t k (q n )) = t k−1 (t m (q n )). 4 Thus, the m ′ = k − 1 for which trivially 1 ≤ k − 1 ≤ n − 1. From the assumption we showed that we have H ,t m (t k (q n )) |= ϕ and hence H ,t k−1 (t m (q n )) |= ϕ.
For axiom (A7) assume H , q n |= {}[ ]ϕ with q n ∈ Q n . This means that exists q n+1 ∈ Q n+1 and 1 ≤ k ≤ n + 1 s.t. s k (q n+1 ) = q n and H , q n+1 |= [ ]ϕ. Further, this implies that for any 1 ≤ i ≤ n + 1, H ,t i (q n+1 ) |= ϕ. We want to prove that H , q n |= [ ]{}ϕ, which amounts to showing that for some arbitrary 1 ≤ m ≤ n with t m (q n ) = q n−1 we can find an 1 ≤ l ≤ n and q ′ n ∈ Q n s.t. s l (q ′ n ) = q n−1 and H , q ′ n |= ϕ. We assume that it exists at least one t m to work with, for otherwise the formula [ ]{}ϕ holds trivially. We achieve the goal using the cubical laws: if m < k then consider the cubical law t m (s k (q n+1 )) = s k−1 (t m (q n+1 )) and set l = k − 1 and q ′ n = t m (q n+1 ) for which we know from above that H ,t m (q n+1 ) |= ϕ; otherwise if k ≤ m (which also means that k ≤ n) then consider the cubical law s k (t m+1 (q n+1 )) = t m (s k (q n+1 )) and set l = k and q ′ n = t m+1 (q n+1 ) (where m + 1 ≤ n + 1) for which we know that H ,t m+1 (q n+1 ) |= ϕ.
For (A7') we can just use propositional reasoning and argue its validity by contraposition with axiom (A7) above. Nevertheless, we want to also give here a model theoretic argument similar to the above. Thus, assume H , q n |= [ {}]ϕ with q n ∈ Q n . This means that exists 1 ≤ k ≤ n and q n−1 s.t. t k (q n ) = q n−1 and H , q n−1 |= [ {}]ϕ, which means that for any q ′ n with s i (q ′ n ) = q n−1 for some 1 ≤ i ≤ n we have H , q ′ n |= ϕ. We want to prove that H , q n |= [ {}] ϕ which amounts to showing that for some arbitrary q n+1 , with s m (q n+1 ) = q n for some 1 ≤ m ≤ n+1, we can find an 1 ≤ l ≤ n + 1 and a q ′′ n s.t. t l (q n+1 ) = q ′′ n and H , q ′′ n |= ϕ. We use the cubical laws: if k < m then consider the cubical law t k (s m (q n+1 )) = s m−1 (t k (q n+1 )) and set l = k and q ′′ n = t k (q n+1 ) for which we have said before that H ,t l (q n+1 ) |= ϕ because there is the s m−1 that reaches a cell which satisfies [ {}]ϕ; otherwise if m ≤ k then consider the cubical law s m (t k+1 (q n+1 )) = t k (s m (q n+1 )) and set l = k + 1 and q ′′ For axiom (A9) assume H , q n |= i ⊤ which means that n ≥ i. Even more, i ⊤ holds in any cell q n ∈ Q n of dimension n. We need to prove that H , q n |= [ {}] i ⊤. The proof is trivial when there is no q n+1 with s j (q n+1 ) = q n . Therefore, we need to prove that for any q n+1 with s j (q n+1 ) = q n , for some 1 ≤ j ≤ n + 1, H , q n+1 |= i ⊤. Because q n+1 ∈ Q n+1 then it must have at least one t map that links it with some cell q ′ n ∈ Q n on the lower level. In q ′ n the formula i ⊤ holds and thus we finished the proof.
This means that n + 1 ≥ i + 1 and thus n ≥ i. Therefore, for any q ′ n ∈ Q n the formula i ⊤ holds because we can go at least i levels down and find any cell satisfying ⊤, hence i ⊤ holds also in q n ∈ Q n . Axiom (A8) can actually be derived from axioms (A9) and (A9') as follows: whereas for i = 1 it is just an instantiation of axiom (A9) for i = 0. As we did for axiom (A7') we leave these so that the reader has a more intuitive understanding of the apparent symmetries of these formulas.
Nevertheless, we give also a model-theoretic argument, hence assume H , q n |= {} i ⊤. This means that exists q n+1 and 1 ≤ j ≤ n + 1 s.t. s j (q n+1 ) = q n and H , q n+1 |= i ⊤. This means that the dimension of q n+1 is greater than i, i.e., n + 1 ≥ i. We want to prove that H , q n |= [ {}] i ⊤ which amounts to showing that for any q ′ n+1 ∈ Q n+1 with s j (q ′ n+1 ) = q n for some 1 ≤ j ≤ n + 1 we have H , q ′ n+1 |= i ⊤. But we know from before that the dimension of q ′ n+1 is at least i; this means that we can go down at least i levels and on the lowest level any cell models ⊤. Hence we have H , q ′ n+1 |= i ⊤. For axiom (A8') we use a similar argument as in the proof based on the semantics of and [ ] this time. For (A5) consider that H , q |= i which means that there exist i different cells q j with 1 ≤ j ≤ i which are the result of the application of a t map to q. Because t is a map it means that there exist at least i different maps t j with 1 ≤ j ≤ i that are applied to q. Therefore, q is of dimension at least i which means that we can go i levels down (by using an inductive argument). This makes the formula i ⊤ true at q.
Case when j > i then choose m = j −1, n = i, k = l, and q a n+1 = q n+1 hence finding the cubical law s n (t j (q n+2 )) = t m (s i (q n+2 )) which makes t j (q n+2 ) = q c n+1 and hence, the desired H , q c n+1 |= ϕ follows as before.
Case when i = j then it is not enough to work only with the i and j as the cubical laws do not apply any more. But there are ways depending on k. We need two cases. When k < j consider l = j − 1, m = j − 1, n = k, and q a n+1 = s k (q n+2 ) as coming from the cubical law s k (s j (q n+2 )) = s l (s k (q n+2 )). Using a second cubical law s k (t j (q n+2 )) = t m (s k (q n+2 )) = q b n we obtain q c n+1 = q ′ n+1 and hence the desired H , q c n+1 |= ϕ. Otherwise, when k ≥ j then choose l = j, m = j, n = k and q a n+1 = s k+1 (q n+2 ) as coming from the cubical law s l (s k+1 (q n+2 )) = s k (s j (q n+2 )). Using as second cubical law t m (s k+1 (q n+2 )) = s k (t j (q n+2 )) = q b n we obtain q c n+1 = q ′ n+1 and hence the desired result as before.
For (A10') assume H , q n |= {} ϕ which by the definition of the semantics it means that ∃q n+1 ∈ Q n+1 , i ≤ n+ 1 : s i (q n+1 ) = q n and ∃q ′ n ∈ Q n , j ≤ n : t j (q n+1 ) = q ′ n and ∃q n−1 ∈ Q n−1 , k ≤ n− 1 : t k (q ′ n ) = q n−1 and H , q n−1 |= ϕ. We want to prove that H , q n |= {} ϕ. This amounts to finding three cells q a n−1 ∈ Q n−1 , q b n ∈ Q n , and q c n−1 ∈ Q n−1 s.t. t m (q n ) = q a n−1 , s n (q b n ) = q a n−1 , and t l (q b n ) = q c n−1 , and H , q c n−1 |= ϕ. We again treat three cases depending on i and j.
Case when i < j then choose m = j −1, n = i, l = k, and q b n = q ′ n and get q a n−1 from the cubical law s n (t j (q n+1 )) = t m (s i (q n+1 )) = q a n−1 . Since q c n−1 = t l (q b n ) = t k (q ′ n ) = q n−1 we get our desired result H , q c n−1 |= ϕ. Case when i > j then choose m = j, n = i−1, l = k, and q b n = q ′ n and get q a n−1 from the cubical law t m (s i (q n+1 )) = s n (t j (q n+1 )) = q a n−1 . We get our desired result H , q c n−1 |= ϕ as before. Case when i = j requires two subcases after k as the cubical laws are not applicable to i and j anymore. We follow a similar reasoning as we did for (A10). When k < j then choose l = j − 1 and have q b n = t k (q n+1 ) and q c n−1 = q n−1 from the cubical law q n−1 = t k (t j (q n+1 )) = t l (t k (q n+1 )). To connect everything consider the cubical law t m (s i (q n+1 )) = s n (t k (q n+1 )) giving m = k and n = j − 1. When k ≥ j then choose l = j and have q b And all is connected right through the cubical law s n (t k+1 (q n+1 )) = t m (s j (q n+1 )) giving m = k and n = j. Table 1 does not have the compactness property.

Theorem 2.17 (compactness failure). The HDML with the semantics of
Proof. Compactness says that for any infinite set of formulas Γ if all the finite subsets S ⊂ Γ are satisfiable than the original Γ is satisfiable.
The compactness failure for HDML is witnessed by the following infinite set of formulas: Any finite subset S = { i ⊤ | i ≤ n} of Γ is satisfiable on a model H n which has Q n = / 0 in any cell q n ∈ Q n of dimension n; i.e., H n , q n |= i ⊤ for all i ⊤ ∈ S.
On the other hand the infinite Γ is not satisfiable on any pointed model, i.e., at a single point. For assume there exists a model H and some cell q ∈ Q m for some level m where all formulas φ ∈ Γ are satisfiable H , q |= φ . But this is not possible as the formula m+1 ⊤ does not hold on any cell from level Q m or any level below. This is because when stripping off one we go one level down cf. the semantics; and we cannot go down more than m levels, cf. q ∈ Q m but we need to strip m + 1 times the after operator . No matter on which level we choose the point cell q in a model there will always be a formula in Γ that will not hold, because of the infiniteness of Γ (also regardless of the infiniteness of the model that we choose).
Intuitively, the compactness failure is due to the fact that the models of HDML are bounded below in their levels and HDML has a modality that goes down the levels (i.e., the after modality ).

Examples of Encodings into Higher Dimensional Modal Logic
This section serves to exemplify ways of using HDML. One may encode other logics for different concurrency models as restrictions of HDML; in this respect we study the relation of HDML with standard modal logic, with CTL, ISTL (a branching time temporal logic over configuration structures), and with linear time temporal logic over Mazurkiewicz traces LTrL. Another way of using HDML is as a general logical framework for studying properties of concurrency models and their interrelation. This is done by finding the appropriate restrictions of HDA and HDML and investigating their relations and axiomatic presentations. Proof. Essentially this result is found in [3]. A HDA K = (Q 0 , Q 1 , s 1 ,t 1 , l) is a special case of HDAs where all Q n = / 0 for n > 1. This is the class of HDAs that encode Kripke frames. Because Q 2 (and all other cells of higher dimension) is empty there are no cubical laws applicable. Therefore, there is no geometric structure on K. Moreover, the restriction on the labeling function l is not applicable (as Q 2 is empty). Add to such a HDA a valuation function V to obtain a Kripke model

Proposition 3.2 (axiomatization of Kripke HDAs). The class of higher dimensional structures corresponding to Kripke structures (from Lemma 3.1) is axiomatized by:
Proof. For any HDA H and any q ∈ Q a cell of any dimension, we prove the double implication: For the if direction if q ∈ Q 1 then the axiom holds trivially because there are no cells on For the only if direction consider a H for which the axiom holds (i.e., for any cell ; we need to show that any Q n with n > 1 is empty. Assume the opposite, that there exists q n ∈ Q n with n > 1. This means that there is a sequence s 1 (. . . s i (q n )) = q 0 of source maps that ends in a cell q 0 ∈ Q 0 of dimension 0. But [ {}]⊥, which means that there cannot be this sequence of source maps unless q n is of dimension at most 1. This is a contradiction and hence the proof is finished. Proof. First we check that we capture exactly the semantics of standard modal logic; This is the same as ∃q ′ 0 ∈ Q 0 reached in "one transition" from q 0 and H , q ′ 0 |= ϕ. (We go only through one transition cell q ′ ∈ Q 1 .) Clearly, with the axiom of Proposition 3.2, H , q n |= ✸ϕ for any q n ∈ Q n for any n ≥ 1. Therefore, ✸ϕ makes sense only interpreted in states from Q 0 .
Second we check that the axioms of standard modal logic for ✸ hold in our axiomatic system. Clearly ✸⊥ ↔ ⊥; just apply (A2') and then (A2) to {} ⊥. It is easy to see that ✷ϕ ↔ ¬✸¬ϕ as ¬{} ¬ϕ [ ]ϕ and the semantic of ✷ϕ is the right one, i.e., for any q ′ 0 ∈ Q 0 , reached through some transition q ′ ∈ Q 1 , It is easy to see how we recover the corresponding inference rule for ✸. We thus have all the axiomatic system of standard modal logic and the proof is finished.
Remark that the axioms (A5)-(A10') particular to HDML are trivially satisfied for all states or transitions (i.e., cells of dimension 0 or 1). This means that for these cells these axioms do not impose any constraints. One can easily check that for each of the axioms (A5)-(A10'), which are implications, either the first formula does not hold or the second formula holds trivially. In fact, in the axiomatic system of Table 2 with the new axiom (19) added, one cannot prove formulas where the same existential modality is stacked twice or more (like {}{} . . . or . . . ). In fact, any such formula is provable unsatisfiable. This is also a reason for using the syntactic definition for the diamond from Theorem 3.3.

Adding an Until operator and encoding standard temporal logic
The basic temporal logic is the logic with only the eventually operator (and the dual always). This language is expressible in the standard modal logic [14]. It is known that the Until operator adds expressiveness (eventually and always operators can be encoded with Until but not the other way around).
The Until operator cannot be encoded in HDML because of the local behavior of the during and after modalities; similar arguments as in modal logic about expressing Until apply to HDML too. The Until modality talks about the whole model (about all the configurations of the system) in an existential manner. More precisely, the Until says that there must exist some configuration in the model, reachable from the configuration where Until is evaluated, satisfying some property ϕ, and in all the configurations on all/some of the paths reaching the ϕ configuration some other property ψ must hold. Hence we need a notion of path in a HDA.

Definition 3.4 (paths in HDAs). A simple step in a HDA is either q
We say that q ∈ π iff q = q j appears in one of the steps in π. The first cell in a path is denoted st(π) and the ending cell in a finite path is en(π). We call a cell q ′ reachable from some other cell q, and denote by q → * q ′ , iff ∃π : st(π) = q ∧ en(π) = q ′ . Overload the notation π → * π ′ to mean that the path π ′ extends π, with the usual definition.
There are two main kinds of Until operator that can be defined on a branching structure like HDA: one is in the style of linear time temporal logic [16]; and the other in the style of computation tree logic (CTL). These two kinds are found defined also over Mazurkiewicz traces or configuration structures. There are proofs that the CTL style of defining the Until yields undecidability both on traces [17] and on configuration structures [18,10] and all these three proofs use different techniques, i.e., encoding a different undecidable problem. On the other hand the LTL style of definition of Until over traces is decidable as part of LTrL [9]; see also the related decidable definition part of the TrPTL logic [7].
In the same spirit as done for temporal logic we boost the expressiveness of HDML by defining an Until operator over higher dimensional structures. We define both styles of Until operators. We then show how the standard LTL logic (with its until operator interpreted over Kripke structures) is encoded into the HDML framework. For the CTL-like definition we discuss if and how the details of the undecidability proofs over Mazurkiewicz traces can be done in the setting of HDML. Note that the proofs in [17,10] lack many of the details. We concentrate on the proof using the Post correspondence problem from [10]. Definition 3.5 (CTL-like Until operator). Define an Until operator ϕ U c ϕ ′ , in the style of CTL, which is interpreted over a HDA in a cell as below: Definition 3.6 (LTL-like Until operator). Define an Until operator ϕ U l ϕ ′ , in the style of LTL, which is interpreted over a HDA in a cell as below: The Definition 3.6 of U l is in the style of LTL in the sense that it looks only at one (concurrent) execution of the system ignoring choices (in the sense of HDA). The Definition 3.5 of U c is more refined because it looks at a single linearization of a concurrent execution; and it is branching in the sense that it is not confined to one single concurrent execution, but the linearization may cross boundaries of concurrent runs, i.e., taking choices.

Proposition 3.7 (modeling CTL Until). The CTL Until modality is encoded syntactically by
Proof. Essential for the proof is the fact that ∃U is interpreted over restricted HDAs which model Kripke structures. Precisely, they have only cells of dimension 0 (the states) and 1 (the transitions), and moreover, we know which are states because the formula ¬ ⊤ holds in all and only the cells of dimension 0. Therefore, the right formula of the ∃U is evaluated only in states because (ϕ ′ ∧ ¬ ⊤) can never hold in a cell of dimension greater than 0. Moreover, the transitions are not important for valuating the ϕ because the formula ⊤ is always true in a transition (because any transition has a target state). On the other hand the formula ⊤ is never true in a state and hence the ϕ has to be true so that the whole left part of the until to hold.
For this proof we only concentrate on showing that the semantics of the ∃U corresponds to the well known CTL semantics. Thus, we want to show that H , q 0 |= ϕ ∃U ϕ ′ is the same as saying that exists a finite sequence of states . By the semantics of U c from Definition 3.5 we know that ∃π a path in H , which goes only through cells of dimension 0 or 1 because H models a Kripke structure cf. Lemma 3.1, hence π is of the form q 0 , q 1 , q ′ 0 , . . . ; and moreover, we also have that Clearly q ′ ∈ Q 0 because ¬ ⊤ must hold in q ′ and hence ϕ ′ holds in a state, i.e., H , q ′ |= ϕ ′ . It remains to show that in all q ′′ which are states (i.e., those q k 0 ∈ Q 0 ) we have that H , q ′′ |= ϕ. But we know that H , q ′′ |= ⊤ because q ′′ , being a cell of dimension 0, has no t map. Therefore, using H , q ′′ |= (ϕ ∨ ⊤) from before, we have that H , q ′′ |= ϕ.
Note that for the full CTL a universal correspondent of U c must be defined over HDAs, but we do not go into these details here.

Partial order models and their logics in HDML
This section is mainly concerned with Mazurkiewicz traces [19] as a model of concurrency based on partial orders, because of the wealth of logics that have been developed for it [7,9]. Higher dimensional automata are more expressive than most of the partial orders models (like Mazurkiewicz traces, pomsets [20], or event structures [21]) as studied in [22,3]. In particular, an extensive part of [3] is devoted to showing how Petri nets are representable as some class of higher dimensional automata. The works of [22,6,3] show (similar in nature) how event structures can be encoded in higher dimensional automata. Mazurkiewicz traces are a particular class of event structures, precisely defined in [23]. We use this presentation, as a restricted partial order, of Mazurkiewicz traces.
In the following we give definitions and standard results on partial orders, event structures, and Mazurkiewicz traces which are needed for the development of the higher dimensional modal logic for these models, in particular for Mazurkiewicz traces. In few words, we isolate the class of higher dimensional automata corresponding to Mazurkiewicz traces (and to partial orders or event structures in general) as the models of the HDML. Then we restrict HDML to get exactly the logics over Mazurkiewicz traces (we focus on the logics presented in [9,24]) and over the more general partial orders called communicating sequential agents in [25] (like ISTL of [18,10]). When one sees the elements of E as the events of a system, the labels can be seen as the names of the actions that the events are instances of. ∀e ∈ E, ↓e is finite, ∀e, e ′ , e ′′ ∈ E, e # e ′ and e ′ ≤ e ′′ implies e # e ′′ , ∀e, e ′ ∈ E, e ∈ C and e # e ′ implies e ′ ∈ C. An event structure is called finitary iff ∀e ∈ E, ↓e is finite.
The second constraint on event structures says that the configurations of an event structure are conflict-free. Define the relation of concurrency for an event structure to be:

Proposition 3.11 (families of configurations). A finitary event structure
Proof. This result is found in [6]. We summarize here the results leading to it. The two relations e ≤ e ′ and e # e ′ are mutually exclusive, because, otherwise, the set ↓e ′ would not be a configuration (because of the second constraint of Definition 3.10).
If two events e, e ′ do not appear together in any configuration of C E then e # e ′ (e # e ′ iff ∄C ∈ C E s.t. e, e ′ ∈ C). If in any configuration where e ′ exists, e exists too then e ≤ e ′ (e ≤ e ′ iff ∀C ∈ C E , e ′ ∈ C ⇒ e ∈ C).
We usually use a labeled poset and work with labeled event structures (E, ≤, # , λ ), or (E, C E , λ ) when using their corresponding family of configurations. Proposition 3.12 (traces as event structures). Any Mazurkiewicz trace, as in Definition 3.9, corresponds to a trace configuration structure, which is a labeled event structure (E, C E , λ ) with an empty conflict relation that respects the following restriction: λ is a nice labeling and context-independent, where nice labeling means ∀e, e ′ ∈ E, λ (e) = λ (e ′ ) ⇒ e ≤ e ′ or e ′ ≤ e and context-independent means Proof. This result is essentially found in [7,23]. We remind how one gets the independence relation of a Mazurkiewicz trace from a trace configuration structure: One can view a configuration as a valuation of events E → {0, 1}, and thus we can view an event structure as a valuation f E : 2 E → {0, 1}, which selects only those configurations that make the event structure.
The terminology that we adopt now steams from the Chu spaces representation of HDAs [22,6]. We fix a set E, which for our purposes denotes events. Consider the class of HDAs which have a single hypercube of dimension |E|, hence each event represents one dimension in the HDA. This hypercube is denoted 3 E , in relation to 2 E , because in the HDA case each event may be in three phases, not started, executing, and terminated (as opposed to only terminated or not started). The valuation from before becomes now E → {0, 1 2 , 1}, where 1 2 means executing. The set of three values is linearly ordered 0 < 1 2 < 1 to obtain an acyclic HDA [6], and all cells of 3 E are ordered by the natural lifting of this order pointwise. The dimension of a cell is equal to the number of 1 2 in its corresponding valuation.

Notation:
In the context of a single hypercube 3 E we denote the cells of the cube by lists of |E| elements e 1 e 2 . . . e |E| where each e i takes values in {0, 1 2 , 1} and represents the status of the i th event of the HDA. With the above conventions, the cells of dimension 0 (i.e., the states of the HDA) are denoted by the corresponding valuation restricted to only the two values {0, 1}; and correspond to the configurations of an event structure. The set of states of such a HDA is partially ordered by the order < we defined before. In this way, from the hypercube 3 E we can obtain any family of configurations C E by removing all 0-dimensional cells that represent a configuration C ∈ C E . 5 By Proposition 3.11 we can reconstruct the event structure.
In Definition 2.3 the interpretation of the during and after modalities of HDML did not take into consideration the labeling of the HDA. The labeling was used only for defining the geometry of concurrency of the HDA. Now we make use of this labeling function in the semantics of the labeled modalities of Definition 3.14. But first we show how the labeling extends to cells of any dimension. Definition 3.13 (general labeling). Because of the condition l(s i (q)) = l(t i (q)) for all q ∈ Q 2 , all the edges e 1 . . . e i−1 1 2 e i+1 . . . e |E| , with e j ∈ {0, 1} for j = i, have the same label. Denote this as the label l i . The label of a general cell q ∈ Q n is the multiset of n labels l j 1 . . . l j n where the j's are exactly those indexes in the representation of q for which e j has value 1 2 . As is the case with multi-modal logics or propositional dynamic logics [26], we extend HDML to have a multitude of modalities indexed by some alphabet Σ (the alphabet of the HDA in our case). This will be the same alphabet as that of the Mazurkiewicz trace represented by the HDA. In propositional dynamic logic there is an infinite number of modalities because they are indexed by an alphabet consisting of the regular expressions; yet these can be expressed in terms of a finite number of basic modalities (indexed by only the basic expressions). In our case we consider only an unstructured alphabet Σ which is considered finite. Definition 3.14 (labeled modalities). Consider two labeled modalities during {a}ϕ and after a ϕ where a ∈ Σ is a label from a fixed alphabet. The interpretation of the labeled modalities is given as: H , q |= {a}ϕ iff assuming q ∈ Q n for some n, ∃q ′ ∈ Q n+1 s.t. s i (q ′ ) = q for some 1 ≤ i ≤ n, l(q ′ ) = l(q)a and H , q ′ |= ϕ. H , q |= a ϕ iff assuming q ∈ Q n for some n, ∃q ′ ∈ Q n−1 s.t. t i (q) = q ′ for some 1 ≤ i ≤ n, l(q) = l(q ′ )a and H , q ′ |= ϕ. Having the labeled modalities one can get the unlabeled variants as a disjunction over all labels The same as in Proposition 3.2 we captured axiomatically in the basic HDML language the Kripke models, the question now is whether we can capture in the basic HDML language with labeled modalities the Mazurkiewicz traces. The initial results in Lemma 3.15 cast the restrictions on labeled event structures of Proposition 3.12 into the HDA setting in the view discussed above. Nevertheless, the context-independence property of the labeling function λ is special and we discuss it afterwards. The notion of empty conflict relation from Definition 3.10 is captured in HDML by the axiom: The notion of nice labeling from Proposition 3.12 is captured in HDML by the axiom: The notion of dependent actions a and b from Definition 3.9 is captured in HDML by the axiom: Proof. Mazurkiewicz  Such restricted HDAs still allow for autoconcurrency which is not the case in Mazurkiewicz traces. The nice labeling axiom (21) removes autoconcurrency. It basically says that two events with the same label cannot be concurrent; i.e., if an event labeled with a has been started then no other event labeled with a can start. Note that this axiom is meaningful on transitions and cells of higher dimension, but not in states; i.e., it is meaningful during the execution of the already started a-labeled events, not before starting them.
The last axiom (22) models the fact that two dependent actions are not concurrent, which is the last restriction in the Definition 3.9 of Mazurkiewicz traces. Note that the nice labeling restriction says that the dependence relation is reflexive, as required in Definition 3.9.
We could not capture the context-independent restriction on the labeling because it does not have just a universal presentation, so that we can capture it with axioms. This restriction is existential in nature, looking through all the higher dimensional automaton for some particular events. In fact it has a mixture of existential and universal assertions. Precisely, a labeling being context-independent is as saying that: if there exists throughout the HDA two events labeled with a and b which are concurrent, then all the pairs of events from the same HDA that are labeled with a and b must be concurrent. Or we can characterize it otherwise with the notion of not-concurrent as: if there exists throughout the HDA two events labeled with a and b which are not concurrent, then all the pairs of events from the same HDA that are labeled with a and b must not be concurrent. We can also have another view on this property, using two validities: either all the pairs of events labeled with a and b are not concurrent (i.e., axiom (22)) or all the pairs of events labeled with a and b are concurrent.
We conjecture that the context-independent restriction on the labeling function cannot be captured just in the basic HDML language, but the more expressive temporal operators are needed, which can talk about the whole HDA structure in an existential manner. Maybe just the eventually temporal modality is enough, instead of the stronger Until operator. Yet another question is whether just the LTL-like Until operator from Definition 3.6 is enough.
In the remainder of this section we show how the LTrL logic of [9] and the ISTL logic of [18,10] is captured in the higher dimensional framework. These logics, as well as those presented in [7,24], are interpreted in some particular configuration of a Mazurkiewicz trace (or of a restricted partial order). We take the view of Mazurkiewicz traces as restricted labeled posets from Proposition 3.9 but we use their representation using their corresponding family of configurations as in Proposition 3.12. Therefore, we now interpret HDML over restricted HDAs as we discussed above. • of the Until operator ϕ U ϕ ′ △ = (ϕ ∨ ⊤) U l (ϕ ′ ∧ ¬ ⊤); • and the next step operator, for a ∈ Σ, a ϕ △ = {a} a ϕ.
When interpreted only in the states of a HDA representing a Mazurkiewicz trace this language has the same behavior as the one presented in [9] Proof. The states of the HDA are the configurations of the Mazurkiewicz trace. Thus, our definition of the LTrL language is interpreted in one trace at one particular configuration; as is done in [9]. The original semantics of LTrL uses transitions from one configuration to another labeled by an element from the alphabet Σ of the trace. It is easy to see that our syntactic definition of a ϕ has the same interpretation as the corresponding one in [9]. The proof is similar to the proof of Theorem 3.3. In particular, when a ϕ is interpreted in some state of the HDA, i.e., in a configuration of the trace, then the formula ϕ must hold in the state reached by going through a transition labeled with a. This means that we just made a single step, cf. the definition of [9], from the initial configuration to a new one where one new event labeled by a has been added.
The Until operator of [9] has the same definition as the one in standard LTL but adapted to the Mazurkiewicz traces setting; thus, in the syntactic definition of U we use the LTL-like U l from Definition 3.6.
The ISTL logic is interpreted over communicating sequential agents (CSA), which are a restricted form of partial orders that still allows choices (as opposed to Mazurkiewicz traces). ISTL interprets the CTL until operator in configurations of a CSA. Therefore, we first need to find the exact restriction of HDAs modeling CSA and then just use the syntactic definition ∃U of Proposition 3.7. We do not go into details here but discuss the undecidability results for ∃U .
In [17] the ∃U is interpreted only over Mazurkiewicz traces and an undecidability proof is given using a simple trace that looks like a grid, with only two labels that are independent. The proof of [10] uses a simple CSA but which allows choices. Intuitively, [10] builds infinitely many grids as in [17]. Both these proofs work with infinite partial orders (i.e., infinitely many events): [17] works on an infinite grid; whereas [10] works with infinitely many finite grids. There are two stages in these algorithms: the first is to encode all and only these infinite structures with some formula (for which the Until definitions are not even needed, but only their weaker forms like ∃G are enough); the second stage is to encode the actual tests in the undecidability problem (the tiling problem in [17] and the Post correspondence problem in [10]). The first stage can be seen as setting the board for the undecidable problem.
We do not pursue further here investigation into the (un)decidability of HDML with the Until operator.

Expressiveness in terms of bisimulations
There are various ways of investigating the expressiveness of a logic. One way that we explored in the previous section is to see what other logics can be syntactically encoded into the studied logic and to isolate the exact restriction of the studied logic (and its models) that belongs to the encoded logic. Another way of looking at the expressiveness of a modal logic is by investigating the kind of bisimulation that it captures. In this section we do this for HDML, with the aim to get more insights into the distinguishing power of the basic language of HDML. By distinguishing power we mean what kind of (two) models can be distinguished by a single HDML formula and what models are indistinguishable. The notion of indistinguishable is given through an appropriate bisimulation; i.e., if the two models are bisimilar (for some specific notion of bisimulation) then an observer cannot distinguish them. The observer, in our case, has only the power to test logical HDML formulas on the two models. Since we will refer to works that consider labeled transition systems, we will use the labeled versions of the HDML modalities as in Definition 3.14.
Other expressiveness results for modal (temporal) logics include investigations into what exact subset of first (or second) order logic they capture, as is done for linear time temporal logic [27] (see [28] for an overview) or for the LTrL [9]. We do not pursue this line of research here.
HDML captures precisely the split-bisimulation and is strictly coarser than ST-bisimulation or history preserving bisimulation. Therefore, we confine our presentation here to only split-bisimulation, and discuss shortly the reasons that make HDML less expressive than the other bisimulations on HDAs. split-bisimulation). The split of a finite path π in a HDA is the sequence split(π) A and q 0 B two initial cells) are split-bisimulation equivalent if there exists a binary relation R between their paths starting at q 0 A respectively q 0 B that respects the following: . The ST-bisimulation replaces the first requirement with equality between ST-traces of the two paths. Intuitively, the ST-trace of a path is like the split-trace only that the end labels l i (·) − are keeping count of which start label they match with; i.e., l i (·) j where at the j th point the corresponding event has been started. Therefore, ST-traces know exactly which event ends; whereas the split-traces may confuse this. History preserving bisimulation is defined using the notions of adjacency and homotopy for HDA and intuitively, for some cell in the HDA we have a grip on its history also. Thus, history preserving bisimulation has access to the whole partially ordered history of the current executing events, ST-bisimulation has access only to some point from the past (i.e., the origin of some event), whereas the split-bisimulation has only a notion of previous step on the path. We come back to these intuitions throughout this section.
A modal logic is said to capture some equivalence relation ∼ if for any two models H and H ′ , they are equated by the ∼ relation iff they are modally equivalent.
To keep the presentation simple we will work with frames instead of models; i.e., with no propositional constants. Before presenting the formal result note that HDML can distinguish branching points, as is the case with bisimulations opposed to trace equivalences; the standard example in process algebras (a(b + c) vs. ab + ac) is distinguished by the HDML formula [ {a}][a]({b}⊤ ∧ {c}⊤). HDML also distinguishes between interleaving and split-2 concurrency, where the standard example of a||b vs. ab + ba is distinguished by the formula {a}{b}⊤ which holds only for a||b.
Proof. Proving the inclusion ≈ s ⊆ HDML ∼ is simple. Use induction on the structure of the formula and use the last two conditions for ≈ s with a smallest extension of the paths, i.e., when only one simple step is added to the path. The split-traces give the label and the s or t needed (when working with {} respectively ).
Proving the other inclusion HDML ∼ ⊆ ≈ s needs the standard assumptions of finite nondeterminism (or image-finite as it is also known) and finite concurrency. This proof uses reductio ad absurdum to show that the relation HDML ∼ is respecting the three conditions of Definition 4.1. Showing these conditions for all the paths is inductive, starting with the empty path and making only simple steps of extending the paths in the conditions 2 and 3, because this is enough to get the general form of these conditions. For the empty paths the condition 1 is trivially satisfied. We work here with simple steps that extend the path with s maps labeled by some a; and the other map t is treated analogous. Consider the initial cells q A HDML ∼ q B , and that s i (q 1 A ) = q A labeled by a (i.e., we extend the empty split-trace with a + ). We will assume that there is no way of extending (with a single step) the empty path in H B cf. condition 2 of Definition 4.1: i.e., Assume that for each cell q i B there exists some formula ϕ i that holds in q 1 A but not in q i B . Hence, q A |= {a}(ϕ 1 ∧ · · · ∧ ϕ n ) but q B |= {a}(ϕ 1 ∧ · · · ∧ ϕ n ), which is a contradiction with the fact that q A and q B are modal equivalent (i.e., model the same formulas). [a]{c}⊤ holds in the pomset process Y but not in X (in their HDA presentation). This example is meant in [29] to distinguish the ST-trace equivalence from all the split-n trace equivalences because the two pomset processes are indistinguishable by any of the split-n trace equivalences.
Nevertheless, when it comes to bisimulation equivalences HDML captures only split-bisimulation. Intuitively, the examples above can be distinguished by HDML because they have different branching points before the problematic autoconcurrency square. HDML becomes stuck when it has to deal with autoconcurrency; i.e., when in a concurrency square with both sides labeled the same, HDML cannot distinguish which of the two events it finishes. But ST-bisimulation and history preserving bisimulation can distinguish the two events by looking at the history. In particular, HDML is unable to distinguish any of the "owl" examples of [29] which are meant to separate the split-n-bisimulations.
In conclusion, HDML sits pretty low in the equivalences spectrum of van Glabbeek and Vaandrager [29], capturing only split-bisimulation. An interesting question for future work is what is a minimal extension to HDML that captures ST-bisimulation, or history preserving bisimulation?

Conclusion
We have investigated a modal logic called HDML which is interpreted over higher dimensional automata. The language of HDML is simple, capturing both the notions of "during" and "after". The associated semantics is intuitive, accounting for the special geometry of the HDAs. An adaptation of the filtration method was needed to prove decidability. We have associated to HDML an axiomatic system which incorporates the standard modal axioms and has a few natural axioms extra, which are related to the cubical laws and to the dimensions of HDAs.
We isolated axiomatically the class of HDAs that encode Kripke structures and shown how standard modal logic is encoded into HDML when interpreted only over these restricted HDAs. We then showed how to extend the expressiveness of HDML using the Until operator by defining two kinds of Until over HDAs: one U l in the LTL style and one U c in the CTL style. Using the U c we showed how to encode syntactically the CTL ∃U into HDML when interpreted over the Kripke HDAs. We also showed how weaker concurrency models like Mazurkiewicz traces or (restrictions of) event structures can be encoded in HDML and how some of their specific properties can be captured axiomatically only in the basic language of HDML. We also looked at encoding specific logics for these restricted models (particularly the LTrL and ISTL) in the extensions of HDML with the Until operators.
In the last technical section we investigated the distinguishing power of HDML and isolated the basic language of HDML as capturing exactly the split-bisimulation. Nevertheless, the power to distinguish different branching points allowed HDML to distinguish all the examples of [29] that were meant there to separate the split-n-trace equivalences and the ST-trace equivalence. In this respect we gave some discussions trying to identify the weak points of HDML compared to ST-bisimulation or history preserving bisimulation.
Interesting further work is to look more into the relation of HDML (and its temporal extensions) with other logics for weaker models of concurrency like with the modal logic of [11] for event structures or other logics for Mazurkiewicz traces. Particularly interesting is to give details of how or if the undecidability results of [10,18] are applicable to our setting.
When investigating deeper the extensions of HDML wrt. the captured bisimulations, the work of [30] is of particular relevance and comparisons with the logics presented there worth wild.

A Completeness
This section is not finished. It presents the main ideas and steps needed to prove the completeness of the axiomatic system for HDML from Table 2; but still some details need to be fit into place. Any comments on this proof are welcome. The complications and details of this completeness proof are as such because of the intricate geometrical structure of the HDA model that we work with. Some of the inductive reasoning that is needed does not follow standard patters, and makes arguments more involved.
We first fix some terminology and notation. Because of the finite model property for HDML from Theorem 2.13 and because compactness fails cf. Theorem 2.17, we are inclined to use atoms in the proof of completeness for HDML and build finite canonical models (instead of using maximal consistent sets and standard canonical model). Definition A.1 (atoms). Recall from Definition 2.4 that C (ϕ) is the subformula closure set of some given formula ϕ. Denote by ¬C (ϕ) = C (ϕ) ∪ {¬ϕ ′ | ϕ ′ ∈ C (ϕ)} the set of subformulas together with their negated forms. A set of formulas A is called an atom for ϕ if A is a maximal consistent subset of ¬C (ϕ). Denote At(ϕ) the set of all atoms for ϕ. For an atom A ∈ At(ϕ) denote byÂ the formula obtained as φ 1 ∧ · · · ∧ φ n with φ i ∈ A.
Intuitively, atoms are sets of formulas which are free of immediate propositional inconsistencies (like φ ∧ ¬φ ).

Lemma A.2 (properties on atoms). Standard results for atoms tell us that for some formula ϕ and any atom A ∈ At(ϕ) is the case that:
(i). for all ψ ∈ ¬C (ϕ) then only one of ψ or ¬ψ are in A; (ii). for all ψ → ψ ′ ∈ ¬C (ϕ) then ψ → ψ ′ ∈ A iff whenever ψ ∈ A then ψ ′ ∈ A;
Proof. By induction on the structure of ψ.
Inductive step: The case for the Boolean connectives follows easily from the properties on atoms. Finally we treat cases for the two modalities. Consider the during modality. The left to right direction is based on the canonicity of H .
For the right to left direction we use the saturation of H . We prove {}ϕ ∈ λ (q n ) ⇒ H , q n |= {}ϕ. Using the saturation of H we have that ∃q n+1 ∈ Q n+1 and ∃0 ≤ i ≤ n + 1 s.t. s i (q n+1 ) = q n and ϕ ∈ λ (q n+1 ). By the induction hypothesis it implies that H , q n+1 |= ϕ. Thus, by the definition we have that H , q n |= {}ϕ.
The proof for the modality is symmetric using the second conditions of canonicity and saturation of H .
For modal logics over complex structures like HDAs the step-by-step method of proving completeness is a first candidate. But we cannot use it in the standard way with maximal consistent sets as the cells of the HDA. Instead we will use atoms, i.e., finite maximal consistent sets. On the other hand, the standard way of using atoms in completeness proofs is to build a finite canonical model and show that it respects the required special structure. This is not easy in our case. In consequence we use a step-by-step method for building a finite model and label the cells with atoms. This model will have the right HDA structure and will respect canonicity properties required by a truth lemma. In this sense we adapt and combine the two methods of step-by-step and atoms-based finite canonical models to HDML. On the other hand the main difficulty of our proof is the construction method which is rather involved. Note that we prove a weak completeness result, which is normal because a strong completeness is out of reach because of the compactness failure.
A first attempt to prove completeness is to try to build a canonical saturated model for any consistent formula. This fails, partly because HDML is a forward looking logic but the special cubical geometry of the HDAs require to construct the backwards part of the HDA (that which is not reachable through the two modalities of HDML). But it is not possible to guarantee the canonicity for this part. Nevertheless, the following notions and results tell us that we can ignore canonicity for this part of the model. Therefore when doing the actual step-by-step construction of the required HDA for some arbitrary consistent formula we will concentrate on respecting canonicity only for the relevant (cf. the results below) part of the structure.
Definition A.5 (pseudo HDA). For a HDA H and a cell q ∈ H we call the forward generated pseudo HDA for the cell q (or pseudo HDA for short) the structure H p q = (Q ′ , s ′ ,t ′ , l ′ ) obtained from H by the following generative definition: • no other cell of Q is in Q ′ ; and where s ′ △ = s| Q ′ , t ′ △ = t| Q ′ , and l ′ △ = l| Q ′ are the respective restriction to this new set of cells Q ′ .
Intuitively, the pseudo HDAs are similar to the idea of a point-generated submodel in standard modal logic. The following lemma intuitively says that HDML satisfaction is invariant under pseudo model construction.
Lemma A.6 (invariance under pseudo HDAs). For a HDA H and a cell q ∈ H for which H p q denotes the pseudo HDA for q, then for any HDML formula ϕ and any cell q p ∈ H p q , we have: Proof. The proof uses induction on the structure of the formula ϕ. Since the pseudo HDA does not change the valuation then the base case for propositional constants and the inductive cases for the Boolean operators are trivial, as we have to look at the same cell. It remains to treat the inductive cases for the two HDML modalities; we will treat only ϕ = {}ψ, and the other modality is treated analogous. Since the set of cells of the pseudo HDA is just a subset of the original H , i.e., Q ′ ⊆ Q, then the right-to-left implication is immediate (using induction on the subformula ψ). For the left-to-right implication consider that H , q p |= ϕ and we show that H p q , q p |= ϕ. From the semantic definition we have that it exists s i (q n+1 ) = q p , for some i, with H , q n+1 |= ψ. From the pseudo HDA Definition A.5, since q p ∈ H p q then also q n+1 ∈ H p q and s ′ i (q n+1 ) = q p . From H , q n+1 |= ψ, by the induction hypothesis we have that H p q , q n+1 |= ψ. Lemma A.8 (truth lemma for pseudo canonical HDAs). In a HDA H which is pseudo canonical for q and saturated wrt. a formula ϕ, with the valuation defined as V (q n ) = {φ ∈ Φ B | φ ∈ λ (q n )}, then for any ψ ∈ ¬C (ϕ) and q n ∈ H p q it holds that H , q n |= ψ iff ψ ∈ λ (q n ).
Proof. The proof follows from the Truth Lemma A.4.
To prove completeness of the axiomatic system all that remains is to show that for any consistent formula ϕ we can build such a pseudo canonical saturated HDA. During the step-by-step construction process we constantly struggle to saturate the HDA (that we work with) while respecting the pseudo canonicity. Such not saturated HDAs are called defective, as they may have defects, which we formally define below. But important is that any of these defects can be repaired. This is what the repair lemma does, using the two enriching and lifting constructions. The completeness theorem then shows that while starting with a minimal pseudo canonical HDA we can incrementally build a defect free pseudo canonical HDA, i.e., a pseudo canonical and saturated HDA.

Definition A.9 (defects). There are two types of defects for H (corresponding to a violation of a saturation condition):
• a D1 defect of H is a cell q n ∈ Q n with {}ψ ∈ λ (q n ) for which there is no q n+1 ∈ Q n+1 and no 1 ≤ i ≤ n + 1, with s i (q n+1 ) = q n and ψ ∈ λ (q n+1 ); • a D2 defect of H is a cell q n ∈ Q n with ψ ∈ λ (q n ) for which there is no q n−1 ∈ Q n−1 and no 1 ≤ i ≤ n − 1, with t i (q n ) = q n−1 and ψ ∈ λ (q n−1 ).
During the construction of the model we cannot work with atoms directly because we will revisit the same cell several times, each time needing to add more restrictions to its label. We are still working with atoms as labels, only that we consider all possible atoms that respect such properties (eg., all the atoms that could extend some consistent set of formulas). In the end of the construction we just pick one, to obtain the pseudo canonical saturated model we are seeking. The key result here is that all the constraints that are gathered during the construction should allow for the existence of at least one respecting atom. We use the following definitions.
Definition A.10 (potential labeling function). We define a potential labeling functionλ : Q → 2 C which for any cell q ∈ Q returns a set of constraints from C. A constraint c ∈ C can be either a consistent set of formulas S ∈ C (ϕ) (call this a set constraint) or a formula {}Â or Â , with A ∈ At(ϕ) an atom, (call these existential constraints). A potential labeling is called potential canonical iff there exists some labeling function λ s.t. for any cell q ∈ Q, λ (q) is consistent with all the constraintsλ (q).
Lemma A.11. A potential labeling is not canonical iff any of the following is the case: • for some cell q the union of all the set constraints inλ (q) is inconsistent; • for some cell q there exists a formula ϕ ∈ A with A appearing in one of the existential constraints as {}Â ∈ λ (q) (or as Â ∈λ (q) Note that increasing the number of constraints means that there is less uncertainty about the ultimate atom that is going to label a cell.
The two constructions that we give below are working on pseudo canonical HDAs, where the minimal such HDA contains only one cell; this is the starting pseudo canonical HDA in the completeness Theorem A. 24.
For a D1 defect, i.e., a cell q as in Definition A.9, the enriching construction adds one new cell that has q as one of its sources and is labeled with an atom containing ϕ. Moreover, all the other maps of this new cell need to be added, together with all the necessary new cells, respecting the cubical laws. The new enriched HDA will not have q as a D1 defect any more.  First remark that we do not change the initial shape of the original H ; we only add fresh cells and fresh maps for these cells; we also add maps to old cells connected to new cells. This concludes the first stage in proving that H ′ ⊲ H . The second stage is proven as Lemma A.14, whereas the third stage is proven as Lemma A.18. Therefore, H ′ ⊲ H .
We show next that we indeed construct a higher dimensional structure. A careful reading of the enriching construction should answer this question in affirmative. We need to make sure that to each new cell we add all the s and t maps according to its dimension and that we link these maps correctly according to the cubical laws.
The enriching construction proceeds as follows. It takes our initial cell q and its dimension n and the formula that gives the D1 defect. It adds a new cell q n+1 of dimension one greater than q and links this with q through the s n+1 map. It labels the new cell s.t. the defect of q is repaired. The labeling is not important for our current argument but it is used in the argument for canonicity. To have the new cell q n+1 correctly added we need to add n more s maps (i.e., the s i maps with 1 ≤ i ≤ n) and n + 1 more t maps to it. The s maps are added by the addSourceMaps and the t maps are added by the addTargetMaps.
Consider now the addSourceMaps function which takes as arguments the cell to which it must add the maps and the dimension of this cell, together with two other arguments used for bookkeeping of the cubical laws that need to be added for each cell. More precisely, the m argument records how many cubical laws the q cell enters into. Note that this function (the same as addTargetMaps) adds maps only if the dimension of the cell is greater than 0, because, by definition, states in a HDA have no maps. addSourceMaps adds only k − 1 maps to its cell argument because one s map has already been added before (e.g., for q n+1 we have added the map s n+1 and it remains to add the other maps from s 1 to s n ). All these maps link to new cells of dimension one lower (i.e., dimension k − 1). Actually there are less new cells because some of the s maps must link to already existing cell so to respect the cubical laws. The m argument tells how many s maps should come only from cubical laws and hence, we add only k − 1 − m new cells. The next loop adds these maps respecting the cubical laws; e.g., for the cell q n−1 n = s n−1 (q) we add the map s n−1 (q n−1 n ) as the result of s n−1 (s n (q)) (which are cells that have already been added) because of the cubical law s n−1 (s n (q)) = s n−1 (s n−1 (q)). In fact, for the cell q 1 n each of its s maps links to some existing cell, thus no new cells are added.
Each of the k − 1 − m new cells are linked with q by the corresponding s i map. It is also added the s k−1 map (i.e., the map with greatest index among the k − 1 maps that the cell needs). This is done so to respect the cubical laws s i (s k (q)) = s k−1 (s i (q)). We now need to recursively add the required s and t maps for the new cell. We call the addSourceMaps for this cell q i k−1 of dimension k − 1 and, depending on the index i in the loop, we specify that k − 1− m − i maps should be added directly through the cubical laws and not by using new cells. We must also carry along the node q to which the cubical laws link. We also add the t maps for q i k−1 by calling the addTargetMaps function.
The function addTargetMaps adds all the t maps of the cell (not one less as the addSourceMaps is doing). addTargetMaps also tries to respect the cubical laws first, and thus the m argument tells which maps come only from a cubical law like t i (t j (q)) = t j−1 (t i (q)). For a cell q of dimension k addTargetMaps adds k − m new cells of dimension k − 1 and links each of these cells through a corresponding t i map. For each new cell a recursive call to addTargetMaps is needed to add all the necessary t maps. The s maps of the new cells are added in the end taking care that all the cubical laws of the form s i (t j (q)) = t j−1 (s i (q)) are respected. All these s maps are linked to cells which come from t maps that have been added by the addSourceMaps function before.
Proof. This lemma is essentially the second stage in the proof of the correctness of the enrich construction from Lemma A.13.
Note that throughout the rest of the paper when we write ϕ ∈λ (q) we mean that the formula ϕ is part of one of the set constraints inλ (q); we use the same notation for the fact that the formula is part of a single constraint when this is clear from the context, as is the case in the paragraph above where we consider only the set constraint build at line 4. Therefore, we do not need to wary about inconsistencies coming from inside one of the new set constraints that the algorithm builds. It remains to see if any of the formulas in the new set constraints is inconsistent with some formula already existing in the potential label of the cell where the new set constraint is added. This cannot happen at line 4 because the cell q n+1 is fresh and has at this point no label attached. Inconsistencies may come from the addSourceMaps function that is called recursively in a depth-first manner.
We explain now how this function works and how the source maps are added by the enrich function.
Starting with the defective cell of dimension n the enrich function adds a new cell q n+1 of dimension n + 1 and adds its highest s map, i.e., s n+1 . Then it calls the function addSourceMaps to add the rest n source maps. This one works in a depth-first manner and adds source maps starting with the highest one. The first call, at line 6 in the body of the enrich itself, adds one less s map, but the other recursive calls add all the maps. Because of the cubical laws, some the the s maps will reach cells that already exist. This is the reason for going in a decreasing order adding first the highest s map, and adding s 1 last. In fact s 1 will have each of its s maps connected to some existing cell. For all the fresh cells that are added, the highest s map will connect to a cell from the old H . The rest of the cells connect to other fresh cells. This is part of the reason for which addSourceMaps works in a depth-first manner when adding the labeling constraints. At the deepest level Q 1 the new cell will connect its only s 1 map to an old cell from H and its new set constraint will be build from the potential canonical old label. When closing the recursions and going up the levels, the function builds the new set constraints from all these lower cells that are connected through the s maps (one of them is from the old H , remember). Therefore, the set constraints of all the fresh cells are eventually build only from the labels of old cells.
Consider any of the fresh cells added by the addSourceMaps function, i.e., except the q n+1 cell added in the body of the enrich. Assume that two formulas ϕ and ¬ϕ come from two different sources containing each a universal formula There is no other way of inconsistencies to creep in the new set constraints for the fresh cells added by the addSourceMaps function. We continue the argument for the addTargetMaps function.
If in addSourceMaps function the accumulation of the set constraints was done in a bottom up fashion after settling the lower cells, i.e., at line 24; now in addTargetMaps function the collection is done in a top down fashion, for t maps collecting from all reachable cells that were previously labeled, i.e., at line 31. The addTargetMaps function works on adding the new t maps also starting with the highest one and always finishing with t 1 . But many of the maps reach already existing cells: the first for loop takes care of such t maps, whereas in the second loop all the s maps reach cells that have been added in the addSourceMaps function. For the old cells in the first loop, the function updates the already existing potential labeling by adding new set constraints. For the fresh cells the second loop, at line 36, adds a completely new potential label with one set constraint, and in the next line adds also an existential constraint. All these fresh cells reached through the t maps have their labels updated when the s maps are added. These connect to already existing cells, from where all the boxes have to be accumulated in the label of the new cell, i.e., these are the contents at lines 42 and 46. Note that for some fresh cell the algorithm adds one set constraint coming from each of its source maps.
After this intuitive presentation it is easy to identify where the inconsistencies in the set constraints can come from: 1. either in the first loop at line 31 when collecting a new box constraint having a box formula [ ]ϕ where the formula ¬ϕ may already be in the potential labelλ (t k−l (q)) as coming from before from some formula [ ]¬ϕ in a box constraint of some cell connected to t k−l (q) through a t map; For 1 it means we are in the first loop, at line 31, in the setting of the cubical law t k+1−m (t k−l+1 (q ′ )) = t k−l (t k+1−m (q ′ )), where q = t k+1−m (q ′ ) and q ′ was introduced before by either a previous application of addTargetMaps or is one of the cells added by the addSourceMaps. Because the two formulas [ ]ψ and [ ]¬ψ may come only from set constraints then the potential label of q ′ contains both [ ][ ]ψ and [ ][ ]¬ψ. We may assume that q ′ is not added by addTargetMaps, but comes from the other two functions; otherwise, we just need to stack several times the [ ] modality until we reach such a cell, and the reasoning would carry over verbatim. As we argued before, there ⊥ which is inconsistent with the existential constraint inλ (q ′′ ) that essentially says that the atom should be consistent also with {}{}ϕ.
For 2) we are in the second loop and the formula ψ was added at line 36 as coming from [ ]ψ ∈λ (q) and the other formulas is added at line 42 (or at line 46 for the same argument) as coming from [ {}]¬ψ ∈λ (t i−1 (s j (q))); i.e., we are in the setting of a cubical law s j (t i (q)) = t i−1 (s j (q)). Assume that q is the defective cell, for otherwise we have less cases to wary about as q would be one of the cells added by addSourceMaps and we would have several [ ] stacked on top of the formulas and the argument would be analog to the one we give below. The fact that [ {}]¬ψ ∈λ (t i−1 (s j (q))) means that it comes from a set constraint of s j (q), i. Proof. The first fresh cell is added at line 2 and is directly linked through s n+1 , at line 3, to the original defective cell from the old H . It remains to check that all other s and t maps of this cell are eventually reaching the old model H . We do this inductively by going down the recursion calls until we find the minimal single descent steps. In particular we have to check only the s maps because from this initial fresh cell q n+1 only s → steps are possible. If s n+1 (q n+1 ) is linked to the cell q in the old H , then for all the other s i (q n+1 ) their s n map is linked to the s i map of q, hence reaching in one s → step H . We used the cubical law s n (s n+1 (q n+1 ) = s n (s n (q n+1 )). We use the similar law s n−1 (s n (s n (q n+1 ))) = s n−1 (s n−1 (s n (q n+1 ))) to argue that taking the descent step using the source s n−1 reaches the old H in two steps. The same reasoning is carried over inductively until the last recursion call.
In conclusion, all fresh cells added by the addSourceMaps reach the old H through any of their sources by following a descent chain formed only of descent steps from s →, which, depending on the index of the source, take longer or shorter to reach H .
The other fresh cells are added in the addTargetMaps, at line 28. It is easy to see that all their immediate t ← possible steps can eventually reach H . An easy inductive reasoning suffices for this argument. Start with the cells added in the addSourceMaps function or at line 7 in the body of the enrich function itself. All these reach in one t ← step a cell that we argued before that it can reach H through a chain of only s →. For the other cells added at deeper recursion calls inside addTargetMaps we can reach the cells from before, which have a descent chain to H .
It remains to show that for all the fresh cells added in the addTargetMaps their s maps also lead to H , i.e., that starting also with a s → step also leads eventually to a descent chain to H . This is done also inductively starting with the cells that are added in the first call to addTargetMaps function, and not inside its body (i.e., this step also considers the first calls inside the addSourceMaps function). Therefore, we consider some cell q ′ which we proved that it eventually reaches H ; this cell has a target, say t k , to the fresh cell q that we are concerned with and itself has a source to some other cell s j (q) = q ′′ . Depending on k, j we use the following cubical laws: if j < k then s j (t k (q ′ )) = t k−1 (s j (q ′ )); if k ≤ j then t k (s j+1 (q ′ )) = s j (t k (q ′ )). Thus, in any case we can have a t ← step from q ′′ to s j (or s j+1 depending on the case), but these cells can reach H , because they are reached from the initial q ′ through a s → step. This base case is finished.
For cells added at deeper recursion calls, inside addTargetMaps, we use the same cubical laws and reach cells that we just proven in the step before that can reach H . Depending on the indexes of the s maps, the descending chains are longer or shorter.
Note that in the proof of Lemma A.14 we made heavy use of the fact that we could go down a descent chain that was made of only s → steps. Because of this we were stacking up [ {}] modalities. We will shortly make precise this method of stacking modalities depending on the descent chain and we will see more use of it and in more varied settings.
Corollary A.17. Proof. This lemma essentially makes the third stage of the proof that the HDA built by the enrich construction extends the old HDA. This proof is based on the fact that the set constraints of each cell are consistent, cf. Lemma A.14. We will make use of the fact that we enrich an old H which has a potential canonical labeling, as we did in the proof of Lemma A.14. The proof is by reductio ad absurdum and assumes for an existential constraint {}λ (q) in theλ (q ′ ) there exists a formula [ {}]¬ψ in the set constraints ofλ (q ′ ) for which the formula ψ is in some set constraint ofλ (q).

For any fresh cell added by the enrich algorithm there exists a maximal descending chain and this one reaches a cell in the old
These two formulas come from other set constraints being under some [ {}] or [ ] box modality; and these bigger formulas in turn come from other set constraints added by the algorithm. And so on until we reach the old H . From here we only know that the labeling in potential canonical; and we will use this in the proof. Therefore there are many ways that the assumed formulas may have come from, and we need to find a way to treat all these different ways.
First we checked all the cases by hand for the particular application of enrich when the old cell is of dimension 2 and hence the new cell that needs to be added (with all its maps) is of dimension 3. Finding a clear pattern in these cases with varied length of the constraint propagation was tedious. 7 The definitions and results above about descent chains are the basis of the general proof pattern that we will develop now further. These chains relate to the histories of a cell and to the notions of adjacency and homotopy.
We take any s map introduced by the algorithm, i.e., s i (q) = q ′ , and make the assumption from above. We will arrive at an inconsistency in the old H , hence the contradiction. (The same proof method works for the t maps and an analog assumption as above only that we use [ ] instead of [ {}].) Note that from cell q we can make a s → descent step to reach q ′ . From Corollary A.17 we know that from the cell q ′ , hence also from q, there exists some descent chain reaching H . If the descent chain is empty, i.e., q ′ ∈ H , and if all the descent chains of q consist in the single descent step to q ′ then the result is trivial. This case corresponds to when the algorithm is at the most deep recursion call. If there are other descent steps starting from q then we are in a nontrivial case.
From Corollary A.17 we know that any two different descent chains starting from q will eventually end up in the same cell. Moreover, we know that any such descent chain eventually reaches the H or the newly added cell q n+1 at line 2 in the algorithm. We can argue that is enough to consider reaching this cell instead of reaching the original H .
The proof method takes two such descent chains starting from q: one going first through q ′ and the other going through some other different cell. For each of these chains we stop at the first cell from H or q n+1 . The idea is that until there we are walking through the fresh cells added by the algorithm, and hence we collect boxes on the way. To such a descent chain that starts from q we associate a formula as follows: considering ψ ∈λ (q), for q s → q ′′ st ←→ * then [ {}]ψ ∈λ (q ′′ ). We continue until the end of the chain where in the case of a t ← descent step eg.
. Both these chains reach eventually the same cell in H , cf. Corollary A.17. Moreover, the chain that reaches H faster can continue through the inside of H until reaching the end cell of the other chain. This traversing of the old H is done under the existential constraints in the potential canonical labeling of H , therefore we can extend the corresponding formula with existential modalities. In the common end cell we have now two formulas, one made only of box modalities and the other which may also have a stack of existential modalities, and both have to be consistent, as being part of the old H . We actually show that these two are inconsistent or cannot be grown to an atom, i.e., lead to an inconsistency in the axiomatic system of HDML.
Thus we work with two chains starting from q and ending in some common cell in H , and to each chain we associate a formula: one adds modalities to ψ (as being inλ (q)) and the other adds modalities to ¬ψ (as coming from the chain that goes through q ′ which we assumed to have a formula [ {}]¬ψ). We denote descent steps that are inside the H , and which are associated with existential modalities, by s respectively t . There is an equal number of s → in each chain (either universal or existential) and hence an equal number of t ← steps also, cf. Corollary A.17. This translates into the formulas also. The purpose is to change these chains so that the descent steps match one by one. If one existential matches one universal then we obtain an existential step that leads to the inconsistency more easy. Also, the purpose is to move as much as possible of the s → steps to the end of the chain and the t ← steps to the beginning of the chain. In the end we will arrive at a contradiction with the fact that in the initial cell which the algorithm starts with there is the formula {}ϕ and hence, by the existential constraints in H , all lower cells are consistent with {} k ϕ depending on the distance from the initial cell.
For For all the patterns that we find in the descent chains there is some axiom associated which helps transform the formulas into the needed ones; we will say that they transform the chains into the proper form. Below we give the patterns with the associated formulas and axioms: chains the two chains match step by step as having the same s or t label and we match either two universal steps, like s →, or one universal step with one existential step which yield an existential step, like For a D2 defect, the lifting construction lifts the defective cell and all the cells that are connected to it by some s or t map, one level up by adding one new s and t map to each of them. The label of the new t map will be the one repairing the D2 defect. The cubical laws make sure that these new maps reach only new cells; none of the old cells (that are lifted) are involved in these new instances of the cubical laws. We need to be careful how we label all these new cells s.t. the canonicity is respected for the new lifted HDA.
The lifting construction is more involved than the enriching construction. We still label the cells with atoms in the end but during the construction the constraints that the atom has to satisfy are changed. This is why we keep the set of all atoms that satisfy the constraints as possible candidates for the final labeling. This means that we are still working with atoms (i.e., maximal consistent sets of formula) but we do not settle on one particular atom until we have finished the construction. Basically the steps (1b) and (1c) are corresponding to Lemma A.11 to show that the new potential labeling is still potential canonical, i.e., that there still exists a way of instantiating the constraints to atoms.
2. The next stage shows that H ′ is a model indeed, i.e., that all the maps are in place and all necessary cubical laws are respected.
3. The last stage shows that the enriched model does not have the old defect and that no new defects are introduced in the potential labeling of the initial cell q. First remark that we do not change the initial shape of the original H ; we only add fresh cells and fresh maps for these cells; we also add maps to old cells connected to new cells. This concludes the first stage in proving that H ′ ⊲ H . The second stage is proven as Lemma A.14, whereas the third stage is proven as Lemma A.18. Therefore, H ′ ⊲ H .
We show next that we indeed construct a higher dimensional structure. A careful reading of the enriching construction should answer this question in affirmative. We need to make sure that to each new cell we add all the s and t maps according to its dimension and that we link these maps correctly according to the cubical laws.
Note that the algorithm finishes with a completely new layer of cells denoted Q −1 ; in the end of the construction we have to rename all the layers Q i into Q i+1 to make justice to the cells that reside there which have now dimension i + 1 as we added one s and one t map to each.
Note that the construction terminates iff q is in a hypercube of finite dimension and in this case we ignore all the cells outside this cube. (The construction always terminates when we use it in the repair lemma A.23.) Clearly the two functions do not change the labels nor the shape of the old H and hence the lifted H ′ has all the structure of H . Now we show that the lifting constructs indeed a HDA. This means that we must make sure that all the (new) cells have the right number of s and t maps and that all the cubical laws are respected.
The lift function takes as input the reference cell q and its dimension n together with the formula ϕ that causes the defect (i.e., ϕ ∈λ (q)). Then the function adds one t map and one s map to q by calling addTargetMap and addSourceMap respectively. These two functions add one new cell and link it with either a t or an s map. All other cells that are connected to q must also be lifted, which is done in the loop of the lift function.
Consider now the addTargetMap which takes as arguments the cell q (and its dimension k) to which the new t map needs to be added. It also takes two sets of formulas which are used to construct the label of the new cell and of the other new cells connected to it recursively. We do not discuss here the labeling because we do this in the Lemmas ?? and ??. The rest of the proof is concerned with the geometric structure of the extended H ′ .
The addTargetMap function adds the new t k+1 map to q, which is the map with the largest index (i.e., the new index showing that the q cell has now dimension one greater, k + 1). It links this with a new cell q k of dimension one lower than the new dimension of the input cell q. The first loop does two operations. First it lifts all the old cells linked to q by an s map (i.e., s i (q)) by adding one t map to each; i.e., it invokes addTargetMap recursively. Then, all these cells enter under new cubical laws that involve the s maps of the newly added q k cell. In this way we also add all the necessary s maps of q k and also respect the new cubical laws s i (t k+1 (q)) = t k (s i (q)).
In the second loop of addTargetMap we add the new t k map to each old cell linked to q by a t i map; i.e., in the recursive invocation of addTargetMap. At the same time we add all the t maps for the new q k cell and link these through the cubical laws t i (t k+1 (q)) = t k (t i (q)).
The construction goes recursively at lower levels until reaching cells of dimension 0. These are the last cells lifted to have dimension 1. Here the recursion stops.
Consider now the similar function addSourceMap which adds one s map to the input cell q of dimension k to make it now of dimension k + 1. Therefore, it adds the map s k+1 (q) = q k−1 . This is also the place where the lifted cells are actually moved to the rightful layer Q k+1 , at the end of the function (i.e., line 39), after both target and source maps have been added.
In the first loop addSourceMap adds a new s k maps to all the old cells linked to q by a t map. This finishes what we started in the second loop of addTargetMap, i.e., finishes lifting all the t i (q) cells. It also takes care to respect all the new cubical laws t i (s k+1 (q)) = s k (t i (q)) and, hence, to add the t i maps to q k .
The second loop complements what we started in the first loop of addTargetMap. We finish adding the s k maps to all the s i (q) cells. It also adds all the s maps to q k and respects the new cubical laws s i (s k+1 (q)) = s k (s i (q)).
In The set S1 is not empty only when the function is applied to the initial cell q from the statement of the lemma. The lemma assumes that q ∈ Q n is of dimension n, denote it q n for this part of the proof, and it contains ϕ ∈λ (q n ) for which all of its n existing s maps contain ¬ϕ. This means that if beforeλ (q n ) was consistent with n now we need to write n + 1. Because of axiom (A5) and Lemma A.2(ii) it means thatλ (q n ) is consistent also with n+1 ⊤. (As a side remark, we use Lemma A.2(ii) tacitly in many places during the proofs of the two constructions lemmas.) The first call to addTargetMap(n,q n ,{ϕ}, / 0) makes use only of S1 and constructs the set {ϕ}∪{ψ | [ ]ψ ∈λ (q n )}. This set is associated to q n−1 = t n+1 (q n ). The proof is easy for this case and uses arguments as in the proof before: if we assume ψ 1 ∧ · · · ∧ ψ k → ⊥ then we get that [ ]⊥ ∈ λ (q n ) which is a contradiction as λ (q n ) is an atom containing ϕ; if we assume ψ 1 ∧ · · · ∧ ψ k → ¬ϕ then we get that [ ]¬ϕ ∈ λ (q n ) which is again a contradiction.
The second call to addTargetMap is made for each s map of a cell q (in the first loop of the body of the addTargetMap) and it uses only the set S2. This means that it labels a cell q n−1 = t n+1 (q) with a set {ψ | [ ]ψ ∈ λ (q)}. Assume ψ 1 ∧ · · · ∧ ψ k → ⊥ which means that [ ]⊥ ∈ λ (q). This is a contradiction because λ (q) is an atom and it contains at least one diamond formula. This is because q has dimension at least 1 (as it has at least one t map) and we show that any cell of dimension n, with n ≥ 1, has a formula n ⊤ ∈ λ (q). We showed before that the topmost cell q n has the formula n+1 ⊤ in its label and hence it is of dimension n + 1. This means that any cell reached through one of its t maps will have the formula n ⊤ because of axiom (A8') which says that n ⊤ → [ ] n ⊤ it means that [ ] n ⊤ ∈ λ (q n ) and by the construction of their labels it means that n ⊤ ∈ λ (t j (q n )). This holds for any cell reached through any number of applications of t maps. On the other hand, the cells reached through an s map from q n , by canonicity, they contain {} n+1 ⊤, which, by axiom (A9') it means that n ⊤ ∈ λ (s j (q n) ).
It remains to see that with each iteration of the first loop the updated label remains a consistent set. This update is necessary when we are trying to respect the cubical laws of the form s i (t k+1 (q)) = t k (s i (q)). The proof of this part follows an inductive argument, where the basis was just proven above and the inductive case is for some i iteration, where we consider that the label is a consistent set (and all the other labels that the construction uses have been built already and, hence, are atoms). Assume that for some [ {}]ψ ∈ λ (t k (s i (q))) there has already been added the ¬ψ to λ (t k+1 (q)). This has happened in two cases: first if ¬ψ comes from λ (q), i.e., [ ]¬ψ ∈ λ (q) which by canonicity it means that {}[ ]¬ψ ∈ λ (s i (q)). On the other hand we also have that [ {}]ψ ∈ λ (s i (q)) (A7 ′ ) → [ {}] ψ ∈ λ (s i (q)). Together with the above it means that {}([ ]¬ψ ∧ ψ) → {} (¬ψ ∧ ψ) (A2),(A2 ′ ) −→ ⊥ ∈ λ (s i (q)) which is a contradiction with the fact that λ (s i (q)) is an atom. The second case is when ¬ψ has been added in a previous iteration, i.e., [ {}]¬ψ ∈ λ (s j (t k+1 (q))) with 1 ≤ j < i. But this means that each of these two cells must have at least one s map and enter the cubical law s j (s i (t k+1 (q))) = s i−1 (s j (t k+1 (q))) = q ′′ . By the canonicity of these lower cells (A2) → ⊥ ∈ λ (q ′′ ) which is a contradiction. The application of addTargetMap in the second loop uses the S3 set also and we are looking at cubical laws of type t i (t k+1 (q)) = t n (t i (q)) where S2 = λ (t i (q)) and S3 = λ (t k+1 (q)). Assume, for the sake of contradiction, that we have [ ]ψ ∈ λ (t k+1 (q)) and [ ]¬ψ ∈ λ (t i (q)). By canonicity it means that [ ]ψ ∈ λ (q) and [ ]¬ψ ∈ λ (q) and from axiom (A6) we have [ ] ¬ψ ∈ λ (q). This means that [ ] ¬ψ ∧ [ ]ψ → ( ¬ψ ∧ [ ]ψ) → (ψ ∧ ¬ψ) (A2 ′ ) → ⊥ ∈ λ (q) which is a contradiction. Lemma A.21. For the enrich algorithm of Lemma A.19 all the new existential constraints that are added to the fresh cells or to cells from the old HDA are consistent with the set constraints of that cell.
Proof. Assume that for the lifted HDA the second canonicity condition is broken; i.e., consider q ∈ Q n and assume t i (q) = q ′ for which ϕ ∈ λ (q ′ ) and ϕ ∈ λ (q), which is the same as ¬ ϕ ∈ λ (q). We take cases after q.
First, clearly, if q, q ′ ∈ H (meaning that 1 ≤ i ≤ n − 1) then the canonicity is assured by the statement of the lemma (i.e., H is canonical).
Second, q ∈ H and q ′ is added by addTargetMap as the new cell linked to q by t n (q) = q ′ . Now we take sub-cases depending on where does the ϕ formula come from.
• If ϕ ∈ S1; this is the case when q is the initial cell from the statement of the lemma and hence it cannot be that ¬ ϕ ∈ λ (q).
• If ϕ ∈{ϕ | [ ]ϕ ∈S3} then q ′ is added by the second call to addTargetMap, which means that we are respecting the cubical laws t i (t k+1 (q k+1 )) = t k (t i (q k+1 )), for 1 ≤ i ≤ k and for some q n+1 for which our q = t i (q k+1 ).
Then by the construction of the label it means that [ ]ϕ ∈ λ (t k+1 (q k+1 )) which by the canonicity of these upper cells it means that [ ]ϕ ∈ λ (q k+1 ). By axiom (A6) it means that [ ] ϕ ∈ λ (q k+1 ) and thus, by the canonicity it means that ϕ ∈ λ (q) which is a contradiction with our initial assumption as the labels are atoms and hence ¬ ϕ cannot be in the label λ (q).
• Lastly, assume that ϕ is one of the formulas accumulated in the label of q ′ as a result of the first loop of addTargetMap. This means that we are respecting the cubical laws s i (t k+1 (q)) = t k (s i (q)) and [ {}]ϕ ∈ λ (s i (q ′ )) = λ (s i (t k+1 (q))) = λ (t k (s i (q))). By canonicity of the other cells it means that [ {}]ϕ ∈ λ (s i (q)) which by axiom (A7') it means that [ {}] ϕ ∈ λ (s i (q)). By canonicity again it means that ϕ ∈ λ (q) which is again a contradiction with our initial assumption.
Third, both q and q ′ are newly added by addTargetMap, meaning that we are looking at the second loop. The proof is the same as before as the construction of the label and axiom (A6) do all the work.
Forth, both q and q ′ are newly added by addSourceMap, which means that we are in the first loop of addSourceMap and there exists a q k+1 with s k+1 (q k+1 ) = q and t i (s k+1 (q k+1 )) = q ′ = s k (t i (q k+1 )) for some i. By the construction of the label of s k+1 (q k+1 ), i.e., λ (q), we have that for our formula ϕ ∈ λ (q ′ ) there exists ϕ ∈ λ (q) because these are added in the label of q in the i step of the loop.
Consider that q ∈ H and q ′ is added by the function addSourceMap. This may be done either in the first or in the second loop, but in any of the cases the construction of the labels ensures that if ϕ ∈ λ (q) then {}ϕ ∈ λ (q ′ ). The same holds for the case when both q and q ′ are newly added by the second call to addSourceMap (in the second loop).
Consider the case when both q and q ′ are newly added by the first call to the function addTargetMap. Our initial assumption says that [ {}]¬ϕ ∈ λ (q ′ ) which means, by the iterative construction of the label of q in the loop, that ¬ϕ ∈ λ (q) which is a contradiction with our initial assumption that ϕ ∈ λ (q).
By now we are sure that the labeling of H ′ is canonical.
Lemma A.22. A finite HDA H that is potential canonical can be transformed into a canonical HDA by revealing one labeling that conforms with the potential labeling; this will be canonical. Moreover the way we generate this specific labeling does not introduce defects.
Proof. Start with the cell that has no existential constraints, but only set constraints. These being consistent sets they can be grown to an atom. Depending on this atom build the rest of the atoms s.t. the existential constraints are respected. This can always be done. In a finite HDA built using the two enrich and lift constructions starting from the minimal potential canonical HDA as is done in the proof of Theorem A.24 there always exists a cell with no existential constraints. Order the cells wrt. the number of existential constraints that they have. Use this order when building the labeling.
Lemma A.23 (repair lemma). For any canonical HDA H that has a defect we can build a corresponding H ′ which is canonical and does not have this defect.
Proof. Consider that the canonical H from the statement has a defect of type D1. Apply the enriching construction to H wrt. the defective cell q n and the formula ψ (where {}ψ ∈ λ (q n )). The enriching lemma ensures that the new model H ′ extends H and is canonical. The enriched model H ′ does not have the defect that H had.
Consider that the canonical H from the statement has a defect of type D2. Apply the lifting construction to H wrt. the defective cell q n (for which ψ ∈ λ (q n )), to obtain, cf. lifting lemma, a canonical H ′ that extends H . It is clear that the new model does not have the defect that H had.
Proof. Using the truth lemma A.8 for pseudo canonical and saturated HDAs, the proof amounts to showing that for any consistent formula ϕ we can build a pseudo canonical saturated H ϕ that has a cell labeled with an atom that contains ϕ. We construct H ϕ in steps starting with H 0 ϕ which contains only one cell q 0 0 of dimension 0. The construction is done in two stages: in the first stage we label the cells with constraints (i.e., we use a potential labeling); and in the second stage we explicit these constraints into corresponding atoms (i.e., we transform the potential labeling into a real labeling). The first stage builds the actual finite HDA, H ϕ , labeling it with a potential canonical labeling, striving to repair all the defects in the constraints of the cells. The final H ϕ is defect-free. Any finite H ϕ has a cell which will have no existential constraints. We start from this cell to explicit the potential labeling into atoms for each cell. During this second phase only the labels of the H ϕ are affected; i.e., they are transformed into atoms consistent with the potential labeling. This construction does not destroy the property of pseudo canonicity of the model H ϕ that we started with. Moreover, it does not introduce defects. Therefore, in the end we are left with the finite, defect-free and pseudo canonical HDA that we were looking for, where the label of the initial cell contains the initial formula.
Start by labeling q 0 0 with set constraints containing ϕ and all other formulas it implies, i.e.,λ (q 0 0 ) = {ϕ} ∪ {ψ | ϕ → ψ}. Trivially, H 0 ϕ is canonical, hence also pseudo canonical and the potential labeling is potential canonical. For each defect in the potential labelλ (q 0 0 ), i.e., in the set constraints, we apply the repair lemma to obtain a new HDA which does not contain the repaired defect, extends the old defective HDA, does not introduce new defects into the just repaired potential labelλ (q 0 0 ) (it may introduce new defects in the new cells), and is pseudo canonical. The algorithm continues repairingλ (q 0 0 ) until all defects are removed. It then continues to repair the new cells in the order that they were added, also respecting the order given below. Note that any atom that is consistent with {ϕ} is also consistent with {ψ | ϕ → ψ}.
The cells used to construct our model are picked (in the right order) from the following sets S i = {q j i | j ∈ ω} where i ∈ ω corresponds to the dimension i. Any of these cells may have defects and thus, we list all the defects, i.e., all the cells, and try to repair them in increasing order (i.e., we treat first defects on level 0 and continue upwards).
Proof. Using the truth lemma A.4, the proof amounts to showing that for any consistent formula ϕ we can build a canonical saturated H ϕ that has a cell labeled with an atom that contains ϕ. We construct H ϕ in steps starting with H 0 ϕ which contains only one cell q 0 0 of dimension 0 labeled with an atom containing ϕ, i.e., λ (q 0 0 ) = A ϕ .
Trivially, H 0 ϕ is canonical. The cells used to construct our model are picked (in the right order) from the following sets S i = {q j i | j ∈ ω} where i ∈ ω corresponds to the dimension i. Any of these cells may have defects and thus, we list all the defects, i.e., all the cells, and try to repair them in increasing order (i.e., we treat first defects on level 0 and continue upwards).
At some step n ≥ 0 in the construction we consider H n ϕ = (Q n , s n ,t n , l n ) canonical. If H n ϕ is not saturated then pick the smallest defect cell of H n ϕ . For a D1 defect, i.e., a cell q k ∈ Q k and formula {}ψ ∈ λ (q k ), apply enrich (k,q k ,ψ) and obtain a model H n+1 ϕ which is canonical, cf. Lemma A.13, and does not have the D1 defect, cf. Lemma A.23. For a D2 defect apply the lifting construction to remove the defect. Moreover, any repaired defect will never appear in any extension model, independent of how many times we apply the enriching or lifting constructions. Both enriching and lifting pick their new cells from S in increasing order. We obtain H ϕ as a limit construction from all the H n ϕ ; i.e., H ϕ = (Q, s,t, l) as Q = n∈ω Q n , s = n∈ω s n , t = n∈ω t n , l = n∈ω l n .