A Unary Semigroup Trace Algebra

Abstract

The Unifying Theories of Programming (UTP) of Hoare and He promote the unification of semantics catering for different concerns, such as, termination, data modelling, concurrency and time. Process calculi like  and CSP can be given semantics in the UTP using reactive designs whose traces can be abstractly specified using a monoid trace algebra. The prefix order over traces is defined in terms of the monoid operator. This order, however, is inadequate to characterise a broader family of timed process algebras whose traces are preordered instead. To accommodate these, we propose a unary semigroup trace algebra that is weaker than the monoid algebra. This structure satisfies some of the axioms of restriction semigroups and is a right P-Ehresmann semigroup. Reactive designs specified using it satisfy core laws that have been mechanised so far in Isabelle/UTP. More importantly, our results improve the support for unifying trace models in the UTP.

1 Introduction

The Unifying Theories of Programming (UTP) [1] is a relational framework for characterising different programming paradigms. It promotes the unification of semantics, while allowing different aspects, such as data, concurrency, termination, time, and so on, to be considered individually. Programs are specified via alphabetised relations in the style of Hehner’s Predicative Programming [2].

Behaviour, and concurrency, in the style of CCS, ACP and CSP [3], can be defined in the UTP via the theory of reactive processes. At its core is the notion of traces, that is, sequences of events that record the history of interactions.

The time dimension has been considered in different ways [4,5,6,7]. In [4], for example, traces are sequences of pairs that encode discrete time units. The first component of a pair records the sequence of events performed during that time, and the second component the set of events refused at that point. In [7], which presents a theory that can be used to give semantics in the UTP to the hardware programming language Handel-C [8] and other synchronous languages, a more abstract view is provided by a parametric model. It requires that the operators for addition and subtraction of pairs, and traces, satisfy a set of axioms.

Semantic models employing traces typically define a prefix relation $\le$ that specifies how a trace can be augmented, encoding some notion of causality. The semantics for CSP, for example, is defined using sequences whose prefix relation is a partial order. In that setting, a trace s is a prefix of t, written $s \le t$, exactly when , that is, there exists a trace u, such that () the concatenation of s with u is t. This led Foster et al. [9] to observe that the prefix order for several trace models can be abstractly defined in terms of a left-cancellative monoid, henceforth referred to as the “monoid trace algebra”.

In [7], however, a pair $(s,r_0)$ is a prefix of $(t,r_1)$ exactly when $s \le t$, but the refusal sets $r_0$ and $r_1$ are not constrained. Anti-symmetry is thus not satisfied and so the prefix relation on traces is merely a pre-order. The monoid trace algebra is unsatisfactory for such a theory of synchronous languages. Solving this problem is not only of theoretical interest to establish the commonality between different trace structures, but more importantly enables key results to be reusable in synchronous process algebra, thus promoting unification of models and results, a key goal of the UTP.

Unification in the UTP can be exploited in various ways, namely via subset embeddings, weakest completion semantics [10], Galois connections and parametric theories. The approach pursued in this paper is a contribution to the latter by generalising the theory of reactive processes even further. The main contribution is the definition of a unary left-cancellative semigroup, obtained by introducing a unary function and weakening of the monoid trace algebra axioms. The pairs from [7] are shown to satisfy this structure, as are finite sequences (traces) of such pairs. There is surprisingly little impact on the proofs already established for reactive processes as demonstrated by the mechanisation of our results in Isabelle/UTP [11].

The paper is structured as follows. In Sect. 2 the theory of reactive processes is introduced, as well as the monoid trace algebra. Our unary semigroup trace algebra is defined in Sect. 3. Our theory of synchronous algebra is characterised in Sect. 4. In Sect. 5 we discuss related work. In Sect. 6 we summarize the main results and provide pointers for future work.

2 Preliminaries

In the UTP programs are specified by alphabetised relations. Variables are used to define computations, with undashed variables (x) capturing the initial value, and dashed variables ($x'$) capturing the later, or final, value. These can be program variables, or auxiliar variables that capture information such as termination or execution time. A UTP theory is characterised by three components: an alphabet, a set of healthiness conditions, and a set of operators.

For example, in a theory of discrete time we may have variables t and $t'$ of type ${\mathbb {N}}$ to record time. The relation $t' = t + 1$ describes a computation whereby time is incremented by one time unit. To define the set of valid time-monotonic computations, a function on predicates can be defined (), so that the set of healthy predicates are the fixed points of $\mathbf {HC}$. When the healthiness conditions are idempotent and monotonic, with respect to the refinement order $\sqsubseteq$, their image forms a complete lattice, which allows reasoning about recursion.

The theory of reactive processes uses the auxiliary variables ok and $ok'$ to capture stability, wait and $wait'$ to record information about termination, tr and $tr'$ to record the history of interactions with the environment, and ref and $ref'$ to record the possibility of refusing interaction. The variable ok indicates whether the previous process is in a stable state, while $ok'$ records this information for the current process. Similarly, wait records termination for the previous process and $wait'$ for the current process. A process only starts executing in a state where ok and $\lnot wait$ are true. Termination occurs when $ok'$ and $\lnot wait'$ are true.

The interactions with the environment are captured by sequences of events, recorded by tr and $tr'$. The variable tr records the sequence of events that took place before the current process started, while $tr'$ records all the events that have been observed so far. Finally, ref and $ref'$ record the set of events that may be refused by the process at the start, and currently.

In the theory of synchronous algebra, as already said, tr and $tr'$ are sequences of pairs, where the first component is a sequence of events, and the second is a set of events that may be refused. The variables ref and $ref'$ are not used.

2.1 Monoid Trace Algebra

To conciliate different trace structures for reactive processes, Foster et al. [9] propose a trace algebra, where tr and $tr'$ are of an abstract type $\mathcal {T}$. Below we reproduce its axioms, where is concatenation, and $\varepsilon$ is the empty trace.

Definition 1 (TA)

A trace algebra () is a monoid satisfying the axioms:

Concatenation is associative (TA1), has the empty trace $\varepsilon$ as both a left and right unit (TA2), and is left-cancellative (TA3). Axiom TA4 eliminates “negative traces” by requiring that whenever the concatenation of x and y is the empty trace then x must also be the empty trace. The dual law can be deduced from axioms TA2 and TA4. We observe that while in [9] right-cancellation is also proposed as an axiom, the laws of the algebra, as well as the results established for the theory of reactive processes, as proved so far in Isabelle/UTP¹, do not depend on this axiom, and so we can safely omit it.

Standard finite sequences, for example, form a trace algebra, where is sequence concatenation and $\langle \rangle$ is the empty sequence. Using the two trace algebra operators it is possible to define a trace prefix relation ($x \le y$) and a trace subtraction operator ($x - y$) as reproduced below.

Definition 2 (Trace prefix)

Definition 3 (Subtraction)

 

A trace x is a prefix of y ($x \le y$) whenever y can be obtained by concatenating x with some trace z. When $x \le y$ the subtraction $y-x$ is z whose concatenation with x is y, specified using the definite description operator ($\iota$), as z is unique by TA3, and otherwise $y-x$ is $\varepsilon$ so that subtraction is total. In [9] it is shown that $(\mathcal {T},\le )$ is a partial order, and that $\varepsilon$ is the least element. As mentioned, this is unsuitable for the synchronous algebra, so in Sect. 3 we pursue a preorder.

2.2 Generalised Reactive Processes

Using the trace algebra, it is possible to define the healthiness conditions that underpin several theories based on reactive processes, reproduced below.

Definition 4 (Generalised Reactive Processes)

$\mathbf {R1}$ requires that a trace can only be extended. $\mathbf {R2}$ requires processes to be insensitive to the initial trace and is specified by substituting tr in P with the empty trace $\varepsilon$ and $tr'$ with the difference $tr'-tr$. Because this difference is only well-defined when $tr \le tr'$, the version $\mathbf {R2c}$ proposed by Foster et al. [9] applies $\mathbf {R2}$ conditionally: is P if c is true, and otherwise is Q. $\mathbf {R2a}$, defined using the greatest lower bound $\sqcap$, is an alternative for $\mathbf {R2}$ having the same fixed points. $\mathbf {R3}$ ensures that P may only start if the previous process has terminated ($\lnot wait$), and otherwise behaves as the identity , which keeps variables unchanged. This ensures that relational composition is sequential composition. Finally, the theory is characterised by $\mathbf {R}$, the composition of all conditions.

While these definitions are applicable to several reactive theories, $\mathbf {R2}$ and $\mathbf {R2a}$, for example, cannot be instantiated for synchronous algebra [7], whose counterparts to $\mathbf {R2}$ and $\mathbf {R2a}$ are reproduced below with subscript $_{S}$. Concatenation () and subtraction ($-_{S}$) of their traces are also annotated with $_{S}$.

Definition 5

$\mathbf {R2}_{S}$ considers the substitution of tr with a sequence whose only element is a pair: the first component is the empty sequence, and the second component is the set of events resulting from taking the second component (snd) of the pair extracted from the last element of tr, well-defined when $\mathbf {R1}$ is applied first.

Clearly the empty trace ($\varepsilon$) of the monoid trace algebra cannot abstractly encode an element that can take several values, such as snd(last(tr)). On the other hand, an examination of the algebraic laws satisfied by $\mathbf {R2}_{S}$, and counterparts to $\mathbf {R1}$ and $\mathbf {R3}$ in [5, 7], reveals a striking similarity with the laws established for generalised reactive designs, which indicates a similar unification is feasible as we demonstrate in Sect. 4 using the algebra we define next.

3 Unary Semigroup Trace Algebra

Instead of a fixed empty trace $\varepsilon$, we introduce a total function to obtain a unary semigroup (). The axioms are defined next in Sect. 3.1. In Sect. 3.2 we classify it according to the literature on semigroups. In Sect. 3.3 we show that the prefix relation is a preorder, and redefine subtraction.

3.1 Axioms

The following axioms can be seen as counterparts to that of the monoid trace algebra, adapted to consider $\varPhi$ and the fact that the structure is not a monoid.

Definition 6 (USTA)

A unary semigroup trace algebra () is a left-cancellative unary semigroup satisfying the following axioms:

Concatenation is associative (USTA1) so that we have a semigroup. Similarly to axiom TA2, we require that $\varPhi (x)$ is a right identity with respect to concatenation with x (USTA2). Concatenation is also left-cancellative (USTA3). From these three axioms we can establish that $\varPhi (x)$ is a left-unit for concatenation.

Lemma 1

Proof

Similarly to axiom TA4 of the monoid trace algebra, axiom USTA4 also eliminates “negative traces”, but when we draw a parallel between $\varepsilon$ and $\varPhi$, the shape of USTA4 is different. The requirement on the second operand y of the concatenation (rather than the first operand x as in axiom TA4) is sufficiently weak to ensure the prefix relation $\le$, defined in terms of , is not anti-symmetric.

To illustrate that axiom TA4 admits structures whose prefix relation $\le$ is not anti-symmetric, we consider the following example.

Example 1

Consider ($\mathcal {S}$, $\gg$, id), where $\mathcal {S}$ contains at least two distinct elements, and id is the identity function. Such structure is a unary semigroup trace algebra. We show that .

Proof

An interesting generalisation of ($\mathcal {S}$, $\gg$, id) is that ( ) satisfies the axioms of a U-semigroup [12, p. 102]. In general, $\varPhi$ is idempotent as we establish next.

Lemma 2

$\varPhi (\varPhi (x)) = \varPhi (x)$

Proof

Using Axiom USTA2.

Moreover, if $\varPhi$ is constant we can obtain the original monoid trace algebra by having .

Theorem 1

Provided , and () is a unary semigroup trace algebra, then ( ) is a monoid trace algebra.

Proof

Axioms TA1, TA2 and TA3 are trivially satisfied. Axiom TA4 can be satisfied by deduction using USTA2 and USTA4.    $\square$

Thus, the monoid trace algebra can be seen as a specialisation of the algebraic structure we propose. This and other results to follow have been mechanised in Isabelle². Moreover, we have used Isabelle’s counter-example generator nitpick to ascertain that axioms USTA1–USTA4 are independent. Next we discuss how the new structure can be classified according to the literature on semigroups.

3.2 Semigroup Properties

To establish key properties of the algebra, we first propose a lemma that is used in proofs to follow. The application of $\varPhi$ to a trace obtained by concatenating x and y is equal to $\varPhi (y)$ as stated in the lemma below.

Lemma 3

Proof

Using Axiom USTA2.

From Lemmas 1 and 3 we can deduce that $\varPhi$ distributes over , a property implicitly satisfied by left-cancellative restriction semigroups [13].

The structure is neither a left nor a right-restriction semigroup, as it satisfies only two (LR1 and LR2) out of four axioms [13] of left restriction semigroups, and three (RR1 to RR3) out of four axioms of right-restriction semigroups.

Theorem 2 (Laws of restriction semigroups)

Proof

(LR1) Using Lemma 1; (RR1) using Axiom USTA2.

(LR2) Using Lemmas 1 and 3; (RR2) using, in addition, Lemma 2.

(RR3)

A fourth axiom of restriction semigroups requires commutativity on the application of $\varPhi$ with respect to as . It is clear from Lemma 1 that this equality cannot hold. We have, however, that the structure satisfies the axioms of right P-Ehresmann semigroups [14], as established next.

Theorem 3

( ) is a right P-Ehresmann semigroup.

Proof (PE1) Using Axiom USTA2; (PE2) using Lemmas 1 and 3.

(PE3)

(PE4) Follows from Lemma 1.    $\square$

Despite proposing axioms based on a generalisation of those of the monoid trace algebra, it is pleasing to find that such a construction satisfies the axioms of a known class of semigroups. Next we study the induced prefix relation $\le$ of the algebra, defined in terms of , and its subtraction operator −.

3.3 Prefix and Subtraction

The prefix relation can be characterised exactly as in Definition 2. In what follows we study its key algebraic properties, starting by showing that it is a preorder.

Theorem 4

Provided ( ) is a USTA then ($\mathcal {T}$,$\le$) is a preorder. (TP1)

Proof (Reflexivity) Using Definition 2 and Axiom USTA2; (Transitivity) Using Definition 2, Axiom USTA1 and predicate calculus.

Moreover, we have that $\le$ satisfies the following laws, numbered to mirror the laws TP1-TP4 of the monoid trace algebra [9].

Theorem 5 (Trace Prefix Laws)

Trace $\varPhi (x)$ is smaller than any other trace (TP2). Law TP3 states that concatenation constructs larger traces, and Law TP4 states that concatenation is monotonic in its right argument. Next, we introduce the subtraction operator.

Definition 7 (Subtraction)

 

Subtraction is defined like in Definition 3 when $x \le y$, and otherwise is defined as $\varPhi (x)$. This deliberate choice of $\varPhi (x)$ is essential to ensure that the following laws TS1-TS10 (numbered after the laws TS1-TS8 in [9] as counterparts) hold. Notably absent from the following list is the counterpart to TS2 of the monoid trace algebra, which we discuss in the sequel. It does not hold in this setting, but this bears no impact on the results established for the reactive theory.

Theorem 6 (Trace Subtraction Laws)

Law TS1 states that the subtraction of a trace $\varPhi (y)$ from another trace is ineffective. Law TS3 states that subtracting a trace from itself is equal to applying $\varPhi$. Laws TS4–TS6 and TS8 capture expected properties of concatenation and subtraction, also satisfied by the monoid trace algebra. The implication in Law TS7 states that if the subtraction $x-y$ is $\varPhi (y)$, and y is a prefix of x, then x and y are the same. The reverse implication follows from Law TS3. The novel laws TS9–TS10 correspond to axioms SSub:same and SSub:subsub in [7, pp. 95–96].

The counterpart to Law TS2 ($\varepsilon - x = \varepsilon$) of the monoid trace algebra [9] could be stated in this setting as $\varPhi (y) - x = \varPhi (y)$. However, this equality does not hold in general. In particular, for example, if $x \le \varPhi (y)$ holds it is not necessarily the case that . Existing proofs for reactive processes do not depend on Law TS2, so the fact that it does not hold in our trace algebra has no practical impact. Next, we focus on instances of the algebra.

4 Trace Models

In this section we focus on instances of our trace algebra, and show that it can be instantiated to yield the traces of [7]. To that end, we consider pairs in Sect. 4.1 whose first component is a USTA. Then in Sect. 4.2 we consider these pairs as elements of finite non-empty sequences and show the lifted structure is a USTA.

4.1 Parametric Pairs

We introduce pairs $\mathcal {P} : \mathcal {H} \times \mathcal {R}$ parametrised by types $\mathcal {H}$ and $\mathcal {R}$, whose $\mathcal {H}$ must be a USTA $(\mathcal {H},+_{\mathcal {H}},\varPhi _{\mathcal {H}})$ where is concatenation, and is the unary function of the USTA. To construct a USTA for parametric pairs $(\mathcal {P},+_{\mathcal {P}},\varPhi _{\mathcal {P}})$, we define concatenation of pairs ($+_{\mathcal {P}}$) and $\varPhi _{\mathcal {P}}$ as follows.

Definition 8

$(h_1,r_1) +_{\mathcal {P}} (h_2,r_2) = (h_1 +_{\mathcal {H}} h_2,r_2)$

$$\begin{aligned} \varPhi _{\mathcal {P}} (h_1,r_1) = (\varPhi _{\mathcal {H}} (h_1), r_1) \end{aligned}$$

Concatenation of $(h_1,r_1)$ and $(h_2,r_2)$ is a pair where: the first component is the result of applying $+_{\mathcal {H}}$ to $h_1$ and $h_2$, and the second component is $r_2$. $\varPhi _{\mathcal {P}}$ is defined as the application of $\varPhi _{\mathcal {H}}$ to the first component. The definition of $+_{\mathcal {P}}$ closely follows the concatenation specified in [7]. However, unlike [7] we do not need to specify subtraction, as instead it can be derived as a lemma below.

Lemma 4

Provided $h_2 \le h_1$, $(h_1,r_1) - (h_2,r_2) = (h_1 - h_2,r_1)$.

With the above construction we can establish that $(\mathcal {P},+_{\mathcal {P}},\varPhi _{\mathcal {P}})$ is a USTA.

Theorem 7

Provided $(\mathcal {H},+_{\mathcal {H}},\varPhi _{\mathcal {H}})$ is a USTA then $(\mathcal {P},+_{\mathcal {P}},\varPhi _{\mathcal {P}})$ is a USTA.

Thus, the pairs of [7] form a USTA. Next, we consider a model for traces constructed from finite non-empty sequences whose elements are pairs of type $\mathcal {P}$.

4.2 Synchronous Traces

As already mentioned, the traces of synchronous process algebra consist of non-empty sequences of pairs [7]. In this section we construct this abstract trace structure stepwise, starting by defining a specialised model of finite non-empty sequences that is a USTA. This is then used to lift pairs of type $\mathcal {P}$ to traces.

Traces. A trace in this setting is a finite non-empty sequence defined via a recursive data type fs below, specified using the Z [15] notation for type constructors.

Definition 9

 

One constructs a sequence with a single element of type $\sigma$, and Cons constructs a sequence where an element is followed by a sequence of type fs. We use angled brackets $\langle a_0, ..., a_n \rangle _{fs}$ to represent consecutive applications of Cons, ending in $One~a_n$, and $\langle a_0 \rangle _{fs}$ for a single construction $One~a_0$. The subscript $_{fs}$ distinguishes finite non-empty sequences from standard finite sequences (that may be empty).

To construct a USTA for an fs parametrised by a given type $\sigma$ that is a USTA , we need to instantiate the respective structure in terms of and $\varPhi _{\sigma }$. We define concatenation ( ) next, and $\varPhi _{fs}$ in the sequel.

Definition 10 (Concatenation of non-empty sequences)

The concatenation of two sequences $\langle x\rangle _{fs}$ and $\langle y\rangle _{fs}$, with one element each, is a sequence whose only element is the result of the sum ($+_{\sigma }$) of x and y. A sequence $\langle x \rangle _{fs}$ concatenated with $\langle a_0, ..., a_n \rangle _{fs}$ is defined as $\langle x+_{\sigma }a_0, ..., a_n \rangle _{fs}$, that is, the first element is the sum ($+_{\sigma }$) of x and the first element $a_0$ of the second sequence. Finally, a sequence $\langle a_0,...,a_n\rangle _{fs}$ concatenated with g has $a_0$ as first element followed by the concatenation of the tail of that sequence with g.

We observe that is distinctive from standard sequence concatenation, so as to induce an appropriate definition for prefixing and subtraction (Definitions 2 and 7). For example, the subtraction of $\langle a\rangle _{fs}$ from itself is the sequence z whose concatenation with $\langle a\rangle _{fs}$ yields $\langle a\rangle _{fs}$ (). Because fs sequences are non-empty, z is the sequence $\langle \varPhi _{\sigma } (a) \rangle _{fs}$ so that $\langle a +_{\sigma } \varPhi _{\sigma } (a)\rangle _{fs} = \langle a\rangle _{fs}$, as required. This in contrast to subtraction of standard sequences, where $\langle a \rangle - \langle a \rangle = \langle \rangle$. Similar reasoning applies to ensure $\le$ is reflexive.

Indeed to show that is a USTA given a type $\sigma$ that is a USTA $(\sigma ,+_{\sigma },\varPhi _{\sigma })$, we define $\varPhi _{fs}$ in terms of $\varPhi _{\sigma }$ as follows.

Definition 11

$\varPhi _{fs} (x) = \langle \varPhi _{\sigma }(last(x)) \rangle _{fs}$

It is defined as the sequence whose only element is obtained by applying $\varPhi _{\sigma }$ to its last element. By construction x is non-empty, so last and head are always well-defined. Thus, provided $\sigma$ is a USTA, a sequence s of type fs can be split into concatenations involving its front and last element, and its head and tail.

Lemma 5

, and .

The functions front and tail are tailored to non-empty sequences. For example, $front(\langle a\rangle _{fs})$ is $\langle \varPhi _{\sigma } (a)\rangle _{fs}$, while $front(\langle a, b\rangle _{fs})$ is $\langle a, \varPhi _{\sigma } (b)\rangle _{fs}$, and $tail(\langle a \rangle _{fs})$ is $\langle \varPhi _{\sigma } (a)\rangle _{fs}$, while $tail(\langle a, b\rangle _{fs})$ is $\langle \varPhi _{\sigma } (a), b\rangle _{fs}$, so that the decomposition holds.

Next we use this structure to instantiate the USTA for fs sequences, which corresponds to the trace structure underlying synchronous process algebra.

Theorem 8

Provided $(\sigma ,+_{\sigma },\varPhi _{\sigma })$ is a USTA, then is a USTA.

As a corollary to this theorem we have that a parametric pair $\mathcal {P}$ whose type parameter $\mathcal {H}$ is a USTA $(\mathcal {H},+_{\mathcal {H}},\varPhi _{\mathcal {H}})$ induces a USTA.

Corollary 1

If $(\mathcal {H},+_{\mathcal {H}},\varPhi _{\mathcal {H}})$ is a USTA, then is a USTA.

This demonstrates that to construct such a USTA it is sufficient to show that $\mathcal {H}$ is a USTA. This is a much more general, and concise, construction, than that proposed in [7], which instead requires satisfying nearly 26 axioms. Moreover, our results do not rely on any assumptions about the type $\mathcal {R}$, thus allowing the second component of such pairs in a trace to record arbitrary information, not only refusal sets as proposed in [7]. Next we focus on key properties of traces leading to a demonstration that we can derive core laws of [7], and the healthiness conditions of the corresponding UTP theory.

Properties. Below we establish key results on the difference of fs sequences.

Theorem 9

Provided $(\sigma ,+_{\sigma },\varPhi _{\sigma })$ is a USTA and $s \le t$, where s, t : fs,

The tail of the difference $t - s$ is the tail of the difference between t and the front of s (S1). Likewise, the head of the difference $t - s$ is equal to the last element of s subtracted from the head of the difference $t - front(s)$ (S2). Related, (S3) establishes that last(s) is a prefix of $head(t - front(s))$.

To illustrate the role of S1, we consider, as an example the subtraction of a fs sequence whose elements are standard sequences. The subtraction of $\langle \langle a\rangle , \langle b\rangle \rangle _{fs}$ from $\langle \langle a\rangle , \langle b, c\rangle , \langle d\rangle \rangle _{fs}$ is $\langle \langle c\rangle , \langle d\rangle \rangle _{fs}$, indicating that the first element where the sequences differ is the inner sequence $\langle b, c\rangle$. The front of $\langle \langle a\rangle , \langle b\rangle \rangle _{fs}$ is $\langle \langle a\rangle ,\langle \rangle \rangle _{fs}$, and so the difference $\langle \langle a\rangle , \langle b, c\rangle , \langle d\rangle \rangle _{fs} - \langle \langle a\rangle ,\langle \rangle \rangle _{fs}$ is $\langle \langle b, c\rangle , \langle d\rangle \rangle _{fs}$. Finally, the $tail(\langle \langle b, c\rangle , \langle d\rangle \rangle _{fs}) = \langle \langle \rangle , \langle d\rangle \rangle _{fs}$ coincides with that of $\langle \langle c\rangle , \langle d\rangle \rangle _{fs}$.

Moreover, we show below that Eq. 3 in [7] also holds in our setting of fs sequences of parametric pairs $\mathcal {P}$, provided $(\mathcal {H},+_{\mathcal {H}},\varPhi _{\mathcal {H}})$ is a USTA.

Lemma 6

.

The concatenation of traces s and t can be decomposed into the concatenation of the front of s with a singleton sequence, whose only element is the result of concatenating ($+_{\mathcal {P}}$) the last pair of s and the head pair of t, and the tail of t.

Reactive Processes. Besides the definition of an abstract trace structure that can be instantiated to yield the trace structure in [7], we discuss next how it can be used to define a generalised theory of reactive processes. Here we focus on the instantiation of the healthiness conditions.

Healthiness Conditions. The functions $\mathbf {R1}$ and $\mathbf {R3}$ are stated like in Sect. 2, but in the context of a USTA , with tr and $tr'$ of type $\mathcal {T}$. $\mathbf {R2}$, on the other hand, must be adapted to accommodate the function $\varPhi$.

Definition 12

Our definition for $\mathbf {R2}$ is stated by replacing $\varepsilon$ with $\varPhi (tr)$. Moreover, the definition for $\mathbf {R2a}$, when compared to Definition 4, requires that, in addition z and tr agree on the application of $\varPhi$. This closely follows a solution proposed in [7, p. 83].

Despite employing a weaker trace algebra, the core properties of $\mathbf {R1}$, $\mathbf {R2}$ and $\mathbf {R3}$, namely idempotency and monotonicity with respect to refinement, continue to hold. Similarly, all laws of reactive processes, and those for other theories built upon reactive processes, namely CSP, continue to hold as demonstrated by the mechanisation in Isabelle/UTP, which features several hundreds of theorems.

Because the existing theories are mechanised we have been able to quickly establish that all relevant properties hold when using our algebra. Proofs of closure for sequential and parallel composition under $\mathbf {R2}$ required small adjustments to take into account $\varPhi$, but were structurally kept unchanged. Next, we illustrate a concrete instantiation of the algebra to accommodate the trace model of [4].

Concrete instantiation for . In what follows we show how our algebra can be instantiated to yield the theory of , that encompasses behaviour and data modelling in a discrete-time setting.

The parametric pair type $\mathcal {P}$ is instantiated with $\mathcal {H}$ as , where $\varSigma$ is a given type of events, which is a USTA . Concatenation () is associative (USTA1), left-cancellative (USTA3) and satisfies USTA4. The empty sequence $\langle \rangle$ is a right-unit (USTA2). The parameter $\mathcal {R}$ is instantiated as , a set of events. Thus, the first component of such a pair is a sequence and the second a set of events. For example, the pair $(\langle a, b\rangle , \{a\})$ records that having performed events a, and then b, the system can refuse to engage in event a.

Therefore, the lifted structure of finite non-empty sequences fs parametrised by the concrete pair structure above, gives rise to a USTA (Corollary 1). For example, in  the sequence $\langle (\langle a, b\rangle , \{a\}), (\langle \rangle ,\varSigma ) \rangle _{fs}$ encodes a situation where: during the first time unit a and b are performed, with a then being refused, and during the following time unit no events are performed ($\langle \rangle$) with the system refusing to engage in any event ($\varSigma$).

Compared with the approach in [4], we have that both concatenation and subtraction of fs sequences (using the lifted structure) is total and closed under the correct type. This provides for a precise encoding of the healthiness conditions proposed in [4] using our abstract algebra. Furthermore, this makes mechanisation of the model in Isabelle/UTP an easier endeavour by eliminating the need to reprove a substantial base of existing theorems of reactive processes.

In the remainder of this section we show two key results that demonstrate $\mathbf {R1}$ and $\mathbf {R2}$ can be instantiated to yield the counterpart definitions for .

Lemma 7

$s \le t \implies front(s) \le t \wedge fst(last(s)) \le fst(head(t-front(s)))$.

This corresponds to the conjunct in the definition of $\mathbf {R1}$ for  as defined in [16], for example, with the understanding that here front is total, whereas in [7, 16] it is a partial function over standard sequences.

The definition of $\mathbf {R2}_{S}$ for  is derived next. First we establish a result for the subtraction of fs traces that depends on the following lemma.

Lemma 8

$s \le t \implies snd(head(t-front(s)) - last(s)) = snd(head(t-front(s)))$.

This lemma states that the second component of the difference, between the head of the difference t and the front of s, and last(s), does not depend on last(s), a result that follows from Lemma 4. For example, the subtraction of $\langle (\langle a\rangle ,r_2)\rangle _{fs}$ from $\langle (\langle a, b\rangle ,r_1)\rangle _{fs}$ yields the sequence $\langle (\langle b\rangle ,r_1) \rangle _{fs}$ as the second component only depends on $r_1$, but not $r_2$. Next, we establish a general result for subtraction of fs traces.

Theorem 10

Provided $s \le t$, where s, t : fs,

Proof

The subtraction $t - s$ can be expressed in terms of the difference $t - front(s)$, and last(s). The head of $t - front(s)$ contains the observations up until the end of the current time unit [16, p. 13]. Together with the pair instantiation as before we can derive the concrete definition of $\mathbf {R2}$ for , similarly to Definition 5 where $\varPhi (tr)$ becomes $\langle (\langle \rangle ,snd(last(tr)))\rangle _{fs}$ following Definitions 8 and 11, and $tr' -_{S} tr$ is as given by Theorem 10.

5 Related Work

Traces are at the core of semantic models for reasoning about causality. Already in Hoare’s CSP book [17] we can find a rich collection of operators and laws for manipulating traces. In the standard semantics [3] of CSP traces are sequences of events ordered by sequence prefixing. Richer semantic models for CSP, such as refusal testing [18, 19] and the finite-linear models [3, p. 256], also record in traces the set of events refused, or accepted, in the latter, before each event.

The modelling of time in semantics for process algebra is often achieved by associating events or state observations with time. Hayes’ reactive timed designs [20], comparable to action systems and TLA, define traces as mappings from time (discrete or continuous) to the values of program variables.

Sherif et al. [4] defined a semantics for  where traces are sequences whose elements are pairs, recording the events performed, and subsequently refused, during a time unit. Wei et al. [5] considered an equivalent model, where events and refusals are recorded separately in two distinct traces of equal length. Woodcock et al. [6] in their semantics for CML define sequences whose elements are events or refusal sets, that implicitly mark the passage of time, a structure pioneered by Lowe and Ouaknine [21] in their timed traces.

Butterfield et al. [7] proposed a parametric theory, which is the inspiration for the work presented in this paper. It generalises the model of   [4] to account for different observation models within a time unit. A similar approach is pursued by Zhu et al. [22], in their semantics for SystemC, who define a trace as a three dimensional sequence structure to account for macro and micro time.

Trace models for true concurrency in process algebra include the works of Barnes [23] and Smith [24]. The latter [24] defines traces whose elements are sequences, with the prefix relation allowing permutations of the inner sequences. This model can likely be instantiated as a trace algebra with elements as sets. Barnes’ SCSP, on the other hand, cannot be instantiated within the setting of [7].

More recently, Foster et al. [9] proposed a left-cancellative monoid trace algebra which is at the core of the mechanisation of several reactive theories in Isabelle/UTP [11]. This enabled Foster et al. [25] to define reactive contracts, as well as a theory for hybrid relations [26]. Their prefix relation over traces, however, is an order, which is inadequate to characterise traces where the relation is not anti-symmetric. Our results are complementary and support the unification of further trace models under the Isabelle/UTP framework.

6 Conclusions

Originally motivated by the goal of mechanising  [4] in the theorem prover Isabelle/UTP [11], we have pursued an ambitious generalisation of the monoid trace algebra [9] to account for a broader family of timed process algebras. We have weakened the monoid axioms, inspired by the observations in [7], to construct a novel unary semigroup trace algebra that is also a right P-Ehresmann semigroup. Compared to the large set of axioms in [7], we have a much smaller set that closely mirrors the axioms of the monoid trace algebra.

Our results support the definition of a parametric UTP theory of reactive processes that abstractly characterises several trace-based semantics. Besides the trace models discussed in [9] our algebra can be instantiated to account for the models discussed in [7, 8], including  [4]. In the future, we hope to accommodate the semantics for the system-level language SystemC [22], and perhaps even other synchronous languages such as Esterel [27].

Besides providing a foundation for the unification of further trace models in the UTP, we have also shown that our work has practical impact via its mechanisation in Isabelle/UTP [11]. It promotes the reuse of a large collection of theorems already established for the theories of reactive processes and reactive designs. It would be interesting, for example, to revisit our mechanisation of a stepwise construction for  [16] in this setting. Another avenue for future work is the mechanisation of the Galois connection in [4] that enables timed models to be verified using untimed tools.

The mechanisation of the timed operators of timed process calculi is likely to benefit from the definition of a timed trace algebra, consisting of an additional function from traces to time, with continuous and discrete versions. Basic processes, such as event prefixing and delay, may also be defined parametrically.

We envision it may be feasible to weaken the unary semigroup trace algebra even further to characterise additional trace structures, such as those of refusal-testing, the finite-linear model, and those of SCSP. However, it is likely that such weakenings may reveal certain laws of reactive processes no longer hold. An open question is the treatment of infinite traces, for example, which seem necessary to give a full account of the hiding operator of CSP. The Isabelle/UTP [11] mechanisation will facilitate the design space exploration of such weakenings, with immediate feedback provided to the proof engineer, a facility we used extensively during the course of developing the algebra presented in this paper.