Internal Report  TCS-90-3

September, 1990

Models and Logics for True Concurrency

Kamal Lodaya^{1}, Madhavan Mukund^{2}, R. Ramanujam^{1}, P.S. Thiagarajan^{2}

Abstract

A distributed computer system consists of different processes or agents that function largely autonomously and coördinate their actions by communicating with each other. In such a situation, actions may be performed by different agents of the system locally, in a concurrent manner.

In this paper, we first discuss formal models of distributed systems in which concurrency is specified explicitly, in contrast to more traditional approaches where concurrency is represented implicitly as a non-deterministic choice between all possible sequentializations of concurrent actions. This naturally leads to models based on partially-ordered sets of actions rather than sequences of actions and is often called the true concurrency approach. The models we focus on are distributed transition systems, elementary net systems and event structures.

In the second half of the paper, we develop a family of logics to specify and reason about the behavioural properties of the models we have described. The logics we define are extensions of temporal logic with new modalities to directly describe concurrency.

This paper is essentially a survey of work done by the authors during the last few years on modelling distributed systems with true concurrency and using logic to reason about these models. The emphasis is on motivating definitions through examples and on presenting major results, without going into too many formal details. We provide pointers to the literature where these details can be found.

1The Institute of Mathematical Sciences, Madras 600 113, INDIA. 2School of Mathematics, SPIC Science Foundation, 92 G.N. Chetty Road, T. Nagar, Madras 600 017,

INDIA.

This report is also published as IMSc/90/12, The Institute of Mathematical Sciences, Madras 600 113, INDIA.

Introduction

The study of distributed systems and computations is an important topic of research in computer science. A distributed system consists of a number of essentially autonomous components that work together to perform a complex task.

A computer network which brings together a heterogeneous collection of computing resources and users dispersed over a wide geographic area is a classic example of a distributed system. Distributed databases constitute yet another class of examples. At a lower level, computer protocols which facilitate efficient and reliable transmission of electronic data and operating systems which coördinate the activities of multiple processes (programs) in the presence of multiple processors can also be viewed as distributed systems. With the advent of VLSI systems, the notion of a distributed system is also becoming relevant at the circuit level.

The theory of distributed systems consists of formulating abstract mathematical models of distributed systems and studying the properties of these models. A basic motivation in the study of formal models is to develop tools and techniques using which one can specify, analyze and implement distributed systems. Another goal is to develop formal means for reasoning about the behaviour of distributed systems. This is important because one would like to ensure that a specification is in some sense consistent before one attempts an analysis or an implementation. Even more importantly, one would like to guarantee that a proposed implementation indeed meets the requirements of a specification.

In this paper, we present some of our work in the last few years on modelling distributed systems with true concurrency and using logic to reason about these models. The emphasis is on motivating definitions through examples and on presenting major results. No attempt will be made to go into formal details; we shall provide pointers to the literature where these details can be found.

In the first part of the paper, we introduce three models called distributed transition systems, elementary net systems and event structures. Using these models, we illustrate some of the fundamental features of distributed systems, such as causality, choice and concurrency.

In the second half of the paper, we develop a family of logics to specify and reason about the behavioural properties of the models considered in the first half of the paper.

A Models for True Concurrency

Typically, a distributed system consists of spatially separated processes or agents performing a joint task. The agents function largely autonomously and coördinate their actions by communicating with each other. In such a situation, actions may be performed by different agents of the system locally, in a concurrent manner.

Informally, we say that two events are concurrent if they occur with no a priori ordering over their occurrences. This is in contrast to a sequential system in which any two events that occur in a computation must be ordered.

In addition to concurrency, two other aspects are of interest in the theory of distributed systems – causality and choice. Causality refers to the fact that certain events in a distributed system can only occur in a fixed order; for example, a message can be received only after it has been sent. The receipt of a message is said to be causally dependent on the sending of the message.

Choice captures the fact that systems can behave in an indeterminate fashion. In other words, at certain points of the computation, the system may choose between alternative events, leading to different behaviours.

As we shall see, labelled transition systems are simple and convenient models of sequential systems which can explicitly describe causality and choice, but which do not have a natural way of representing concurrency. One way of describing concurrency in the framework of transition systems is in terms of indeterminacy. In this approach, the fact that a set of actions may be performed concurrently is represented by permitting the system to choose between all possible sequentializations of the actions. This approximation of concurrency by interleaving is used in various algebraic approaches to the theory of distributed systems such as CCS [Milner 1989], CSP [Hoare 1984] and ACP [Bergstra et al 1984].

Such an implicit representation of concurrency leads to problems in analyzing system behaviour, due to the combinatorial explosion in the number of possible interleavings. We follow an alternative approach, called “true concurrency”, where concurrency is represented explicitly in the models.

[figure: s_{0}; s_{1}; s_{2}; s_{3}; s_{4}; s_{5}; b; a; a; a; b; b; b; a]

Figure 1: A transition system

Many abstract models of distributed systems have been suggested which explicitly deal with the phenomena of causality, choice and concurrency. Here, we shall consider three of these models — distributed transition systems, elementary net systems and event structures. We shall also discuss a model called communicating sequential agents. This model, based on a restricted class of event structures, captures in a natural way the intuitive picture of a distributed system as a collection of sequential agents coördinating their actions through communication.

1 Distributed Transition Systems

Before discussing models of concurrent systems, let us briefly look at sequential systems. Transition systems are a basic model of sequential systems.

Definition 1.1 A (Σ-labelled) transition system is a triple T S = (S, Σ, →) where

(i). S is a set of states.

(ii). Σ is a set of actions.

(iii). → ⊆ S × Σ × S is the transition relation.

If (s, a, s′) ∈ →, then the idea is that the action a can occur at state s and after the execution of a the system assumes the state s′. We shall often write s→^{a}s′ instead of (s, a, s′) ∈ →.

Figure 1 is a graphical representation of a transition system. The nodes of the graph represent the states of the system. The edges, labelled by actions from Σ, reflect the transition relation →.

Clearly the structure of a transition system captures both the basic phenomena present in sequential systems — causality and choice. The transition relation can be used to determine the causal dependancies between system states. Choice is specified by branching in the transition system. In other words, if s→^{a}s′ and s→^{b}s′′ both belong to the transition relation, then the system at state s can choose between the actions a and b. For example, at s_{1} the system shown in Figure 1 can either move by an a to s_{2} or move by a b to s_{3}. In general, different choices available to the system at a state may be labelled by the same action. In other words, the behaviour could be nondeterministic. For instance, at s_{0} this system can move on b either to s_{5} or to s_{1}.

In this example, starting at s_{1}, either the action a can occur followed by the action b or the action b can occur followed by the action a. In the interleaving approach to concurrency, this situation often amounts to saying that a and b can occur concurrently at s_{1}.

However, we would like to maintain a clear distinction between nondeterminism and concurrency. Hence, to describe concurrency in a transition system, we enrich the relation → by permitting a transition to be labelled by a finite set of actions from Σ, rather than just by a single action. Thus, we will now have elements in → of the form s→^{u}s′, where u is a finite subset of Σ. The idea is that the actions in u can occur at s with no order over their occurrences. When they have all occurred, the resulting state is s′. The set of actions u is termed a concurrent step.

[figure: f_{∅}; f_{a}; f_{b}; f_{c}; f_{ab}; f_{ac}; f_{bc}; f_{abc}; b; b; b; b; a; a; a; a; c; c; c; c; {a, b, c}]

Figure 2: A “cube” generated by a concurrent step

Henceforth, given a set X, ℘(X) denotes the set of subsets of X and ℘_{fin}(X) denotes the set of finite subsets of X. We can now formally define distributed transition systems as follows.

Definition 1.2 A distributed transition system (dts) is a triple DT S = (S, Σ, →) where

(i). S is a set of states.

(ii). Σ is a set of actions.

(iii). → ⊆ S × ℘_{fin}(Σ) × S is the step transition relation satisfying for all s, s′ in S:

(a) s→^{∅}s′ iff s = s′.

(b) for all u ∈ ℘_{fin}(Σ), if s→^{u}s′ then there exists a function f: ℘(u) → S such that f(∅) = s, f(u) = s′ and for every v_{1}, v_{2} ∈ ℘(u) with v_{1} ⊆ v_{2}, it is the case that f(v_{1}) ⟶^{v_{2}−v_{1}}f(v_{2}).

We often say that DT S = (S, Σ, →) is a dts over Σ. For convenience, we write s→^{a}s′ instead of s⟶^{{a}}s′.

The new definition of → is a bit involved because we have to ensure that any non-trivial “substep” of a concurrent step is also performed as a concurrent step. The function f in clause (3.b) is said to define a u-cube (from s to s′). The existence of the u-cube guarantees that the mutual independence of the actions in u holds for all the substeps as well. For example, Figure 2 shows the cube generated by a concurrent step consisting of three events. To avoid cluttering up the figure, “interior” arrows such as

f_{∅} ⟶^{{a,b}}f_{ab} and f_{b} ⟶^{{a,c}}f_{abc} have not been drawn.

Figure 3 is an example of a distributed transition system modelling the allocation of a shared resource to different processes within a system. In the example, we have 3 processes P_{1}, P_{2} and P_{3} functioning in an operating environment that supports multiprocessing. The resource — say, for example, blocks of memory — is available in “units”. There are totally 5 units available. The 3 processes require 2, 3 and 5 units of the resource at a time respectively. In this dts, Σ = {a_{1}, a_{2}, a_{3}, r_{1}, r_{2}, r_{3}}, where a_{i} denotes that process P_{i} has been allocated the entire amount of the resource that it needs and r_{i} denotes that P_{i} has released the resource it has been allocated. The states of the dts are ordered pairs consisting of the number of unallocated units of the resource available in the system along with the set of processes currently in possession of their required quota of the shared resource.

Thus, at the state (5, ∅), no processes are active and all 5 units of the resource are available. At this state, the system can either allocate units of the resource to one of the three processes, or perform a concurrent step allocating resources to both P_{1} and P_{2}. Notice that the transition from (3, {P_{1}}) to (2, {P_{2}}) can either be performed as a concurrent step {a_{2}, r_{1}} or by interleaving the two actions. In

[figure: (0, {P_{3}}); (5, ∅); (3, {P_{1}}); (2, {P_{2}}); (0, {P_{1}, P_{2}}); a_{3}; r_{3}; a_{1}; a_{1}; r_{1}; r_{1}; a_{2}; a_{2}; r_{2}; r_{2}; {a_{2}, r_{1}}; {a_{1}, r_{2}}; {a_{1}, a_{2}}; {r_{1}, r_{2}}]

Figure 3: A distributed transition system

one interleaving, however, (5, ∅) is reached as an intermediate state, at which point the resource can be allocated to P_{3} instead of P_{2}. Thus, in this case, the effect of the interleavings is not quite the same as that of the concurrent step.

In general, it is important to note that clause (3.b) in Definition 1.2 is merely an implication. The existence of a function from ℘(u) into S which fulfills the stated requirements does not guarantee the existence of a concurrent step. This is line with our philosophy that concurrency should be clearly differentiated from interleaving. As we have seen above, interleavings may permit unintended deviations from the behaviour expected of a concurrent step. In fact, it is possible to have a concurrent step as well as an interleaving of the step performed at a state but leading to two different states.

Finally, we introduce the important notion of reachability in a transition system. Given T S = (S, Σ, →) we define R(s_{0}), the reachability set of s_{0} ∈ S, as the least subset of S containing s_{0} satisfying:

If s ∈ R(s_{0}), a ∈ Σ and s→^{a}s′, then s′ ∈ R(s_{0}).

Thus, R(s_{0}) is the set of states reachable from s_{0} in a finite number of steps using →.

2 Elementary Net Systems

In a distributed transition system, concurrency is explicitly introduced into a transition system by permitting transitions between states via finite sets of actions called concurrent steps. In effect, the notion of a state is left unchanged and the transition relation is enriched to model concurrency.

An alternative way of introducing concurrency into a transition system is to “distribute” the states of the system. The states of a dts correspond to the global states of the concurrent system being modelled by the dts. Rather than regard these global states as indivisible entities, we can break them up into atomic components which can be regarded as the local states of the different processes within the system. The global states of the system can then be characterized in terms of the local states.

By distributing the states of the model in this manner, we can clearly distinguish concurrency from choice without having to define a transition relation involving sets of actions as in a dts. Instead, the transition relation is designed to capture the fact that the change of state accompanying each event occurrence in the system is “localized” to those processes that actually participate in the event. As a result, when an event occurs, only specific local components of the global state are affected, leaving the rest of the components untouched. Thus, two events that are enabled at a global state of the system can occur concurrently if the local states that they affect are disjoint. On the other hand, if the local states

[figure: b_{1}; b_{2}; e_{1}; e_{2}; e_{3}; b_{3}; b_{4}; e_{4}; e_{5}]

Figure 4: An elementary net system

affected by the two events overlap, they cannot both occur in the same computation at that state and so a choice must be made between them.

Net theory deals with models of concurrent systems based on this approach. Here we describe elementary net systems, which are a basic model in this theory. We begin with the definition of a net.

Definition 2.1 A net is a triple N = (B, E, F) where B and E are disjoint sets and F ⊆ (B×E)∪(E×B) satisfies:

∀x ∈ B ∪ E : ∃y ∈ B ∪ E : (x, y) ∈ F or (y, x) ∈ F.

The elements of B are called conditions and are used to denote atomic local states. The elements of E are called events and are used to represent atomic actions. The flow relation F models a fixed neighbourhood relation between the conditions and events of a system. This flow relation determines the way in which the atomic actions affect the atomic local states. The restriction on F in the definition of a net ensures that there are no isolated conditions or events.

We can now define an elementary net system as follows.

Definition 2.2 An elementary net system is a quadruple N = (B, E, F, c_{in}) where

(i). N_{N} = (B, E, F) is a net called the underlying net of N.

(ii). c_{in} ⊆ B is the initial case.

Figure 4 is an example of an elementary net system. We have used the conventional graphical notation for nets — conditions are represented by circles, events by boxes and the flow relation by directed arcs. The “marked” conditions denote the initial case c_{in}.

For e in E the conditions “pointing into” e via F are called the pre-conditions of e and are denoted by ^{•}e. Similarly, the conditions “pointing away” from e via F are called the post-conditions of e and are denoted by e^{•}. More formally we have

•e =^{def} {b | (b, e) ∈ F }

e^{•} =^{def} {b | (e, b) ∈ F }

A state of a net system, called a case, consists of a set of conditions c ⊆ B. The conditions in c are said to hold when the system is at the case c. Thus, c_{in} is the set of conditions that hold when the system starts up.

The system moves from one case to another through the occurrence of events from E. An event can occur at a case iff all its pre-conditions hold and none of its post-conditions do at the case. When an event occurs all its pre-conditions cease to hold and all its post-conditions begin to hold.

In graphical terms, an event e can occur at a case c iff all the conditions pointing into e are “marked” at c and none of the conditions pointing away from e are. For example, in Figure 4, the event e_{1} can occur at the initial case c_{in} = {b_{1}, b_{2}}. When e_{1} occurs, we “unmark” all the pre-conditions of e_{1} and “mark” all its post-conditions, leaving the other conditions in c_{in} untouched. Thus, after the occurrence of e_{1}, the system is at the case {b_{2}, b_{3}}.

We can formalise this by defining →_{N} ⊆ ℘(B) × E × ℘(B), the (elementary) transition relation generated by the net N = (B, E, F) as follows.

→_{N} = {(x, e, x′) | x − x′ = ^{•}e, x′ − x = e^{•}}

Using this transition relation, we can associate a transition system with an elementary net system as follows

Definition 2.3 Let N = (B, E, F, c_{in}) be a net system.

(i). C_{N}, the state space of N, is the least subset of ℘(B) containing c_{in} such that if c ∈ C_{N} and (c, e, c′) ∈ →_{N_{N}} then c′ ∈ C_{N}.

(ii). T S_{N} = (C_{N} , E, →_{N}) is the transition system associated with N, where →_{N} is →_{N_{N}} restricted to C_{N} × E × C_{N}.

For the net system shown in Figure 4, {{b_{1}, b_{2}}, {b_{1}, b_{4}}, {b_{2}, b_{3}}, {b_{3}, b_{4}}} is its state space.

Let N = (B, E, F, c_{in}) be a net system with c ∈ C_{N} and e ∈ E. Then e is said to be enabled at c — denoted c[e⟩ — iff there exists c′ ∈ C_{N} such that c→^{e}c′, where as usual c→^{e}c′ abbreviates (c, e, c′) ∈ →_{N}.

As we had mentioned at the beginning of this section, we can clearly separate concurrency from choice once we have distributed the global states of a transition system into local components.

Let N = (B, E, F, c_{in}) be a net system and e, e′ ∈ E. We say that e and e′ can occur concurrently at a case c — denoted c[{e, e′}⟩ — iff c[e⟩ and c[e′⟩ and (^{•}e ∪ e^{•}) ∩ (^{•}e′ ∪ e′^{•}) = ∅. Thus, e and e′ can occur concurrently at a case if they can occur individually and their “neighbourhoods” are disjoint.

Similarly we can define the notion of conflict. Let N be a net system as above with e, e′ ∈ E. e and e′ are said to be in conflict at a case c iff c[e⟩ and c[e′⟩ but not c[{e, e′}⟩. Thus, if e and e′ are in conflict at c, it means that they are both individually enabled at c, but they cannot occur together at c. For the computation to proceed, the conflict must be resolved by making a (nondeterministic) choice between the two events.

The definition of →_{N} is designed to ensure that the notion of change of state in an elementary net system is fairly restricted.

First, notice that an event must cause the same change in the system state whenever it occurs; its pre-conditions cease to hold and its post-conditions begin to hold. Thus, if c_{1}→^{e}c_{2} and c_{3}→^{e}c_{4} are both possible in a net system, then it must be the case that c_{1} − c_{2} = c_{3} − c_{4} = ^{•}e and c_{2} − c_{1} = c_{4} − c_{3} = e^{•}.

Further, to determine whether an event e is enabled at a case c, it is sufficient to look at the conditions contained in ^{•}e and e^{•}. e is enabled at c iff ^{•}e ⊆ c and e^{•} ∩ c = ∅ — no “side-conditions” are involved in the enabling of an event.

Finally, it turns out that the transition system T S_{N} associated with a net system N is deterministic; that is, c→^{e}c′ and c→^{e}c′′ implies that c′ = c′′. To connect up with other approaches to the theory of distributed systems, nondeterminism can be introduced into T S_{N} by labelling the events in E. We shall come back to this point later in this section.

Let us consider an example of modelling a distributed system using an unlabelled elementary net system. Consider the problem of sharing resources in a distributed system. Suppose that there are two processes P_{1} and P_{2} in the system which require access to a common resource r. Suppose that r can be used by only one process at a time – r could, for instance, be a printer. Then, when one of the processes is granted access to r, the other process should be prevented from accessing r till the first process releases it. This will ensure that at any state during a computation of the system, at most one process can actually be using that resource.

Figure 5 models a solution to this problem of mutual exclusion. In this net system the process P_{i}, i = 1, 2, is represented by the conditions {b_{0}^{i}, b_{1}^{i}, b_{2}^{i}, b_{3}^{i}} and the events {e_{0}^{i}, e_{1}^{i}, e_{2}^{i}, e_{3}^{i}}. Each process is modelled as a simple loop consisting of four events — getting access to r (e_{0}^{i}), utilizing r (e_{1}^{i}), releasing r (e_{2}^{i}) and performing some internal computations not involving r (e_{3}^{i}). At the initial case, both processes are waiting for access to r. The additional condition a functions as an arbitrator which enforces mutual

[figure: a; b_{0}^{1}; b_{0}^{2}; e_{0}^{1}; e_{0}^{2}; b_{1}^{1}; b_{1}^{2}; e_{1}^{1}; e_{1}^{2}; b_{2}^{1}; b_{2}^{2}; e_{2}^{1}; e_{2}^{2}; b_{3}^{1}; b_{3}^{2}; e_{3}^{1}; e_{3}^{2}]

Figure 5: Mutual exclusion

exclusion of access to r. For example, suppose that e_{0}^{2} occurs initially, giving P_{2} access to r. Since a ceases to hold e_{0}^{1} is no longer enabled. Thus, P_{1} can gain access to r only after P_{2} releases r by the occurrence of e_{2}^{2}. It is easy to check that b_{1}^{1} and b_{1}^{2} can never hold together in this net system. On the other hand, the conditions b_{3}^{1} and b_{3}^{2} can hold at the same case — that is, the events e_{3}^{1} and e_{3}^{2} which do not involve the use of r can occur concurrently in this system.

Finally, we show that we can describe the behaviour of elementary net systems in terms of distributed transition systems. Consider an elementary net system N = (B, E, F, c_{in}). The transition system T S_{N} contains information about the causality and conflict present in N. To describe the concurrency present in N, it is sufficient to augment T S_{N} with additional transitions labelled by concurrent steps, as follows.

We first extend the notion of a pair of events being concurrently enabled at a case to a set of events. Let u = {e_{1}, e_{2}, …, e_{n}} be a finite subset of E. We say that u is concurrently enabled at a case c ∈ C_{N} — denoted c[u⟩ — iff c[e_{i}⟩ for each e_{i} ∈ u and, further, c[{e_{1}, e_{2}}⟩ for every pair of distinct events e_{1}, e_{2} ∈ u.

We can then define the step transition relation ⇒_{N} as follows.

⇒_{N} = {(c, u, c′) | c, c′ ∈ C_{N} , c[u⟩ and c − c′ = ^{•}u, c′ − c = u^{•}}

Here ^{•}u and u^{•} denote the unions of the pre-conditions and post-conditions of the events contained in u. Note that →_{N} is “included” in ⇒_{N} in the sense that if (c, e, c′) ∈ →_{N} then (c, {e}, c′) ∈ ⇒_{N}. We can then immediately establish the following.

Proposition 2.4 DT S_{N} = (C_{N} , E, ⇒_{N}) is a distributed transition system over E.

It is easy to verify that the concurrency and choice present in N is precisely captured by the dts DT S_{N}.

However, notice that this dts is deterministic, for the same reason that the transition system T S_{N} is. As we had mentioned earlier, we can introduce nondeterminism by labelling the events.

Definition 2.5 A Σ-labelled elementary net system is a pair N_{Σ} = (N , ϕ), where N = (B, E, F, c_{in}) is an elementary net system, called the underlying net system of N_{Σ}, Σ is a set of labels and ϕ: E → Σ is the labelling function.

The notions we have developed for net systems can be transported to labelled net systems in the obvious way. To represent the behaviour of a labelled net system N_{Σ} as a dts, we can define DT S_{N_{Σ}} to be the dts over Σ obtained by using the labelling function ϕ to rename the actions in DT S_{N}, the dts over E generated by the underlying net system N.

However, in general we need to place a restriction on the labelling function in order to get a neat translation from labelled net systems to dts’s. In a dts, we have restricted concurrent steps to be sets of actions. On the other hand, a labelled net system N_{Σ} may generate a concurrent step in DT S_{N_{Σ}} where two distinct events in the step have the same label. To avoid dealing with multisets in concurrent steps that arise in this fashion, we require that events which can occur concurrently in the underlying net system N have distinct labels.

Let N_{Σ} = (B, E, F, c_{in}, ϕ) be a Σ-labelled net system. The labelling function ϕ is said to be co-injective if it satisfies the following condition.

∀e_{1}, e_{2} ∈ E : (∃c ∈ C_{N} : c[{e_{1}, e_{2}}⟩) implies ϕ(e_{1}) ≠ ϕ(e_{2}).

Proposition 2.6 Let N_{Σ} = (N , ϕ) be a Σ-labelled elementary net system, where N = (B, E, F, c_{in}), such that ϕ is co-injective. Then DT S_{N_{Σ}} = (C_{N} , Σ, ⇒_{N_{Σ}}) is a dts over Σ, where

⇒_{N_{Σ}} = {(c, ϕ(u), c′) | (c, u, c′) ∈ ⇒_{N} }.

3 Event Structures

To reason about the behaviour of a distributed transition system or an elementary net system, we have to examine all the computations of the underlying “machines” defined by the model. For this, it is convenient to work with an abstract representation of the entire behaviour of the system. This behavioural description should include information about all the computations of the system, explicitly identifying the causal dependancies and concurrency present within each computation. In addition, it should also have a way of describing the branching points in the system behaviour.

Before discussing behavioural representations of concurrent systems, let us first go back to sequential transition systems. A computation of a sequential transition system T S = (S, Σ, →) starting at some state s_{0} ∈ S is an alternating sequence of actions and states which obeys the transition relation →. We shall restrict our attention to the maximal computations of the system — those that cannot be extended by performing any more actions. Thus, a maximal computation is a finite sequence just in case a state is reached at the end of the sequence from which no transition is possible; otherwise, it is an infinite sequence.

A natural way to group together the sequences which correspond to computations of T S = (S, Σ, →) starting from s_{0} is in the form of a tree. The nodes of the tree are labelled by states from S and the edges are labelled by actions from Σ. The root node is labelled by the initial state s_{0}. Each maximal path in the tree now corresponds to a computation of the system. The branching points in the tree are the states where the system makes choices between different possible actions.

In the case of models exhibiting concurrency, the situation is more complicated. A computation of such a system is a partially ordered set of actions, not a simple sequence, so we need a more sophisticated method of collecting all the computations together in a single structure. An elegant way of achieving this is to use event structures. Event structures are behavioural models of distributed systems in which causality, concurrency and choice (conflict) are represented explicitly.

Prime event structures, introduced in [Nielsen et al 1980], are the simplest type of event structures. They have a rich theory and are closely related to both net systems and domains. Since we deal only with prime event structures in this paper, henceforth we shall simply call them event structures.

Definition 3.1 An event structure is a triple ES = (E, ≤, #) where

(i). E is a set of event occurrences.

(ii). ≤ ⊆ E × E is a partial order called the 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.

An element of E represents the occurrence of an event within a specific context. Thus, if the same event can occur in different contexts, “copies” of it will be present in the event structure. This is why we have called the elements of E event occurrences rather than events.

[figure: □; e_{1}; □; e_{2}; □; e_{3}; □; e_{4}; □; e_{5}; □; e_{6}; □; e_{7}; □; e_{8}; □; e_{9}; □; e_{10}]

Figure 6: An event structure

If e_{1} ≤ e_{2}, then e_{2} is causally dependent on e_{1}. Thus, in any computation of the system, e_{2} can occur only if e_{1} has already occurred. As usual we let ≥ stand for ≤^{−1}.

The # relation identifies pairs of events which are inconsistent with each other and hence cannot both occur during the same computation. The last clause of the Definition 3.1 ensures that if e_{1} # e_{2} then events that are causally dependent on e_{1} are in conflict with events that are causally dependent on e_{2} — in other words, the inconsistency of e_{1} and e_{2} is inherited by events that follow these two events.

Two events that are neither causally related nor in conflict with each other can both occur within a computation with no order over their occurrence. We can thus define the concurrency relation co in an event structure ES = (E, ≤, #) in terms of ≤ and # as follows.

co =^{def} E × E − ( ≤ ∪ ≥ ∪ # ).

Notice that co, like #, is irreflexive and symmetric. Clearly, every pair of distinct events in an event structure belongs to exactly one of the four relations {≤, ≥, #, co}.

It is useful 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 : [ e_{1} ≤ e and e′_{1} ≤ e′ and e_{1} # e′_{1}

implies e_{1} = e and e′_{1} = e′ ].

#_{μ} identifies the minimal elements (under ≤) of the # relation and is hence called the minimal conflict relation. #_{μ} identifies the actual 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.

Figure 6 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. The # relation is then uniquely determined by the last part of Definition 3.1. 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}.

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 3.2 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 6, {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.

We are particularly interested in a restricted subset of configurations called local configurations. 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 [Nielsen et al 1980].

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

We now define LC_{ES} = {↓e | e ∈ E} to be the set of local configurations of the event structure ES = (E, ≤, #).

We do so because a (general) configuration c ⊆ E can be viewed as a global state of the system. Parts of a global configuration may change independent of each other, due to the spatial separation and the partial autonomy of the individual agents in the system being modelled by the event structure. A finite global configuration c is completely characterized by specifying the maximal events (with respect to ≤) which belong to c. Each local configuration ↓e corresponding to a maximal event e ∈ c can be regarded as a local state which contributes to the global state at c.

When we reason about the behaviour of an event structure, we would like to make assertions about properties that are satisfied by the global configurations — that is, properties that hold at the global states of the system. However, a global state can be completely described in terms of all the local states that are part of that global state. Thus, we shall restrict ourselves to specifying properties at the local configurations. Using combinations of these assertions, we can describe global configurations of the event structure. Further, the assertions that we can make about a global configuration are tied down to the assertions that we can make about the local configurations that constitute the global configuration. This will become clearer in the second part of the paper where we discuss how to specify properties of distributed systems.

As we had mentioned at the beginning of this section, an event structure is a single entity which describes all the computations of a distributed system. Thus, we need a means of “extracting” individual computations from an event structure. Since a configuration represents a set of events that have happened so far, in general an arbitrary configuration represents a partial computation of the system. If we consider configurations which are maximal (with respect to inclusion) we obtain the maximal computations of the event structure. We call these the runs of the event structure. It is easy to verify the following characterization of runs. Let r ⊆ E. Then r is a run iff

∀e ∈ E : e ∈ r iff ∀e′ ∈ E : e # e′ implies e′ ∉ r

Next, let us look at some useful restrictions on event structures. We begin with the auxiliary relation #_{μ}. 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. We would like to rule out such structures, since they model behaviours which are intuitively infeasible. We can therefore restrict our attention to well branching event structures.

Definition 3.4 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}.

Well branching is a fairly weak restriction. A stronger and more useful restriction is that of finitariness. An event structure ES = (E, ≤, #) is said to be finitary in case ↓e is a finite set for every e ∈ E. Finitariness captures the important fact that in any realizable system, an event can be causally dependent on only a finite set of events. An event with an infinite past can never actually occur.

There is a systematic way of describing the behaviour of elementary net systems using finitary event structures. To do this, we require labelled event structures. A labelled event structure is a pair ES_{Σ} = (ES, ϕ) where ES = (E, ≤, #) is an event structure and ϕ: E → Σ is a labelling function.

Constructing a labelled finitary event structure describing the behaviour of a net system involves an intermediate stage where the net system is “unfolded” to generate an acyclic structure. The details are a bit involved and can be found in [Nielsen et al 1980], [Thiagarajan 1990]. We shall merely present an example.

[figure: e_{0}^{1}; e_{0}^{2}; e_{1}^{1}; e_{1}^{2}; e_{2}^{1}; e_{2}^{2}; e_{3}^{1}; e_{3}^{2}; e_{0}^{1}; e_{0}^{2}; e_{0}^{2}; e_{0}^{1}; e_{1}^{1}; e_{1}^{2}; e_{1}^{2}; e_{1}^{1}; …; …; …; …]

Figure 7: A labelled event structure

Consider the elementary net system in Figure 5 modelling mutual exclusion. The labelled event structure in Figure 7 describes the behaviour of this system. In this case, the event occurrences in the event structure are labelled by the events of the net system.

Given a finitary event structure ES, we can construct a dts DT S_{ES} which exhibits the same behaviour as ES. Let C_{ES}^{fin} denote the set of finite configurations of the finitary event structure ES = (E, ≤, #). We can define the step transition relation →_{ES} ⊆ C_{ES}^{fin} × ℘_{fin}(E) × C_{ES}^{fin} as follows:

→_{ES} = {(c, u, c′) | c ∩ u = ∅ and c ∪ u = c′ and
∀e_{1}, e_{2} ∈ u : e_{1} ≠ e_{2} implies e_{1} co e_{2}}

Proposition 3.5 DT S_{ES} = (C_{ES}^{fin}, E, →_{ES}) is a dts over E.

As in the case of elementary net systems, it turns out that DT S_{ES} is always deterministic. Once again, we can use labelled event structures to permit nondeterminism in this dts. As before, we have to restrict the labelling to be co-injective to rule out multisets in concurrent steps. In other words, given ES_{Σ} = (E, ≤, #, ϕ), we require that for every e_{1}, e_{2} ∈ E : e_{1} co e_{2} implies ϕ(e_{1}) ≠ ϕ(e_{2}). We then have the following result.

Proposition 3.6 Let ES_{Σ} = (ES, ϕ) be a Σ-labelled event structure where ϕ is a co-injective labelling function. Then DT S_{ES_{Σ}} = (C_{ES}^{fin}, Σ, ⇒_{ES_{Σ}}) is a dts over Σ where

⇒_{ES_{Σ}} = {(c, ϕ(u), c′) | (c, u, c′) ∈ →_{ES}}.

4 Communicating Sequential Agents

In an event structure, the entire behaviour of a distributed system is specified as a single entity. Individual computations of the system can be identified using the notion of a run. However, no further information is provided about the structure of the system.

Consider a distributed system consisting of a finite set of sequential agents performing a joint task, using communication to coördinate their activities. When reasoning about the behaviour of such a system, it is convenient to associate the events occurring in the system with the agents involved in the events. This can be captured by restricting event structures to a model called communicating sequential agents (csa’s).

Let N denote the set of natural numbers {1,2,3 … }. We shall use elements of N as names for the agents in our system.

Definition 4.1 A system of communicating sequential agents (csa) is a triple CSA = (E, ≤, η), where

(i). E is a non-empty set of event occurrences.

(ii). ≤ is a partial order on E called the causality relation.

(iii). η: E → ℘_{fin}(N) is a naming function assigning to each e in E a non-empty finite subset of N.

(iv). Let E_{j} = {e | e ∈ E and j ∈ η(e)}. Then, for every e in E:

∀j ∈ N : ↓e ∩ E_{j} is totally ordered by ≤ .

We interpret j ∈ η(e) as the agent j participating in the event e. Thus η(e) = {1, 2} can stand for a synchronization “handshake” between agents 1 and 2.

The poset (E_{j}, ≤_{j}), where ≤_{j} is ≤ restricted to E_{j} × E_{j}, represents the local behaviour of agent j in CSA. Usually, we say “agent j” to denote this poset.

As in an event structure, if e_{1} ≤ e_{2} then e_{2} causally depends on e_{1}; in no run of CSA can e_{2} occur without e_{1} having occurred earlier.

To separate concurrency from conflict, both the causality relation ≤ and the naming function η are used. In a csa, each agent is defined to be sequential. Thus, given any two events e and e′ which both involve the same agent – that is η(e) and η(e′) are not disjoint — e and e′ must either be causally related or in conflict. So if e and e′ are incomparable with respect to ≤ and η(e) ∩ η(e′) ≠ ∅, then e and e′ are in conflict.

The motivation for the last condition in Definition 4.1 should now be clear: we do not wish an event occurrence to causally depend upon conflicting event occurrences. This condition also implicitly ensures that the basic conflict in the system is generated within agents — in effect, choices are made locally by individual agents and then propogated across agents via ≤.

On the other hand, if two events e and e′ are unordered and their combined past does not contain any conflicting events then they must be concurrent. Since choices are assumed to be made locally, it is sufficient to check that for each agent j, the combined past of e and e′ does not have incomparable events involving j. In other words, if (↓e ∪ ↓e′) ∩ E_{j} is totally ordered by ≤ for every j, then the two events e and e′ are concurrent.

If e ∈ E_{j}, the local state ↓e includes the local history of agent j as well as the “latest” local histories of all other agents with which j has communicated upto this state. Let LC_{CSA} = {↓e | e ∈ E} be the set of local states of CSA.

By suitably restricting the naming function η, we can capture interesting subclasses of csa’s.

The first restriction is on the number of agents. In a general csa, we may have an unbounded number of agents in the system. By restricting the range of η to a finite subset {1, 2, …, n} of N, we obtain csa’s which may have upto n agents, which we call n-csa’s.

As we had mentioned earlier, if η(e) is not a singleton, the interpretation is that the event e is performed jointly by the agents mentioned by η(e). This intuitively corresponds to “handshaking” or synchronous communication between agents. By restricting η so that | η(e) | = 1 for every event e in E, we effectively rule out this type of synchronous communication. Instead, in such an asynchronous csa, the agents communicate by sending messages to each other. The sending and receiving of a message are regarded as two distinct actions, each involving only one agent at a time.

Finally, we say that a csa is finitary in case ↓e is a finite set for every e in E. The motivation for defining finitary csa’s is the same as the motivation for defining finitary event structures — any computation of a real system can be traced back to some starting point, so the past of any event occurring during the computation must be finite.

Figure 8 is an example of an asynchronous csa consisting of two agents, a producer and a consumer, communicating via an unbounded buffer. The producer can produce zero or more items and then quit. The consumer can consume items produced by the producer as long as the items are available in the buffer. The events in the csa are labelled p, q and c to denote these three types of actions.

[figure: p; q; c; p; q; c; p; q; c; p; q; c; …; …; …; E_{1}; E_{2}]

Figure 8: An asynchronous csa

B Logics for Concurrency

We now turn our attention to the problem of reasoning about the behaviour of distributed systems.

A specification language is simply a formalism in which one specifies behaviours of systems under study. Thus, a specification language for distributed systems is one in which we can describe behavioural properties of distributed systems.

The specification language should permit us to combine simple specifications together to construct more complex specifications, reflecting the intuition that large systems can be broken down into more manageable subsystems. This calls for disjunctive and conjunctive abilities in the language.

In addition, since we are dealing with distributed systems we expect to describe properties like causality, choice and concurrency. For this, we will need to be able to specify the relationships that hold between system states as the computation proceeds.

Our requirements suggest the use of a formal logic with boolean connectives and temporal modalities as our specification language. Temporal logic is a branch of modal logic which is used to study structures of states varying with time. We will design a variety of modal logics which are extensions of temporal logic to deal with the models of distributed systems developed in Part A.

We begin with a quick sketch of classical propositional modal logic. We assume the existence of P, a countable set of atomic propositions {p_{0}, p_{1}, …}. The well-formed formulas of our logic L_{0} are defined inductively:

• Every p ∈ P is a formula of L_{0}.

• If α and β are formulas of L_{0}, then so are ¬α, α ∨ β and ◇α.

¬α is to be read as “not α”, α ∨ β is to be read as “α or β”, and ◇α is to be read as “Diamond α”. The intended meaning of ◇α is “α becomes true eventually”.

Formulas are to be interpreted over frames. In our set-up, a frame is a transition system T S = (S, Σ, →). A model M is a frame with a valuation function; i.e M = (T S, V), where T S = (S, Σ, →) is a transition system and V: S → ℘(P). For example, if V (s) = {p_{1}, p_{3}}, we interpret this to mean that propositions p_{1} and p_{3} are true at state s and, further, that no other proposition is true at s.

The notion of a formula α being true at a state s in a model M = (T S, V) where T S = (S, Σ, →), denoted as M, s ⊧ α, is defined inductively as follows:

(i) M, s ⊧ p iff p ∈ V (s), for p ∈ P.

(ii) M, s ⊧ ¬α iff M, s |̸= α.

(The notation M, s |̸= α stands for “It is not the case that M, s ⊧ α”) (iii) M, s ⊧ α ∨ β iff M, s ⊧ α or M, s ⊧ β. (iv) M, s ⊧ ◇α iff ∃s′ ∈ R(s) : M, s′ ⊧ α.

(Recall that R(s) is the set of states reachable from s via →)

M, s ⊧ α can be interpreted as the assertion that the model M at state s is an implementation of the specification α. We say α is satisfiable if there exists a model M = (T S, V), where T S = (S, Σ, →), and there exists a state s ∈ S such that M, s ⊧ α. We say that α is M-valid if M, s ⊧ α for every s ∈ S. We say that α is valid — and denote this by ⊧ α — if α is M-valid for every model M. It is easy to see that α is valid iff ¬α is not satisfiable.

The following derived formulas are useful.

α ∧ β =^{def} ¬(¬α ∨ ¬β)  the conjunction of α and β.

α ^{⊃} β =^{def} ¬α ∨ β α implies β

α ≡ β =^{def} (α ^{⊃} β) ∧ (β ^{⊃} α) logical equivalence of α and β

□α  =^{def} ¬(◇¬α)  “Henceforth” α
True  =^{def} p_{0} ∨ ¬p_{0}
False  =^{def} ¬T rue

It can easily be verified that for any model M = ((S, →), V) and s ∈ S,

M, s ⊧ □α iff ∀s′ ∈ R(s) : M, s′ ⊧ α.

A number of interesting properties of transition systems can be expressed using this logic. Suppose that we are using transition systems to model a distributed system consisting of n processes which can compete for a shared resource r. Let the atomic proposition c_{i} stand for “Process i has access to the resource r”. Then

□ ⋀_{i∈{1,2,...,n}}(c_{i} ^{⊃} ⋀_{i≠j} ¬c_{j})

expresses a so-called safety property. It says that at any system state, at most one process has control of the shared resource r. This will ensure, for instance, that in case r is a shared piece of data then the sequence of values assumed by r during the history of the system will be well-defined. Broadly speaking, safety properties assert that “bad” situations never arise in the system.

Similarly, if we let the proposition rq_{i} stand for “Process i requires access to resource r”, the formula

□ ⋀_{i∈{1,2,...,n}}(rq_{i} ^{⊃} ◇c_{i})

expresses a liveness property. It says that any request made by a process for the shared resource is eventually granted by the system. In general, liveness properties specify that something “good” occurs eventually.

This logical framework is very simple, but for that reason is also not as expressive as we would wish. In particular, we would like to devise logics to reason about models with true concurrency. In the rest of this section, we shall show how such logics can be defined for the formal models presented in Part A.

1 Logic for Distributed Transition Systems

Recall that in a dts, a concurrent step consists of a transition labelled by a finite set of actions. This leads us to augment the simple modal logic considered earlier with one additional modality, ⟨u⟩, where u is a finite subset of Σ, the set of actions.

Let L_{DT S} be the language whose well formed formulas are given by:

• Every p ∈ P is a formula of L_{DT S}.

• If α and β are formulas of L_{DT S} then so are ¬α, α ∨ β, ◇α and ⟨u⟩α, where u is a finite subset of Σ.

Thus, the logic L_{DT S} is parametrized by Σ. To emphasize this, we will write L_{DT S}^{Σ} instead of L_{DT S}.

As one may expect, the frames for our logic are dts’s over Σ. A model is a pair M = (DT S, V), where DT S = (S, Σ, →) is a dts over Σ and V: S → ℘(P) is the valuation function. Given s ∈ S, the notion M, s ⊧ α is defined as before for the atomic propositions and for the connectives ¬ and ∨ and the modality ◇. For the new modality we define:

M, s ⊧ ⟨u⟩α iff ∃s′ ∈ S : s→^{u}s′ and M, s′ ⊧ α.

[figure: s_{0}; s_{1}; s_{2}; s_{3}; s′_{0}; s′_{1}; s′′_{1}; s′_{2}; s′_{3}; a; b; c; a; a; b; c]

Figure 9: Varieties of branching in transition systems

Relative to the new notion of models, satisfiability and validity are defined as before. We will write ⊧_{DT S}^{Σ} α to denote that α is a valid formula in this logic. Let SAT _{DT S}^{Σ} denote the set of all satisfiable formulas from L_{DT S}^{Σ}.

Before considering an example, we introduce some notational conventions. The derived modality [u] is defined as:

[u]α =^{def} ¬⟨u⟩¬α

Where u is a singleton {a}, we will write ⟨a⟩α instead of ⟨{a}⟩α. For the empty step, we write ⟨∅⟩α.

Now that the modalities are indexed by steps, we can clearly identify the branching points in a transition system. For example, consider the transition systems shown in Figure 9. In the first system, starting at s_{0} we can perform a and then choose between b and c whereas in the second system, at s′_{0} we have to decide right away whether we are going to execute a followed by b or a followed by c. The first situation is captured by the formula ⟨a⟩(⟨b⟩True ∧ ⟨c⟩True) while the second can be expressed as ⟨a⟩(⟨b⟩True ∧ [c]False) ∧ ⟨a⟩(⟨c⟩True ∧ [b]False).

In this logic, we can distinguish between interleavings and true concurrency. For instance, the formula ⟨a⟩⟨b⟩True ∧ ⟨b⟩⟨a⟩True ∧ [{a, b}]False is satisfiable. At the state where this formula is true, both the interleavings ab and ba can occur, but the corresponding concurrent step {a, b} is not enabled. On the other hand, it is easy to see that the formula ⟨{a, b}⟩α ^{⊃} ⟨a⟩⟨b⟩α is a valid formula, because the definition of a dts guarantees the existence of a function f associated with each step, breaking it up into substeps.

Returning briefly to the system of n processes considered earlier, assume that the shared resource r represents a data item in a shared block of memory. Let ud_{i} denote the act of process i updating the value of r. Then, the specification

□ ⋀_{i≠j}[{ud_{i}, ud_{j}}]False

requires that the memory manager never permit two distinct processes to concurrently update r.

Let us consider another example. The writing of a paper can be seen as a sequential activity: work out what you want to say, write it out, get it typed. In the case of a joint paper, the work may be divided up in terms of sections. One policy the authors may follow is to work out all the sections before preparing a typescript, with meetings for discussion and correction in between. That is, the authors satisfy

⟨W K⟩(worked ∧ ⟨W R⟩(written ∧ ⟨T Y ⟩typed))
where W K = {work out §1, work out §2, work out §3 }

W R = {write §1, write §2, write §3 } T Y = {type §1, type §2, type §3 }

and worked, written and typed are atomic propositions indicating the end of the working out, writing and typing steps respectively. Here we have assumed that there are three authors each of whom is responsible for one section.

The concurrent steps are necessary, since they express the fact that this is a joint paper; if the interleaving of the actions required for the three sections were present, we could not rule out the possibility that the three authors were separately writing three (single-section) papers.

The states we are using are global states. The person working out §2 may refer to a lemma in §1; the person doing the word processing for §1 may use the macros defined in §3.

It becomes necessary to use sequentializations when a complete record of the writing of the paper is required. For example, a mistake pointed out by the referee in §2 may be traced to the lemma in §1, which may be just a case of wrong typing thanks to a misapplication of the macro from §3.

This sort of mixture of independent actions and synchronization is well described in a dts framework.

We now turn to the formal theory of the language L_{DT S}^{Σ}. Typical questions one asks of such a logic include:

• Is the set of valid formulas axiomatizable?

• Is the satisfiability problem decidable?

The answers to these questions provide a good deal of insight into the strengths and weaknesses of the logic and, most importantly, into the expressive power of the logic.

It turns out that both these questions have positive answers for L_{DT S}^{Σ}. Consider the following logical system ND.

The System ND

AXIOM SCHEMES

(A0) All the substitutional instances of the tautologies of Propositional Calculus.

(A1) (a) □(α ^{⊃} β) ^{⊃} (□α ^{⊃} □β) (Deductive Closure)

(b) [u](α ^{⊃} β) ^{⊃} ([u]α ^{⊃} [u]β)

(A2)  □α ^{⊃} [u]α ∧ □□α  (Reachability)
(A3)  α ≡ ⟨∅⟩α  (Empty Step)
(A4,k) (for k ≥ 1)  (Step Axiom)

⟨u⟩α ∧ ⋀_{v⊆u}[v] ⋁_{i=1}^{k} β_{v}^{i} ^{⊃} ⋁_{f∈F (u,k)} ⋀_{v_{1}⊆u} ⟨v_{1}⟩(γ_{v_{1}} ∧ ⋀_{v_{1}⊆v_{2}⊆u} ⟨v_{2} − v_{1}⟩γ_{v_{2}})

where F (u, k) is the set of all functions {f | f: ℘(u) → {1, 2, …, k}} and

γ_{v} = \{ \begin{matrix}β_{v}^{f(v)} ∧ α & if v = u \\ β_{v}^{f(v)} & if v ⊂ u \end{matrix}

INFERENCE RULES

(MP) \frac{α, α ^{⊃} β}{β} (TG) \frac{α}{□α}

Axioms A0 to A2 and the rules MP and TG are standard. The characteristic axioms of dts’s are A3 and A4,k. A3 captures the fact that the empty step cannot change the state of the system. A4,k is actually an infinite set of axioms, finitely presented. The complicated formulation of A4,k is necessary to describe the fact that each concurrent step u in a dts can be broken up into concurrent substeps which are specified by the associated function f: ℘(u) → S.

A formula α is called a thesis of the system ND — denoted ⊢_{ND} α — iff α can be derived in a finite number of steps using the axioms and inference rules of ND.

Theorem 1.1

(i). ND is a sound and complete axiomatization of the valid formulas in L_{DT S}^{Σ}. In other words, ⊢_{ND} α iff ⊧_{DT S}^{Σ} α for every α ∈ L_{DT S}^{Σ}.

(ii). The satisfiability problem for this logic (i.e. the membership problem for SAT _{DT S}^{Σ}) is decidable in nondeterministic exponential time.

It turns out that combining concurrency, captured by the step notion, with determinacy leads to a very expressive class of models. The frame T S = (S, Σ, →) is said to be deterministic if for every s ∈ S and every u ∈ ℘_{fin}(Σ) there exists at most one s′ ∈ S such that s→^{u}s′. A model is deterministic if its underlying frame is.

The formula α is said to be deterministically satisfiable if there exists a deterministic model for α. Similarly, α is said to be deterministically valid if α is valid over the class of deterministic models. Let ⊧_{Det}^{Σ} α denote that α is deterministically valid and let DSAT _{DT S}^{Σ} denote the set of deterministically satisfiable formulas in L_{DT S}^{Σ}.

It turns out that the deterministically valid formulas in L_{DT S}^{Σ} are axiomatizable. Thanks to determinacy, one obtains a much simpler axiomatization than for the general case. Let D denote the logical system obtained from ND by dropping the infinitary set of axioms A4,k (k ≥ 1) and adding two new axioms:

(A5)  ⟨u⟩α ^{⊃} ⟨v⟩⟨u − v⟩α  (v ⊆ u)  (Weak Step Axiom)
(A6)  ⟨u⟩α ^{⊃} [u]α  (Determinacy)

Let ⊢_{D} α denote that α is derivable in D.

Theorem 1.2

(i). D is a sound and complete axiomatization of the deterministically valid formulas in L_{DT S}^{Σ}. In other words, ⊢_{D} α iff ⊧_{Det}^{Σ} α for every α ∈ L_{DT S}^{Σ}.

(ii). The membership problem for DSAT _{DT S}^{Σ} is undecidable.

The surprise here is that determinacy adds a sufficient amount of expressive power to make the satisfiability problem undecidable. By combining concurrent steps in a deterministic fashion, it turns out that we can encode the two-dimensional grid of natural numbers N×N. We can then use this encoding to reduce some undecidable tiling problems described by Wang [Wang 1961] and Harel [Harel 1985] to the problem of deterministic satisfiability in our logic. This negative result was shown by Parikh [Parikh 1989].

A variety of positive and negative results can be obtained in this logical framework by studying the effect of placing suitable restrictions on dts’s. For instance, we can restrict the set of actions Σ to be finite. Alternatively, we can demand the dts as a whole be finite — that is, the set of states and the set of transitions are both finite. We can also incorporate ideas from trace theory, arising out of the work of Mazurkiewicz [Mazurkiewicz 1989], and define trace transition systems, which permit both local and global specifications of concurrency. Finally, we can also study a smooth generalization of Propositional Dynamic Logic [Harel 1984] obtained by extending the notion of a regular program to permit concurrent steps as atomic actions. The details can be found in a forthcoming paper [Lodaya et al 1991].

The logical language L_{DT S}^{Σ} can also be interpreted over Σ-labelled elementary net systems and Σlabelled event structures, where the labelling function is co-injective. The frames that we use are the corresponding dts’s, as defined in Part A. Thus, a Σ-labelled elementary net system N_{Σ} = (N , ϕ), where N = (B, E, F, c_{in}), gives rise to a model (DT S_{N_{Σ}}, V), where V: C_{N} → ℘(P). Similarly, a Σ-labelled event structure ES_{Σ} = (ES, ϕ), where ES = (E, ≤, #), defines a model (DT S_{ES_{Σ}}, V), where V: C_{ES}^{fin} → ℘(P).

Let SAT _{N}^{Σ} and SAT _{ES}^{Σ} denote the set of formulas from L_{DT S}^{Σ} satisfiable in models generated by Σ-labelled elementary net systems and Σ-labelled event structures respectively.

Theorem 1.3 SAT _{DT S}^{Σ} = SAT _{N}^{Σ} = SAT _{ES}^{Σ}.

In other words, this logic cannot discriminate between these classes of models.

2 Logic for Event Structures

We now turn from dts’s to event structures as frames for our logic. In the logic for dts’s, we used the global state approach to reasoning about the behaviour of the system. In this approach, assertions are made by a “global” observer of the system who can “see” the distributed system in its entirety in any given state. This is appropriate for dts’s, since the states of a dts do in fact correspond to the global states of the system being modelled.

Alternatively, we can reason about the system from the point of view of the local states of the system. Here, assertions are made by individual agents in the system and hence the nature of the assertion is determined by the “visibility” of the system state from that agent’s point of view. This approach is more suitable for reasoning based on event structures, where we can use a local configuration ↓e to represent the local state of the system at the point where the event e has just occurred.

Another feature of the dts logic is that concurrency is described by explicitly specifying the actions which are to be performed concurrently and describing the effect of such actions. This approach is natural for dts’s because the models themselves are action-based. On the other hand, in an event structure it is more convenient to specify concurrency in an abstract manner by simply asserting facts about concurrent events without specifying which actions are to be performed concurrently.

The key notions in the theory of event structures are those of causality, conflict and concurrency. This leads us to extend the language L_{0} by adding modalities to capture these notions. It turns out to be fruitful to split up causality into two parts, allowing us to specify both “past” and “future” behaviour.

The logic L_{ES} is built up as follows: again fix P = {p_{0}, p_{1}, …}, a countable set of atomic propositions. Then the well-formed formulas of L_{ES} are given by:

• Every p ∈ P is a formula of L_{ES}.

• If α and β are formulas of L_{ES}, then so are ¬α, α ∨ β, ◇α, ◇ - α, △α and ▽α.

Here, the modalities ◇ and ◇ - denote the future and past respectively. △ will be used to describe concurrency and ▽ will be used to capture conflict.

Frames for this logic are event structures, or rather the local configurations of event structures. More precisely, a frame is a pair (ES, LC_{ES}), where ES = (E, ≤, #) is an event structure and LC_{ES} is the set of local configurations of ES.

A model is a pair M = ((ES, LC_{ES}), V) where ES is frame and V : LC_{ES} → ℘(P) is a valuation function. If p ∈ V (↓e) then this is taken to mean that p is true at the local state ↓e in the model M.

The notion of a formula α being true at a local state ↓e in the model M = ((ES, LC_{ES}), V) is denoted as M, ↓e ⊧ α and is defined inductively as follows:

(i) M, ↓e ⊧ p iff p ∈ V (↓e), for p ∈ P.

(ii) M, ↓e ⊧ ¬α iff M, ↓e |̸= α. (iii) M, ↓e ⊧ α ∨ β iff M, ↓e ⊧ α or M, ↓e ⊧ β. (iv) M, ↓e ⊧ ◇α iff ∃e′ : e < e′ and M, ↓e′ ⊧ α.

(v) M, ↓e ⊧ ◇ - α iff ∃e′ : e′ < e and M, ↓e′ ⊧ α. (vi) M, ↓e ⊧ ▽α iff ∃e′ : e # e′ and M, ↓e′ ⊧ α. (vii) M, ↓e ⊧ △α iff ∃e′ : e co e′ and M, ↓e′ ⊧ α.

Notice that we have defined the modalities ◇ and ◇ - in an irreflexive manner. This is necessary for the axiomatization which follows.

The notions of satisfiability and validity are defined as usual. ⊧_{ES} α will denote that α is a valid formula in L_{ES}.

The derived connectives ∧, ^{⊃} , ≡, □ are defined as before. In addition, we set

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

We can also define a useful derived modality as follows:

Sα =^{def} α ∨ ◇α ∨ ◇ - α ∨ ▽α ∨ △α

Sα is to be read as “Somewhere α”. Its dual Eα =^{def} ¬S¬α, read as “Everywhere α” expands as follows:

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

Thus Eα describes a property invariant over the entire model.

Many interesting features of event structures can be expressed in this logic. Recall that the maximal computations of event structures are termed runs. We can use an atomic proposition ρ to mark out a run with the formula ρ ≡ ▽ · ¬ρ. For any model M = ((ES, LC_{ES}), V), if the formula ρ ≡ ▽ · ¬ρ is M-valid, then {e | M, ↓e ⊧ ρ} constitutes a run of ES. Using this method of marking out runs, we can express liveness and safety properties in event structures. Let α represent a liveness property. Then S(ρ ∧ α) is M-valid for a model M just in case every computation of the underlying event structure contains a local state where α is true. Similarly, if β represents an undesirable situation, the formula E(ρ ^{⊃} ¬β) expresses the safety property that β does occur at any state of the run marked by ρ.

In a similar spirit the formula χ ≡ □¬χ∧□ - ¬χ can be used to capture the notion of a cut — a maximal set of pair-wise incomparable events. Within a computation, a cut corresponds to a global state. Thus we can use the notion of a cut in conjunction with that of a run to look “sideways” from a local state and make assertions about the current global state.

The formula ▽α ^{⊃} □▽α describes the fact that conflict is inherited in a prime event structure. The formula △α ^{⊃} □ - (△α∨◇α) expresses the fact that the configurations of an event structure are “consistent” by asserting that the unified past of any pair of events in co is conflict-free.

Due to lack of space, we will not provide a separate detailed example for this logic. The logic presented in the next section, called L_{CSA}, is also based on event structures. We shall provide a detailed example for that logic. It will not be difficult to see how that example can be translated into the present framework.

Consider the logical system E.

The System E

AXIOM SCHEMES

(A0) All the substitutional instances of the tautologies of Propositional Calculus.

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

(ii) □ - (α ^{⊃} β) ^{⊃} (□ - α ^{⊃} □ - β) (iii) ▽ · (α ^{⊃} β) ^{⊃} (▽ · α ^{⊃} ▽ · β) (iv) △ · (α ^{⊃} β) ^{⊃} (△ · α ^{⊃} △ · β)

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

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

(A3) (i) α ^{⊃} ▽ · ▽α  (Symmetry of # and co)

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

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

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

(A5)  ▽α ^{⊃} □▽α  (Conflict inheritance)
(A6)  △α ^{⊃} □ - (◇α ∨ △α)  (Conflict-free past)
(A7) (i) ◇α ^{⊃} □(α ∨ ◇α ∨ ◇ - α ∨ ▽α ∨ △α)  (Relating <,# and co)

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

(v) ▽α ^{⊃} △ · (◇α ∨ ▽α ∨ △α) (vi) △α ^{⊃} □(◇ - α ∨ ▽α ∨ △α)

INFERENCE RULES

(MP) \frac{α}{α ^{⊃} β}

(TG) (i) \frac{α}{□α}  (ii) \frac{α}{□ - α}  (iii) \frac{α}{△ · α}  (iv) \frac{α}{▽ · α}

(UNIQ) \frac{p̂^{⊃} α}{α} where p is an atomic proposition not appearing in α

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

Axioms A0 to A4 and inference rules MP and TG are standard. A5 expresses the fact that conflict is inherited via ≤. A6 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 ≤, ≥, # 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 [Burgess 1980]. Given a proposition p, the definition of p̂ ensures that it can be true in at most one local configuration. Hence, we can label each local configuration ↓e by a distinct formula p̂_{e}. The rule UNIQ allows us to construct this labelling, which is crucial in demonstrating the completeness of the axiomatization.

Let ⊢_{E} α denote that α is a thesis of the system E.

Theorem 2.1 E is a sound and complete axiomatization of the valid formulas in L_{ES}. In other words, ⊢_{E} α iff ⊧_{ES} α.

Recall that we had defined an auxiliary relation #_{μ} in an event structure, called the minimal conflict relation. We can define a modality ▽_{μ} to capture the relation #_{μ}.

It is possible to strengthen L_{ES} by replacing the modality ▽ by the modality ▽_{μ}. Let us call this new language L_{ES}^{μ}. To obtain a useful comparison with L_{ES}, and also to obtain an axiomatization, we must change the notion of a frame. For this language, we define a frame to be a pair (ES, LC_{ES}) where ES is a well branching event structure. Recall that a well branching event structure is one in which the # relation can be completely specified using the relations #_{μ} and ≤. As usual, a model is a frame together with a valuation function. Models based on well branching frames are called well branching models.

The semantics of L_{ES}^{μ} is the same as that of L_{ES} except that the clause for ▽ is replaced by:

M, ↓e ⊧ ▽_{μ}α iff ∃e′ : e #_{μ} e′ and M, ↓e′ ⊧ α.

In L_{ES}^{μ}, we can obtain ▽ as a derived modality:

▽α =^{def} ▽_{μ}α ∨ ▽_{μ}◇α ∨ ◇ - ▽_{μ}α ∨ ◇ - ▽_{μ}◇α

As before, ▽ · α denotes the formula ¬▽¬α. It is easy to verify that ▽ · α can be expressed as follows:

▽ · α =^{def} ▽ ·_{μ}α ∧ ▽ ·_{μ}□α ∧ □ - ▽ ·_{μ}α ∧ □ - ▽ ·_{μ}□α

In a well branching model, the derived modalities ▽ and ▽ · have precisely the same interpretation as the corresponding modalities of L_{ES}. On the other hand, there is no obvious way to characterize the minimal conflict relation #_{μ} using the modality ▽. In this connection, we can establish the following result.

Theorem 2.2 For well branching models, the language L_{ES}^{μ} is strictly more expressive than L_{ES}.

Informally, this result says that we can use formulas from L_{ES}^{μ} to differentiate models which are indistinguishable using the language L_{ES}.

An example of the use of ▽_{μ} is in systems where agents have names, like csa’s. For each event e that process i participates in, we can assign an atomic proposition τ_{i} to the local configuration ↓e. Suppose that there are n agents in the system, with “names” τ_{1}, τ_{2}, …, τ_{n}. Then the formula ⋀_{1≤i≤n}(τ_{i} ^{⊃} ▽ ·_{μ}τ_{i})

expresses the fact that all choices in behaviour are made locally by individual agents.

The axiom system E_{μ} is obtained by adding the following axiom schemes to the system E.

(A1) (v) ▽ ·_{μ}(α ^{⊃} β) ^{⊃} (▽ ·_{μ}α ^{⊃} ▽ ·_{μ}β)  (Deductive Closure)
(A3) (iii)α ^{⊃} ▽ ·_{μ}▽_{μ}α  (Symmetry of #_{μ})
(A6) (ii) ▽_{μ}α ^{⊃} □ - (◇α ∨ △α)  (Minimal Conflict)

A1(v) and A3(iii) are standard. A6(ii) is the characteristic axiom describing the #_{μ} relation as the minimal conflict relation.

Let ⊢_{E}^{μ} α denote that α is a thesis of the system E_{μ} and let ⊧_{ES}^{μ} α denote that α is valid over the class of well branching models. Then we get:

Theorem 2.3 E_{μ} is a sound and complete axiomatization of the valid formulas in L_{ES}^{μ}. In other words, ⊢_{E}^{μ} α iff ⊧_{ES}^{μ} α.

3 Logic for Communicating Sequential Agents

We now wish to study a means of talking about a central feature of many distributed systems — the communication pattern between the components of the system that ensure coördination. For this, we shall define a logic that is to be interpreted over csa’s.

Let P = {p_{0}, p_{1}, …} be a countable set of atomic propositions, and T = {τ_{0}, τ_{1}, …}, a countable set of type propositions disjoint from P. The formulas of L_{CSA} are built up as follows:

• Every member of P ∪ T is a formula of L_{CSA}.

• If α and β are formulas of L_{CSA}, then so are ¬α, α ∨ β, ◇_{i}α and ◇ -_{i}α.

The formula τ_{i} asserts that the observer is located in agent i. ◇_{i} and ◇ -_{i} capture the “visible” future and past of agent i. This will become clearer when we define the formal semantics of these modalities.

A frame for L_{CSA} is a pair (CSA, LC_{CSA}), where CSA = (E, ≤, η) is a system of communicating sequential agents and LC_{CSA} is the set of local states of CSA. A model is a pair M = ((CSA, LC_{CSA}), V) where (CSA, LC_{CSA}) is a frame and V: LC_{CSA} → ℘(P ∪ T ) is a valuation function such that

τ_{i} ∈ V (↓e) iff i ∈ η(e).

The notion M, ↓e ⊧ α can be defined inductively as follows:

(i) M, ↓e ⊧ α iff α ∈ V (↓e), for α ∈ P ∪ T .

(ii) M, ↓e ⊧ ¬α iff M, ↓e |̸= α. (iii) M, ↓e ⊧ α ∨ β iff M, ↓e ⊧ α or M, ↓e ⊧ β. (iv) M, ↓e ⊧ ◇ -_{i}α iff ∃e′ ∈ E_{i} : e′ ≤ e and M, ↓e′ ⊧ α.

(v) M, ↓e ⊧ ◇_{i}α iff \{ \begin{matrix}(e ∈ E_{i}) : & ∃e′ ∈ E_{i} : e ≤ e′ and M, ↓e′ ⊧ α. \\ (e ∉ E_{i}) : & ∀e′ ∈ E_{i} : if e′ ≤ e then M, ↓e′ ⊧ ◇_{i}α. \end{matrix}

Note that ◇ -_{i} behaves like a normal past modality — it covers all events that lie in the i-past of e. However ◇_{i}α is different: in agent j, j ≠ i, it asserts that upto the last communication from i, there is a future for agent i satisfying α. In case there is no communication from agent i at all, agent j can assert ◇_{i}α for any formula α.

Define □ -_{i}α =^{def} ¬◇ -_{i}¬α and □_{i}α =^{def} ¬◇_{i}¬α. It can be verified that □_{i}α ^{⊃} ◇ -_{i}□_{i}α is a valid formula over csa’s. It asserts that an invariant formula about an agent must be supported by a communication from that agent. Thus □_{i} is a “strong” modality whereas ◇_{i} is “weak” unlike in standard modal logic. This asymmetry arises from the fact that in distributed systems, the past of other agents can be completely obtained by messages, while the possibilities for the future are only locally known.

Notice that the formula τ_{i} ∧ τ_{j} is satisfied at a local state ↓e only if {i, j} ⊆ η(e) and thus specifies a synchronization between agents i and j. The infinite set of formulas {τ_{i} ^{⊃} ¬τ_{j} | i ≠ j} together specify that each event is in at most one agent and hence can specify asynchronous csa’s.

Consider the formula ◇ -_{i}α ∧ ◇ -_{i}β ^{⊃} ◇ -_{i}(α ∧ ◇ -_{i}β) ∨ ◇ -_{i}(β ∧ ◇ -_{i}α). This specifies that agent i is backwards linear – during a computation if we look back at any two events involving agent i, then they must be ordered. This captures the fact that agents in a csa are sequential.

Similarly, the formula ◇ -_{i}α ^{⊃} ◇ -_{i}(α ∧ □ -_{i}(¬α ^{⊃} □ -_{i}¬α)) can be used to specify finitary csa’s, i.e those where each event has a finite past. This formula asserts that if α is true somewhere in the past, then we can find an “earliest” point where α is true.

The principal advantage of this logic is that communication between agents in a distributed system can be easily expressed: ¬τ_{i} ∧ ◇ -_{i}α ∧ τ_{j} can be used to specify that i has communicated the truth of α to j sometime in the past.

We shall present a detailed example of reasoning with this logic at the end of this section. First, we present our main technical results for this logic.

We begin with logical system C defined below.

The System C

AXIOM SCHEMES

(A0) All the substitutional instances of the tautologies of Propositional Calculus.

(A1) (a) □ -_{i}(α ^{⊃} β) ^{⊃} (□ -_{i}α ^{⊃} □ -_{i}β)  (Deductive closure)

(b) □_{i}(α ^{⊃} β) ^{⊃} (□_{i}α ^{⊃} □_{i}β)

(A2) (a) τ_{i} ^{⊃} (□ -_{i}α ^{⊃} α)  (Local reflexivity)

(b) τ_{i} ^{⊃} (□_{i}α ^{⊃} α)

(A3)  ◇ -_{i}◇ -_{j}α ^{⊃} ◇ -_{j}α  (Transitivity)
(A4) (a) ◇ -_{i}α ^{⊃} □_{i}◇ -_{i}α  (Relating past and future)

(b) ◇_{i}α ^{⊃} □ -_{i}◇_{i}α

[figure: finitary ; n-csa’s; finitary ; n-acsa’s; n-csa’s; n-acsa’s; finitary csa’s; finitary acsa’s; csa’s; acsa’s]

Figure 10: Subclasses of csa’s

(A5)  ◇ -_{i}α ∧ ◇ -_{i}β ^{⊃} ◇ -_{i}(α ∧ ◇ -_{i}β) ∨ ◇ -_{i}(β ∧ ◇ -_{i}α).  (Backward linearity)
(A6)  □_{i}α ^{⊃} ◇ -_{i}□_{i}α  (Communication)
(A7) (a) □ -_{i}τ_{i}  (Type axioms)
(b) τ_{i} ^{⊃} □_{i}τ_{i}

INFERENCE RULES

(MP) \frac{α, α ^{⊃} β}{β}  (TG□ -_{i}) \frac{α}{□ -_{i}α}  (TG□_{i}) \frac{α}{τ_{i} ^{⊃} □_{i}α}

Axioms A0 to A4 are standard axioms suitably modified to reflect the special interpretation of ◇_{i}. A5 asserts that individual agents are sequential. A6 captures that fact that knowledge about another agent’s future can only be obtained via communication. A7 ensures that the type propositions from T are assigned consistently. The rules MP and TG□ -_{i} are standard. The standard form of the rule TG□_{i} will not preserve validity because of the communication requirement imposed by the semantics of □_{i}.

Let ⊢_{C} α denote that α is a thesis of the system C. Let ⊧_{CSA} α denote that α is valid over the class of models based on csa’s. We then have the following result.

Theorem 3.1 C is a sound and complete axiomatization of the valid formulas of L_{CSA}. In other words ⊢_{C} α iff ⊧_{CSA} α for every α ∈ L_{CSA}.

When we introduced csa’s in Part A, we had defined various subclasses of csa’s. Let CSA = (E, ≤, η) be a csa. Recall that CSA is an n-csa if η(E) ⊆ {1, 2, …, n} — that is, there are at most n agents in the system. CSA is an asynchronous-csa (acsa) if ∀e ∈ E : | η(e) | = 1. CSA is finitary if ∀e ∈ E : ↓e is a finite set. We can combine these notions; for example, an n-acsa is an acsa with a bounded number of agents. Similarly, we can have finitary n-csa’s, finitary acsa’s and, finally, finitary n-acsa’s. Figure 10 pictorially represents the relationships between these various classes. The arrows in the figure indicate inclusion.

Let C denote one of the subclasses of csa’s mentioned above. Then we can define the notions of satisfiability and validity relative to C. Thus, a formula α is C-satisfiable if we can find a model M = ((CSA, LC_{CSA}), V) for α such that CSA ∈ C. We let SAT C denote the set of C-satisfiable formulas in L_{CSA}. α is C-valid if it is valid over the class of models based on frames in C.

We can axiomatize the C-valid formulas for all these subclasses. The required axiomatizations are obtained by suitably combining the system C with the following axiom schemes.

AUXILIARY AXIOM SCHEMES AND INFERENCE RULES

(A8)  τ_{1} ∨ τ_{2} ∨ … ∨ τ_{n}  (n agents)
(A9)  τ_{i} ^{⊃} ¬τ_{j}, for i ≠ j  (disjoint agents)
(A10)(a) ◇ -_{i}α ^{⊃} ◇ -_{i}(α ∧ □ -_{i}(¬α ^{⊃} □ -_{i}¬α))  (well-founded agents and communications)
(b) ◇ -_{i}α ^{⊃} ◇ -_{i}(α ∧ □ -_{j}□ -_{i}¬α), for i ≠ j

Theorem 3.2 (i). The logical system C_{A} =^{def} C + (A9) is sound and complete for the class of models based on acsa’s.

(ii). The logical system C_{F} =^{def} C +(A10) is sound and complete for the class of models based on finitary csa’s.

(iii). The logical system C_{F A} =^{def} C_{A} + (A10) is sound and complete for the class of models based on finitary acsa’s.

(iv). The logical system C_{n} =^{def} C + (A8), n ∈ N, is sound and complete for the class of models based on n-csa’s.

(v). The logical system C_{nA} =^{def} C_{A} + (A8), n ∈ N, is sound and complete for the class of models based on n-acsa’s.

(vi). The logical system C_{nF} =^{def} C_{F} + (A8), n ∈ N, is sound and complete for the class of models based on finitary n-csa’s.

(vii). The logical system C_{nF A} =^{def} C_{F A} + (A8), n ∈ N, is sound and complete for the class of models based on finitary n-acsa’s.

We also have the following relationship between satisfiability in subclasses with an unbounded number of agents and the corresponding subclasses with only a bounded number of agents.

Theorem 3.3 Let C range over csa’s, acsa’s, finitary csa’s and finitary acsa’s. Let nC, n ∈ N, denote the corresponding class with a bounded number of agents n. Then SAT C = ⋃_{n} SAT_{nC}.

We now give a detailed example of how communication between agents can be specified in L_{CSA}. Consider a distributed database accessed by n processes which communicate with each other by exchanging messages. A protocol is needed whereby the processes can commit to a distributed transaction. When each committed process knows that all the others have also committed it can go ahead and perform its local share of the distributed transaction. For this, the following requirement must be met.

If any process commits to the transaction then it eventually knows that all processes in the system have also committed.

Such distributed transaction commit protocols commonly arise in the design of distributed systems [Pinter et al 1984].

We now specify the protocol requirement in our logical language. Let {c_{1}, …, c_{n}} be a set of atomic propositions, where c_{j} is read to mean “process j has committed to the transaction”. The formula

⋀_{i}(τ_{i} ∧ c_{i} ^{⊃} ◇_{i}(⋀_{j} ◇ -_{i}c_{j}))  (1)

expresses the requirement above.

A two-stage implementation of this protocol may use two local boolean variables in each process P_{i}:

• a variable l_{i} in which process P_{i} records whether it can participate in the transaction or not, and

• a variable, which we also call c_{i}, to record the commitment of the process to the transaction.

The implementation can perhaps run as follows:

Process P_{i}:

(i). As soon as a local decision l_{i} is made, broadcast l_{i} to all other processes;

(ii). When l_{j} is heard from all j, set c_{i} to T rue;

(iii). As soon as c_{i} is set, broadcast it to all other processes;

(iv). When c_{j} is heard from all j, perform transaction; (v). Acknowledge all incoming messages.

All processes follow the same protocol in a symmetric manner. This is, of course, a naïve protocol. However, our aim here is to merely illustrate the use of our logical language. Let us again, by abuse of notation, use {l_{1}, …, l_{n}} to denote another set of atomic propositions. Consider now the following formulas:

⋀_{i}(τ_{i} ^{⊃} (c_{i} ≡ ⋀_{j} ◇ -_{j}l_{j}))  (2)

“c_{i} is set T rue only when l_{j} is heard from all other processes P_{j}”

⋀_{i}(τ_{i} ∧ c_{i} ^{⊃} ◇_{i} ⋀_{j} ◇ -_{j}◇ -_{i}c_{i})  (3)

“if c_{i} is set, then it will be broadcast and acknowledged”

Note that here an agent has to assert something about the state of other agents and this can be done only using messages from them. The formula ◇_{i}◇ -_{j}◇ -_{i}c_{i} says that agent i has received an acknowledgment from agent j of the message c_{i} sent from i to j. This is necessary because we assume that messages may be lost in this network.

It is easy to verify that the formulas 2 and 3 together imply the requirement 1 above. In fact, we can use the axiom system C and logically deduce the requirement from 2 and 3. This verifies that the simple protocol above meets its specification.

Note that the protocol above works for only one transaction, in the sense that the commitment is stable; once a process commits to the transaction, it stays committed. When a protocol is needed for several transactions, we can index the transactions by sequence numbers and modify the specification above appropriately.

While the preceding example illustrates the specification of a protocol which assumes complete connectivity in the network of communicating agents, we can also specify protocols which demand specific patterns of connectivity. Since agents are syntactically mentioned in formulas, this logic is particularly suited for describing communications which name specific agents. We illustrate this point with another detailed example.

Assume that processes P_{0}, P_{1}, …, P_{n−1} are connected in a ring and communicate with each other only by exchanging messages. A process P_{i} can communicate only with its neighbours P_{i−1} and P_{i+1} on the ring. Here and in the sequel, addition and subtraction are assumed to be modulo n.

Assume that each process P_{i} maintains a variable x_{i} taking values in N and whose value initially is v_{i}, for 0 ≤ i ≤ n − 1. It is desired to specify a distributed protocol which computes the greatest common divisor of the values v_{0}, …, v_{n−1}. Let result denote the value of the constant gcd(v_{0}, v_{1}, …, v_{n−1}). When the computation terminates, the variables x_{i}, i ∈ {0, …, n − 1} should satisfy

x_{0} = x_{1} = … = x_{n−1} = result

Since our logical language is propositional in nature we cannot express values of variables and hence assume countably many propositions X_{i}^{k}, k ∈ N, to denote “x_{i} = k”. With this understanding we write such propositions as equalities. Similarly we assume propositions to denote “k < l”, “k = i − j” etc. The protocol requirement is then specified by

⋀_{i}(τ_{i} ∧ (x_{i} = v_{i}) ^{⊃} ◇_{i} ⋀_{k} ◇ -_{k}(x_{k} = result))

An algorithm for computing the gcd can be descibed as follows: process P_{i}, at any state, compares the current value of x_{i}, with the current values of its neighbours, x_{i−1} and x_{i+1}. In case x_{i} is smaller, nothing needs to be done; if x_{i−1} is smaller, x_{i} is updated to be x_{i}−x_{i−1}; similarly, if x_{i+1} is smaller, x_{i} is updated to be x_{i} − x_{i+1}. Whenever the value of x_{i} changes, this is communicated to the neighbouring processes. Eventually, all values stabilize at the greatest common divisor.

As before, we assume that messages may fail and hence received messages are always acknowledged. Let ◇_{i→j}α abbreviate the formula τ_{i} ∧ ◇_{i}◇ -_{j}◇ -_{i}α. (In some sense, this stands for “i sends the message α to j and receives an acknowledgment”)

Our protocol can now be specified as

⋀_{i}(τ_{i} ^{⊃} □_{i}δ ∧ □ -_{i}δ)

where δ =^{def} δ_{0} ∧ δ_{1} ∧ δ_{2} ∧ δ_{3} is given by:

δ_{0} : (x_{i} = v ^{⊃} ⋀_{j ∈ {i−1, i+1}} ◇_{i→j}(x_{i} = v))

“neighbours are always kept informed of current x_{i} value”

δ_{1} : (x_{i} = v ^{⊃} □_{i}(x_{i} = v′ ^{⊃} v′ ≤ v))

“values are never increased”

δ_{2} : (x_{i} = v ∧ ◇ -_{i−1}(x_{i−1} = v′) ∧ v′ < v ^{⊃} ◇_{i}(x_{i} = v′′ ∧ v′′ = v − v′))

“if x_{i−1} < x_{i} then x_{i} := x_{i} − x_{i−1}”

δ_{3} : (x_{i} = v ∧ ◇ -_{i+1}(x_{i+1} = v′) ∧ v′ < v ^{⊃} ◇_{i}(x_{i} = v′′ ∧ v′′ = v − v′))

“if x_{i+1} < x_{i} then x_{i} := x_{i} − x_{i+1}”

It is easy to see that this specifies a distributed implementation of Euclid’s algorithm for computing the gcd.

Discussion

In this paper, we have looked at models for distributed systems which emphasize their non-sequential behaviour and considered their logical characterization using an assortment of modal logics.

A fair amount of theory has been developed for the models we have considered. Our notion of a distributed transition system is only one of several that have been considered; alternative formulations include those of Degano and Montanari [Degano et al 1987] and Boudol and Castellani [Boudol et al 1988]. Stark has defined a related class of model called concurrent transition systems [Stark 1989]. In net theory, more general net systems include Petri nets, Predicate/transition nets and coloured nets [Brauer et al 1987]. As far as event structures are concerned, we have only considered prime event structures in this paper; other classes of event structures include stable event structures and general event structures [Winskel 1987] as well as flow event structures [Boudol 1990]. Systems of communicating sequential agents were introduced in [Lodaya et al 1989b], as a generalization of the n-agent event structures described in [Lodaya et al 1987].

The models that we have dealt with in this paper are closely related to each other. We have described how labelled net systems and labelled event structures give rise to dts’s in a natural way. A strong relationship also exists between elementary net systems and prime event structures ([Nielsen et al 1980], [Nielsen et al 1990]). The connection between csa’s and event structures is described in [Lodaya et al 1989b]. By establishing formal connections between models in this manner, we can translate results obtained using one class of models to other classes.

As for the logics that we have described here, the main results that we have are sound and complete axiomatizations for different classes of models (see [Lodaya et al 1991], [Lodaya et al 1989a], [Lodaya et al 1989b], [Lodaya et al 1987], [Mukund 1990], [Mukund et al 1989] and [Mukund et al 1991]). For the logic for distributed transition systems, we also have various decidability and undecidability results [Lodaya et al 1991]. However, for the logics for event structures and csa’s, the decidability question remains open.

Several attempts have been made to use logics to characterize the behaviour of distributed programs. Temporal modalities have been traditionally interpreted over different types of tense structures ([Burgess 1984], [Burgess 1980]). Using the interleaving approach to modelling concurrency, various authors have used temporal logics defined on sequences and trees to describe concurrent computations (see e.g. [Clarke et al 1986], [Gabbay et al 1980], [Pnueli 1977]). Pinter and Wolper have extended this work to true concurrency by explicitly using partial orders to represent concurrent computations [Pinter et al 1984]. Katz and Peled have defined a first-order temporal logic over sets of partial orders [Katz et al 1989].

However, the use of classes of behavioural structures for distributed systems as frames for logics seems to be relatively new. Penczek has used event structures as frames [Penczek 1988]. He was the first to use an explicit modality to represent conflict. Reisig [Reisig 1986] is working on logics which directly use elementary net systems as frames. Christiansen [Christiansen 1989] has worked with csa-like frames; he uses an indexed △ modality in his logic to describe concurrency across agents.

Trace theory is a language theoretic approach to describing concurrency which we have not considered. This formalism also gives rise to models of distributed systems with true concurrency. Here, along with an alphabet of actions, one is given an independence relation declaring which actions in the system are concurrent. Instead of viewing a computation as a string of symbols from the alphabet, one now considers sequences made up of sets of concurrent actions (sequences of concurrent steps, in our framework), which are called traces. Like strings, traces form a monoid, called a partially commutative monoid, and so one can meaningfully talk about trace languages. A syntactic Kleene-like characterization of regular trace languages has been given by Ochmanski [Ochmanski 1985], while a characterization in terms of automata has been obtained by Zielonka [Zielonka 1987]. The pomsets of Gischer and Pratt [Pratt 1986] are similar to traces.

Logics for trace theory have not been considered in the literature. We believe that results like the ones in Part B, Section 1 can be obtained [Lodaya et al 1991].

Another widely prevalent approach to modelling concurrency is algebraic. One way of describing sequential nondeterministic programs is through regular expressions, by interpreting the operators ^{•}, + and * as sequential composition, choice and iteration. Similarly, in the algebraic approach to concurrency, one introduces an operator to denote the parallel composition of programs. Program behaviour is specified by modelling the language operators in an appropriate semantic domain. Popular languages for concurrency include CSP [Hoare 1984], CCS [Milner 1989] and ACP [Bergstra et al 1984], and the models most often used are transition systems [Plotkin 1981] and equational algebras [Bergstra et al 1984]. Most of this work has been based on interleaving models and only recently have attempts been made to give a “truly concurrent” semantics to these languages ([Degano et al 1989], [van Glabbeek et al 1987], [Olderog 1987]). An earlier denotational semantics using event structures as domains was given in [Winskel 1982].

In this framework, Hennessy and Milner [Hennessy et al 1985] have used action-indexed logics to characterize computations of sequential nondeterministic systems. Assuming an interleaving model of concurrency, this characterization extends to the computations of distributed systems. This work has been considerably extended by Stirling [Stirling 1987]. However, the emphasis here is on axiomatizing program equivalences using equational logic. Our use of action-indexed logics for models exhibiting true concurrency is inspired by this work, but we have concentrated on axiomatizing the valid formulas, as is traditional in logic.

Logics in which the modalities are indexed by programs, rather than just actions, arose in the framework of program verification [Hoare 1969]. Programs with parallel composition operators have been considered by several authors (e.g [Apt et al 1980]). Dynamic logics, originally defined over sequential programs [Harel 1984], have been extended with an operator for intersection to model synchronization [Peleg 1987]. However, a lot of work remains to be done on characterizing models for true concurrency using program-indexed logics.

References

[Apt et al 1980] Apt K R, Francez N, de Roever W P 1980 A proof system for communicating sequential processes, ACM Trans. Prog. Lang. and Sys. 2,3:359-385. [Also Moitra A 1983 Letter, same journal 5,3:500-501.]

[Bergstra et al 1984] Bergstra J A, Klop J W 1984 Process algebra for synchronous communication, Inf. Control 60,1-3:109-137.

[Boudol 1990] Boudol G 1990 Flow event structures and flow nets, LNCS 469:62-95.

[Boudol et al 1988] Boudol G, Castellani I 1988 A non-interleaving semantics for CCS based on proved transitions, Fund. Inf. XI:433-452.

[Brauer et al 1987] Brauer W, Reisig W, Rozenberg G (eds.) 1987 Petri nets: central models and their properties, LNCS 254.

[Burgess 1984] Burgess J P 1984 Basic tense logic, in Gabbay D, Guenthner F (eds.): Handbook of philosophical logic II (Dordrecht: D Reidel) pp. 89-133.

[Burgess 1980] Burgess J P 1980 Decidability for branching time, Studia Logica XXXIX,2/3:203-218.

[Christiansen 1989] Christiansen S 1989 A logical characterization of linear n-agent event structures, M.Sc. thesis, Computer Science Dept, Århus Univ, Århus, Denmark.

[Clarke et al 1986] Clarke E M, Emerson E A, Sistla A P 1986 Automatic verification of finitestate concurrent programs using temporal logic specifications, ACM Trans. Prog. Lang. and Sys. 8,2:244-263.

[Degano et al 1987] Degano P, Montanari U 1987 Concurrent histories: A basis for observing distributed systems, J. Comput. Sys. Sci. 34:422-461.

[Degano et al 1989] Degano P, de Nicola R, Montanari U 1989 Partial orderings descriptions and observations of nondeterministic concurrent processes, LNCS 354:438-466.

[Gabbay et al 1980] Gabbay D, Pnueli A, Shelah S, Stavi J 1980 On the temporal analysis of fairness, Proc. 7th ACM Conf. Princ. of Prog. Lang. pp. 163-173.

[van Glabbeek et al 1987] van Glabbeek R, Vaandrager F 1987 Petri net models for algebraic theories of concurrency, LNCS 259:224-242.

[Harel 1984] Harel D 1984 Dynamic logic, in Gabbay D, Guenthner F (eds.): Handbook of philosophical logic II (Dordrecht: D Reidel, 1984) pp. 497-604.

[Harel 1985] Harel D 1985 Recurring dominoes: making the highly undecidable highly understandable, Ann. Disc. Math. 24:51-72.

[Hennessy et al 1985] Hennessy M, Milner R 1985 Algebraic laws for nondeterminism and concurrency, J. ACM 32:137-161.

[Hoare 1969] Hoare C A R 1969 An axiomatic basis for computer programming, Comm. ACM 12,10:576-580, 583.

[Hoare 1984] Hoare C A R 1984 Communicating sequential processes (New York:Prentice-Hall).

[Katz et al 1989] Katz S, Peled D 1989 An efficient verification method for parallel and distributed programs, LNCS 354:489-507.

[Lodaya et al 1991] Lodaya K, Parikh R, Ramanujam R, Thiagarajan P S 1991 Logics for distributed transition systems (in preparation).

[Lodaya et al 1989a] Lodaya K, Ramanujam R, Thiagarajan P S 1989a A logic for distributed transition systems, LNCS 354:508-522.

[Lodaya et al 1989b] Lodaya K, Ramanujam R, Thiagarajan P S 1989b Temporal logics for communicating sequential agents: I, Report IMSc/89/15, Inst. Math. Sc., Madras, India (to appear in Int. J. Found. of Comput. Sci.).

[Lodaya et al 1987] Lodaya K, Thiagarajan P S 1987 A modal logic for a subclass of event structures, LNCS 267:290-303. [Also Lodaya K, Thiagarajan P S 1989 A correction to “A modal logic for a subclass of event structures,” Report DAIMI-PB-275, Computer Science Dept, Århus Univ, Århus, Denmark.]

[Mazurkiewicz 1989] Mazurkiewicz A 1989 Basic notions of trace theory, LNCS 354:285-363.

[Milner 1989] Milner R 1989 Communication and concurrency (New York:Prentice-Hall).

[Mukund 1990] Mukund M 1990 Expressiveness and completeness of a logic for well branching prime event structures, Report TCS-90-1, School of Math., SPIC Science Foundation, Madras, India.

[Mukund et al 1989] Mukund M, Thiagarajan P S 1989 An axiomatization of event structures, LNCS 405:143-160.

[Mukund et al 1991] Mukund M, Thiagarajan P S 1991 A logical characterization of well branching event structures (to appear in Theor. Comput. Sci.).

[Nielsen et al 1980] Nielsen M, Plotkin G, Winskel G 1980 Petri nets, event structures and domains I, Theor. Comput. Sci. 13,1:86-108.

[Nielsen et al 1990] Nielsen M, Rozenberg G, Thiagarajan P S 1990 Behavioural notions for elementary net systems, Distr. Comput. 4,1:45-57.

[Ochmanski 1985] Ochmanski E 1985 Regular trace languages, Ph.D. thesis, Warsaw, Poland [summary in 1985 Bull. EATCS 27.]

[Olderog 1987] Olderog E-R 1987 Operational Petri net semantics for CCSP, LNCS 266:196-223.

[Parikh 1989] Parikh R 1989 Decidability and undecidability in distributed transition systems, in Narasimhan R (ed.): A perspective in theoretical computer science — commemorative volume for Gift Siromoney (Singapore:World Scientific) pp. 165-198.

[Peleg 1987] Peleg D 1987 Concurrent dynamic logic, J. ACM 34,2:450-479.

[Penczek 1988] Penczek W 1988 A temporal logic for event structures, Fund. Inf. XI:297-326.

[Pinter et al 1984] Pinter S, Wolper P 1984 A temporal logic for reasoning about partially ordered computations, Proc. 3rd ACM Conf. Princ. of Dist. Comput. pp. 28-37.

[Plotkin 1981] Plotkin G 1981 A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Dept, Århus Univ, Århus, Denmark.

[Pnueli 1977] Pnueli A 1977 The temporal logic of programs, Proc. 18th IEEE Conf. Found. of Comput. Sci. pp 46-57.

[Pratt 1986] Pratt V 1986 Modelling concurrency with partial orders, Int. J. Parallel Programming 15,1:33-71.

[Reisig 1986] Reisig W 1986 Towards a temporal logic for causality and choice in distributed systems, LNCS 354:603-627.

[Stark 1989] Stark E W 1989 Concurrent transition systems, Theor. Comput. Sci. 64:221-269.

[Stirling 1987] Stirling C 1987 Modal logics for communicating systems, Theor. Comput. Sci. 49:311-347.

[Thiagarajan 1990] Thiagarajan P S 1990 Some behavioural aspects of net theory, Theor. Comput. Sci. 71:133-153.

[Wang 1961] Wang H 1961 Proving theorems by pattern recognition II, Bell Syst. Tech. J. 40:1-41.

[Winskel 1982] Winskel G 1982 Event structure semantics for CCS and related languages, LNCS 140:561-577.

[Winskel 1987] Winskel G 1987 Event structures, LNCS 255:325-392.

[Zielonka 1987] Zielonka W 1987 Notes on finite asynchronous automata, RAIRO Inf. Th. et Appl. 21,2:99-135.