A Logical Characterization of Well Branching Event Structures^{1}

Madhavan Mukund and P. S. Thiagarajan

School of Mathematics SPIC Science Foundation 92, G. N. Chetty Road T. Nagar, Madras 600 017 India

Abstract

We develop a tense logic for reasoning about the occurrences of events in a subclass of prime event structures called well branching event structures. The well branching property ensures that two events being in conflict can always be traced back — via the causality relation — to two events being in minimal conflict. Two events are in minimal conflict if they are in conflict and their “unified” past is conflict-free. Thus the minimal conflict relation captures the branching points of the computations supported by the event structure. Our logical language has explicit modalities for talking about causality, conflict, concurrency and minimal conflict. We define the semantics of this logic using well branching event structures as Kripke frames. Our main result is a sound and complete axiomatization of the valid formulas over the chosen class of frames.

1This paper appears in Theoretical Computer Science, 96, 1, (1992) 35-72.

1 Introduction

Event structures have come to play a central role in the formal study of distributed systems. They clearly capture the intuition concerning the non-sequential and indeterminate behaviours of distributed systems. They have a rich mathematical structure [13, 18]. There are natural bridges to other theories of distributed systems such as net theory and the theory of trace languages [13, 14]. Event structures can be used to provide the non-interleaved denotational semantics of CCS-like languages as demonstrated by Winskel [18]. Hence there is a good deal of motivation for developing a logical framework to reason about the behaviours of distributed systems as represented by event structures.

The general problem of developing proof systems based on syntactic presentations of event structures (via, say, a CCS-like language) appears to be difficult. Here we attempt something more modest. Our aim will be to characterize a subclass of prime event structures called well branching event structures using a suitably chosen version of tense logic. The modalities that we introduce in our logic will permit us to explicitly talk about three basic features of distributed systems: causality, conflict and concurrency. The strong characterization result proved here should lead to a deeper understanding of the interplay between the behavioural aspects of distributed systems as captured by event structures and tense logic.

Prime event structures are in some sense the basic form of event structures. A prime event structure consists of a set of event occurrences partially ordered by a causality relation. In addition, the structure contains a binary conflict relation between the events. The conflict relation is required to be irreflexive, symmetric and inherited via the causality relation. The idea is that an event can occur in a computation only if all the events that lie in its past have occurred in the computation. No two events that are in the conflict relation can both occur in a computation. Two events that are neither causally related nor in conflict are said to be concurrent; whenever they both occur in a computation, they do so with no order over their occurrences.

In a well branching prime event structure two events being in conflict can always be traced back — via the causality relation — to two events being in minimal conflict. Two events are said to be in in minimal conflict if they are in conflict and no two events in their (unified) past are in conflict. In such an event structure, the branching points of a computation — where the system chooses between alternate courses of action — can be clearly identified in terms of a choice made between two events in minimal conflict. These ideas will become more transparent in the next section where we present a brief formal introduction to well branching prime event structures.

Prime event structures that model the behaviour of realizable distributed systems will certainly be well branching. In fact, such event structures will have at least two other attributes which we do not handle in this paper. Firstly, the events will be labelled with the elements of an action set. Secondly, these event structures will be finitary; every event will have at most a finite number of events lying in its past. The problems that arise when one tries to handle these two attributes will be discussed in the concluding section.

Turning now to our logical language, it is a tense (temporal) logic with the usual past and future modalities. In addition it has three unary modalities for expressing concurrency, conflict and minimal conflict. Actually, in the present work, where only well branching event structures are admitted, the conflict modality can be expressed in terms of the past, future and minimal conflict modalities. We have included the conflict modality as a first class object in our language mainly for technical reasons. More remarks regarding this point can be found in Section 3 which presents the language and develops a Kripke-style semantics for it with well branching prime event structures serving as the frames.

The conflict modality was introduced by Penczek [15]. He also introduced the logical means for talking about the maximal computations of an event structure called runs. In [16] he uses a modality called the immediate conflict modality. However this modality is not interpreted as the minimal conflict relation. Instead, it is given a rather weak interpretation. We will discuss in greater detail how our work relates to Penczek’s work in the concluding section.

The main technical contribution of this paper is a sound and complete axiomatization of validity with respect to the chosen semantics. The axiomatization is presented in Section 4. The completeness proof, which is somewhat formidable, is spread over Section 5 and the Appendix. In the last section we discuss related work and issues.

Figure 1: An Event Structure

2 Event Structures

In this paper, we will deal only with prime event structures and hence we will simply call them event structures.

Definition 2.1 An event structure is a triple ES = (E, <, #) where

(i) E is a set of events (or better, event occurrences).

(ii) < ⊆ E × E is an irreflexive and transitive causality relation.

(iii) # ⊆ E × E is an irreflexive and symmetric conflict relation.

(iv) # is inherited via < in the sense that e_{1} # e_{2} < e_{3} implies that e_{1} # e_{3} for every e_{1}, e_{2}, e_{3} in E.

Usually the causality relation is required to be a partial ordering relation. We have made it a strict partial ordering relation because it fits in better with the completeness argument.

Let ES = (E, <, #) be an event structure. Then

id =^{def} {(e, e) | e ∈ E}
> =^{def} {(e, e′) | (e′, e) ∈ <}
≤ =^{def} < ∪ id
≥ =^{def} > ∪ id and
co =^{def} E × E − ( ≤ ∪ ≥ ∪ # ).

The relation co is called the concurrency relation. Observe that the relations {<, >, #, co, id} partition E × E.

It is necessary to define one more auxiliary relation. Let ES = (E, <, #) be an event structure and e, e′ ∈ E. Then

e #_{μ} e′ =^{def} e # e′ and ∀e_{1}, e′_{1} ∈ E : [ \begin{matrix}e_{1} ≤ e and e′_{1} ≤ e′ and e_{1} # e′_{1} \\ implies e_{1} = e and e′_{1} = e′ ]. \end{matrix}

#_{μ} identifies the minimal elements (under <) of the # relation and is hence called the minimal conflict relation. The # relation identifies pairs of events which are inconsistent with each other and therefore cannot both occur during any run of the system. #_{μ} identifies the branching points in the behaviour where choices are made between conflicting events. This “basic” conflict then propagates to causally related events and “generates” other conflicts.

In general, there may be events in # whose inconsistency cannot be traced back to a pair of events in #_{μ} — a typical example consists of two infinite descending chains of events in # with each other. However, it is difficult to find useful examples of concurrent systems for modelling which one requires such event structures. We shall therefore restrict our attention to the class of well branching event structures.

Definition 2.2 Let ES = (E, <, #) be an event structure. ES is well branching iff

∀e, e′ ∈ E : e # e′ implies ∃e_{1}, e′_{1} ∈ E : e_{1} ≤ e and e′_{1} ≤ e′ and e_{1} #_{μ} e′_{1}.

Assuming well branching, we can specify an event structure by displaying its < and #_{μ} relations. The # relation is then uniquely determined by part (iv) of Definition 2.1.

Figure 1 is an example of an event structure. The squiggly lines represent the #_{μ} relation. The causality relation is shown in the form of the associated Hasse diagram. In this event structure, e_{1} # e_{6} because e_{1} #_{μ} e_{2} < e_{6}. It is also easy to see that e_{6} co e_{7}.

Notice that a well branching event structure may have infinite descending chains of events — and even pairs of infinite descending chains of events in # with each other. All that well branching ensures is that every pair of events in # is “guarded” below by a pair of events in #_{μ}. Thus, in Figure 2, every pair (e_{i}, f_{j}), i, j ≥ 0, is in #. However, each such element in # can be traced back to the pair (e′_{k}, f′_{k}) ∈ #_{μ},

Figure 2: A Well Branching Event Structure that is not Well Founded

where k = max(i, j), and so the event structure is well branching. Thus, well branching is a fairly weak restriction and does not, in particular, imply well foundedness with respect to <.

The states of an event structure are called configurations. A configuration identifies a set of events that have occurred “so far”. An event can occur only if all the events in its past have occurred. Two events that are in conflict can never both occur in the same stretch of behaviour. Before formalizing these notions it will be convenient to adopt the following notation.

Let ES = (E, <, #) be an event structure and X ⊆ E. Then

↓X = {e′ | ∃e ∈ X : e′ ≤ e}

For the singleton {e}, we shall write ↓e instead of ↓{e}.

Definition 2.3 Let ES = (E, <, #) be an event structure and c ⊆ E. Then c is a configuration iff

(i) c = ↓c (left-closed)

(ii) (c × c) ∩ # = ∅ (conflict-free)

For the event structure shown in Figure 1, {e_{2}, e_{5}, e_{6}} is a configuration. {e_{2}, e_{5}, e_{10}} is not a configuration because it is not left-closed and {e_{3}, e_{7}, e_{8}} is not a configuration because it is not conflict-free.

Let C_{ES} denote the set of configurations of the event structure ES. In this paper, we will be concerned with only the local configurations of an event structure. The notion of a local configuration is based on a simple but crucial observation which lies at the heart of the theory of event structures [13].

Proposition 2.4 Let ES = (E, <, #) be an event structure and e ∈ E. Then ↓e is a configuration.

Proof Follows easily from the definitions.

□

We now define LC_{ES} = {↓e | e ∈ E} to be the set of local configurations of the event structure ES = (E, <, #). We shall interpret the formulas of our logical language only at the local configurations of an event structure.

The configuration ↓e corresponds to the state of the system when the event e has just occurred and thus represents the view of the system seen by observers participating in e. Suppose that ES = (E, <, #) models the behaviour of a system of communicating sequential processes. Then at least one process or agent will be involved in the occurrence of each event. If the agent j participates in e, then ↓e will represent the local history of agent j upto the stage where e has occurred, together with the “latest” histories of all the agents that have communicated with the agent j upto the occurrence of e. This will be true of every agent that participates in e. In other words, ↓e represents a “synchronized” set of local states of the agents that participate in the occurrence of e.

Another motivation for only considering local configurations comes from the work of Nielsen, Plotkin and Winskel. In [13], they show that the poset (C_{ES}, ⊆) of configurations ordered under inclusion is prime algebraic and coherent. The fact that this poset is prime algebraic basically means that certain configurations in the poset are “special”. These are called the prime elements of the poset. An arbitrary configuration is completely characterized by the prime elements that it dominates in the poset. It turns out that the prime elements of the poset (C_{ES}, ⊆) are precisely the local configurations, so it makes sense to tie our assertions about the event structure to these configurations.

3 The Language and its Models

We fix P = {p_{1}, p_{2}, …}, a countably infinite set of atomic propositions. We let p, q with or without subscripts range over P. The formulas of our language are then defined inductively as follows:

(i) Every member of P is a formula.

(ii) If α and β are formulas then so are ¬α, α ∨ β, □α, □ - α, ▽ · α, △ · α and ▽ ·_{μ}α.

□ and □ - will denote the future and past modalities of tense logic respectively. ▽ · will capture conflict, △ · will capture concurrency and ▽ ·_{μ} will capture minimal conflict.

For the rest of the paper, Φ will denote the set of formulas of our language. We let α, β, γ and δ with or without subscripts range over Φ.

A frame is an ordered pair F r = (ES, LC_{ES}) where ES = (E, <, #) is a well branching event structure and LC_{ES} is the set of local configurations of ES. The members of LC_{ES} will play the role of possible worlds in the Kripke-style semantics we are about to define.

A model is an ordered pair M = (F r, V) where F r = (ES, LC_{ES}) is a frame and V: P ⟶ 2^{LC^{ES}} is a valuation function.

Let M = (F r, V) be a model with F r = (ES, LC_{ES}), ES = (E, <, #), and ↓e ∈ LC_{ES}. Then the notion of a formula α being satisfied at the local configuration ↓e in the model M is denoted as M, ↓e ⊧ α and is defined inductively as follows:

M, ↓e ⊧ p  iff ↓e ∈ V (p), for p ∈ P.
M, ↓e ⊧ ¬α  iff M, ↓e |̸= α.
M, ↓e ⊧ α ∨ β iff M, ↓e ⊧ α or M, ↓e ⊧ β.
M, ↓e ⊧ □α  iff ∀e′ ∈ E : e < e′ implies M, ↓e′ ⊧ α.
M, ↓e ⊧ □ - α  iff ∀e′ ∈ E : e′ < e implies M, ↓e′ ⊧ α.
M, ↓e ⊧ ▽ · α  iff ∀e′ ∈ E : e # e′ implies M, ↓e′ ⊧ α.
M, ↓e ⊧ △ · α  iff ∀e′ ∈ E : e co e′ implies M, ↓e′ ⊧ α.
M, ↓e ⊧ ▽ ·_{μ}α iff ∀e′ ∈ E : e #_{μ} e′ implies M, ↓e′ ⊧ α.

The formula α is satisfiable if there exists a model M = ((ES, LC_{ES}), V) and a local configuration ↓e ∈ LC_{ES} such that M, ↓e ⊧ α. α is M-valid — denoted M ⊧ α — iff M, ↓e ⊧ α for every ↓e ∈ LC_{ES}. α is valid — and this is denoted by ⊧ α — iff α is M-valid for every model M.

We define the derived connectives of the Propositional Calculus (PC) such as ∧, ^{⊃} and ≡ in terms of ¬ and ∨ in the usual way. In addition, we define

◇α =^{def} ¬□¬α
◇ - α =^{def} ¬□ - ¬α
▽α =^{def} ¬▽ · ¬α
△α =^{def} ¬△ · ¬α
▽_{μ}α =^{def} ¬▽ ·_{μ}¬α

It is easy to verify that ▽α ≡ ▽_{μ}α∨◇ - ▽_{μ}α∨▽_{μ}◇α∨◇ - ▽_{μ}◇α is a valid formula. Thus we could eliminate the modality ▽ · from the definition of the language and instead make it a derived modality using ▽ ·_{μ}, □ and □ - . However, it will be very convenient to keep ▽ · in the logic as a basic operator. We will instead throw in the above “definition” of ▽ · in terms of ▽ ·_{μ}, □ and □ - as an axiom of our logical system. In [9], it is shown that the language which contains the ▽ · operator but not the ▽ ·_{μ} operator is strictly less expressive for the class of models based on well branching event structures.

Also, notice that the usual reflexive forms of the future and past operators are easily expressible in our logic. α ∧ □α defines a reflexive future operator while α ∧ □ - α defines the corresponding reflexive past operator.

A number of interesting properties of distributed computations can be expressed in our language. To illustrate, consider a finite set of sequential agents A_{1}, A_{2}, …, A_{n}. Assume that {Q_{1}, Q_{2}, …, Q_{n}}

is a collection of pair-wise disjoint finite non-empty sets. Q_{i} is the set of local states that agent A_{i} can assume. The agents communicate with each other asynchronously. The means for associating an event structure with such a system will be assumed to be available (see for example [10]). Let us call such event structures Communicating Sequential Agents (CSAs).

To reason about such systems in our logic, we specify certain “frame axioms”, and focus on models based on CSAs over which these axioms are valid. We can then use these frame axioms in conjunction with the general proof system for event structures (which is presented in the next section) to derive facts about this class of models.

To begin with, suppose that for each i and each q ∈ Q_{i} we have an atomic proposition, also called q for convenience, which denotes that the current local state is q. We first make the following assertions

(where Q = ⋃_{i} Q_{i}).

(i) ⋁_{q∈Q} q

(ii) ⋀_{q,q′∈Q, q≠q′} q ^{⊃} ¬q′

These ensure that the local configurations of the models we consider can be mapped uniquely to the state space of the agents. In this framework, at_{i} =^{def} ⋁_{q∈Q_{i}} q will denote the fact that the current local

configuration belongs to A_{i}.

We can capture the fact that the individual agents are sequential — i.e. they exhibit no concurrency in their local behaviours — by asserting

(iii) ⋀_{i}(at_{i} ^{⊃} △ · (¬at_{i}))

The next assertion expresses the important fact that (non-deterministic) choices in the behaviour are made locally by the individual agents.

(iv) ⋀_{i}(at_{i} ^{⊃} ▽ ·_{μ}at_{i})

To reason about the behaviour of the agents, it is convenient to have the means for talking about the computations of an event structure ES. Let (C_{ES}, ⊆) be the poset of configurations of ES ordered under inclusion. The maximal elements of this poset correspond to the maximal (i.e. “non-extendable”) computations of the event structure, which we shall call the runs of the event structure.

Following [15], we reserve a proposition ρ to designate a run. Let ES = (E, <, #) be an event structure. It is easy to verify that r ⊆ E is a run iff

∀e ∈ E : (e ∈ r iff ∀e′ ∈ E : e # e′ implies e′ ∉ r).

Keeping this in mind, we can demand that the local configurations satisfying ρ constitute a run in any model we consider by asserting the following:

(v) ρ ≡ ▽ · ¬ρ

Now suppose that the agents are running a common protocol to achieve a stable property — that is, once the property is satisfied in a run it remains true for the remainder of the run. For instance the agents may be running a protocol such as the snapshot algorithm [3], superimposed on the actual computation, to detect the termination of the main computation.

Let α denote the fact that an individual agent has “recognized”, as a result of running the protocol, that the system has achieved a stable property – in this case, α would denote that the agent has detected that the main computation has terminated. If the protocol has worked correctly, α will be become true in any run within an agent only if the stable property has in fact been achieved, and so α itself must be “stable” within each agent. The formula ⋀_{j}[at_{j} ∧ ρ ^{⊃} (α ^{⊃} □((at_{j} ∧ ρ) ^{⊃} α))] can be used to specify this.

In addition, to verify the protocol we have to check that in each run of the system, if A_{i} achieves a local state satisfying α then every other agent also eventually achieves a local state satisfying α. Notice that any pair of local states that occur in the same run must either be ordered or in co with each other. As a result, during a run A_{i} can “look across” to all the local states of some other agent A_{j} which belong to the same run using the modalities □, □ - and △ · . Hence, we can specify the correctness of the protocol by asserting:

at_{i} ∧ ρ ∧ α ^{⊃} ⋀_{j≠i}[ \begin{matrix}□((at_{j} ∧ ρ) ^{⊃} ◇(at_{j} ∧ ρ ∧ α))∧ \\ □ - ((at_{j} ∧ ρ) ^{⊃} ◇(at_{j} ∧ ρ ∧ α))∧ \\ △ · ((at_{j} ∧ ρ) ^{⊃} ◇(at_{j} ∧ ρ ∧ α))] \end{matrix}

On the other hand, suppose that the agents are meant to constitute a non-terminating system. We can specify that the system is free from “local” deadlock by asserting that every run is “perpetual” within each agent as follows:

⋀_{i}((at_{i} ∧ ρ) ^{⊃} ◇(at_{i} ∧ ρ))

We can also specify the weaker property that the system as a whole has no finite computations, though individual agents may terminate, as follows:

⋀_{i}\{(at_{i} ∧ ρ) ^{⊃} \begin{matrix}[◇(at_{i} ∧ ρ))∨ \\ ⋁_{j≠i}( \begin{matrix}□((at_{j} ∧ ρ) ^{⊃} ◇(at_{j} ∧ ρ))∧ \\ □ - ((at_{j} ∧ ρ) ^{⊃} ◇(at_{j} ∧ ρ))∧ \\ △ · ((at_{j} ∧ ρ) ^{⊃} ◇(at_{j} ∧ ρ)))]\} \end{matrix} \end{matrix}

This formula asserts that in case an agent is unable to make progress within a run, it must be able to look across to some other agent which is non-terminating, thereby ensuring that the run is infinite.

The intuitive notion of frame axioms used in the example can be formalized. Let A = {α_{1}, α_{2}, …, α_{n}} be a finite set of formulas. Then, we will say that A semantically entails β — and denote this by A ⊧ β — iff for every model M, if M ⊧ α_{1} ∧ α_{2} ∧ … ∧ α_{n} then M ⊧ β. Thus, in the example above, the intention is that the formulas we use for specifying properties about the class of models based on CSAs should be semantically entailed by the frame axioms (i) through (v) together with a suitably chosen set of assertions satisfied by a protocol. This will then ensure that the protocol (semantically) meets the specifications.

We can relate the notions of semantic entailment and validity. To do this, we introduce the modality E defined as follows:

Eα =^{def} α ∧ □α ∧ □ - α ∧ ▽ · α ∧ △ · α

Eα is to be read as “everywhere α”. From the semantics it is obvious that if Eα is satisfied at a local configuration in a model then α is satisfied at every local configuration in the model. We then have the following result.

Theorem 3.1 {α_{1}, α_{2}, …, α_{n}} ⊧ β iff ⊧ E(α_{1} ∧ α_{2} ∧ … ∧ α_{n}) ^{⊃} β

Proof Follows easily from the definitions.

□

4 The Axiom System

Our axioms are a combination of standard modal logic axioms and tense logic axioms [1, 4], along with a few new axioms which reflect the restrictions imposed on the relations <, # and co in the definition of event structures. We first present the logical system in full, and then provide some explanatory remarks.

AXIOM SCHEMES

(A1) All the substitution instances of the tautologies of propositional logic.

(A2) (i) □(α ^{⊃} β) ^{⊃} (□α ^{⊃} □β) (Deductive Closure)

(ii) □ - (α ^{⊃} β) ^{⊃} (□ - α ^{⊃} □ - β)

(iii) ▽ · (α ^{⊃} β) ^{⊃} (▽ · α ^{⊃} ▽ · β)

(iv) △ · (α ^{⊃} β) ^{⊃} (△ · α ^{⊃} △ · β)

(v) ▽ ·_{μ}(α ^{⊃} β) ^{⊃} (▽ ·_{μ}α ^{⊃} ▽ ·_{μ}β)

(A3) (i) □α ^{⊃} □□α (Transitivity of <)

(ii) □ - α ^{⊃} □ - □ - α

(A4) (i) α ^{⊃} ▽ · ▽α (Symmetry of #, #_{μ} and co)

(ii) α ^{⊃} ▽ ·_{μ}▽_{μ}α

(iii) α ^{⊃} △ · △α

(A5) (i) α ^{⊃} □◇ - α (Relating past and future)

(ii) α ^{⊃} □ - ◇α

(A6) ▽α ^{⊃} □▽α (Conflict inheritance)

(A7) ▽α ≡ ▽_{μ}α ∨ ◇ - ▽_{μ}α ∨ ▽_{μ}◇α ∨ ◇ - ▽_{μ}◇α (Well Branching)

(A8) (i) ▽_{μ}α ^{⊃} □ - (◇α ∨ △α) (Conflict-free past)

(ii) △α ^{⊃} □ - (◇α ∨ △α)

(A9) (i) ◇α ^{⊃} □(α ∨ ◇α ∨ ◇ - α ∨ ▽α ∨ △α) (Relating weak and

(ii) ▽α ^{⊃} ▽ · (α ∨ ◇α ∨ ◇ - α ∨ ▽α ∨ △α) strong modalities)

(iii) △α ^{⊃} △ · (α ∨ ◇α ∨ ◇ - α ∨ ▽α ∨ △α)

(iv) ◇ - α ^{⊃} □ - (α ∨ ◇α ∨ ◇ - α ∨ △α)

(A10) ▽α ^{⊃} △ · (◇α ∨ ▽α ∨ △α) (Relating △ · and ▽ · )

(A11) △α ^{⊃} □(◇ - α ∨ ▽α ∨ △α) (Relating △ · and □)

(A12) ▽α ^{⊃} □ - (◇α ∨ ▽α ∨ △α) (Relating ▽ · and □ - )

INFERENCE RULES

(MP)  \frac{α ^{⊃} β, α}{β}
(TG)  (i) \frac{α}{□α}  (ii) \frac{α}{□ - α}  (iii) \frac{α}{▽ · α}  (iv) \frac{α}{△ · α}  (v) \frac{α}{▽ ·_{μ}α}

(UNIQ)

\frac{p̂^{⊃} α}{α}

where p is an atomic proposition not appearing in α and p̂ =^{def} p ∧ □¬p ∧ □ - ¬p ∧ △ · ¬p ∧ ▽ · ¬p

Axioms A1 and A2 and inference rules MP and TG are standard. A3 and A4 are versions of the modal logic axioms T and B respectively which express the transitivity of < and the symmetry of #, #_{μ} and co. A5 is the standard tense logic axiom relating the past and future modalities. A6 expresses the fact that conflict is inherited via <. A7 captures the fact that the event structure is well branching. A8(i) characterizes #_{μ} as the minimal conflict relation while A8(ii) ensures that any two events related by co have consistent (i.e. conflict-free) pasts. The remaining axioms are necessary to capture the fact that the relations <, <^{−1}, # and co “cover” the event structure – i.e., any two distinct events are related by one of these relations.

The rule UNIQ is adapted from [2]. Notice that given a proposition p, the formula p̂ can be true at at most one local configuration, by the definition of p̂. Hence, we can label each local configuration ↓e_{i} by a distinct formula p̂_{i}. The rule UNIQ allows us to construct this labelling, which is crucial in demonstrating the completeness of the axiomatization.

A formula α is a thesis if it is derivable in our axiom system. We denote that α is a thesis by ⊢ α.

Theorem 4.1 (Soundness) If ⊢ α then ⊧ α.

Proof It is routine to verify that the axioms A1 to A12 are valid and that the rules MP and TG preserve validity.

To show that UNIQ preserves validity requires a little bit of work. We have to show that if p̂^{⊃} α is valid, and p does not appear in α, then α is valid as well.

This is equivalent to showing that if ¬α is satisfiable then p̂ ∧ ¬α is satisfiable (i.e. |̸= α implies |̸= p̂^{⊃} α.)

Suppose that ¬α is satisfiable. Then there exists a model M = ((ES, LC_{ES}), V) and a local configuration ↓e_{0} ∈ LC_{ES} such that M, ↓e_{0} ⊧ ¬α. For β ∈ Φ, let V oc(β) denote the set of propositions that appear in β — V oc(β) is to be read as the vocabulary of β.

Define a new valuation function V′ as follows:

∀q ∈ P : V′(q) = \{ \begin{matrix}V (q) & if q ∈ V oc(¬α) \\ \{↓e_{0}\} & otherwise \end{matrix}

Let M′ = ((ES, LC_{ES}), V′). Let β ∈ Φ such that V oc(β) ⊆ V oc(¬α). It is easy to verify the following, by induction on the structure of β.

∀↓e ∈ LC_{ES} : M′, ↓e ⊧ β iff M, ↓e ⊧ β.

Thus we have M′, ↓e_{0} ⊧ ¬α. At the same time, since p ∉ V oc(¬α), M′, ↓e_{0} ⊧ p̂. So M′, ↓e_{0} ⊧ p̂ ∧ ¬α and we are done.

□

We can now define the notion of a theory. Let A = {α_{1}, α_{2}, …, α_{n}} be a finite set of formulas (here we mean concrete formulas and not schemes closed under substitution). We say that A derives β — which we denote as A ⊢ β — iff we can derive β in a finite number of steps using the formulas {α_{1}, α_{2}, …, α_{n}} in conjunction with our axioms and inference rules.

To ensure that our axiomatization is sound for finite theories, we have to parametrize the rule (UNIQ) by the theory. For example, consider the following derivation, where p, q ∈ P.

p̂^{⊃} q̂ ⊢ p̂^{⊃} q̂  (Assumption)
p̂^{⊃} q̂ ⊢ q̂  (UNIQ)

It is easy to verify that p̂^{⊃} q̂ |̸= q̂, and so the rule (UNIQ) is not sound as it stands. Instead, for the theory A, we have to define the rule (UNIQ_{A}) as follows:

(UNIQ_{A})

\frac{A ⊢ p̂^{⊃} α}{A ⊢ α}

where p is an atomic proposition appearing neither in α nor any of the formulas in A and

p̂ =^{def} p ∧ □¬p ∧ □ - ¬p ∧ △ · ¬p ∧ ▽ · ¬p

The remaining axioms and inference rules do not change for finite theories. The axiomatization presented earlier then turns out to be a special case of the general axiomatization of finite theories, where the set of assumptions A is empty.

Recall that Eα stands for the formula α ∧ □α ∧ □ - α ∧ ▽ · α ∧ △ · α. We then have the following result.

Theorem 4.2 (Deduction) {α_{1}, α_{2}, …, α_{n}} ⊢ β iff ⊢ E(α_{1} ∧ α_{2} ∧ … ∧ α_{n}) ^{⊃} β.

Proof Set α = α_{1} ∧ α_{2} ∧ … ∧ α_{n}. It suffices to show that α ⊢ β iff ⊢ Eα ^{⊃} β.

Suppose ⊢ Eα ^{⊃} β. Then we have α ⊢ Eα ^{⊃} β. Using the inference rule (TG), it is easy to see that the following is a derived inference rule:

\frac{A ⊢ γ}{A ⊢ Eγ}

Hence, since α ⊢ α, we get α ⊢ Eα. Using (MP), we can then derive α ⊢ β.

The proof in the other direction is by induction on the length of the derivation α ⊢ β. Let A = {α_{1}, α_{2}, …, α_{n}}. The base case, where β is an instance of one of the axioms or is one of the formulas α_{i} ∈ A is straightforward. For the induction step, the only interesting case is when the rule (UNIQ_{A}) is used to derive β. We then know that at some earlier step in the derivation we have α ⊢ p̂^{⊃} β, where p does not appear in α or β. By the induction hypothesis, we have ⊢ Eα ^{⊃} (p̂^{⊃} β). Rewriting this we get ⊢ (Eα ∧ p̂) ^{⊃} β and hence ⊢ p̂^{⊃} (Eα ^{⊃} β). We can then apply (UNIQ_{∅}) to obtain ⊢ Eα ^{⊃} β.

□

From Theorems 3.1, 4.1 and 4.2 it follows that A ⊢ β implies A ⊧ β. We will be able to prove the implication in the other direction when we establish the completeness of the axiomatization.

We shall need some theses and derived inference rules to prove the completeness of our axiom system. For convenience, we shall merely state these theses and rules here. The theses and rules are derived in detail in [12].

We begin with some standard theses and inference rules of the modal logic system K [4]. In what follows we let ⨀ range over the set {□, □ - , ▽ · , △ · , ▽ ·_{μ}}. ◯ will abbreviate ¬ ⨀ ¬. We have adopted the convention that in any formula (scheme) the same value is substituted for all appearances of ⨀. Thus, for example, ⨀ α ^{⊃} ◯ α would actually stand for □α ^{⊃} ◇α, □ - α ^{⊃} ◇ - α, ▽ · α ^{⊃} ▽α, △ · α ^{⊃} △α and

▽ ·_{μ}α ^{⊃} ▽_{μ}α.

(TK1) ⨀(α ∧ β) ≡ ⨀ α ∧ ⨀ β

(TK2) ◯(α ∧ β) ^{⊃} ◯ α ∧ ◯β (TK3) ⨀ α ∧ ◯β ^{⊃} ◯ (α ∧ β)

(DRK)  (i) \frac{α ^{⊃} β}{⨀ α ^{⊃} ⨀ β}  (ii) \frac{α ^{⊃} β}{◯α ^{⊃} ◯ β}

We shall also need the “dual” versions of some of the axioms.

(T6Dual) ◇α ^{⊃} ▽ · ▽α
(T8Dual) ◇ - α ^{⊃} △ · (◇ - α ∨ △α)
(T10Dual) △α ^{⊃} ▽ · (◇ - α ∨ ▽α ∨ △α)
(T11Dual) ◇α ^{⊃} △ · (◇α ∨ ▽α ∨ △α)
(T12Dual) ◇ - α ^{⊃} ▽ · (◇ - α ∨ ▽α ∨ △α)

In addition, we need the following theses concerning p̂.

(Tp̂) (i) ◇p̂^{⊃} ¬p ∧ □ - ¬p ∧ ▽ · ¬p ∧ △ · ¬p

(ii) ◇ - p̂^{⊃} ¬p ∧ □¬p ∧ ▽ · ¬p ∧ △ · ¬p
(iii) ▽p̂^{⊃} ¬p ∧ □¬p ∧ □ - ¬p ∧ △ · ¬p
(iv) △p̂^{⊃} ¬p ∧ □¬p ∧ □ - ¬p ∧ ▽ · ¬p
(v) ▽(p̂ ∧ α) ^{⊃} ▽ · (p̂^{⊃} α)

Finally, we need a restricted type of substitution rule.

Let f : P → P be a function mapping atomic propositions to atomic propositions. We can extend f in an obvious way to f̂: Φ → Φ through the syntax of our language, namely:

f̂(q) = f(q), for all q ∈ P

f̂(¬α) = ¬f̂(α)

f̂(α ∨ β) = f̂(α) ∨ f̂(β)

f̂(⨀ α) = ⨀(f̂(α)), where ⨀ ∈ {□, □ - , ▽ · , △ · , ▽ ·_{μ}}

Since f̂ is uniquely determined by f, henceforth we shall always write f(α) instead of f̂(α) for all f : P → P and α ∈ Φ.

The derived inference rule that we want is

(SUB)  \frac{α}{f(α)}  (f : P → P)

5 Completeness

We now wish to show that the axiomatization presented in the previous section is complete.

As usual, by a consistent formula, we shall mean a formula whose negation is not a thesis of our system. Our proof of completeness will establish that every consistent formula is satisfiable — in other words, we show that if ⊬ ¬α then |̸= ¬α.

The finite set of formulas {α_{1}, α_{2}, …, α_{m}} is consistent iff α_{1} ∧ α_{2} ∧ … ∧ α_{m} is consistent. A set of formulas is consistent iff every finite subset is. A Maximal Consistent Set (MCS) is a consistent set of formulas which is not properly included in any other consistent set.

We shall assume the usual properties associated with MCSs. We shall also assume Lindenbaum’s Lemma which says that any consistent set of formulas can be extended to an MCS.

In a model, the set of formulas satisfied at each local configuration is an MCS. Thus, given a frame, we can define a model by associating an MCS with each local configuration, instead of specifying a valuation function. Following [1] we call a function assigning MCSs to a frame a chronicle, and a frame together with a chronicle a chronicle structure.

Clearly not every chronicle structure corresponds to a model. We need to define coherency conditions which must be satisfied by the chronicle in order to yield a model. When these conditions are satisfied, the chronicle is said to be perfect. A perfect chronicle defines a model where the set of formulas satisfied by each local configuration is exactly equal to the MCS assigned to that local configuration by the chronicle.

To show that a consistent formula α_{0} is satisfiable, we shall incrementally construct a chronicle structure which will eventually be perfect and yield a model for α_{0}.

Before defining chronicles and perfect chronicle structures, we need to define four binary “semantic” relations over MCSs as follows.

Definition 5.1 Let A, B be maximal consistent sets.

(i) A ˜< B =^{def} {α | □α ∈ A} ⊆ B.

(ii) A ˜# B =^{def} {α | ▽ · α ∈ A} ⊆ B.

(iii) A c̃o B =^{def} {α | △ · α ∈ A} ⊆ B.

(iv) A ˜#_{μ} B =^{def} {α | ▽ ·_{μ}α ∈ A} ⊆ B.

The next result follows from standard arguments, using axiom A5 for (i) and axiom A4 for (ii) to (iv).

Proposition 5.2 Let A, B be maximal consistent sets.

(i) A ˜< B iff {◇β | β ∈ B} ⊆ A  iff {β | □ - β ∈ B} ⊆ A
iff {◇ - α | α ∈ A} ⊆ B.
(ii) A ˜# B iff {▽β | β ∈ B} ⊆ A iff {β | ▽ · β ∈ B} ⊆ A
iff {▽α | α ∈ A} ⊆ B.
(iii) A c̃o B iff {△β | β ∈ B} ⊆ A iff {β | △ · β ∈ B} ⊆ A
iff {△α | α ∈ A} ⊆ B.
(iv) A ˜#_{μ} B iff {▽_{μ}β | β ∈ B} ⊆ A iff {β | ▽ ·_{μ}β ∈ B} ⊆ A
iff {▽_{μ}α | α ∈ A} ⊆ B.

We shall use ˜> to denote the relation ( ˜<)^{−1}.

The semantic relations defined on MCSs are designed to behave like their counterparts in an event structure. We now verify that our definitions do have the desired effect.

Proposition 5.3

(i) ˜< is transitive.

(ii) ˜#, c̃o and ˜#_{μ} are symmetric.

(iii) ˜#_{μ} ⊆ ˜#.

Proof (i) and (ii) follow at once from axioms A3 and A4. (iii) follows from A7.

□

We can now define the notion of a chronicle structure.

Definition 5.4 A chronicle structure is a triple CH = (ES, T, μ) where

(i) ES = (E, <, #) is a well branching event structure with #_{μ} as its minimal conflict relation.

(ii) T is a function, called a chronicle over ES, which assigns an MCS to each ↓e ∈ LC_{ES}.

(iii) μ ⊆ #_{μ}.

Abusing notation, we shall always talk of a chronicle T assigning an MCS to an event e rather than to the corresponding local configuration ↓e. Notice that we have augmented the chronicle structure with a parameter μ which singles out a special subset of #_{μ}. This will be needed because the relation #_{μ} is not stable with respect to our incremental construction of chronicle structures. The exact role played by μ will become clearer when we describe the construction.

Next, we need the notion of coherence.

Definition 5.5 Let CH = (ES, T, μ) be a chronicle structure, where ES = (E, <, #). CH is coherent iff it satisfies the following conditions.

(i) ∀e, e′ ∈ E : e < e′ implies T (e) ˜< T (e′).

(ii) ∀e, e′ ∈ E : e # e′ implies T (e) ˜# T (e′).

(iii) ∀e, e′ ∈ E : e co e′ implies T (e) c̃o T (e′).

(iv) ∀e, e′ ∈ E : (e, e′) ∈ μ implies T (e) ˜#_{μ} T (e′).

Coherence ensures that the chronicle is consistent with the underlying frame. Notice that for the #_{μ} relation, the chronicle need only be coherent with respect to the special subset μ.

A coherent chronicle may still have “gaps”. These gaps can be described in terms of “unfulfilled requirements”, in the following sense.

Definition 5.6 Let CH = (ES, T, μ) be a coherent chronicle structure, where ES = (E, <, #).

(i) A live future requirement is a pair (e, ◇α) such that e ∈ E and ◇α ∈ T (e) and there does not exist e′ such that e < e′ and α ∈ T (e′).

(ii) A live past requirement is a pair (e, ◇ - α) such that e ∈ E and ◇ - α ∈ T (e) and there does not exist e′ such that e′ < e and α ∈ T (e′).

(iii) A live choice requirement is a pair (e, ▽α) such that e ∈ E and ▽α ∈ T (e) and there does not exist e′ such that e # e′ and α ∈ T (e′).

(iv) A live concurrent requirement is a pair (e, △α) such that e ∈ E and △α ∈ T (e) and there does not exist e′ such that e co e′ and α ∈ T (e′).

(v) A live minimal choice requirement is a pair (e, ▽_{μ}α) such that e ∈ E and ▽_{μ}α ∈ T (e) and there does not exist e′ such that (e, e′) ∈ μ and α ∈ T (e′).

(vi) A live requirement is a pair (e, β) such that (e, β) is a live future requirement or a live past requirement or a live choice requirement or a live concurrent requirement or a live minimal choice requirement.

Once again, observe that the liveness of a minimal choice requirement is defined with respect to μ and not with respect to #_{μ}.

We can now state the criteria under which a chronicle structure is perfect.

Definition 5.7 The chronicle structure CH = (ES, T, μ) is perfect iff it satisfies the following three conditions.

(i) CH is coherent.

(ii) CH has no live requirements.

(iii) μ = #_{μ}, where #_{μ} is the minimal conflict relation of ES.

From the work of Burgess [1], it follows that demonstrating the satisfiability of a consistent formula reduces to the problem of constructing a certain type of perfect chronicle structure.

Lemma 5.8 Let  CH = (ES, T, μ)  be  a  perfect  chronicle  structure,  where

ES = (E, <, #), and let α_{0} be a formula such that for some e_{0} ∈ E, α_{0} ∈ T (e_{0}). Then α_{0} is satisfiable.

Proof Let V_{T} : P → 2^{LC^{ES}} be given by:

∀p ∈ P : V_{T} (p) = {↓e | e ∈ E and p ∈ T (e)}.

Consider the model M_{T} = ((ES, LC_{ES}), V_{T}).

Claim ∀α ∈ Φ : ∀e ∈ E : M_{T} , ↓e ⊧ α iff α ∈ T (e)

Proof of Claim We omit the proof, which is a simple induction on the structure of α.

Now, since we know that α_{0} ∈ T (e_{0}), we get M_{T} , ↓e_{0} ⊧ α_{0}.

□

For the rest of the section, we fix a consistent formula α_{0}. The aim is to construct a perfect chronicle structure CH = (ES, T, μ), with ES = (E, <, #), such that α_{0} ∈ T (e_{0}) for some e_{0} ∈ E.

We shall build up CH inductively. With this in mind, we fix a countably infinite set of events Ẽ = {e_{0}, e_{1}, e_{2}, …}. Let {q_{0}, q_{1}, …, q_{x}} be the set of atomic propositions that appear in α_{0}. Fix an enumeration of P of the form q_{0}, q_{1}, …, q_{x}, p_{0}, p_{1}, . . .. Finally, fix an enumeration of Ẽ × Φ, where Φ is the set of formulas in our language.

For clarity of presentation, we shall omit a couple of lengthy proofs from this section. These proofs are provided in the Appendix. This section together with the Appendix provides a complete account of the inductive construction.

The general idea is to begin by extending α_{0} to an MCS A_{0}. We can then define a chronicle structure CH_{0} = (ES_{0}, T_{0}, ∅), where ES_{0} = ({e_{0}}, ∅, ∅) and T_{0}(e_{0}) = A_{0}.

At stage i in our inductive construction, we shall eliminate one live requirement (e, β) from CH_{i} = (ES_{i}, T_{i}, μ_{i}), where ES_{i} = (E_{i}, <_{i}, #_{i}) and e ∈ E_{i}. In general, this will involve adding an event e_{i+1} to E_{i}. For example, if β is of the form △β_{0}, we shall add an event e_{i+1} such that e co e_{i+1} and extend T_{i} to T_{i+1} so that β_{0} ∈ T_{i+1}(e_{i+1}) and T_{i+1}(e) c̃o T_{i+1}(e_{i+1}).

When we add e_{i+1} to E_{i}, we also have to fix the relationship between e_{i+1} and all the other events in E_{i}. To then extend T_{i} to a coherent chronicle T_{i+1} on ES_{i+1}, we will need to selectively modify the MCSs assigned by T_{i} to the events in E_{i}. While doing this, we have to ensure that live requirements that have been killed at earlier steps remain killed. To achieve all this, we will need to “name” each event e_{i} that we add to our chronicle structure by the formula p̂_{i}. Recall that for p ∈ P, p̂ abbreviates the formula p ∧ □¬p ∧ □ - ¬p ∧ ▽ · ¬p ∧ △ · ¬p.

Keeping all this in mind, we shall assume that the chronicle structure CH_{i} = (ES_{i}, T_{i}, μ_{i}) constructed at stage i satisfies a set of inductive conditions IC. IC captures the fact that E_{i} contains events from {e_{0}, e_{1}, …, e_{i}}, each event being “named” by p̂_{i} — i.e. p̂_{i} ∈ T_{i}(e_{i}). IC also ensures that α_{0} ∈ T_{i}(e_{0}) is maintained as an invariant condition, and that T_{i} is a coherent chronicle on ES_{i}. The detailed description of IC is given in the Appendix.

To ensure that CH_{0} conforms to IC, we have to be careful about extending α_{0} to an MCS A_{0}. Since we want to have T_{0}(e_{0}) = A_{0}, we must ensure that p̂_{0} ∈ A_{0}.

Define the function g_{0} : P → P as follows.

∀p ∈ P : g_{0}(p) = \{ \begin{matrix}p, & if p ∈ \{q_{0}, q_{1}, …, q_{x}\} \\ p_{i+1}, & if p = p_{i} for i ≥ 0 \end{matrix}

In other words, replace p_{0} by p_{1}, p_{1} by p_{2} … but leave the atomic propositions q_{0}, q_{1}, …, q_{x} untouched. For α ∈ Φ, let α′ abbreviate g_{0}(α).

Extend the consistent set {α_{0}} to a maximal consistent set A. Let A′ = g_{0}(A). Clearly A′ is free of p_{0}.

Lemma 5.9 A′ is consistent and α_{0} ∈ A′. Moreover A′ ∪ {p̂_{0}} is consistent.

Proof Suppose A′ is not consistent. Then we must have ⊢ ¬α′ for some α′ ∈ A′. Let h_{0} : P → P be given by:

∀p ∈ P : h_{0}(p) = \{ \begin{matrix}p, & if p ∈ \{q_{0}, q_{1}, …, q_{x}\} ∪ \{p_{0}\} \\ p_{i−1}, & if p = p_{i} for i ≥ 1 \end{matrix}

It is easy to check that h_{0}(α′) = α. Then, by the derived inference rule SUB, ⊢ ¬α, which is a contradiction because α ∈ A. Hence A′ is consistent. Since g_{0}(α_{0}) = α_{0}, α_{0} ∈ A′.

Next, we must verify that A′ ∪ p̂_{0} is consistent. Suppose not. Then ⊢ p̂_{0} ^{⊃} ¬α′ for some α′ ∈ A′. By the choice of g_{0}, α′ is free of p_{0}. Hence, by UNIQ, ⊢ ¬α′, which contradicts the consistency of A′.

□

Now extend A′ ∪{p̂_{0}} to an MCS A_{0}. Set CH_{0} = (ES_{0}, T_{0}, ∅), where ES_{0} = ({e_{0}}, ∅, ∅) and T_{0}(e_{0}) = A_{0}. We can verify that CH_{0} satisfies the inductive conditions IC.

We now proceed to construct CH_{i+1} from CH_{i}. The basic idea is to “kill” some live requirement (e, β) present in CH_{i}. While doing so, we do not wish to “disturb” the fact that α_{0} ∈ T_{i}(e_{0}) and p̂_{j} ∈ T_{i}(e_{j}) for each e_{j} ∈ E_{i}, 0 ≤ j ≤ i. At the same time, in case the event e_{i+1} is added to E_{i} to kill (e, β), it should be named p̂_{i+1}, for which we shall have to “shift up” propositions p_{i+1}, p_{i+2} … as we did for p_{0} using g_{0}. Consequently, we shall demand two things of the live requirement (e, β) chosen to be “killed”.

(i) At most the propositions q_{0}, q_{1}, …, q_{x}, p_{0}, p_{1}, …, p_{i} may appear in β.

(ii) Among all the live requirements in CH_{i} which satisfy (i), (e, β) has the least index in the enumeration which we have fixed for Ẽ × Φ.

To be precise, for j ≥ 0 let Σ_{j} = {q_{0}, q_{1}, …, q_{x}} ∪ {p_{0}, p_{1}, …, p_{j}}. Let Φ_{j} be the least subset of Φ containing Σ_{j} such that if γ and δ are in Φ_{j} then so are ¬γ, γ ∨ δ, □γ, □ - γ, ▽ · γ, △ · γ and ▽ ·_{μ}γ. Clearly Φ = ⋃_{j≥0} Φ_{j}.

Among all the live requirements of the form (e′, β′) in CH_{i} which satisfy the condition β′ ∈ Φ_{i}, let (e, β) be the live requirement with the least index (in the enumeration we have fixed for Ẽ × Φ). If there are no such live requirements, set CH_{i+1} = CH_{i}. Otherwise, assume that e = e_{j}, j ∈ {0, 1, …, i}. We shall deal in detail with the case where β is of the form ▽_{μ}β_{0}.

The live requirement (e_{j}, ▽_{μ}β_{0}) in CH_{i} can be killed in two different ways. In fact, this is the reason why we give a detailed treatment of this case. For all other cases (e, β) can be killed in only one way. This will become clearer as we proceed.

The first case corresponds to the situation where there already exists e_{k} ∈ E_{i} such that β_{0} ∈ T_{i}(e_{k}) and e_{j} #_{μ}_{i} e_{k}, but (e_{j}, e_{k}) ∉ μ_{i}. In other words, e_{k} was added at stage k < i to kill some other live requirement, and (e_{j}, e_{k}) “accidentally” happens to belong to #_{μ}_{i}. In general, we cannot assume that the event e_{k} kills the live requirement (e_{j}, ▽_{μ}β_{0}) because #_{μ}_{i} is not stable with respect to our inductive construction. For example, given (e_{j}, e_{k}) ∈ #_{μ}_{i}, we may add e_{i+1} to E_{i} to kill a past requirement of the form (e_{k}, ◇ - γ), and set e_{i+1} <_{i+1} e_{k} and e_{i+1} #_{i+1} e_{j} whereby (e_{j}, e_{k}) ∉ #_{μ}_{i+1}. As a result, if the liveness of minimal choice requirements were to be defined with respect to the relation #_{μ}_{i}, requirements assumed to be killed at earlier stages in the construction may become live again at later stages.

This is precisely the reason why we identify a special subset of #_{μ}_{i} by μ_{i}. From the way we build up μ_{i}, it will turn out that if an element of #_{μ}_{i} is included in μ_{i}, then it will always remain in #_{μ}_{n} for all n > i. Thus, by killing a minimal choice requirement using an element in μ_{i}, we can ensure that the requirement never becomes live again.

On the other hand, it will turn out that R_{i} ⊆ R_{i+1} for R ∈ {<, >, #, co}. The inductive conditions IC will then ensure that for live requirements of the form (e_{j}, ◇β_{0}), (e_{j}, ◇ - β_{0}), (e_{j}, ▽β_{0}) and (e_{j}, △β_{0}), once the requirement has been killed at some stage k, the requirement never becomes live again at any later stage.

Suppose then that there exists e_{k} ∈ E_{i} such that e_{j} #_{μ}_{i} e_{k} and β_{0} ∈ T_{i}(e_{k}) and, further, T_{i}(e_{j}) ˜#_{μ} T_{i}(e_{k}). Set E_{i+1} = E_{i}, <_{i+1}=<_{i}, #_{i+1} = #_{i} and T_{i+1} = T_{i}. Finally, set μ_{i+1} = μ_{i} ∪ {(e_{j}, e_{k}), (e_{k}, e_{j})}.

It is easy to verify that CH_{i+1} is a well defined chronicle structure. We know that ES_{i+1} = ES_{i} and T_{i+1} = T_{i}, so all we have to check is that μ_{i+1} ⊆ #_{μ}_{i+1}. Since μ_{i} ⊆ #_{μ}_{i} by the inductive hypothesis and the new elements added to μ_{i} to obtain μ_{i+1} were assumed to be in #_{μ}_{i}, we know that μ_{i+1} ⊆ #_{μ}_{i}. But clearly #_{μ}_{i} = #_{μ}_{i+1} and so μ_{i+1} ⊆ #_{μ}_{i+1} as well.

It is straightforward to check that CH_{i+1} satisfies the inductive conditions IC. Clearly (e_{j}, ▽_{μ}β_{0}) is no longer a live requirement in CH_{i+1}. It is also easy to see that for all β′ ∈ Φ_{i} and for all e_{k} ∈ E_{i}, if (e_{k}, β′) is not a live requirement in CH_{i} then it is not a live requirement in CH_{i+1} either.

Now we consider the more difficult case. Assume that there does not exist e_{k} ∈ E_{i} with e_{j} #_{μ}_{i} e_{k} such that β_{0} ∈ T_{i}(e_{k}) and T_{i}(e_{j}) ˜#_{μ} T_{i}(e_{k}).

To kill the live requirement (e_{j}, ▽_{μ}β_{0}) in this case, we will extend ES_{i} to ES_{i+1} so that E_{i+1} = E_{i} ∪ {e_{i+1}} and R_{i+1} ∩ (E_{i} × E_{i}) = R_{i} for R ∈ {<, >, #, co}. We will transform T_{i} to T_{i+1} in such a way that T_{i+1}(e_{k}) ∩ Φ_{i} = T_{i}(e_{k}) ∩ Φ_{i} for all e_{k} ∈ E_{i}, 0 ≤ k ≤ i. We will ensure that (e_{j}, e_{i+1}) ∈ μ_{i+1} and β_{0} ∈ T_{i+1}(e_{i+1}) so that (e_{j}, ▽_{μ}β_{0}) is not a live requirement in CH_{i+1}. Naturally, in all this we must ensure that CH_{i+1} satisfies the inductive assumptions IC.

The actual steps involved in the construction are as follows.

First we must “free” p_{i+1} so that e_{i+1} can be labelled with p̂_{i+1}. To do this, define the function g_{i+1} : P → P as follows:

∀p ∈ P : g_{i+1}(p) = \{ \begin{matrix}p, & if p ∈ \{q_{0}, q_{1}, …, q_{x}\} ∪ \{p_{0}, p_{1}, …, p_{i}\} \\ p_{k+1}, & if p = p_{k} for k ≥ i + 1 \end{matrix}

In other words, g_{i+1} replaces p_{i+1} by p_{i+2}, p_{i+2} by p_{i+3} … but leaves q_{0}, q_{1}, …, q_{x} and p_{0}, p_{1}, …, p_{i} untouched. For α ∈ Φ, let α′ abbreviate g_{i+1}(α).

For convenience, let A_{k} denote T_{i}(e_{k}) and let A′_{k} denote g_{i+1}(A_{k}) for e_{k} ∈ E_{i}, 0 ≤ k ≤ i. By Lemma 5.9, A′_{k} is consistent for all such k.

The next step in the construction is to transform T_{i} to T_{i+1}. We begin by creating a consistent set of formulas containing β_{0} and p̂_{i+1} which is in ˜#_{μ} with A′_{j}.

Lemma 5.10 A′_{i+1} = {α′ | ▽ ·_{μ}α′ ∈ A′_{j}} ∪ {β_{0}} ∪ {p̂_{i+1}} is consistent.

Proof Suppose not. Then ⊢ p̂_{i+1} ^{⊃} ¬(α′ ∧ β_{0}) for some α′ such that ▽ ·_{μ}α ∈ A_{j}. The definition of g_{i+1} ensures that α′ is free of p_{i+1}. Since we chose (e_{j}, ▽_{μ}β_{0}) as the live requirement to be killed at stage i, we know that ▽_{μ}β_{0} ∈ Φ_{i} and so β_{0} ∈ Φ_{i} as well. But p_{i+1} ∉ Σ_{i}, so β_{0} is also free of p_{i+1}. Hence, by the rule UNIQ, we get ⊢ ¬(α′ ∧ β_{0}). By TG, we then get ⊢ ▽ ·_{μ}¬(α′ ∧ β_{0}) and hence ⊢ ¬▽_{μ}(α′ ∧ β_{0}). Now, consider the function h_{i+1} : P → P given by:

∀p ∈ P : h_{i+1}(p) = \{ \begin{matrix}p, & if p ∈ \{q_{0}, q_{1}, …, q_{x}\} ∪ \{p_{0}, p_{1}, …, p_{i+1}\} \\ p_{k−1}, & if p = p_{k} for k ≥ i + 2 \end{matrix}

Since h_{i+1}(¬▽_{μ}(α′ ∧ β_{0})) = ¬▽_{μ}(α ∧ β_{0}), using the derived rule SUB we get ⊢ ¬▽_{μ}(α ∧ β_{0}). But we began with ▽ ·_{μ}α ∈ A_{j}. Since ▽_{μ}β_{0} ∈ A_{j} as well and A_{j} is an MCS, by TK3 we get ▽_{μ}(α ∧ β_{0}) ∈ A_{j}. So ▽_{μ}(α ∧ β_{0}) is consistent, which is a contradiction.

□

Extend A′_{i+1} to an MCS B_{i+1}. We now have to go back and extend A′_{j} to an MCS that is in ˜#_{μ} with B_{i+1}.

Lemma 5.11 A′_{j} ∪ {β | ▽ ·_{μ}β ∈ B_{i+1}} is consistent.

Proof Suppose not. Then ⊢ α′ ^{⊃} ¬β for some α ∈ A_{j} and ▽ ·_{μ}β ∈ B_{i+1}. But then, by axiom A4(ii), ▽ ·_{μ}▽_{μ}α ∈ A_{j} and hence ▽ ·_{μ}▽_{μ}α′ ∈ A′_{j}. As a result, ▽_{μ}α′ ∈ A′_{i+1} ⊆ B_{i+1}. Now, applying DRK(ii) to ⊢ α′ ^{⊃} ¬β, we get ⊢ ▽_{μ}α′ ^{⊃} ▽_{μ}¬β, which then implies that ▽_{μ}¬β ∈ B_{i+1}. This contradicts the assumption that ▽ ·_{μ}β ∈ B_{i+1}.

□

Now extend A′_{j} ∪ {β | ▽ ·_{μ}β ∈ B_{i+1}} to an MCS B_{j}. It is easy to verify that B_{j} ˜#_{μ} B_{i+1}.

T_{i+1} will assign B_{i+1} to e_{i+1} and B_{j} to e_{j}. We must now extend T_{i+1} to the events in E_{i} − {e_{j}}. We shall deal with the concrete case where e_{k} ∈ E_{i} − {e_{j}} and e_{k} <_{i} e_{j}. Let A_{k}^{∗} = {β | □ - β ∈ B_{j}}.

Lemma 5.12 A′_{k} ∪ A_{k}^{∗} is consistent.

Proof Suppose not. Then ⊢ α′ ^{⊃} ¬β for some α ∈ A_{k} and □ - β ∈ B_{j}. Since T_{i} was a coherent chronicle on ES_{i}, we must have had A_{k} ˜< A_{j}. So, ◇ - α ∈ A_{j} and hence ◇ - α′ ∈ A′_{j} ⊆ B_{j}. Applying DRK(ii) to ⊢ α′ ^{⊃} ¬β we get ⊢ ◇ - α′ ^{⊃} ◇ - ¬β, which implies that ◇ - ¬β ∈ B_{j}. This contradicts the assumption □ - β ∈ B_{j}.

□

Extend A′_{k} ∪ A_{k}^{∗} to an MCS B_{k}. It is straightforward to verify that B_{k} ˜< B_{j}.

For the cases e_{k} >_{i} e_{j}, e_{k} #_{i} e_{j} and e_{k} co_{i} e_{j}, we set A_{k}^{∗} to {β | □β ∈ B_{j}}, {β | ▽ · β ∈ B_{j}} and {β | △ · β ∈ B_{j}} respectively. In each case, by an argument similar to Lemma 5.12, A′_{k} ∪ A_{k}^{∗} is consistent and can be extended to an MCS B_{k}.

At this stage, for each e_{k} ∈ E_{i+1}, 0 ≤ k ≤ i + 1, we have managed to find an MCS B_{k} which shall use to define T_{i+1}. We can now define CH_{i+1} = (ES_{i+1}, T_{i+1}, μ_{i+1}), where ES_{i+1} = (E_{i+1}, <_{i+1}, #_{i+1}), as follows:

(i) E_{i+1} = E_{i} ∪ {e_{i+1}}.

(ii) <_{i+1} =<_{i} \begin{matrix}∪ & \{(e_{k}, e_{i+1}) | e_{k} ∈ E_{i}, 0 ≤ k ≤ i, and B_{k} ˜< B_{i+1}\} \\ ∪ & \{(e_{i+1}, e_{k}) | e_{k} ∈ E_{i}, 0 ≤ k ≤ i, and B_{i+1} ˜< B_{k}\} \end{matrix} .

(iii) >_{i+1} = (<_{i+1})^{−1}.

(iv) #_{i+1} = #_{i} ∪ {(e_{k}, e_{i+1}), (e_{i+1}, e_{k}) | e_{k} ∈ E_{i}, 0 ≤ k ≤ i, and B_{k} ˜# B_{i+1}}.

(v) co_{i+1} = (E_{i+1} × E_{i+1}) − (<_{i+1} ∪ >_{i+1} ∪ #_{i+1} ∪ id_{i+1}).

(vi) ∀e_{k} ∈ E_{i+1} : T_{i+1}(e_{k}) = B_{k}.

(vii) μ_{i+1} = \{ \begin{matrix}μ_{i} ∪ \{(e_{j}, e_{i+1}), (e_{i+1}, e_{j})\} & if the live requirement considered at stage \\ & i was of the form (e_{j}, ▽_{μ}β_{0}) \\ & (which we are assuming to be the case) \\ μ_{i} & otherwise \end{matrix}

We have to do a fair amount of work to prove the next result. The details are given in the appendix.

Lemma 5.13 CH_{i+1} is a well defined chronicle structure which satisfies the inductive conditions IC.

Clearly, by our construction, the live requirement (e_{j}, ▽_{μ}β_{0}) that we selected for killing in CH_{i} is not live in CH_{i+1}. To ensure that our inductive construction works properly, we finally have to show that all live requirements killed at earlier stages remain “dead” in CH_{i+1}.

Lemma 5.14 ∀e ∈ E_{i} : ∀α ∈ Φ_{i} : (e, α) is not a live requirement in CH_{i} implies that it is not a live requirement in CH_{i+1}.

Proof This follows from the following two observations.

(i) In extending CH_{i} to CH_{i+1} we preserve the semantic relationships between the MCSs assigned by T_{i}.

(ii) Formulas from Φ_{i} are left untouched in the MCSs assigned by T_{i} during the process of “shifting up” propositions to accommodate p̂_{i+1} in T_{i+1}(e_{i+1}).

□

The other four types of live requirements — (e_{j}, ◇β_{0}), (e_{j}, ◇ - β_{0}), (e_{j}, ▽β_{0}), (e_{j}, △β_{0}) — are also killed by adding an event e_{i+1} to E_{i} and extending ES_{i} to ES_{i+1} and T_{i} to T_{i+1} in a suitable manner. The procedure is almost identical to that described above for the case (e_{j}, ▽_{μ}β_{0}). Virtually the only change to be made is in the step where B_{i+1} is constructed. For live requirements of the form (e_{j}, ◇β_{0}), (e_{j}, ◇ - β_{0}), (e_{j}, ▽β_{0}) and (e_{j}, △β_{0}), B_{i+1} and B_{j} must be suitably defined so that B_{j} ˜< B_{i+1}, B_{j} ˜> B_{i+1}, B_{j} ˜# B_{i+1} and B_{j} c̃o B_{i+1} respectively. The new event e_{i+1} can then be “hooked up” to the other events in E_{i} exactly as described above, yielding a chronicle structure CH_{i+1} in which the requirement considered at stage i is no longer live. In all four cases μ_{i} is left untouched — i.e μ_{i+1} = μ_{i}.

Thus, we can construct an infinite sequence of chronicle structures CH_{0}, CH_{1}, … so that each member of the sequence satisfies the inductive conditions IC. Now define CH = (ES, T, μ) where:

• ES = (E, <, #), with E = ⋃_{i≥0} E_{i}, <= ⋃_{i≥0} <_{i}, and # = ⋃_{i≥0} #_{i}.

• T : E → 2^{Φ} is given by:

∀e_{i} ∈ E : T (e_{i}) = ⋃{T_{j}(e_{i}) ∩ Φ_{j} | j ≥ i}.

• μ = ⋃_{i≥0} μ_{i}.

We can then verify the following result, whose proof is given in the Appendix.

Lemma 5.15 CH = (ES, T, μ) is a perfect chronicle structure in which α_{0} ∈ T (e_{0}).

From the preceding lemma and Lemma 5.8 it follows that every consistent formula α_{0} is satisfiable. We have thus established our main result.

Theorem 5.16 (Completeness) If ⊧ α then ⊢ α.

It is straightforward to extend this result to obtain completeness for finite theories.

Corollary 5.17 Let {α_{1}, α_{2}, …, α_{n}} be a finite set of formulas. If {α_{1}, α_{2}, …, α_{n}} ⊧ β then {α_{1}, α_{2}, …, α_{n}} ⊢ β.

Proof By Theorem 3.1, we know that {α_{1}, α_{2}, …, α_{n}} ⊧ β iff ⊧ E(α_{1} ∧α_{2} ∧…∧α_{n}) ^{⊃} β. Since our axiomatization is complete, we know that ⊧ E(α_{1} ∧α_{2} ∧…∧α_{n}) ^{⊃} β implies ⊢ E(α_{1} ∧α_{2} ∧…∧α_{n}) ^{⊃} β. By Theorem 4.2, {α_{1}, α_{2}, …, α_{n}} ⊢ β iff ⊢ E(α_{1} ∧ α_{2} ∧ … ∧ α_{n}) ^{⊃} β and we are done.

□

6 Discussion

In this paper we have obtained a sound and complete axiomatization of the class of well branching prime event structures. We have achieved this using a temporal logic which appears to be rich in expressive power.

Our completeness proof leans heavily on the techniques developed in our earlier work [11]. However, the logic considered there did not have the ▽ ·_{μ} operator. Moreover the frames for the logic consisted of all prime event structures. As noted earlier, what we really need is a logic that characterizes finitary prime event structures. It is easy to check that every finitary prime event structure is also well branching. Thus the present work, in comparison to [11] represents advances on two fronts; the set of frames has been suitably shrunk (though not as much as we would have liked) and the logical language, due to the addition of the ▽ ·_{μ} operator, is provably more expressive [9]. The present completeness proof also requires some new ideas and is a lot more delicate.

Partial orders have also been considered as structures for temporal logics by — among others — Pinter and Wolper [17] and Katz and Peled [5]. In these studies assertions are tied directly to the global states of the system. Also, there are no modalities for directly expressing concurrency and conflict.

In [6, 7] and in the much improved [8] a subclass of event structures is used to model systems of communicating sequential agents. The logical language consists of future and past modalities indexed by the names of the agents. There are no modalities to express conflict and concurrency.

As mentioned earlier, Penczek [15, 16] has carried out closely related work. He was the first one to identify the ▽ · operator and use it to exploit the important notion of a run. In [15] a sound and complete axiomatization of (all) prime event structures is given. In our notation, the logical language consists of the □, □ - and the ▽ · operators with neither the △ · operator nor the ▽ ·_{μ} operator. Moreover, a special proposition ρ is reserved in the language and is used to mark the runs of an event structure. A frame consists of an event structure together with a run. The valuation function is required to ensure that the special proposition ρ is assigned the run associated with the frame.

It is easy to check that we could, if we wished to, follow the same route using well branching event structures. As in [15] we would add ρ ≡ ▽ · ¬ρ as an axiom to our system. We would then get a sound and complete axiomatization (with respect to the extended notion of frames and models) in the presence of the additional operators △ · and ▽ ·_{μ}. Consequently the resulting logic would be more powerful in comparison to [15] with the added advantage that non-well branching event structures would not arise in the process of producing models for consistent formulas.

We feel however that it is better to retain a “pure” notion of frames and embed the notion of a run into theories concerning specific applications as indicated in Section 3. This is so because this nice idea of Penczek to logically talk about runs can be extended in a number of useful ways. And these extensions, if brought into the “core” language, would lead to more and more elaborate notions of frames. It would then be difficult to distinguish the foundation from the superstructure, so to speak.

For instance one could reserve a special proposition τ and use it mark the sequential components of an event structure. By a sequential component we mean a maximal co-free subset of the events. The axiom τ ≡ △ · ¬τ will then capture this notion. One could reserve two more propositions λ and χ and use them to mark the maximal chains and anti-chains of an event structure. The respective characteristic axioms would be λ ≡ △ · ¬λ ∧ ▽ · ¬λ and χ ≡ □¬χ ∧ □ - ¬χ. We could go further down this road but we will stop here. The point however is that the logic presented here appears to be well suited for capturing many interesting behavioural notions concerning event structures.

Turning now to [16], Penczek also introduces what he calls an immediate conflict operator which we will denote here as ▽ · _{m} . However, all that is required of the corresponding frame relation #_{m} is that it should generate the conflict relation # via the causality relation in the obvious sense. As a result, for a fixed # very many subsets of # could play the role of #_{m}. In particular, #_{m} could be # itself! Stated differently, all that is demanded semantically from ▽ · _{m} is that the axiom A7 be sound. The problem of course is that A8(i) which is in some sense the characteristic axiom for the minimal conflict relation cannot be formulated in [16] due to the absence of the △ · operator.

It is worth pointing out in this connection that the term immediate conflict is suggested by net theory. With each event structure, one can associate a special kind of net called an occurrence net [18]. For occurrence nets the notion of two events being in immediate conflict is well-defined — they should share a pre-condition. However, the means for associating occurrence nets with event structures suggested in [18], and also in [13], would identify #_{m} with #. Thus the notion of immediate conflict, applied to prime event structures, is not an interesting behavioural notion.

At present we do not know any thing about the decidability of our system. The finite model property does not hold and hence standard filtration techniques are not applicable. It seems difficult to identify a suitable notion of a pseudo model in which the causality relation will be just a preorder. Stated differently, what is lacking is a finite representation of event structures that are possibly infinite but “regular”. The model checking problem is also at present not meaningful because we do not know what finite but “cyclic” event structures look like. Notice in this connection that the weaker system of [15] is shown by Penczek to be decidable.

As mentioned in Section 1, we lack the means for handling labelled event structures. One possibility would be to introduce next state and previous state operators and use reserved propositions to code up the label set. Once again due to the lack of a suitable notion of a pseudo model, standard techniques cannot be applied to obtain completeness.

Finally the problem of characterizing finitary event structures seems to be a difficult one. The standard well foundedness axiom for irreflexive frames ◇ - α ^{⊃} ◇ - (α ∧ □ - ¬α) will certainly be sound for finitary event structures. However, the past of an event will in general be a partially ordered set rather than a totally ordered set. Hence even well foundedness seems to be hard to capture let alone finitariness.

Acknowledgments Mogens Nielsen independently came up with the idea of replacing the conflict operator by the more useful minimal conflict operator. We thank him for useful discussions.

U. Goltz and W. Penczek found a mistake in an earlier version of this work. In the process of fixing this mistake, we were led to the well branching property.

We also thank the anonymous referees for their constructive comments and suggestions for improving the presentation.

References

[1] Burgess, J. P., Basic Tense Logic, In The Handbook of Philosophical Logic, Vol. II, eds. Gabbay, D. and Guenthner, F., D. Reidel Publishing Company, Dordrecht, The Netherlands (1984) 89-133.

[2] Burgess, J. P., Decidability for Branching Time, Studia Logica, XXXIX, 2/3 (1980) 203-218.

[3] Chandy, K. M. and Lamport, L., Distributed Snapshots: Determining Global States of Distributed Systems, ACM Transactions on Computer Systems, 3, 1 (1985) 63-75.

[4] Hughes, G. E. and Creswell, M. J., An Introduction to Modal Logic, Methuen and Co., London (Reprinted in 1982).

[5] Katz, S. and Peled, D., An Efficient Verification Method for Parallel and Distributed Programs, Springer Lecture Notes in Computer Science 354 (1989) 489-507.

[6] Lodaya, K and Thiagarajan, P. S., A Modal Logic for a Subclass of Event Structures, Springer Lecture Notes in Computer Science 267 (1987) 290-303.

[7] Lodaya, K. and Thiagarajan, P. S., A Correction to “A Modal Logic for a Subclass of Event Structures”, Report DAIMI-PB-275, Computer Science Department, Aarhus University, Aarhus, Denmark (1989).

[8] Lodaya, K., Ramanujam, R. and Thiagarajan, P. S., Temporal Logics for Communicating Sequential Agents, Report IMSc/89/15, The Institute of Mathematical Sciences, Madras, India (1989).

[9] Mukund, M., Expressiveness and Completeness of a Logic for Well Branching Prime Event Structures, Report TCS-90-1, School of Mathematics, SPIC Science Foundation, Madras, India (1990).

[10] Mukund, M. and Thiagarajan, P. S., A Petri Net Model of Asynchronously Communicating Sequential Processes, In Perspectives in Theoretical Computer Science — Commemorative Volume for Gift Siromoney, ed. Narasimhan, R., World Scientific, Singapore (1989) 165-198.

[11] Mukund, M. and Thiagarajan, P. S., An Axiomatization of Event Structures, Springer Lecture Notes in Computer Science 405 (1989) 143-160.

[12] Mukund, M. and Thiagarajan, P. S., An Axiomatization of Well Branching Prime Event Structures, Report TCS-90-2, School of Mathematics, SPIC Science Foundation, Madras, India (1990).

[13] Nielsen, M., Plotkin, G. and Winskel, G., Petri Nets, Event Structures and Domains: Part I, Theoretical Computer Science, 13, 1 (1980) 86-108.

[14] Nielsen, M., Rozenberg, G. and Thiagarajan, P. S., Behavioural Notions for Elementary Net Systems, Distributed Computing, 4, 1 (1990) 45-57.

[15] Penczek, W., A Temporal Logic For Event Structures, Fundamenta Informaticae, XI, (1988) 297-326.

[16] Penczek, W., A Temporal Logic for the Local Specification of Concurrent Systems, In Information Processing 89, ed. Ritter, G. X., Elsevier Science Publishers B.V. (1989) 857-862.

[17] Pinter, S. and Wolper, P., A Temporal Logic for Reasoning About Partially Ordered Computations, Proc. 3^{rd} ACM Symposium on Principles of Distributed Computing, Vancouver (1984) 28-37.

[18] Winskel, G., Event Structures, Springer Lecture Notes in Computer Science 255 (1987) 325-392.

A Appendix

Here we fill in the details of the completeness proof which are missing in Section 5. In this appendix, we describe in detail the inductive hypotheses IC which are used in our incremental construction of a perfect chronicle and then provide the proofs of Lemmas 5.13 and 5.15.

First, we need some preliminary results concerning the semantic relations defined on MCSs. We begin with a characterization of ˜#_{μ} in terms of ˜#.

Lemma A.1 Suppose A and B are MCSs such that A ˜# B and p is an atomic proposition such that

p̂ ∈ B and ▽_{μ}p̂ ∈ A. Then A ˜#_{μ} B.

Proof It suffices to show that {▽_{μ}β | β ∈ B} ⊆ A. Suppose that β ∈ B and ▽_{μ}β ∉ A. Then, since A is an MCS, ¬▽_{μ}β ∈ A and hence ▽ ·_{μ}¬β ∈ A. We know that ▽_{μ}p̂ ∈ A, so in fact ▽_{μ}p̂ ∧ ▽ ·_{μ}¬β ∈ A. Hence, by TK3, ▽_{μ}(p̂ ∧ ¬β) ∈ A and so, by axiom A7, ▽(p̂ ∧ ¬β) ∈ A as well. But, by Tp̂(v), ▽(p̂ ∧ ¬β) ^{⊃} ▽ · (p̂^{⊃} ¬β) so we must have ▽ · (p̂^{⊃} ¬β) ∈ A. Then, since A ˜# B, (p̂^{⊃} ¬β) ∈ B by the definition of ˜#. But (p̂^{⊃} ¬β) ∈ B and p̂ ∈ B implies that ¬β ∈ B, which is a contradiction.

□

Let E = {e_{1}, e_{2}, e_{3}} be a set of three events. Suppose we choose relations R_{12}, R_{13} ∈ {<, >, #, co} and let e_{1} R_{12} e_{2} and e_{1} R_{13} e_{3}. It is easy to verify that we can always complete the “triangle”, choosing an appropriate R_{23} ∈ {<, >, #, co}, such that setting e_{2} R_{23} e_{3} yields a valid event structure ES = (E, <, #).

The next lemma establishes an analogous result for MCSs.

Lemma A.2 Let A, B and C be distinct MCSs such that A R̃_{1} B and A R̃_{2} C for R̃_{1}, R̃_{2} ∈ { ˜<, ˜>, ˜#, c̃o} as specified in Table 1. Then it must be the case that B R̃_{3} C, R̃_{3} ∈ { ˜<, ˜>, ˜#, c̃o}, for at least one of the options specified for R̃_{3} in the corresponding row of Table 1.

R̃_{1}  R̃_{2}  R̃_{3}
˜<  ˜<  ˜<, ˜>, ˜#, c̃o
˜<  ˜>  ˜>
˜<  ˜#  ˜#
˜<  c̃o  ˜>, ˜#, c̃o
˜>  ˜>  ˜<, ˜>, c̃o
˜>  ˜#  ˜<, ˜#, c̃o
˜>  c̃o  ˜<, c̃o
˜#  ˜#  ˜<, ˜>, ˜#, c̃o
˜#  c̃o  ˜>, ˜#, c̃o
c̃o  c̃o  ˜<, ˜>, ˜#, c̃o

Table 1:

Proof Consider the case where A ˜< B and A ˜< C. Since B and C are distinct, there exists β ∈ B such that β ∉ C. Now, suppose that (B, C) ∉ { ˜>, ˜<, ˜#, c̃o}. Then, by Proposition 5.2, there exist γ_{1}, γ_{2}, γ_{3}, γ_{4} ∈ B such that ◇γ_{1} ∉ C, ◇ - γ_{2} ∉ C, ▽γ_{3} ∉ C and △γ_{4} ∉ C.

Let δ =^{def} β∧γ_{1}∧γ_{2}∧γ_{3}∧γ_{4}. Since A ˜< B and δ ∈ B, Proposition 5.2 guarantees that ◇δ ∈ A. Hence, by axiom A9(i) we must have □(δ ∨ ◇δ ∨ ◇ - δ ∨ ▽δ ∨ △δ) ∈ A, since A is an MCS. But then, since A ˜< C, we appeal to the definition of ˜< to conclude that (δ ∨ ◇δ ∨ ◇ - δ ∨ ▽δ ∨ △δ) ∈ C. Hence, δ ∈ C or ◇δ ∈ C or ◇ - δ ∈ C or ▽δ ∈ C or △δ ∈ C. If δ ∈ C, then β ∈ C as well. Alternatively, if ◇δ ∈ C, then since δ =^{def} β ∧ γ_{1} ∧ γ_{2} ∧ γ_{3} ∧ γ_{4} and ⊢ ◇(β ∧ γ_{1} ∧ γ_{2} ∧ γ_{3} ∧ γ_{4}) ^{⊃} ◇β ∧ ◇γ_{1} ∧ ◇γ_{2} ∧ ◇γ_{3} ∧ ◇γ_{4} (TK2), we must have ◇γ_{1} ∈ C. Similarly, if ◇ - δ ∈ C then ◇ - γ_{2} ∈ C, if ▽δ ∈ C then ▽γ_{3} ∈ C and if △δ ∈ C then △γ_{4} ∈ C. In any case, we obtain a contradiction.

The proofs of the other cases are similar. Instead of axiom A9(i), we would have to use axioms A5, A6, A9(ii) to A9(iv) and A10 and theses T8Dual, T11Dual and T12Dual.

The requirement that the MCSs be distinct is strictly necessary only for the cases which use axiom A9, but the more restrictive statement of the lemma will be sufficient for our purposes.

□

Note that there are no entries for ˜#_{μ} in the table above. It turns out that it is sufficient to establish the following result in this connection.

Lemma A.3 Let A, B and C be MCSs such that A ˜#_{μ} B and A ˜> C. Then, either B ˜> C or B c̃o C.

Proof Similar to the proof of Lemma A.2, using axiom A8(i).

□

The next lemma demonstrates why we have been naming MCSs using formulas of the form p̂.

Lemma A.4 Let A be an MCS such that p̂ ∈ A, p ∈ P. Then, for any other MCS B, (A, B) can be in at most one of the semantic relations { ˜<, ˜>, ˜#, c̃o}.

Proof Consider the case where A ˜# B. By Proposition 5.2, we know that ▽p̂ ∈ B. But ▽p̂^{⊃} ¬p∧□¬p∧ □ - ¬p∧△ · ¬p by the thesis Tp̂(iii). By again appealing to Proposition 5.2, it follows that (A, B) ∉ { ˜<, ˜>, c̃o}. A similar argument can be used for the cases A ˜< B, A ˜> B and A c̃o B.

□

With these preliminaries out of the way, we can now describe in detail the inductive hypotheses IC. Recall that at stage i we assume that we have built up a chronicle structure CH_{i} = (ES_{i}, T_{i}, μ_{i}), where ES_{i} = (E_{i}, <_{i}, #_{i}). Henceforth let co_{i} and #_{μ}_{i} denote the concurrency and minimal conflict relations of ES_{i} respectively. The inductive conditions satisfied by CH_{i} consist of five clauses.

(C1) E_{i} ⊆ {e_{0}, e_{1}, …, e_{i}}.

(C2) For 0 ≤ j ≤ i, if e_{j} ∈ E_{i} then p̂_{j} ∈ T_{i}(e_{j}).

(C3) α_{0} ∈ T_{i}(e_{0}).

(C4) ∀e_{j}, e_{k} ∈ E_{i}, 0 ≤ j, k ≤ i : T_{i}(e_{j}) R̃ T_{i}(e_{k}) iff e_{j} R_{i} e_{k}, where R ∈ {<, >, #, co}.

(C5) ∀e_{j}, e_{k} ∈ E_{i}, 0 ≤ j, k ≤ i : (e_{j}, e_{k}) ∈ μ_{i} implies T_{i}(e_{j}) ˜#_{μ} T_{i}(e_{k}).

(C2) ensures that each event e_{j} present in E_{i} is assigned the unique name p̂_{j} by T_{i}. Note that the “⇐” direction of (C4) along with (C5) imply that CH_{i} is coherent. We have chosen to state the conditions separately because it turns out to be more convenient. Also, note that (C4) does not cover the case e_{j} #_{μ}_{i} e_{k}. It is thus possible that e_{j} #_{μ}_{i} e_{k} whereas (T_{i}(e_{j}), T_{i}(e_{k})) ∉ ˜#_{μ}.

Before beginning the proof of Lemma 5.13, we explicitly state and prove a result which has been mentioned in passing while describing the inductive construction.

Recall that we had abbreviated T_{i}(e_{k}) by A_{k} for all e_{k} ∈ E_{i}. To kill the live requirement (e_{j}, ▽_{μ}β_{0}), we constructed an MCS B_{i+1} containing β_{0} and modified the MCS A_{j} to an MCS B_{j} such that B_{j} ˜#_{μ} B_{i+1}. We then modified the MCSs A_{k} corresponding to events e_{k} ∈ E_{i} − {e_{j}} to MCSs B_{k}, ensuring that the relationship between A_{j} and A_{k} was preserved between B_{j} and B_{k}.

We can now verify the following result.

Lemma A.5 For all e_{k} ∈ E_{i}, 0 ≤ k ≤ i, the following conditions hold:

(i) B_{k} ∩ Φ_{i} = T_{i}(e_{k}) ∩ Φ_{i} and p̂_{k} ∈ B_{k}.

(ii) For k ≠ j, if A_{k} R̃ A_{j} then B_{k} R̃ B_{j} for R̃ ∈ { ˜<, ˜>, ˜#, c̃o}.

Proof

(i) By the definition of g_{i+1}, for every α ∈ Φ_{i} we have g_{i+1}(α) = α and so α ∈ A′_{k} iff α ∈ A_{k}. But then our construction ensures that A′_{k} ⊆ B_{k} and hence T_{i}(e_{k}) ∩ Φ_{i} ⊆ B_{k} ∩ Φ_{i}.

To establish B_{k} ∩ Φ_{i} ⊆ T_{i}(e_{k}) ∩ Φ_{i}, suppose that there exists α ∈ B_{k} ∩ Φ_{i} such that α ∈ B_{k} − A_{k}. Then α ∉ A_{k} and consequently ¬α ∈ A_{k}. But this would imply that ¬α ∈ A′_{k} ⊆ B_{k} as well, which contradicts the consistency of B_{k}.

Since p̂_{k} ∈ Φ_{i} and p̂_{k} ∈ T_{i}(e_{k}) for all e_{k} ∈ E_{i}, it follows from the previous argument that p̂_{k} ∈ B_{k} as well.

(ii) Consider the case A_{k} ˜< A_{j}. Then {β | □ - β ∈ B_{j}} = A_{k}^{∗} ⊆ B_{k} by construction and so B_{k} ˜< B_{j}. (A_{k}^{∗} was defined immediately preceding Lemma 5.12). Similar remarks apply to the other cases.

□

Now we can prove Lemma 5.13.

Lemma 5.13 CH_{i+1} is a well defined chronicle structure which satisfies the inductive conditions IC.

Proof To verify that CH_{i+1} is a well defined chronicle structure, we have to check that ES_{i+1} is a well branching event structure and that μ_{i+1} ⊆ #_{μ}_{i+1}. It is then clear from the definition of T_{i+1} that T_{i+1} is a chronicle on ES_{i+1}.

Some of the inductive conditions can be verified before proving that CH_{i+1} is a chronicle structure.

Condition (C1) Assuming that E_{i} ⊆ {e_{0}, e_{1}, …, e_{i}}, our construction guarantees that E_{i+1} ⊆ {e_{0}, e_{1}, …, e_{i+1}}, so CH_{i+1} satisfies condition (C1).

Condition (C2) Lemma A.5(i) guarantees that we have not disturbed any of the formulas p̂_{k} in going from T_{i}(e_{k}) to T_{i+1}(e_{k}) for e_{k} ∈ E_{i}. We have also ensured that p̂_{i+1} ∈ B_{i+1} = T_{i+1}(e_{i+1}), so CH_{i+1} satisfies (C2).

Condition (C3) We know that α_{0} ∈ T_{i}(e_{0}) since CH_{i} satisfied condition (C3). Since α_{0} ∈ Φ_{0} ⊆ Φ_{i}, by Lemma A.5(i), α_{0} ∈ T_{i+1}(e_{0}) as well, so CH_{i+1} satisfies (C3).

Condition (C4) To verify that CH_{i+1} satisfies (C4) requires more effort. We have to show the following:

∀e_{k}, e_{m} ∈ E_{i+1} : ∀R ∈ {<, >, #, co} : e_{k} ≠ e_{m} implies (e_{k} R_{i+1} e_{m} iff B_{k} R̃ B_{m})

There are two cases to consider — either {e_{k}, e_{m}} ⊆ E_{i} or one of the two events is e_{i+1}.

Case 1: e_{k} and e_{m} both belong to E_{i}.

From the definition of ES_{i+1} it is clear that <_{i}=<_{i+1} ∩(E_{i} × E_{i}) and #_{i} = #_{i+1} ∩ (E_{i} × E_{i}). From this it also follows at once that co_{i} = co_{i+1} ∩ (E_{i} × E_{i}). Hence, we can conclude that e_{k} R_{i+1} e_{m} iff e_{k} R_{i} e_{m}, for R ∈ {<, >, #, co}. Since CH_{i} satisfies (C4) by the induction hypothesis, we know that e_{k} R_{i} e_{m} iff A_{k} R̃ A_{m} for R ∈ {<, >, #, co}. Thus, we only have to verify that A_{k} R̃ A_{m} iff B_{k} R̃ B_{m}.

We first show that A_{k} R̃ A_{m} implies B_{k} R̃ B_{m}, for R ∈ {<, >, #, co}.

In case e_{k} = e_{j} or e_{m} = e_{j}, the result follows from Lemma A.5(ii). Hence assume that e_{k} ≠ e_{j} and e_{m} ≠ e_{j}.

Suppose that A_{k} R̃ A_{m} for some R ∈ {<, >, #, co}. We shall deal with the case where A_{k} c̃o A_{m}. The other cases can be handled similarly.

First, since CH_{i} satisfies (C4), we know that e_{k} co_{i} e_{m}. Since ES_{i} is an event structure, the pairs (e_{k}, e_{j}) and (e_{m}, e_{j}) must each belong to one of the relations {<_{i}, >_{i}, #_{i}, co_{i}}. Thus, we have to consider all possible “triangles” involving these three events which fix e_{k} co_{i} e_{m}. Once again, we shall consider only one representative case.

Consider the case where e_{k} co_{i} e_{j} and e_{m} co_{i} e_{j}. From the induction hypothesis (C4) and Lemma A.5(ii) it follows that B_{k} c̃o B_{j} and B_{m} c̃o B_{j}. Note that B_{k} ≠ B_{m} because p̂_{k} ∈ B_{k} and p̂_{k} ∉ B_{m}. Hence, we can appeal to Lemma A.2 and conclude that (B_{k}, B_{m}) belongs to at least one relation from the set { ˜<, ˜>, ˜#, c̃o}. However, by Lemma A.4 B_{k} and B_{m} cannot be related by more that one of these four relations. Hence B_{k} and B_{m} must be related by exactly one of these four relations. Since △p̂_{k} ∈ A_{m} and (△p̂_{k})′ = △p̂_{k}, we know that △p̂_{k} ∈ A′_{m} ⊆ B_{m} as well. Then by Tp̂(iv), we have □¬p_{k} ∈ B_{m} and □ - ¬p_{k} ∈ B_{m} and ▽ · ¬p_{k} ∈ B_{m} and hence, by Proposition 5.2, (B_{k}, B_{m}) ∉ { ˜<, ˜>, ˜#}. Thus, it must be the case that B_{k} c̃o B_{m}.

Next, we must show that B_{k} R̃ B_{m} implies A_{k} R̃ A_{m} for R ∈ {<, >, #, co}. Suppose that (B_{k}, B_{m}) ∈ R̃, for some R ∈ {<, >, #, co} and (A_{k}, A_{m}) ∉ R̃. Since ES_{i} is an event structure, we know that (e_{k}, e_{m}) ∈ R_{i}^{∗} for some R^{∗} ∈ {<, >, #, co}. Then, since T_{i} satisfies condition (C4), it must be the case that (A_{k}, A_{m}) ∈ R̃^{∗} and so R^{∗} ≠ R. But, by the preceding argument, we must have (B_{k}, B_{m}) ∈ R̃^{∗} as well. This is a contradiction, because p̂_{k} ∈ B_{k} and thus, by Lemma A.4, (B_{k}, B_{m}) can belong to at most one semantic relation from { ˜<, ˜>, ˜#, c̃o}.

Case 2: e_{k} = e_{i+1} or e_{m} = e_{i+1}.

Assume without loss of generality that e_{m} = e_{i+1}. We first show that (B_{k}, B_{i+1}) is contained in exactly one of the semantic relations { ˜<, ˜>, ˜#, c̃o}.

By Lemma A.4, (B_{k}, B_{i+1}) can belong to at most one of the four semantic relations because p̂_{k} ∈ B_{k}. Hence it suffices to show that (B_{k}, B_{i+1}) is contained in at least one of the four relations.

If e_{k} = e_{j}, we know that B_{j} ˜#_{μ} B_{i+1}, which implies that B_{j} ˜# B_{i+1}

since ˜#_{μ} ⊆ ˜#.

On the other hand, suppose e_{k} ∈ E_{i}−{e_{j}}. Since ES_{i} is an event structure, we know that (e_{k}, e_{j}) ∈ R_{i} for some R ∈ {<, >, #, co}. Since ES_{i} satisfies (C4), A_{k} R̃ A_{j}. So, by Lemma A.5(ii) we know that B_{k} R̃ B_{j}. Since we also know that B_{j} ˜# B_{i+1}, we can appeal to Lemma A.2 to show that (B_{k}, B_{i+1}) must belong to at least one semantic relation.

Returning to the main proof, we know that (B_{k}, B_{i+1}) belongs to exactly one semantic relation from the set { ˜<, ˜>, ˜#, c̃o}. By the definition of <_{i+1} and #_{i+1}, the result follows at once for the case where (e_{k}, e_{i+1}) ∈ {<_{i+1}, >_{i+1}, #_{i+1}}. Therefore, consider the case where e_{k} co_{i+1} e_{i+1}. This implies that (B_{k}, B_{i+1}) ∉ { ˜<, ˜>, ˜#} and so it must be the case that B_{k} c̃o B_{i+1}.

Having verified that (C4) holds, we can show that ES_{i+1} is well defined.

Claim: ES_{i+1} is a well branching event structure

It suffices to show that ES_{i+1} is an event structure. Since E_{i+1} is a finite set it will then follow that ES_{i+1} is in fact well branching.

We know that ES_{i} is an event structure and that <_{i}=<_{i+1} ∩(E_{i} × E_{i}) and #_{i} = #_{i+1} ∩ (E_{i} × E_{i}). By the definition of <_{i+1} and #_{i+1}, it then follows that <_{i+1} and #_{i+1} are irreflexive and that #_{i+1} is symmetric. Thus, all we have to establish is that <_{i+1} is transitive and that #_{i+1} is inherited via <_{i+1}.

Now suppose that e_{k} <_{i+1} e_{l} <_{i+1} e_{m}. Since T_{i+1} satisfies (C4), we know that B_{k} ˜< B_{l} ˜< B_{m}. Hence, by Lemma A.2 it follows that B_{k} ˜< B_{m}. Thus, by (C4), we have e_{k} <_{i+1} e_{m} and so <_{i+1} is transitive.

Next, suppose that e_{k} #_{i+1} e_{l} <_{i+1} e_{m}. Once again, by (C4) we have B_{k} ˜# B_{l} ˜< B_{m} and thus B_{k} ˜# B_{m} by Lemma A.2. So, by (C4), e_{k} #_{i+1} e_{m}. Hence #_{i+1} is inherited via <_{i+1}. This establishes the claim.

Now all that remains to be shown is that CH_{i+1} satisfies (C5) and that μ_{i+1} ⊆ #_{μ}_{i+1}.

Condition(C5) We have to verify the following:

∀e_{k}, e_{m} ∈ E_{i+1} : (e_{k}, e_{m}) ∈ μ_{i+1} implies T_{i+1}(e_{k}) ˜#_{μ} T_{i+1}(e_{m}).

Suppose both e_{k} and e_{m} belong to E_{i}. Then (e_{k}, e_{m}) ∈ μ_{i}. Since CH_{i} was a chronicle structure, in ES_{i} we must have had e_{k} #_{μ}_{i} e_{m}. Hence e_{k} #_{i} e_{m} as well. So e_{k} #_{i+1} e_{m}, since #_{i} = #_{i+1} ∩ (E_{i} × E_{i}). Therefore, since T_{i+1} satisfies (C4), B_{k} ˜# B_{m}. We also know that A_{k} ˜#_{μ} A_{m} in CH_{i} by the inductive assumption (C5). Hence, ▽_{μ}p̂_{k} ∈ A_{m}. Since (▽_{μ}p̂_{k})′ = ▽_{μ}p̂_{k}, ▽_{μ}p̂_{k} ∈ A′_{m} ⊆ B_{m} as well. But, by Lemma A.1, from B_{k} ˜# B_{m} and ▽_{μ}p̂_{k} ∈ B_{m} we get B_{k} ˜#_{μ} B_{m}.

On the other hand, suppose that e_{k} = e_{i+1} or e_{m} = e_{i+1}. Without loss of generality, assume that e_{m} = e_{i+1}. Then e_{k} = e_{j} and by the construction of B_{j} and B_{i+1} we are assured that B_{j} ˜#_{μ} B_{i+1}.

Claim: μ_{i+1} ⊆ #_{μ}_{i+1}

Since T_{i+1} satisfies (C5), we know that (e_{k}, e_{m}) ∈ μ_{i+1} implies that B_{k} ˜#_{μ} B_{m} and so B_{k} ˜# B_{m}. Thus, since T_{i+1} satisfies (C4), e_{k} #_{i+1} e_{m}. Now suppose that e_{l} ∈ E_{i+1} such that e_{l} <_{i+1} e_{k}. Then, by (C4), we know that B_{l} ˜< B_{k}. Hence, by Lemma A.3, either B_{l} ˜< B_{m} or B_{l} c̃o B_{m} which implies, again by (C4), e_{l} <_{i+1} e_{m} or e_{l} co_{i+1} e_{m}. Symmetrically, for any e_{l} <_{i+1} e_{m} we can argue that e_{l} <_{i+1} e_{k} or e_{l} co_{i+1} e_{k}. Hence e_{k} #_{μ}_{i+1} e_{m}.

□

Finally, we prove Lemma 5.15. Recall that our inductive construction yielded a chronicle structure CH = (ES, T, μ), where:

• ES = (E, <, #), with E = ⋃_{i≥0} E_{i}, <= ⋃_{i≥0} <_{i}, and # = ⋃_{i≥0} #_{i}.

• T : E → 2^{Φ} is given by:

∀e_{i} ∈ E : T (e_{i}) = ⋃{T_{j}(e_{i}) ∩ Φ_{j} | j ≥ i}.

• μ = ⋃_{i≥0} μ_{i}.

Lemma 5.15 CH = (ES, T, μ) is a perfect chronicle structure in which α_{0} ∈ T (e_{0}).

Proof  We establish this result by proving a series of claims.  As usual, let

co = (E × E) − (< ∪ > ∪ # ∪ id).

Claim 1 T assigns an MCS to each element of E.

Proof of Claim First, we show that for every e ∈ E, T (e) is a consistent set. Consider e_{k} ∈ E. Suppose that α, β ∈ T (e_{k}). Let α ∈ Φ_{i} and β ∈ Φ_{j}. Let n = MAX(i, j, k). Then, by Lemma A.5(i), it follows that α ∧ β ∈ T_{n}(e_{k}). Since T_{n}(e_{k}) is an MCS, α ∧ β is consistent and so T (e_{k}) must be consistent.

Next, we show that T (e_{k}) is an MCS. Suppose that T (e_{k}) ∪ {β} is consistent and β ∉ T (e_{k}). Let β ∈ Φ_{i} and n = MAX(i, k). Then, since T_{n}(e_{k}) is an MCS, we must have β ∈ T_{n}(e_{k}) or ¬β ∈ T_{n}(e_{k}). If β ∈ T_{n}(e_{k}), then β ∈ T (e_{k}) by the definition of T, which is a contradiction. On the other hand, if ¬β ∈ T_{n}(e_{k}) then ¬β ∈ T (e_{k}), again by the definition of T, which implies that T (e_{k}) ∪ {β} is not consistent, which is again a contradiction.

Claim 2

(i) ∀R ∈ {<, >, #, co} : R_{i} = R ∩ (E_{i} × E_{i}). (ii) ∀e_{j}, e_{k} ∈ E : ∀R ∈ {<, >, #, co} : e_{j} R e_{k} iff e_{j} R_{n} e_{k} where

n = MAX(j, k). (iii) ES is an event structure. (iv) ∀e_{j} ∈ E : p̂_{j} ∈ T (e_{j}).

Proof of Claim (i) follows at once from the fact that at every stage i, in passing from CH_{i} to CH_{i+1} we ensured that <_{i}=<_{i+1} ∩(E_{i} × E_{i}) and #_{i} = #_{i+1} ∩ (E_{i} × E_{i}), which also implies that co_{i} = co_{i+1} ∩ (E_{i} × E_{i}). (ii) and (iii) follow immediately from (i). (iv) follows from Lemma A.5(i) and the definition of T.

Claim 3 ∀e_{j}, e_{k} ∈ E : ∀R ∈ {<, >, #, co} : e_{j} R e_{k} iff T (e_{j}) R̃ T (e_{k}).

Proof of Claim Let e_{j} R e_{k} — say e_{j} co e_{k}. Consider △ · α ∈ T (e_{j}). We have to verify that α ∈ T (e_{k}). Let △ · α ∈ Φ_{i} and let n = MAX(i, j, k). Then △ · α ∈ T_{n}(e_{j}). We know by Claim 2 that e_{j} co_{n} e_{k} and, since T_{n} satisfied the inductive condition (C4), T_{n}(e_{j}) c̃o T_{n}(e_{k}). Hence α ∈ T_{n}(e_{k}) and so α ∈ T (e_{k}). Hence T (e_{j}) c̃o T (e_{k}). The other cases can be proved in a similar manner.

Next, suppose that T (e_{j}) R̃_{1} T (e_{k}) for some R_{1} ∈ {<, >, #, co} and that (e_{j}, e_{k}) ∉ R_{1}. Since ES is an event structure, (e_{j}, e_{k}) belongs to some relation R_{2} ∈ {<, >, #, co} such that R_{1} ≠ R_{2}. By the first part of the argument, we must have (T (e_{j}), T (e_{k})) ∈ R̃_{2} as well. But, by Claim 2, p̂_{k} ∈ T (e_{k}). Hence, by Lemma A.4, (T (e_{j}), T (e_{k})) belongs to at most one semantic relation and so we have a contradiction.

Henceforth, we let #_{μ} denote the minimal conflict relation in ES.

Claim 4

(i) ∀e_{j}, e_{k} ∈ E : (e_{j}, e_{k}) ∈ μ implies T (e_{j}) ˜#_{μ} T (e_{k}).

(ii) μ ⊆ #_{μ}.

Proof of Claim

(i) Let e_{j}, e_{k} ∈ E, such that (e_{j}, e_{k}) ∈ μ. Then it must be the case that for some n, (e_{j}, e_{k}) ∈ μ_{n}. But then, since CH_{n} satisfied (C5) we know that T_{n}(e_{j}) ˜#_{μ} T_{n}(e_{k}). From this, we can conclude that T_{n}(e_{j}) ˜# T_{n}(e_{k}) and hence e_{j} #_{n} e_{k} since CH_{n} satisfied (C4). Hence e_{j} # e_{k} as well, and so, by Claim 3, T (e_{j}) ˜# T (e_{k}). Also, since we must have had ▽_{μ}p̂_{k} ∈ T_{n}(e_{j}), we must have ▽_{μ}p̂_{k} ∈ T (e_{j}) as well. Hence, by Lemma A.1, it must be the case that T (e_{j}) ˜#_{μ} T (e_{k}).

(ii) By part (i), if (e_{j}, e_{k}) ∈ μ then T (e_{j}) ˜#_{μ} T (e_{k}). This implies that T (e_{j}) ˜# T (e_{k}) and so we must have e_{j} # e_{k} by Claim 3. Suppose that e_{m} < e_{j} in ES. Then, by Claim 3, we know that T (e_{m}) ˜< T (e_{j}) and hence, by Lemma A.3, T (e_{m}) ˜< T (e_{k}) or T (e_{m}) c̃o T (e_{k}). From this, using Claim 3 again, we can conclude that e_{m} < e_{k} or e_{m} co e_{k}. Similarly, for any e_{l} < e_{k}, we can verify that e_{l} < e_{j} or e_{l} co e_{j}. Thus e_{j} #_{μ} e_{k}.

Claim 5 T kills all requirements in CH.

Proof of Claim Suppose that e_{k} ∈ E and β ∈ T (e_{k}) where β is of the form ◇α, ◇ - α, ▽α, △α or ▽_{μ}α. Then, we must show that there exists e_{j} ∈ E such that α ∈ T (e_{j}) and e_{j} > e_{k}, e_{j} < e_{k}, e_{j} # e_{k}, e_{j} co e_{k} or e_{j} μ e_{k} respectively.

Once again, we establish this for only one concrete case. Suppose that β = ▽_{μ}α. Let ▽_{μ}α ∈ Φ_{i} and m = MAX(i, k). Then ▽_{μ}α ∈ T_{m}(e_{k}). Let n be the index of (e_{k}, ▽_{μ}α) in the enumeration we have fixed for Ẽ × Φ. Then for some l, m ≤ l ≤ m + (n − 1), (e_{k}, ▽_{μ}α) must be the live requirement chosen to be killed in CH_{l} and hence in CH_{l+1} we have e_{j} ∈ E_{l+1} such that (e_{j}, e_{k}) ∈ μ_{l+1} and α ∈ T_{l+1}(e_{j}). Clearly α ∈ Φ_{m} and since l + 1 > m, we must have α ∈ T (e_{j}) and (e_{j}, e_{k}) ∈ μ as required.

Claim 6 μ = #_{μ}.

Proof of Claim By Claim 4(ii), we know that μ ⊆ #_{μ}. Hence it suffices to show that #_{μ} ⊆ μ.

Suppose e_{j} #_{μ} e_{k}. Then e_{j} # e_{k} and so, by Claim 3, T (e_{j}) ˜# T (e_{k}). We know that p̂_{j} ∈ T (e_{j}) and thus ▽p̂_{j} ∈ T (e_{k}). From the axiom A7 we can conclude that {▽_{μ}p̂_{j}, ◇ - ▽_{μ}p̂_{j}, ▽_{μ}◇p̂_{j}, ◇ - ▽_{μ}◇p̂_{j}}∩ T (e_{k}) ≠ ∅.

Suppose that ◇ - ▽_{μ}p̂_{j} ∈ T (e_{k}). By Claim 5, there exists e_{m} such that e_{m} < e_{k} and ▽_{μ}p̂_{j} ∈ T (e_{m}). Once again, by Claim 5, there exists e_{l} such that (e_{m}, e_{l}) ∈ μ and p̂_{j} ∈ T (e_{l}). If e_{l} and e_{j} are distinct events, T (e_{l}) and T (e_{j}) must belong to some semantic relation from the set { ˜<, ˜>, ˜#, c̃o}. However, for any p ∈ P, from the definition of p̂ it follows that no semantic relation can exist between two MCSs which both contain p̂. Hence we must have e_{l} = e_{j} and thus (e_{m}, e_{j}) ∈ μ. Since μ ⊆ #_{μ}, e_{m} #_{μ} e_{j}, which contradicts e_{j} #_{μ} e_{k}. In a similar fashion, we can show that ▽_{μ}◇p̂_{j} and ◇ - ▽_{μ}◇p̂_{j} cannot be in T (e_{k}).

Hence we must have ▽_{μ}p̂_{j} ∈ T (e_{k}). Again applying Claim 5 and the reasoning above, we must in fact have (e_{j}, e_{k}) ∈ μ and we are done.

Claim 7 ES is a well branching event structure.

Proof of Claim From Claim 2(iii) we already know that ES is an event structure, so all we have to verify is that ES is well branching.

Suppose e_{j}, e_{k} ∈ E such that e_{j} # e_{k}. Then, by Claim 3, T (e_{j}) ˜# T (e_{k}) and, since p̂_{j} ∈ T (e_{j}), ▽p̂_{j} ∈ T (e_{k}). Once again, from A7 we can conclude that {▽_{μ}p̂_{j}, ◇ - ▽_{μ}p̂_{j}, ▽_{μ}◇p̂_{j}, ◇ - ▽_{μ}◇p̂_{j}} ∩ T (e_{k}) ≠ ∅.

If ▽_{μ}p̂_{j} ∈ T (e_{k}), then clearly (e_{j}, e_{k}) ∈ μ by previous arguments and hence e_{j} #_{μ} e_{k} by Claim 4(ii). On the other hand, if ◇ - ▽_{μ}p̂_{j} ∈ T (e_{k}), then we have shown in the proof of Claim 6 that there exists e_{m} < e_{k} such that e_{m} #_{μ} e_{j}. Using a similar argument, we can show that if ▽_{μ}◇p̂_{j} ∈ T (e_{k}), then there exists e_{l} < e_{j} such that e_{l} #_{μ} e_{k} and, finally, if ◇ - ▽_{μ}◇p̂_{j} ∈ T (e_{k}) then there exist e_{l} < e_{j} and e_{m} < e_{k} such that e_{l} #_{μ} e_{m}.

Hence, given e_{j} # e_{k} in ES, there must exist e_{l} ≤ e_{j} and e_{m} ≤ e_{k} such that e_{l} #_{μ} e_{m} and so ES is well branching.

From Claims 1 through 4 and Claim 7, we can conclude that CH is a coherent chronicle structure. Claims 5 and 6 then show that CH is in fact perfect.

The fact that α_{0} ∈ T (e_{0}) follows immediately from the fact that α_{0} ∈ Φ_{0}, by definition, and that α_{0} ∈ T_{0}(e_{0}) by construction.

□