Modal Logic over Higher Dimensional Automata^{⋆}

Cristian Prisacariu

Dept. of Informatics, Univ. of Oslo, P.O. Box 1080 Blindern, N-0316 Oslo, Norway.

                            cristi@ifi.uio.no

Abstract. 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 a complete 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 can be restricted to LTrL (the linear time temporal logic over Mazurkiewicz traces).

1 Introduction

Higher dimensional automata (HDAs) are a general formalism for modeling concurrent systems [14,21]. 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. 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 [15] do a fairly good job [17].

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 [9] and strong results like decidability and expressive completeness are known [5, 20]. For general partial orders, temporal logics usually become undecidable [2]. For the more expressive event structures there are fewer works; a modal logic is investigated in [6].

There is hardly any work on logics for higher dimensional automata [17] 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).

⋆ The appendix is for reviewing purpose only and should not be regarded as part of the paper; it contains the full proofs for all the results. 0 A technical report of this paper, containing proofs and more explanations, appeared as [18].

2  C. Prisacariu

PSfrag replacements q_{0}^{1}

q_{0}^{4}
q_{0}^{3}
q_{0}^{2}
a
b
a
b
q_{2}

Fig. 1. Example of a HDA with two concurrent events.

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 filtration argument. 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 [7] 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 [7].

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 an Until operator, in the style of temporal logics. We show how this variant of HDML, when interpreted over the class of HDAs corresponding to Kripke structures, can be particularized to LTL [11]. A second variant, in Section 3.3, decorates the HDML modalities with labels. This multi-modal variant of HDML together with the Until operator, when interpreted over the class of HDAs that encodes Mazurkiewicz traces, becomes LTrL [20] (the linear time temporal logic over Mazurkiewicz traces).

2 Modal Logic over Higher Dimensional Automata

In this section we define a higher dimensional automaton (HDA) following the definition and terminology of [17,21]. 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 [17, 21] 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_{0}^{1} to q_{0}^{4}, 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_{0}^{3} both events have finished, whereas in state q_{0}^{1} 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, \overline{s}, \overline{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}.  (1)

In H, the \overline{s} and \overline{t} denote the collection of all the maps from all the families (i.e., for all n). A higher dimensional structure (Q, \overline{s}, \overline{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, \overline{s}, \overline{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 configuration 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 configuration of the system before the starting of the i^{th} event, whereas the target cell t_{i}(q) represents the configuration of the system immediately after the termination of the i^{th} event. A transition of Q_{1} represents a configuration 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_{0}^{1}, q_{0}^{2}) and the first target cell of q_{1}^{1} is q_{0}^{2} (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_{1}^{2} = (q_{0}^{2}, q_{0}^{3}) and the first source of q_{1}^{2} is q_{0}^{2}.

We propose the language of higher dimensional modal logic for talking about concurrent systems. HDML follows the tradition and style of standard modal languages [3].

1 Later, in Definition 3.12, the labeling is extended naturally to all cells.

H, q ⊧ ϕ  iff ϕ ∈ V(q).
H, q |̸= ⊥
H, q ⊧ φ_{1} → φ_{2} iff when H, q ⊧ φ_{1} then H, q ⊧ φ_{2}.
H, q ⊧ {}φ  iff assuming q ∈ Q_{n} for some n,

∃q′ ∈ Q_{n+1} s.t.s_{i}(q′) = q for some 1 ≤ i ≤ n, and H, q′ ⊧ φ.

H, q ⊧ ⟨⟩φ  iff assuming q ∈ Q_{n} for some n,

∃q′ ∈ Q_{n−1} s.t.t_{i}(q) = q′ for some 1 ≤ i ≤ n, and H, q′ ⊧ φ. Table 1. Semantics for HDML.

Definition 2.2 (higher dimensional modal logic). A formula φ in higher dimensional modal logic is constructed using the grammar below, from a set Φ_{B} of atomic propositions, with ϕ ∈ Φ_{B}, which are combined using the propositional symbols ⊥ and → (from which all other standard propositional operations are generated), and using the modalities {} and ⟨⟩.

φ := ϕ | ⊥ | φ → φ | {}φ | ⟨⟩φ

We call {} the during modality and ⟨⟩ the terminate modality. The intuitive reading of {}φ is: “pick some event from the ones currently not running (must exist at least one not running) and start it; in the new configuration of the system (during which, one more event is concurrently executing) the formula φ must hold”. The intuitive reading of ⟨⟩φ is: “pick some event from the ones currently running concurrently (must exist one running) and terminate it; in the new configuration of the system the formula φ must hold”. This intuition is formalized in the semantics of HDML.

The choice of our notation is biased by the intuitive usage of these modalities where the terminate modality talks about what happens after some event is terminated; in this respect being similar to the standard diamond modality of dynamic logic. Later, in Section 3.3, these modalities are decorated with labels. The during modality talks about what happens during the execution of some event and hence we adopt the notation of Pratt [12].

The models of HDML are higher dimensional structures together with a valuation function V : Q → 2^{Φ_{B}} which associates a set of atomic propositions to each cell (of any dimension). This means that V assigns some propositions to each state of dimension 0, to each transition of dimension 1, to each square of dimension 2, to each cube of dimension 3, etc. Denote a model of HDML by H = (Q, s, t, l, V). A HDML formula is evaluated in a cell of such a model H.

One may see the HDML models as divided into levels, each level increasing the concurrency complexity of the system; i.e., level Q_{n} increases the complexity compared to level Q_{n−1} by adding one more event (to have n events executing concurrently instead of n − 1). The levels are linked together through the s_{i} and t_{i} maps. With this view in mind the during and terminate modalities should be understood as jumping from one level to the other; the {} modality jumps one level up, whereas the ⟨⟩ modality jumps one level down.

Definition 2.3 (satisfiability). Table 1 defines recursively the satisfaction relation ⊧ of a formula φ w.r.t. a model H in a particular n-cell q (for some arbitrary n); denote this as H, q ⊧ φ. The notions of satisfiability and validity are defined as usual.

Both modalities have an existential flavor. In particular note that H, q_{0} |̸= ⟨⟩φ, for q_{0} ∈ Q_{0} a state, because there is no event executing in a state, and thus no event can be terminated. Similarly, for the during modality, H, q_{n} |̸= {}φ for any n-cell q_{n} ∈ Q_{n} when all sets Q_{k}, with n < k, are empty (i.e., the family of sets Q is bounded by n). This says that there can be at most n events running at the same time, and when reaching this limit one cannot start another event and therefore {}φ cannot be satisfied.

The universal correspondents of {} and ⟨⟩ are defined in the standard style of modal logic. We denote these modalities by respectively [{}]φ and [ ]φ. The intuitive reading of [ ]φ is: “pick any of the events currently running concurrently and after terminating it, φ must hold in the new configuration of the system”. Note that this modality holds trivially for any state q_{0} ∈ Q_{0}, i.e., H, q_{0} ⊧ [ ]φ.

2.1 Decidability and completeness

In the rest of this section we prove that satisfiability for HDML is decidable using the filtration technique [3]. Then we give an axiomatic system for HDML and prove its soundness and completeness. Completeness is based on constructing canonical models.

The filtration for the states is the same as in the standard modal logic, but for cells of dimension at least 1 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.10) is more involved due to the complexities of the definition of filtration given in Definition 2.5.

Definition 2.4 (subformula closure). The subformula closure of a formula φ is the set of formulas C(φ) defined recursively as:

\begin{matrix}C(ϕ) & =^{△} & \{ϕ\}, for ϕ ∈ Φ_{B} \\ C(φ_{1} → φ_{2}) & =^{△} & \{φ_{1} → φ_{2}\} ∪ C(φ_{1}) ∪ C(φ_{2}) \\ C(\{\}φ) & =^{△} & \{\{\}φ\} ∪ C(φ) \\ C(⟨⟩φ) & =^{△} & \{⟨⟩φ\} ∪ C(φ) \end{matrix}

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.) The size of the subformula closure of a formula φ is linear in the size of the formula, |C(φ)| ≤ |φ|.

Definition 2.5 (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 ∈ ℕ:

q ≡ q′ iff for anyψ ∈ C(φ) then (H, q ⊧ ψ iffH, q′ ⊧ ψ).

A filtration model H^{f} of H through the closure set C(φ) is a structure (Q^{f}, s^{f}, t^{f}, l^{f}, V^{f}):

Q_{n}^{f} =^{△} {[q_{n}] | q_{n} ∈ Q_{n}}, where [q_{n}] is
[q_{0}] =^{△} {q′ | q_{0} ≡ q′} when q_{0} ∈ Q_{0}, otherwise,
[q_{n}] =^{△} {q′ | q_{n} ≡ q′ ∧ t_{i}(q′) ∈ [p_{i}] ∧ s_{i}(q′) ∈ [p′_{i}]
for all 1 ≤ i ≤ n and for some fixed [p_{i}], [p′_{i}] ∈ Q_{n−1}^{f}}.
s_{i}^{f}([q_{n}]) =^{△} [q_{n−1}] iff for all p ∈ [q_{n}], s_{i}(p) ∈ [q_{n−1}].
t_{i}^{f}([q_{n}]) =^{△} [q_{n−1}] iff for all p ∈ [q_{n}], t_{i}(p) ∈ [q_{n−1}].
V^{f}([q]) =^{△} V(q).

Proposition 2.6 (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 (sketch). Essentially, the proof amounts to showing that the definitions of s_{i}^{f} and t_{i}^{f} are that of maps (as required in a higher dimensional structure) and that they respect the cubical laws (see full proof as Lemma A.3).

Lemma 2.7 (sizes of filtration sets). Each set Q_{n}^{f} of the filtration H^{f} obtained in Definition 2.5 has finite size which depends on the size of the formula φ used in the filtration; more precisely each Q_{n}^{f} is bounded from above by 2^{|φ|·N} where N = n! · ∑_{k=0}^{n} \frac{2^{k}}{(n−k)!}.

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_{0}^{f}. Each of the 2^{|φ|} equivalence classes in which Q_{1}^{f} 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_{0}^{f}, 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 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_{n−1}^{f}. Thus we get a maximum of 2^{|φ|} · (|Q_{n−1}^{f}|)^{2·n} subdivisions. Calculating this series gives the bound on the size of Q_{n}^{f} as being 2^{|φ|·N} where N = n! · ∑_{k=0}^{n} \frac{2^{k}}{(n−k)!}.

Lemma 2.8 (filtration lemma). Let H^{f} be the filtration of H through the closure set C(φ), as in Definition 2.5. For any formula ψ ∈ C(φ) and any cell q ∈ H, we have H, q ⊧ ψ iff H^{f}, [q] ⊧ ψ.

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:

\begin{matrix}|⊥|_{uc} =^{△} |ϕ|_{uc} & =^{△} & 0, for ϕ ∈ Φ_{B} \\ |φ_{1} → φ_{2}|_{uc} & =^{△} & max(|φ_{1}|_{uc}, |φ_{2}|_{uc}) \\ |\{\}φ|_{uc} & =^{△} & 1 + |φ|_{uc} \\ |⟨⟩φ|_{uc} & =^{△} & max(0, |φ|_{uc} − 1) \end{matrix}

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.9 (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.

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 ∈ ℕ^{∗} 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 φ.

Theorem 2.10 (small model property). If a HDML formula φ is satisfiable then it is satisfiable on a finite model with no more than ∑_{n=0}^{|φ|} 2^{|φ|·N} cells where N = n! · ∑_{k=0}^{n} \frac{2^{k}}{(n−k)!} .

Proof. Note first that it is easy to prove that any formula ⟨⟩i → ⟨⟩^{i}⊤ is valid, for any i ∈ ℕ^{∗}. Because of this, the downwards concurrency measure for a formula may be misleading as |⟨⟩i|_{dc} = 1 whereas |⟨⟩^{i}⊤|_{dc} = i. On the other hand the dimension |⟨⟩i| grows faster than linear with i. It is easy to see that |⟨⟩i| > |⟨⟩^{i}⊤|_{dc}. If our formula φ has subformulas of the kind |⟨⟩i|_{dc} then the measure |φ|_{dc} must be adjusted accordingly. In any case, it is clear that even after adjustment |φ|_{dc} ≤ |φ| − |φ|_{uc}.

Assume that there exists a model H and a cell q ∈ Q_{l} in this model for which H, q ⊧ φ. We can prove, analogous to the proof of Lemma 2.9, that for a formula φ one needs to look at cells of dimension at least |φ|_{dc}. A more coarse approximation is to say that one needs all the sets Q_{n} with n ≤ |φ| − |φ|_{uc}. Thus, we can safely assume l ≤ |φ| − |φ|_{uc}.

From Lemma 2.9 we know that we need to consider only the sets Q_{m} for m ≤ l + |φ|_{uc} ≤ |φ|, and all other sets Q are empty. From Lemma 2.8 we know that we can build a filtration model H^{f} s.t. the formula φ is still satisfiable and, by Lemma 2.7, we know that all the sets Q_{m}^{f} have a finite number of cells. Thus we can sum up all the cells in all the Q_{m}^{f}, with m ≤ |φ|.

Corollary 2.11 (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.10.

In the following we go on giving an axiomatic system for HDML and prove it sound and complete. 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.

Theorem 2.12 (soundness). The axiomatic system of Table 2 is sound. Formally ∀φ : ⊢ φ ⇒ ⊧ φ.

Proof (sketch). The proof tests that all axioms are valid and that all inference rules preserve validity. We check only the non-standard axioms (A5) to (A9’).

We fix now some terminology and notation. Denote by ¬C(φ) = C(φ) ∪ {¬φ′ | φ′ ∈ C(φ)} the set of subformulas, as in Definition 2.4, 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 φ. Atoms are sets of formulas which are free of immediate propositional inconsistencies (like ϕ ∧ ¬ϕ).

Axiom schemes: (A1) All instances of propositional tautologies.

(A2) {}⊥ ↔ ⊥  (A2’) ⟨⟩⊥ ↔ ⊥
(A3) {}(φ ∨ φ′) ↔ {}φ ∨ {}φ′ (A3’) ⟨⟩(φ ∨ φ′) ↔ ⟨⟩φ ∨ ⟨⟩φ′
(A4) [{}]φ ↔ ¬{}¬φ  (A4’) [ ]φ ↔ ¬⟨⟩¬φ
(A5) ⟨⟩i → ⟨⟩^{i}⊤ ∀i ∈ ℕ^{∗}  (A5’) {}^{i}⊤ → {}i ∀i ∈ ℕ^{∗}
(A6) ⟨⟩[ ]φ → [ ]⟨⟩φ  (A6’) {}[{}]φ → [{}]{}φ
(A7) {}[ ]φ → [ ]{}φ  (A7’) ⟨⟩[{}]φ → [{}]⟨⟩φ
(A8) {}⟨⟩^{i}⊤→ [{}]⟨⟩^{i}⊤ ∀i ∈ ℕ (A8’) ⟨⟩⟨⟩^{i}⊤→ [ ]⟨⟩^{i}⊤ ∀i ∈ ℕ
(A9) ⟨⟩^{i}⊤→ [{}]⟨⟩⟨⟩^{i}⊤ ∀i ∈ ℕ  (A9’) {}⟨⟩⟨⟩^{i}⊤→ ⟨⟩^{i}⊤ ∀i ∈ ℕ

Inference rules:

(R1) φ  φ → φ′ ; \overline{(MP)} ; φ′  (R2) φ → φ′ ; \overline{(D)} ; \{\}φ → \{\}φ′  (R2’) φ → φ′ ; \overline{(D)} ; ⟨⟩φ → ⟨⟩φ′
(R3) Uniform variable substitution.

Table 2. Axiomatic system for HDML.

Lemma 2.13 (properties on atoms). Standard results for atoms tell us that for some formula φ and any atom A ∈ At(φ) then we have that: (i). for all ψ ∈ ¬C(φ) then only one of ψ or ¬ψ are in A; (ii). for all ψ → ψ′ ∈ ¬C(φ) then ψ → ψ′ ∈ A iff whenever ψ ∈ A then ψ′ ∈ A; (iii). if ψ ∈ ¬C(φ) and ψ is consistent then there exists an A ∈ At(φ) s.t. ψ ∈ A; (This

is an analog of Lindenbaum’s Lemma.) (iv). any consistent set of formulas S ⊆ ¬C(φ) can be grown to an atom A_{S} ∈ At(φ).

Definition 2.14 (canonical saturated HDA). A HDA is called canonical for the formula φ if a canonical labeling λ : Q → At(φ) can be attached to the HDA. A labeling is canonical if the following conditions hold:

1. for any q_{n} ∈ Q_{n}, q_{n−1} ∈ Q_{n−1}, for some n > 0, and ∀0 ≤ i ≤ n, if s_{i}(q_{n}) = q_{n−1} then ∀ψ ∈ ¬C(φ) if ψ ∈ λ(q_{n}) then {}ψ ∈ λ(q_{n−1}),

2. for any q_{n} ∈ Q_{n}, q_{n−1} ∈ Q_{n−1}, for some n > 0, and ∀0 ≤ i ≤ n, if t_{i}(q_{n}) = q_{n−1} then ∀ψ ∈ ¬C(φ) if ψ ∈ λ(q_{n−1}) then ⟨⟩ψ ∈ λ(q_{n}).

A canonical HDA is called saturated if:

1. whenever {}ψ ∈ λ(q_{n−1}) then ∃q_{n} ∈ Q_{n} and ∃0 ≤ i ≤ n s.t. s_{i}(q_{n}) = q_{n−1} and ψ ∈ λ(q_{n}),

2. whenever ⟨⟩ψ ∈ λ(q_{n}) then ∃q_{n−1} ∈ Q_{n−1} and ∃0 ≤ i ≤ n s.t. t_{i}(q_{n}) = q_{n−1} and ψ ∈ λ(q_{n−1}).

Lemma 2.15 (truth lemma). In a canonical saturated HDA H with the valuation defined as V(q_{n}) = {ϕ ∈ Φ_{B} | ϕ ∈ λ(q_{n})}, it holds that H, q_{n} ⊧ ψ iff ψ ∈ λ(q_{n}).

To prove completeness of the axiomatic system all that remains is to show that for any consistent formula φ we can build such a canonical saturated HDA. While building the canonical saturated HDA we constantly struggle to saturate the HDA (that we work with) while respecting the 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 canonical HDA we can incrementally build a defect free canonical HDA.

Definition 2.16 (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}).

For two HDAs, H_{1} and H_{2} we say that H_{2} extends H_{1} (written H_{2} ▷ H_{1}) iff H_{2} has all the cells (with the same labels) and maps of H_{1} and possibly some new cells and maps (i.e., some extra structure).

Lemma 2.17 (enriching construction). For a canonical model H, there exists a construction (see Appendix), which we call enriching of the H w.r.t. q and a formula {}φ ∈ λ(q), builds a model H′ which is canonical and extends H (i.e., H′ ▷ H).

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 following lifting construction lifts all the cells of each level one level up by adding one new s and t map to each. 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 extended H′.

Lemma 2.18 (lifting construction). For a canonical model H, there exists a construction (see Appendix), which we call lifting of the H w.r.t. q and a formula ⟨⟩φ ∈ λ(q), builds a model H′ which is canonical and extends H (i.e., H′ ▷ H).

Lemma 2.19 (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 w.r.t. 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. It is clear that 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 w.r.t. 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.

Theorem 2.20 (completeness). The axiomatic system of Table 2 is complete. Formally ∀φ : ⊧ φ ⇒ ⊢ φ.

Proof. Using the truth lemma 2.15, 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_{i}^{j} | 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}, \overline{s^{n}}, \overline{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 2.17, and does not have the D1 defect, cf. Lemma 2.19. 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, \overline{s}, \overline{t}, l) as Q = ⋃_{n∈ω} Q^{n}, \overline{s} = ⋃_{n∈ω} \overline{s^{n}}, \overline{t} = ⋃_{n∈ω} \overline{t^{n}}, l = ⋃_{n∈ω} l^{n}.

3 Examples of Encodings into Higher Dimensional Modal Logic

This section serves to exemplify two main ways of using HDML. One usage is as a highly expressive logic in which many other logics for different concurrency models can be encoded; in this respect we study the relation of HDML with standard modal logic, LTL, and with linear time temporal logic over Mazurkiewicz traces LTrL. The other usage is as a general theoretical framework for studing different logics for different concurrency models (that can be expressed as some class of HDA) and their interrelation. This is done by finding the apropriate restrictions of HDA and HDML and investigating their relations in HDML.

3.1 Encoding standard modal logic into HDML

Lemma 3.1 (Kripke structures). The class of Kripke structures is captured by the class of higher dimensional structures where all sets Q_{n}, for n > 1, are empty.

Proof. Essentially this result is found in [21]. A HDA K = (Q_{0}, Q_{1}, s_{1}, t_{1}, l) is a special case of HDAs where all Q_{n} = ∅ 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 (Q_{0}, Q_{1}, s_{1}, t_{1}, l, V).

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 (sketch). For any HDA H and any q ∈ Q a cell of any dimension, we prove the double implication: H, q ⊧ ¬⟨⟩⊤ → [{}][{}]⊥ iff H is as in Lemma 3.1.

Theorem 3.3 (standard modal logic). Consider the syntactic definition ♢φ =^{△} {}⟨⟩φ. The language of standard modal logic uses only ♢ and is interpreted only over higher dimensional structures as defined in Lemma 3.1 and only in cells of Q_{0}.

Proof (sketch). First we check that we capture exactly the semantics of standard modal logic. Second we check that we recover the axiomatic system of standard modal logic for ♢ from the axiomatic system of HDML.

3.2 Adding an Until operator and encoding LTL

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 [3] and thus is expressible in HDML too. It is known that the Until operator U adds expressivity to LTL (eventually and always operators can be encoded with U but not the other way around).

The Until operator cannot be encoded in HDML because of the local behavior of the during and terminate modalities; similar arguments as in modal logic about expressing U 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 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_{n−1} ⟶^{s_{i}} q_{n} with

s_{i}(q_{n}) = q_{n−1} or q_{n} ⟶^{t_{i}} q_{n−1} with t_{i}(q_{n}) = q_{n−1}, where q_{n} ∈ Q_{n} and q_{n−1} ∈ Q_{n−1}

and 1 ≤ i ≤ n. A path π =^{△} q^{0} ⟶^{α^{0}} q^{1} ⟶^{α^{1}} q^{2} ⟶^{α^{2}} … is a sequence of single steps

q^{j} ⟶^{α^{j}} q^{j+1}, with α^{j} ∈ {s_{i}, t_{i}}. 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(π).

In the same spirit as done for temporal logic we boost the expressivity of HDML by defining an U operator over higher dimensional structures. Using this operator we can encode the standard Until operator of LTL.

Definition 3.5 (Until operator). Define an Until operator φ U φ′ which is interpreted over a HDA in a cell as below:

H, q ⊧ φ U φ′ iff ∃π ∈ H s.t. st(π) = q ∧ en(π) = q′,
H, q′ ⊧ φ′, and ∀q′′ ∈ π, q′′ ≠ q′ then H, q′′ ⊧ φ.

Proposition 3.6 (modeling LTL). The LTL Until modality is encoded syntactically by φ \overline{U} φ′ =^{△} (φ∨⟨⟩⊤) U (φ′ ∧¬⟨⟩⊤) when \overline{U} is interpreted only in states of Kripke HDAs as in Lemma 3.1.

3.3 Partial order models and their logics in HDML

This section is mainly concerned with Mazurkiewicz traces [8] as a model of concurrency based on partial orders, because of the wealth of logics that have been developed for it [9,20]. Higher dimensional automata are more expressive than most of the partial orders models (like Mazurkiewicz traces, pomsets [13], or event structures [10]) as studied in [16, 21]. The works of [16, 17, 21] 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 [19]. 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 [4, 20]) and over general partial orders (like ISTL of [1]).

Definition 3.7 (partial orders). A partially ordered set (or poset) is a set E equipped with a partial order ≤, (E, ≤). The history of an element e ∈ E (denoted ↓e) is ↓e = {e′ | e′ ≤ e}. The notion of history is extended naturally to a set of elements C ⊆ E (denoted ↓C). A configuration is a finite and history closed set of elements (i.e., C =↓C). Denote by C the set of all configurations. The immediate successor relation ⋖ ⊆ E×E is defined as e ⋖ e′ iff e ≠ e′ and e ≤ e′ and ∀e′′ ∈ E, e ≤ e′′ ≤ e′ implies e = e′′ or e′ = e′′. A Σ-labeled poset (E, ≤, λ) is a poset with a labeling function λ : E → Σ which maps each element to a label from Σ. Define a transition relation on the configurations of a labeled poset as ⟶⊆ C × Σ × C given by C ⟶^{a} C′ iff ∃e ∈ E s.t. λ(e) = a and e ∉ C and C′ = C ∪ {e}.

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.

Definition 3.8 (Mazurkiewicz traces). Consider a symmetric irreflexive independence relation I ⊆ Σ × Σ and its complement D = Σ × Σ \ I, called the dependence relation. Mazurkiewicz traces are labeled posets restricted by the independence relation as follows:

∀e ∈ E, ↓e is finite,
∀e, e′ ∈ E, e ⋖ e′ ⇒ (λ(e), λ(e′)) ∈ D,
∀e, e′ ∈ E, (λ(e), λ(e′)) ∈ D ⇒ e ≤ e′ or e′ ≤ e.

Definition 3.9 (event structures). Consider a symmetric irreflexive relation # ⊆ E × E. This conflict relation is added to a poset to form an event structure (E, ≤, # ) where the following restrictions apply:

∀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:

co = E × E \ ( # ∪ ≤ ∪ ≤^{−1}).

Proposition 3.10 (families of configurations). A finitary event structure (E, ≤, # ) is uniquely determined by its family of configurations C_{E} (denoted (E, C_{E})).

Proof (sketch). This result is found in [17]. 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.9).

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.11 (traces as event structures). Any Mazurkiewicz trace, as in Definition 3.8, corresponds to a trace configuration structure, which is a labeled event structure (E, C_{E}, λ) 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

∀a, b ∈ Σ, (λ^{−1}(a) × λ^{−1}(b)) ∩ co ≠ ∅ ⇒ (λ^{−1}(a) × λ^{−1}(b)) ∩ ⋖ = ∅ .

Proof (sketch). This result is essentially found in [9, 19]. We remind how one gets the independence relation of a Mazurkiewicz trace from a trace configuration structure:

I = {(a, b) | (λ^{−1}(a) × λ^{−1}(b)) ∩ co ≠ ∅}.

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 [16,17]. 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, \frac{1}{2}, 1\}, where \frac{1}{2} means executing. The set of three values is linearly ordered 0 < \frac{1}{2} < 1 to obtain an acyclic HDA [17], and all cells of 3^{E} (i.e., the configurations) are ordered by the natural lifting of this order pointwise. The dimension of a cell is equal to the number of \frac{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, \frac{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}.^{2} By Proposition 3.10 we can reconstruct the event structure.

In Definition 2.3 the interpretation of the during and terminate 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.13. But first we show how the labeling extends to cells of any dimension.

Definition 3.12 (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} \frac{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 \frac{1}{2}.

As is the case with multi-modal logics or propositional dynamic logics, 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.

2 We remove also all those cells of higher dimension that are connected with the 0-dimensional cells that we have removed.

Definition 3.13 (labeled modalities). Consider two labeled modalities during {a}φ and terminate ⟨a⟩φ where a ∈ Σ is a label from a fixed alphabet. The interpretation of the labeled modalities is given below:

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 {}φ =^{△} ⋁_{a∈Σ}{a}φ.

In the remaining of this section we show how the LTrL logic of [20] is captured in the higher dimensional framework. This logic, as well as those presented in [4, 9], are interpreted in some particular configuration of a Mazurkiewicz trace (or of a partial order). We take the view of Mazurkiewicz traces as restricted labeled posets from Proposition 3.8 but we use their representation using their corresponding family of configurations as in Proposition 3.11. Therefore, we now interpret HDML over restricted HDAs as we discussed above.

Proposition 3.14 (encoding LTrL). The language of LTrL consists of the propositional part of HDML together with the syntactic definitions of the Until operator \overline{U} from Definition 3.6 and \overline{⟨a⟩}φ =^{△} \{a\}⟨a⟩φ for 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 [20]

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 [20]. 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 \overline{⟨a⟩}φ has the same interpretation as the one in [20]. The proof is similar to the proof of Theorem 3.3. The Until operator of [20] has the same definition as the one in standard LTL and thus we use the one defined in Proposition 3.6; the proof is easily adapted to the Mazurkiewicz traces setting.

4 Conclusion

We have introduced a modal logic called HDML which is interpreted over higher dimensional automata. According to our knowledge, this has not been done before. 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 extra only few natural axioms related to the cubical laws and to the dimensions of HDAs. This system was proven to be complete for 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 extended the expressiveness of HDML by defining an Until operator over HDAs. Using this Until operator, the LTL was encoded into HDML when interpreted over the Kripke HDAs.

As future work we are investigating a tableaux system for HDML. We are also trying to understand better the relation of HDML with other logics for weaker models of concurrency like with the modal logic of [6] for event structures or other logics for Mazurkiewicz traces. Particularly interesting is how our results relate to the undecidability results of [2] or to the logic of [1].

Regarding the expressiveness of HDML, our current work focuses on finding the kind of bisimulation that is characterized by HDML (and its extensions from Section 3). Standard bisimulations for concurrent systems like ST-bisimulation or split-bisimulation are not characterized by HDML because of the during modality and the “during” behaviour of HDML.

Acknowledgements: I thank Martin Steffen and Olaf Owe for their useful comments.

References

1. R. Alur, K. L. McMillan, and D. Peled. Deciding Global Partial-Order Properties. Formal Methods in System Design, 26(1):7–25, 2005.

2. R. Alur and D. Peled. Undecidability of partial order logics. Inf. Process. Lett., 69(3):137–143, 1999.

3. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic, volume 53 of Cambridge Tracts in Theor. Comput. Sci. Cambridge Univ. Press, 2001.

4. V. Diekert and P. Gastin. LTL Is Expressively Complete for Mazurkiewicz Traces. In ICALP’00, volume 1853 of LNCS, pages 211–222. Springer, 2000.

5. V. Diekert and P. Gastin. From local to global temporal logics over Mazurkiewicz traces. Theor. Comput. Sci., 356(1-2):126–135, 2006.

6. K. Lodaya, M. Mukund, R. Ramanujam, and P. S. Thiagarajan. Models and Logics for True Concurrency. Technical Report IMSc-90-12, Inst. Mathematical Science, Madras, India, 1990.

7. K. Lodaya, R. Parikh, R. Ramanujam, and P. S. Thiagarajan. A Logical Study of Distributed Transition Systems. Inf. Comput., 119(1):91–118, 1995.

8. A. W. Mazurkiewicz. Basic notions of trace theory. In REX Workshop, volume 354 of LNCS, pages 285–363. Springer, 1988.

9. M. Mukund and P. S. Thiagarajan. Linear Time Temporal Logics over Mazurkiewicz Traces. In MFCS’96, volume 1113 of LNCS, pages 62–92. Springer, 1996.

10. M. Nielsen, G. D. Plotkin, and G. Winskel. Petri nets, event structures and domains. In Semantics of Concurrent Computation, volume 70 of LNCS, pages 266–284. Springer, 1979.

11. A. Pnueli. The temporal logic of programs. In FOCS’77, pages 46–57. IEEE Computer Society Press, 1977.

12. V. R. Pratt. A Practical Decision Method for Propositional Dynamic Logic: Preliminary Report. In STOC’78, pages 326–337. ACM Press, 1978.

13. V. R. Pratt. Modeling Concurrency with Partial Orders. J. Parallel Programming, 15(1):33–71, 1986.

14. V. R. Pratt. Modeling concurrency with geometry. In POPL’91, pages 311–322, 1991.

15. V. R. Pratt. Chu spaces and their interpretation as concurrent objects. In Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 392–405. Springer, 1995.

16. V. R. Pratt. Higher dimensional automata revisited. Math. Struct. Comput. Sci., 10(4):525– 548, 2000.

17. V. R. Pratt. Transition and Cancellation in Concurrency and Branching Time. Math. Struct. Comput. Sci., 13(4):485–529, 2003.

18. C. Prisacariu. Modal Logic over Higher Dimensional Automata – technicalities. Technical Report 393, Univ. Oslo, January 2010.

19. B. Rozoy and P. S. Thiagarajan. Event structures and trace monoids. Theor. Comput. Sci., 91(2):285–313, 1991.

20. P. S. Thiagarajan and I. Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. Information and Computation, 179(2):230–249, 2002.

21. R. J. van Glabbeek. On the Expressiveness of Higher Dimensional Automata. Theor. Comput. Sci., 356(3):265–290, 2006.

A Proofs

Proposition A.1 (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 + |φ|.

Lemma A.2. Any two sets [p], [q] ∈ Q_{n}^{f}, for some n ∈ ℕ, are disjoint.

Proof. By induction on n.

The base case for n = 0 is easy as the definition of Q_{0}^{f} results in the equivalence classes on Q_{0} generated by the equivalence relation ≡, which are disjoint.

Inductive step: Consider [p], [q] ∈ Q_{n}^{f}, 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) for any 1 ≤ i ≤ n and some fixed [p′_{i}], [q′_{i}] ∈ Q_{n−1}^{f}, t_{i}(r) ∈ [p′_{i}] and t_{i}(r) ∈ [q′_{i}]. By the induction hypothesis we know that [p′_{i}] and [q′_{i}] are disjoint, which, together with (2) before, implies that [p′_{i}] = [q′_{i}] for all 1 ≤ i ≤ n. Because of this and (1) it implies that [q] = [p]. Therefore we have proven that if two sets [p], [q] ∈ Q_{n}^{f} have a cell in common then they must be the same. (Note that a similar treatment of s_{i} is needed.)

Lemma A.3.

1. The definitions of s_{i}^{f} and t_{i}^{f} are that of maps (as required in a higher dimensional structure).

2. The s_{i}^{f} and t_{i}^{f} respect the cubical laws of a higher dimensional structure.

Proof. For 1. we give the proof only for t_{i}^{f}, as the proof for s_{i}^{f} is analogous. We use reductio ad absurdum and assume, for some [q] ∈ Q_{n}^{f}, that t_{i}^{f}([q]) = [p] and t_{i}^{f}([q]) = [p′] with [p] ≠ [p′] and [p], [p′] ∈ Q_{n−1}^{f}. From the definition we have that for all q ∈ [q] both t_{i}(q) ∈ [p] and t_{i}(q) ∈ [p′]. From Lemma A.2 we know that [p] and [p′] are disjoint and we know that t_{i} is a map (i.e., the outcome is unique), therefore we have the contradiction.

For 2. we have to prove, for some arbitrary chosen [q] ∈ Q_{n}^{f} and for any 1 ≤ i < j ≤ n that

t_{i}^{f}(t_{j}^{f}([q])) = t_{j−1}^{f}(t_{i}^{f}([q])).

(Note that t_{i}^{f} on the left side is different than the t_{i}^{f} on the right side, as the left one is applied to elements of Q_{n−1}^{f} whereas the right one is applied to elements of Q_{n}^{f}.) 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_{i}^{f}(t_{j}^{f}([q])) = [q_{n−2}] with [q_{n−2}] ∈ Q_{n−2}^{f}. This leads to considering that t_{j}^{f}([q]) = [q_{n−1}] with [q_{n−1}] ∈ Q_{n−1}^{f}, and t_{i}^{f}([q_{n−1}]) = [q_{n−2}]. From the definition we have both:

(1) ∀q ∈ [q] : t_{j}(q) ∈ [q_{n−1}],

(2) ∀q ∈ [q_{n−1}] : t_{i}(q) ∈ [q_{n−2}]. Therefore, from the two we have that

(3) ∀q ∈ [q] : t_{i}(t_{j}(q)) ∈ [q_{n−2}].

We want to prove that [q_{n−2}] = t_{j−1}^{f}(t_{i}^{f}([q])), for which we can assume, wlog., that t_{i}^{f}([q]) = [q′_{n−1}] for some [q′_{n−1}] ∈ Q_{n−1}^{f}. Therefore, it amounts to proving that t_{j−1}^{f}([q′_{n−1}]) = [q_{n−2}]. For this it is enough to find some p ∈ [q′_{n−1}] s.t. t_{j−1}(p) ∈ [q_{n−2}], because by the Definition 2.5 (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}].

Proof (of Lemma 2.8). By induction on the structure of the formula ψ.

Base case: For ψ = ϕ is immediate from the definition of V^{f}.

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 H, q ⊧ ⟨⟩ψ′ iff H^{f}, [q] ⊧ ⟨⟩ψ′. Considering the only if implication we assume that (cf. definition of satisfiability from Table 1) ∃q′ ∈ Q_{n−1} : t_{i}(q) = q′ ∧ q′ ⊧ ψ′ for some 1 ≤ i ≤ n, and have to prove that ∃[p] ∈ Q_{n−1}^{f} : t_{i}^{f}([q]) = [p] ∧ [p] ⊧ ψ′ for some 1 ≤ i ≤ n. Because q ∈ [q] and t_{i}(q) = q′, using the definition of [q] it implies that for all q ∈ [q] is that t_{i}(q) ∈ [q′] which, by the definition of t_{i}^{f}, implies that t_{i}^{f}([q]) = [q′]. (Thus we have found the [q′] ∈ Q_{n−1}^{f}.) From the induction hypothesis we have that H, q′ ⊧ ψ′ implies that H^{f}, [q′] ⊧ ψ′. This ends the proof.

Consider now the if implication and assume ∃[p] ∈ Q_{n−1}^{f} : t_{i}^{f}([q]) = [p] ∧ [p] ⊧ ψ′ for some 1 ≤ i ≤ n. From the definition of t_{i}^{f} we have that t_{i}(q) ∈ [p]; which is the same as picking some p′ ∈ [p] with t_{i}(q) = p′. From the induction hypothesis we know that H^{f}, [p] ⊧ ψ′ iff H, p ⊧ ψ′ for any p ∈ [p] (in particular H, p′ ⊧ ψ′). Thus ∃p′ ∈ Q_{n−1} : t_{i}(q) = p′ ∧ H, p′ ⊧ ψ′ for some 1 ≤ i ≤ n, finishing the proof.

When we take ψ = {}ψ′ we use analogous arguments as in the proof of ⟨⟩ψ′. In this case we work with the definition of s_{i}^{f} and we look for cells of higher dimension (instead of lower dimension).

Proof (of Lemma 2.9). 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 that 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. By the induction hypothesis this means that it is enough to consider only cells of at most dimension k − 1 + |φ|_{uc} for which k + |φ|_{uc} is a safe approximation.

Proposition A.4 (theorems). The following are derivable in the axiomatic system of Table 2:

⊢ {}(φ → φ′) → ({}φ → {}φ′), ⊢ ⟨⟩(φ → φ′) → (⟨⟩φ → ⟨⟩φ′), ⊢ (⟨⟩[ ]φ ∧ ⟨⟩[ ]¬φ) → ⊥, ⊢ ⟨⟩[{}]⊥ → [{}]⊥, ⊢ {}⊤ → [ ]{}⊤, ⊢ ⟨⟩⊤ → ({}[ ]φ → ⟨⟩{}φ), ⊢ {}⊤ → (⟨⟩[{}]φ → {}⟨⟩φ), ⊢ [{}]⟨⟩⊤. Moreover, one can use the following derived rules:

\begin{matrix}φ ; \overline{,} ; [\{\}]φ & φ ; \overline{,} ; [ ]φ \\ φ → φ′ ; \overline{,} ; [\{\}]φ → [\{\}]φ′ & φ → φ′ ; \overline{.} ; [ ]φ → [ ]φ′ \end{matrix}

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

third theorem is a consequence of (A6): ⟨⟩[ ]φ ∧ ⟨⟩[ ]¬φ →^{(A6)} [ ]⟨⟩φ ∧ ⟨⟩[ ]¬φ →^{SML}

⟨⟩(⟨⟩φ ∧ [ ]¬φ) →^{SML} ⟨⟩⟨⟩(φ ∧ ¬φ) →^{(A2′)} ⊥. The forth theorem is a consequence of

(A7’): ⟨⟩[{}]⊥ →^{(A7′)} [{}]⟨⟩⊥ →^{(A2′)} [{}]⊥. The fifth theorem is a consequence of the theo-

rem before by contraposition. The sixth theorem is a consequence of (A7): ({}[ ]φ →^{(A7)} [ ]{}φ) ↔ ({}[ ]φ ∧ ⟨⟩⊤ → [ ]{}φ ∧ ⟨⟩⊤) but [ ]{}φ ∧ ⟨⟩⊤ → ⟨⟩{}φ which means that ({}[ ]φ ∧ ⟨⟩⊤ → ⟨⟩{}φ) ↔ ⟨⟩⊤ → ({}[ ]φ → ⟨⟩{}φ). The seventh theorem is derivable in an analogous way as the one above only that we use axiom (A7’). The eighth theorem is just the instantiation of axiom (A9) when i = 0 (i.e., ⟨⟩^{0}⊤ =^{△} ⊤).

Proof (of Theorem 2.12). Before proving soundness we should have some intuition about the non-standard axioms (A5) to (A9’). First consider the four axioms (A6) to (A7’) that each relates to one of the four 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). Axiom (A6’) embodies the cubical law where α and β are both instantiated to s (e.g., s_{i}(s_{j}(q)) = s_{j−1}(s_{i}(q))). 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)).

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, as we said before, the dimension of a cell is given by the number of events that are currently executing concurrently.

– Axiom (A5’) {}^{i}⊤ → {}i says something of the opposite (it looks at the upper levels instead of at the lower levels like the axiom before). The axiom says that if from the current cell it can move i levels up (i.e., can reach a cell of dimension i greater than the current cell) then is must be that from the current cell there can be started at least i different new events.

– Axiom (A9) ⟨⟩^{i}⊤ → [{}]⟨⟩⟨⟩^{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.

– Axioms (A8) and (A8’) intuitively say that if some cell has dimension greater than i then all the cells on that level have dimension greater than i.

For soundness of the axiomatic system it is enough to prove that the axioms (A5) to (A9’) are valid. We start with axiom (A6) and assume H, q_{n} ⊧ ⟨⟩[ ]φ for some q_{n} ∈ Q_{n} and arbitrary n. 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})). 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 (A6’) 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} ⊧ [{}]φ. Which means that for any q_{n+2} with s_{l}(q_{n+2}) = q_{n+1} for some 1 ≤ l ≤ n + 2, we have H, q_{n+2} ⊧ φ. We want to show that H, q ⊧ [{}]{}φ which reduces to showing that for an arbitrary q′_{n+1} ∈ Q_{n+1} with s_{m}(q′_{n+1}) = q for some 1 ≤ m ≤ n + 1, we can find an 1 ≤ m′ ≤ n + 2 s.t. s_{m′}(q_{n+2}) = q′_{n+1}. This is done by the cubical laws: if m ≤ k consider s_{m}(s_{k+1}(q_{n+2})) = s_{k}(s_{m}(q_{n+2})) and make m′ = k + 1 (it is clear that m′ ≤ n + 2) and thus H, s_{m}(s_{m′}(q_{n+2})) ⊧ [{}]{}φ because we have said that H, s_{k}(s_{m}(q_{n+2})) ⊧ [{}]{}φ; otherwise, if k < m then consider the law s_{k}(s_{m+1}(q_{n+2})) = s_{m}(s_{k}(q_{n+2})) (as m + 1 ≤ n + 2) and take m′ = k, thus having H, s_{m}(s_{m′}(q_{n+2})) ⊧ [{}]{}φ because H, s_{k}(s_{m+1}(q_{n+2})) ⊧ [{}]{}φ.

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 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 ⊧ [ ]{}φ which amounts to showing that for some arbitrary 1 ≤ m ≤ n with t_{m}(q) = 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} ⊧ φ. This is done with 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 axiom (A7’) 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

3 We do not consider the k because the case for m = k is trivial from the assumption above, where we know that for t_{k} and any t_{l} it is the case that H, t_{l}(t_{k}(q_{n})) ⊧ φ.

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′′_{n} = t_{k+1}(q_{n+1}) for which it holds that H, t_{l}(q_{n+1}) ⊧ φ because H, s_{m}(t_{l}(q_{n+1})) ⊧ [{}]φ.

For axiom (A8) 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 amount 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 based on the semantics of ⟨⟩ and [ ] this time.

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.

For axiom (A9’) assume H, q_{n} ⊧ {}⟨⟩⟨⟩^{i}⊤ which means that exists q_{n+1} ∈ Q_{n+1} with s_{j}(q_{n+1}) = q_{n} for some 1 ≤ j ≤ n + 1 s.t. H, q_{n+1} ⊧ ⟨⟩⟨⟩^{i}⊤. 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}.

Axioms (A5) and (A5’) require inductive arguments and we left them at the end. For (A5) use induction on i, where the base case ⟨⟩1 → ⟨⟩^{1}⊤ is trivial. 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. Therefore, q is of dimension at least i and any t_{j}(q) is of dimension at least i − 1. By the induction hypothesis we have that H, t_{j}(q) ⊧ ⟨⟩^{i−1}⊤ and therefore H, q ⊧ ⟨⟩⟨⟩^{i−1}⊤, i.e., H, q ⊧ ⟨⟩^{i}⊤.

For axiom (A5’) we also use induction where the base case for {}^{1}⊤ → {}1 is trivial. Consider that H, q ⊧ {}^{i}⊤ which means that it exists s_{j}(q′) = q s.t. H, q′ ⊧ {}^{i−1}⊤. By the induction hypothesis we have that H, q′ ⊧ {}i − 1 which means that there are at least i − 1 different q′′ with s_{k}(q′′) = q′ for some k. Pick one such q′′ and note that q, q′, q′′ enter into a cubical law: if k > j then s_{j}(s_{k}(q′′)) = q = s_{k−1}(s_{j}(q′′)), or if k ≤ j then s_{k}(s_{j+1}(q′′)) = q = s_{j}(s_{k}(q′′)). Any of the cases brings a cell different than q′ (either s_{j}(q′′) or s_{j+1}(q′′)) which is linked through an s map to q. Similarly, all the i − 1 different q′′ bring a different cell that links to q through an s map. Thus we have shown that q is linked with i different cells through one of their s maps.

For i > 2 we need to make sure that we really have new cells for each q′′. Assume (by reductio ad absurdum) that for two different q′′_{k} and q′′_{l}, with s_{k}(q′′_{k}) = q′ = s_{l}(q′′_{l}) and wlog. k > j and l > j, we have s_{j}(q′′_{k}) = s_{j}(q′′_{l}) = q′_{j}.^{4} On another hand, because of the above cubical laws we have s_{l−1}(q′_{j}) = s_{k−1}(q′_{j}) which can be possible only when k = l. This, together with the fact that both q′′_{k} and q′′_{l} are linked with some q′′′ by an s map, we can find them in the following cubical law: s_{k}(s_{k+1}(q′′′)) = s_{k}(s_{k}(q′′′)). If this is the case then there are some other cubical laws applicable: s_{j}(s_{k+1}(q′′′)) = q′_{j} = s_{j}(s_{k}(q′′′)). From this we get s_{k}(s_{j}(q′′′)) = s_{j}(s_{k+1}(q′′′)) = s_{j}(s_{k}(q′′′)) =

4 Analogous arguments can be given for the other three cases depending on j, k, l.

s_{k−1}(s_{j}(q′′′)). This means that from the cell s_{j}(q′′′) there are two different s maps (i.e., s_{k−1} and s_{k}) that end in the same cell q′_{j}. This is not possible and hence we have the contradiction.

Proof (of Lemma 2.15). By induction on the structure of ψ.

Base case: ψ = ϕ ∈ Φ_{B}. From the definition we have H, q_{n} ⊧ ϕ iff ϕ ∈ V(q_{n}) iff ϕ ∈ λ(q_{n}).

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.

We prove H, q_{n} ⊧ {}φ ⇒ {}φ ∈ λ(q_{n}). From the definition we know that ∃q′ ∈ Q_{n+1} and ∃0 ≤ i ≤ n+1 s.t. s_{i}(q′) = q_{n} and H, q′ ⊧ φ. From the induction hypothesis we have that H, q′ ⊧ φ iff φ ∈ λ(q′). Together with the canonicity of H we have that {}φ ∈ λ(q_{n}). Proof finished.

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.

Proof (of Lemma 2.17).

f u n c t i o n e n r i c h (n ,q ,φ){
Q_{n+1} := Q_{n+1} ∪ {q_{n+1}}; / /f r e s h c e l l

u p d a t e map s_{n+1} s.t. s_{n+1}(q_{n+1}) = q;

l a b e l q_{n+1} with λ(q_{n+1}) = {φ} ∪ {ψ | [{}]ψ ∈ λ(q)};
addSourceMaps (n+1 ,q_{n+1} , 0 ,∅) ;
addTargetMaps (n+1 ,q_{n+1} , 0 ,∅) ;

}

f u n c t i o n addSourceMaps (k ,q ,m,q′){
i f (k>=1){
Q_{k−1} := Q_{k−1} ∪ {q_{k−1}^{1}, …, q_{k−1}^{k−1−m}}; / /f r e s h c e l l s
f o r (l=1 t o m){

u p d a t e map t_{k−l} s.t. t_{k−l}(q) = t_{k−m}(t_{k−l+1}(q′)) ; }

f o r ( i=k−1−m t o 1){

u p d a t e map s_{i} s.t. s_{i}(q) = q_{k−1}^{i};

u p d a t e map s_{k−1} s.t. s_{k−1}(q_{k−1}^{i}) = s_{i}(s_{k}(q)) ;

l a b e l q_{k−1}^{i} with λ(q_{k−1}^{i}) = λ(s_{k}(q)) ;
addSourceMaps (k−1,q_{k−1}^{i} ,k−1−m−i ,q ) ;
addTargetMaps (k−1,q_{k−1}^{i} , 0 ,∅) ;

}}}

f u n c t i o n addTargetMaps (k ,q ,m,q′){
i f (k >= 1){
Q_{k−1} := Q_{k−1} ∪ {q_{k−1}^{1}, …, q_{k−1}^{k−m}}; / /f r e s h c e l l s
f o r (l=0 t o m−1){

u p d a t e map t_{k−l} s.t. t_{k−l}(q) = t_{k+1−m}(t_{k−l+1}(q′)) ; }

f o r ( i=k−m t o 1){

u p d a t e map t_{i} s.t. t_{i}(q) = q_{k−1}^{i};

i f (m=0 && i=k) l a b e l q_{k−1}^{i} by λ(q_{k−1}^{i}) = {ψ | [ ]ψ ∈ λ(q)};
e l s e l a b e l q_{k−1}^{i} by λ(q_{k−1}^{i}) = λ(t_{k}(q)) ;
i f (k > 1){
addTargetMaps (k−1,q_{k−1}^{i} ,k−m−i ,q ) ;
f o r ( j =1 t o k−1){ / /add k−1 maps s_{j} t o q_{k−1}^{i} c f . c u b i c a l laws

i f ( j<i ) u p d a t e map s_{j} s.t. s_{j}(t_{i}(q)) = t_{i−1}(s_{j}(q)) ; e l s e u p d a t e map s_{j} s.t. t_{i}(s_{j+1}(q)) = s_{j}(t_{i}(q)) ; }}}}}

For the sake of the presentation, in the algorithm we omitted the fact that after we finish adding all necessary formulas to a label (and before using this label further) we grow the label set to an atom cf. Lemma 2.13(iv). We can do this because we prove in the following that all the labels that we build are consistent sets. Similarly for the lifting construction in Lemma 2.18.

The proof has four stages: 1) we show that the enriched model is an extension of the old model (i.e., H′ ▷ H); 2) we show that any set of formulas that the construction attaches as a label to a new cell is a consistent set, so that it can be grown to an atom, as required; 3) we show that the extended model H′ is still canonical; 4) we show that H′ is a model indeed, i.e., that all the maps are in place and all necessary cubical laws are respected. The proof makes use of the axioms (A7),(A7’), and (A9).

First of all remark that we do not change the initial shape or labels of the original H; we only add fresh cells and fresh maps for these cells. This means that the enriched HDA extends H.

Before proving that the enriched model H′ is canonical, we should make sure that we indeed construct only consistent sets as labels. In this way Lemma 2.13(iv) can be applied to grow each set that we construct into an atom. There are only two places where we actually construct sets of formulas as labels; in all other places we just reuse labels of other existing cells which are already atoms.

The first set that we construct is in the enrich function itself. Assume that this set is not consistent, which means two cases: 1) ψ_{1} ∧ ⋯ ∧ ψ_{k} → ⊥, for ψ_{i} ∈ λ(q_{n+1}) and [{}]ψ_{i} ∈ λ(q) with 1 ≤ i ≤ k, and 2) ψ_{1} ∧ ⋯ ∧ ψ_{k} → ¬φ, for ψ_{i} ∈ λ(q_{n+1}), [{}]ψ_{i} ∈ λ(q), and {}φ ∈ λ(q). For case 1) we know from modal logic that [{}]ψ_{1} ∧ ⋯ ∧ [{}]ψ_{k} → [{}](ψ_{1} ∧ ⋯ ∧ ψ_{k}) which, together with the assumption, it means that [{}]ψ_{1} ∧ ⋯ ∧ [{}]ψ_{k} → [{}]⊥. This means that [{}]⊥ ∈ λ(q) which is a contradiction with the fact that λ(q) is an atom containing an existential modality, namely, {}φ. For case 2) we follow a similar argument to obtain [{}]ψ_{1} ∧ ⋯ ∧ [{}]ψ_{k} → [{}](ψ_{1} ∧ ⋯ ∧ ψ_{k}) → [{}]¬φ → ¬{}φ. But this is a contradiction because the atom λ(q) already contains {}φ and by Lemma 2.13(i) it cannot contain ¬{}φ.

The second set of formulas that the enrich construction adds is in the addTargetMaps. Assume that the set is inconsistent, i.e., ψ_{1} ∧ ⋯ ∧ ψ_{k} → ⊥ for ψ_{j} ∈ λ(q_{n}^{i}) and [ ]ψ_{j} ∈ λ(q_{n+1}) with 1 ≤ j ≤ k, where t_{i}(q_{n+1}) = q_{n}^{i}. By arguments similar as before we get [ ]ψ_{1} ∧ ⋯ ∧ [ ]ψ_{k} → [ ](ψ_{1} ∧ ⋯ ∧ ψ_{k}) → [ ]⊥ which would mean that [ ]⊥ ∈ λ(q_{n+1}). But this is not possible because of the axiom (A9) which essentially says that there must be ⟨⟩⊤ ∈ λ(q_{n+1}), hence the contradiction. To be more precise, consider our initial cell q_{n} ∈ Q_{n} of dimension n and hence H, q_{n} ⊧ ⟨⟩^{n}⊤ which by axiom (A9) it means that [{}]⟨⟩⟨⟩^{n}⊤ ∈ λ(q_{n}). By the construction of the label of q_{n+1} we have ⟨⟩⟨⟩^{n}⊤ ∈ λ(q_{n+1}). Because of this, we have an existential formula ⟨⟩⊤ in the label that contains all the [ ]ψ_{j} at any level, and hence at any depth of recursion calls to addTargetMaps. This means that at any recursive call the set of formulas that addTargetMaps builds is consistent.

We now prove that the enriched model H′ is canonical. It is easier to treat the second canonicity condition and we do that now. Assume that for the enriched HDA the second canonicity condition is broken; i.e., assume t_{i}(q) = q′ for which φ ∈ λ(q′) and ⟨⟩φ ∉ λ(q), which is the same as ¬⟨⟩φ ∈ λ(q) cf. Lemma 2.13(i) because λ(q) is an atom. We take cases after q. First, clearly, if q, q′ ∈ H then the canonicity is assured by the statement of the lemma (i.e., H is canonical).

The rest is easy if we note that for new cells the only place where t_{i} maps are added is in the addTargetMaps function which is called in three places: for q_{n+1}, for cells added as targets for source maps s_{i}, and for cells added as targets of termination maps t_{i}. For all these cases the fact that ¬⟨⟩φ ∈ λ(q) implies that [ ]¬φ ∈ λ(q), and the construction of the label of q′ = t_{i}(q) implies that ¬φ ∈ λ(q′) which is impossible because λ(q′) is constructed as an atom and by our assumption φ ∈ λ(q′).

Assume now that for the enriched HDA the first canonicity condition is broken; i.e., assume it exists s_{i}(q) = q′ for which φ ∈ λ(q) and {}φ ∉ λ(q′). We now take cases after q. First, if q, q′ ∈ H (i.e., is part of the old model that we have just enriched) then the assumption is violated because these cells respect the canonicity conditions (by the statement of the lemma).

Second, assume that q = q_{n+1} and q′ = q_{n}^{i} is one of the cells added by the function addSourceMaps(n+1,q_{n+1}). Each of these cells is labeled by λ(q_{n}^{i}) = λ(s_{n+1}(q_{n+1})). By our assumption, this means that {}φ ∉ λ(q_{n}), which, because λ(q_{n}^{i}) is an atom it means that ¬{}φ ∈ λ(q_{n}^{i}). By axiom (A2’) it means that [{}]¬φ ∈ λ(s_{n+1}(q_{n+1})). This means, by the construction of the label of q_{n+1}, that ¬φ ∈ λ(q_{n+1}). This is a contradiction as the atom λ(q_{n+1}) already has φ.

Third, assume q is one of the cells added by the addSourceMaps(n+1,q_{n+1}) at some recursion depth; i.e., q = q_{k}^{i} for some 0 < k ≤ n (i.e., q_{k}^{i} ∉ Q_{0} ∧ q_{k}^{i} ∉ Q_{n+1}) and for some 1 ≤ i ≤ k. Note that s_{k}(q_{k}^{i}) = s_{i}(s_{k+1}(q_{k+1}^{j})) where s_{i}(q_{k+1}^{j}) = q_{k}^{i} and that s_{i}(s_{k+1}(q_{k+1}^{j})) ∈ H and s_{k+1}(q_{k+1}^{j}) ∈ H. By assumption φ ∈ λ(q_{k}^{i}) = λ(s_{k+1}(q_{k+1}^{j})) and [{}]¬φ ∈ λ(q_{k−1}) where s_{j}(q_{k}^{i}) = q_{k−1} for some 1 ≤ j ≤ k. But λ(q_{k−1}) = λ(s_{i}(s_{k+1}(q_{k+1}^{j}))). Because it is part of the old H, s_{i}(s_{k+1}(q_{k+1}^{j})) respects the canonicity constraints, meaning that ¬φ ∈ λ(s_{k+1}(q_{k+1}^{j})) which is impossible as the atom λ(s_{k+1}(q_{k+1}^{j})) already contains φ by assumption.

Lastly, assume q is one of the cells added by addTargetMaps(); i.e., q = q_{k}^{i} = t_{i}(q_{k+1}) for some 1 ≤ i ≤ k and some recursion depth k. The initial assumption says that s_{j}(q_{k}^{i}) = q′, for some 1 ≤ j ≤ k. Wlog. we assume j < i and thus we are in the case when q′ = s_{j}(t_{i}(q_{k+1})) = t_{i−1}(s_{j}(q_{k+1})). This means that there is a source from q_{k+1} to a cell q′′ which has a target to q′. But the cases above have treated q′′ and q′ and their target link respects the canonicity. Because of this and of the assumption [{}]¬φ ∈ λ(q′), implies ⟨⟩[{}]¬φ ∈ λ(q′′), call this (*). From (*), by axiom (A7’) it means that [{}]⟨⟩¬φ ∈ λ(q′′) (**). Note that addTargetMaps() builds the same labels λ(q_{k}^{i}) for all i ≤ k and by the construction of these labels it means that [ ]φ ∈ λ(q_{k+1}). From this and addSourceMaps() we have two cases: (i) [{}][ ]φ ∈ λ(q′′), (ii) {}[ ]φ ∈ λ(q′′). From (i) and (**) a simple reasoning gives that [{}](⟨⟩¬φ ∧ []φ) → [{}]⟨⟩(¬φ ∧ φ) → [{}]⊥ by (A2’). Which means that [{}]⊥ ∈ λ(q′′), and thus ⊥∈ λ(q_{n+1}) which is a contradiction. From (ii) we have by (A7) that [ ]{}φ ∈ λ(q′′) and together with (*) we have ⟨⟩({}φ ∧ [{}]¬φ) → ⟨⟩{}(φ ∧ ¬φ) → ⊥ by axioms (A2) and (A2’). This is a contradiction as ⊥∉ λ(q′′).

We should also make sure 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 take 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}^{n−1} = s_{n−1}(q) we add the map s_{n−1}(q_{n}^{n−1}) 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_{n}^{1} 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_{k−1}^{i} 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_{k−1}^{i} 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 (of Lemma 2.18).

The lifting construction is the following:

f u n c t i o n l i f t (n ,q ,φ){
addTargetMap (n ,q ,{φ},λ(q) ,∅) ;
addSourceMap (n ,q ,λ(q) ,∅) ;
f o r ( a l l c e l l s q′ ≠ q){
addTargetMap (n ,q′ ,∅,λ(q′) ,∅) ;

addSourceMap (n ,q′ ,λ(q′) ,∅) ;

}}

f u n c t i o n addTargetMap (k ,q ,S1 ,S2 ,S3){
Q_{k−1} :=Q_{k−1} ∪ {q_{k−1}}; / /f r e s h c e l l

u p d a t e map t_{k+1} s.t. t_{k+1}(q) = q_{k−1} ;

l a b e l q_{k−1} with λ(q_{k−1}) =S1∪{φ | [ ]φ ∈ S2∪ S3};
f o r ( i =1 t o k){
r_{k−2}^{i}:= addTargetMap (k−1,s_{i}(q) ,∅,λ(s_{i}(q)) ,∅) ;
Q_{k−2} :=Q_{k−2} ∪ {r_{k−2}^{i}};

u p d a t e map s_{i} s.t. s_{i}(t_{k+1}(q)) = r_{k−2}^{i};

λ(q_{k−1}):=λ(q_{k−1}) ∪ {φ | [{}]φ ∈ λ(r_{k−2}^{i})}; / /u p d a t e l a b e l

}

f o r ( i =1 t o k){
q_{k−2}^{i}:= addTargetMap (k−1,t_{i}(q) ,∅,λ(t_{i}(q)) ,λ(q_{k−1}) ) ;
Q_{k−2} :=Q_{k−2} ∪ {q_{k−2}^{i}};

u p d a t e map t_{i} s.t. t_{i}(t_{k+1}(q)) = q_{k−2}^{i}; }

return q_{k−1} ;

}

f u n c t i o n addSourceMap (k ,q ,S1 ,S2){
Q_{k−1} :=Q_{k−1} ∪ {q_{k−1}}; / /f r e s h c e l l

u p d a t e map s_{k+1} s.t. s_{k+1}(q) = q_{k−1} ;

l a b e l q_{k−1} with λ(q_{k−1}) = {{}φ | φ ∈ S1∪ S2};
f o r ( i =1 t o k){ / /add a f r e s h s_{k} map t o each t_{i}(q)
r_{k−2}^{i}:= addSourceMap (k−1,t_{i}(q) ,λ(t_{i}(q)) ,∅) ;
Q_{k−2} :=Q_{k−2} ∪ {r_{k−2}^{i}};

u p d a t e map t_{i} s.t. t_{i}(s_{k+1}(q)) = r_{k−2}^{i};

λ(q_{k−1}):=λ(q_{k−1}) ∪ {⟨⟩φ | φ ∈ λ(r_{k−2}^{i})}; / /u p d a t e l a b e l

}

f o r ( i =1 t o k){ / /add a f r e s h s_{k} map t o each s_{i}(q)
q_{k−2}^{i}:= addSourceMap (k−1,s_{i}(q) ,λ(s_{i}(q)) ,λ(q_{k−1}) ) ;
Q_{k−2} :=Q_{k−2} ∪ {q_{k−2}^{i}};

u p d a t e map s_{i} s.t. s_{i}(s_{k+1}(q)) = q_{k−2}^{i}; }

return q_{k−1} ;

}

The proof has the same four stages as the proof of Lemma 2.17: 1) showing that H′ ▷ H; 2) showing that the labeling introduces only consistent sets of formulas, so that they can be grown to atoms; 3) showing that H′ is still canonical; 4) showing that H′ is a model indeed, i.e., that all the maps are in place and all necessary cubical laws are respected. The proof makes use of the axioms (A5), (A6), (A6’), (A7’), (A8’), and (A9’).

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. Also 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 2.19.) Clearly the two functions do not change the labels nor the shape of the old H and hence the lifted H′ extends H. We continue to show that H′ is canonical.

Generally the proof of canonicity will flow nicely from the labeling, but first we must make sure that the labels introduced by the construction are consistent sets (here is where the axioms are put to work).

Each application of any of the two functions adds a single new cell and builds its label as well as its s and t maps. Consider the addTargetMap function; there are two places where the label is changed, first is in the beginning where the three input sets are used, and second is in the first loop where in each iteration the label is updated. 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_{b}) for which none of its s maps contain φ. This means that if before we could write ⟨⟩n ∈ λ(q_{n}) now we need to write ⟨⟩n + 1. Because of axiom (A5) and Lemma 2.13(ii) it means that ⟨⟩^{n+1}⊤ ∈ λ(q_{n}). (As a side remark, we use Lemma 2.13(ii) tacitly in many places during the proofs of the two constructions lemmas.)

The first call to addTargetMap(n,q_{n},{φ},λ(q_{n}),∅) makes use of only sets S1 and S2 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 we have that {}[{}]¬ψ ∈ λ(q′′) and {}[{}]ψ ∈ λ(q′′). From axiom (A6’) we have that

[{}]{}ψ ∈ λ(q′′) and thus [{}]{}ψ ∧{}[{}]¬ψ → {}({}ψ ∧[{}]¬ψ) → {}{}(ψ ∧¬ψ) →^{(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.

For the labels added by the addSourceMap function it is easy to see that no inconsistencies can appear. In the beginning of the function, the label is constructed by applying the {} modality to the formulas from S2 and S3. This cannot give inconsistencies. Then, in the first loop of the function, the label is updated by adding formulas that apply the ⟨⟩ modality, and again we cannot get inconsistencies.

Next we show that H′ is canonical. 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 φ ∈ {φ | [ ]φ ∈ S2} then [ ]φ ∈ λ(q) and the assumption says that [ ]¬φ ∈ λ(q). This is a contradiction as [ ]φ ∧ [ ]¬φ → [ ](φ ∧ ¬φ) → [ ]⊥ ∈ λ(q) which is not possible because, as we showed before, λ(q) contains at least one existential formula, i.e., ⟨⟩^{k}⊤, where k is the dimension of 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.

Assume that for the lifted HDA the first canonicity condition is broken; i.e., consider q ∈ Q_{n} and assume s_{i}(q) = q′ for which φ ∈ λ(q) and {}φ ∉ λ(q′), which is the same as ¬{}φ ∈ λ(q′), or, by axiom (A4), [{}]¬φ ∈ λ(q′). We again take cases after q.

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. Now we show that the lifting constructs indeed a HDA. This means that we must make sure that all the 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., ⟨⟩φ ∈ λ). 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 three sets of formulas which are used to construct the label of the new cell. We do not discuss here the labeling because we did this before. The rest of the proof is concerned with the geometric structure of the extended H′.

The addTargetMap function adds a new cell q_{k−1} of dimension one lower than that of the input cell q. It 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). The first loop does two operations. First it lifts all the old cells linked to q by an s map by adding one t map to each. Then, all these cells enter under new cubical laws that involve the s maps of the newly added q_{k−1} cell. In this way we add all the necessary s maps of q_{k−1} and also lift all the cells linked by an s map to q and respect cubical laws s_{i}(t_{k+1}(q)) = t_{k}(s_{i}(q)). In the second loop we add the new t_{k} map to each old cell linked to q by a t_{i} map. At the same time we add all the t maps for the new q_{k−1} 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}. In the first loop the function adds the 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−1}.

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−1} and respects the new cubical laws s_{i}(s_{k+1}(q)) = s_{k}(s_{i}(q)).

Proof (of Proposition 3.2). We prove the double implication

H, q ⊧ ¬⟨⟩⊤ → [{}][{}]⊥ iff H is as in Lemma 3.1,

for some HDA H and any q ∈ Q a cell of any dimension. For the if direction if q ∈ Q_{1} then H, q |̸= ¬⟨⟩⊤ and hence the axiom holds trivially. When q ∈ Q_{0} then H, q ⊧ ¬⟨⟩⊤ and thus it must be that H, q ⊧ [{}][{}]⊥. This is true because for any q′ ∈ Q_{1} with s_{1}(q′) = q it is the case that H, q′ ⊧ [{}]⊥ because there are no q′′ ∈ Q_{2} cf. Lemma 3.1.

For the only if direction consider a H for which the axiom holds; 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 H, q_{0} ⊧ ¬⟨⟩⊤ → [{}][{}]⊥, 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 (of Theorem 3.3). First we check that we capture exactly the semantics of standard modal logic; H, q_{0} ⊧ ♢φ iff H, q_{0} ⊧ {}⟨⟩φ iff ∃q′ ∈ Q_{1} s.t. s_{1}(q′) = q_{0} and H, q′ ⊧ ⟨⟩φ iff ∃q′_{0} ∈ Q_{0} s.t. t_{1}(q′) = q′_{0} and H, q′_{0} ⊧ φ. 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 ¬{}⟨⟩¬φ ↔^{(A4)} [{}]¬⟨⟩¬φ ↔^{(A4′)} [{}][ ]φ and the semantic of □φ

is the right one, i.e., for any q′_{0} ∈ Q_{0}, reached through some transition q′ ∈ Q_{1}, is the case that H, q′_{0} ⊧ φ. We prove now that ♢(φ ∨ φ′) ↔ ♢φ ∨ ♢φ′. This is because

{}⟨⟩(φ ∨ φ′) ↔^{(A3′)} {}(⟨⟩φ ∨ ⟨⟩φ′) ↔^{(A3)} {}⟨⟩φ ∨ {}⟨⟩φ′ ↔^{def} ♢φ ∨ ♢φ′.

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.

Proof (of Proposition 3.6). Essential for the proof is the fact that \overline{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 \overline{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 \overline{U} corresponds to the well known LTL semantics. Thus, we should have H, q_{0} ⊧ φ \overline{U} φ′ iff exists a finite sequence q_{0}^{1}, …, q_{0}^{k} with q_{0}^{1} = q_{0}, H, q_{0}^{k} ⊧ φ′, H, q_{0}^{i} ⊧ φ for all 1 ≤ i < k, and for any 1 < i ≤ k q_{0}^{i} is reachable through a single transition from q_{0}^{i−1}. We have H, q_{0} ⊧ (φ ∨ ⟨⟩⊤) U (φ′ ∧ ¬⟨⟩⊤) and by the semantics of U from Definition 3.5 we know that ∃π a path in the Kripke structure (i.e., going only through cells of dimension 0 or 1; which means is of the form q_{0}, q_{1}, q′_{0}, …) s.t. st(π) = q_{0} ∧ en(π) = q′, H, q′ ⊧ (φ′ ∧ ϕ_{0}), and ∀q′′ ∈ π, q′′ ≠ q′ then H, q′′ ⊧ (φ ∨ ⟨⟩⊤). 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′′ ∈ 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 the before we have that H, q′′ ⊧ φ.