key: cord-0060863-ay37w0i0 authors: Ribeiro, Pedro title: A Unary Semigroup Trace Algebra date: 2020-04-01 journal: Relational and Algebraic Methods in Computer Science DOI: 10.1007/978-3-030-43520-2_17 sha: 800618e77f7dfa6ca03f5e6d04d1f16718a33216 doc_id: 60863 cord_uid: ay37w0i0 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 [Image: see text] 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. 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 ≤ 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 ≤ t, exactly when s ≤ t ⇔ ∃ u • s u = t, 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 ≤ 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. 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 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 HC(P ) = P ∧ t ≤ t on predicates can be defined ( =), so that the set of healthy predicates are the fixed points of HC. When the healthiness conditions are idempotent and monotonic, with respect to the refinement order , 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 ¬ wait are true. Termination occurs when ok and ¬ 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. 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 T . Below we reproduce its axioms, where is concatenation, and ε is the empty trace. A trace algebra (T , , ε) is a monoid satisfying the axioms: Concatenation is associative (TA1), has the empty trace ε 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 x y = ε ⇒ y = ε can be deduced from axioms TA2 and TA4. We observe that while in [9] rightcancellation 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 1 , do not depend on this axiom, and so we can safely omit it. Standard finite sequences, for example, (seq A, , ) form a trace algebra, where is sequence concatenation and is the empty sequence. Using the two trace algebra operators it is possible to define a trace prefix relation (x ≤ y) and a trace subtraction operator (x − y) as reproduced below. A trace x is a prefix of y (x ≤ y) whenever y can be obtained by concatenating x with some trace z . When x ≤ y the subtraction y − x is z whose concatenation with x is y, specified using the definite description operator (ι), as z is unique by TA3, and otherwise y − x is ε so that subtraction is total. In [9] it is shown that (T , ≤) is a partial order, and that ε is the least element. As mentioned, this is unsuitable for the synchronous algebra, so in Sect. 3 we pursue a preorder. Using the trace algebra, it is possible to define the healthiness conditions that underpin several theories based on reactive processes, reproduced below. . R1 requires that a trace can only be extended. R2 requires processes to be insensitive to the initial trace and is specified by substituting tr in P with the empty trace ε and tr with the difference tr − tr . Because this difference is only well-defined when tr ≤ tr , the version R2c proposed by Foster et al. [9] applies R2 conditionally: P c Q is P if c is true, and otherwise is Q. R2a, defined using the greatest lower bound , is an alternative for R2 having the same fixed points. R3 ensures that P may only start if the previous process has terminated (¬ wait), and otherwise behaves as the identity II , which keeps variables unchanged. This ensures that relational composition is sequential composition. Finally, the theory is characterised by R, the composition of all conditions. While these definitions are applicable to several reactive theories, R2 and R2a, for example, cannot be instantiated for synchronous algebra [7] , whose counterparts to R2 and R2a are reproduced below with subscript S . Concatenation ( S ) and subtraction (− S ) of their traces are also annotated with S . 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 R1 is applied first. Clearly the empty trace (ε) 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 R2 S , and counterparts to R1 and 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. Instead of a fixed empty trace ε, we introduce a total function Φ : T → T to obtain a unary semigroup (T , , Φ). 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. The following axioms can be seen as counterparts to that of the monoid trace algebra, adapted to consider Φ and the fact that the structure is not a monoid. is a leftcancellative unary semigroup satisfying the following axioms: Concatenation is associative (USTA1) so that we have a semigroup. Similarly to axiom TA2, we require that Φ(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 Φ(x ) is a left-unit for concatenation. Proof. Similarly to axiom TA4 of the monoid trace algebra, axiom USTA4 also eliminates "negative traces", but when we draw a parallel between ε and Φ, the shape of USTA4 is different. The requirement on the second operand y of the concatenation x y (rather than the first operand x as in axiom TA4) is sufficiently weak to ensure the prefix relation ≤, defined in terms of , is not anti-symmetric. To illustrate that axiom TA4 admits structures whose prefix relation ≤ is not anti-symmetric, we consider the following example. Example 1. Consider (S, , id ), where S contains at least two distinct elements, x y = y and id is the identity function. Such structure is a unary semigroup trace algebra. We show that ∃ a, b : An interesting generalisation of (S, , id ) is that (T , , id ) satisfies the axioms of a U -semigroup [12, p. 102 ]. In general, Φ is idempotent as we establish next. Proof. Axioms TA1, TA2 and TA3 are trivially satisfied. Axiom TA4 can be satisfied by deduction using USTA2 and USTA4. 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 2 . 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. To establish key properties of the algebra, we first propose a lemma that is used in proofs to follow. The application of Φ to a trace obtained by concatenating x and y is equal to Φ(y) as stated in the lemma below. From Lemmas 1 and 3 we can deduce that Φ 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. Proof. (LR1) Using Lemma 1; (RR1) using Axiom USTA2. (LR2) Using Lemmas 1 and 3; (RR2) using, in addition, Lemma 2. A fourth axiom of restriction semigroups requires commutativity on the appli- . 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. Proof. (PE1) Using Axiom USTA2; (PE2) using Lemmas 1 and 3. 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 ≤ of the algebra, defined in terms of , and its subtraction operator −. 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. Moreover, we have that ≤ satisfies the following laws, numbered to mirror the laws TP1-TP4 of the monoid trace algebra [9] . Trace Φ(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. Subtraction is defined like in Definition 3 when x ≤ y, and otherwise is defined as Φ(x ). This deliberate choice of Φ(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. x states that the subtraction of a trace Φ(y) from another trace is ineffective. Law TS3 states that subtracting a trace from itself is equal to applying Φ. 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 Φ(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 (ε−x = ε) of the monoid trace algebra [9] could be stated in this setting as Φ(y) − x = Φ(y). However, this equality does not hold in general. In particular, for example, if x ≤ Φ(y) holds it is not necessarily the case that (ιz • Φ(y) = x z ) = Φ(y). 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. 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. We introduce pairs P : H×R parametrised by types H and R, whose H must be a USTA (H, + H , Φ H ) where + H : H×H → H is concatenation, and Φ H : H → H is the unary function of the USTA. To construct a USTA for parametric pairs (P, + P , Φ P ), we define concatenation of pairs (+ P ) and Φ P as follows. Concatenation of (h 1 , r 1 ) and (h 2 , r 2 ) is a pair where: the first component is the result of applying + H to h 1 and h 2 , and the second component is r 2 . Φ P is defined as the application of Φ H to the first component. The definition of + 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. With the above construction we can establish that (P, + P , Φ 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 P. As already mentioned, the traces of synchronous process algebra consist of nonempty 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 P to 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. fs ::= One σ | Cons σ × fs One constructs a sequence with a single element of type σ, and Cons constructs a sequence where an element is followed by a sequence of type fs. We use angled brackets a 0 , ..., a n fs to represent consecutive applications of Cons, ending in One a n , and a 0 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 σ that is a USTA (σ, σ , Φ σ ), we need to instantiate the respective structure (fs, fs , Φ fs ) in terms of σ and Φ σ . We define concatenation ( fs ) next, and Φ fs in the sequel. fs : fs × fs → fs ∀ x , y : σ; f , g : fs • One x fs One y = One (x + σ y) One x fs Cons (y, f ) = Cons (x + σ y, f ) The concatenation of two sequences x fs and y fs , with one element each, is a sequence whose only element is the result of the sum (+ σ ) of x and y. A sequence x fs concatenated with a 0 , ..., a n fs is defined as x + σ a 0 , ..., a n fs , that is, the first element is the sum (+ σ ) of x and the first element a 0 of the second sequence. Finally, a sequence a 0 , ..., a n 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 fs 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 a fs from itself is the sequence z whose concatenation with a fs yields a fs (ιz • a fs = a fs fs z ). Because fs sequences are non-empty, z is the sequence Φ σ (a) fs so that a + σ Φ σ (a) fs = a fs , as required. This in contrast to subtraction of standard sequences, where a − a = . Similar reasoning applies to ensure ≤ is reflexive. Indeed to show that (fs, fs , Φ fs ) is a USTA given a type σ that is a USTA (σ, + σ , Φ σ ), we define Φ fs in terms of Φ σ as follows. It is defined as the sequence whose only element is obtained by applying Φ σ to its last element. By construction x is non-empty, so last and head are always well-defined. Thus, provided σ 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 . The functions front and tail are tailored to non-empty sequences. For example, , while tail ( a, b fs ) is Φ σ (a), b 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 (σ, + σ , Φ σ ) is a USTA, then (fs, fs , Φ fs ) is a USTA. As a corollary to this theorem we have that a parametric pair P whose type parameter H is a USTA (H, + H , Φ H ) induces a (fs, fs , Φ fs ) USTA. This demonstrates that to construct such a USTA it is sufficient to show that 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 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. 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 S 1, we consider, as an example the subtraction of a fs sequence whose elements are standard sequences. The subtraction of a , b fs from a , b, c , d fs is c , d fs , indicating that the first element where the sequences differ is the inner sequence b, c . The front of a , b fs is a , fs , and so the difference a , b, c , d fs − a , fs is b, c , d fs . Finally, the tail ( b, c , d fs ) = , d fs coincides with that of c , d fs . Moreover, we show below that Eq. 3 in [7] also holds in our setting of fs sequences of parametric pairs P, provided (H, + H , Φ H ) is a USTA. Lemma 6. s fs t = front(s) fs last(s) + P head (t) fs fs tail (t). 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 (+ 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 R1 and R3 are stated like in Sect. 2, but in the context of a USTA (T , , Φ), with tr and tr of type T . R2, on the other hand, must be adapted to accommodate the function Φ. Our definition for R2 is stated by replacing ε with Φ(tr ). Moreover, the definition for R2a, when compared to Definition 4, requires that, in addition z and tr agree on the application of Φ. This closely follows a solution proposed in [7, p. 83 ]. Despite employing a weaker trace algebra, the core properties of R1, R2 and 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 R2 required small adjustments to take into account Φ, but were structurally kept unchanged. Next, we illustrate a concrete instantiation of the algebra to accommodate the trace model of [4] . In what follows we show how our algebra can be instantiated to yield the theory of Circus Time, that encompasses behaviour and data modelling in a discrete-time setting. The parametric pair type P is instantiated with H as seq Σ, where Σ is a given type of events, which is a USTA (seq Σ, , ). Concatenation ( ) is associative (USTA1), left-cancellative (USTA3) and satisfies USTA4. The empty sequence is a right-unit (USTA2). The parameter R is instantiated as P Σ, 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 ( a, b , {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 Circus Time the sequence ( a, b , {a}), ( , Σ) 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 ( ) with the system refusing to engage in any event (Σ). 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 R1 and R2 can be instantiated to yield the counterpart definitions for Circus Time. This corresponds to the conjunct in the definition of R1 for Circus Time 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 R2 S for Circus Time is derived next. First we establish a result for the subtraction of fs traces that depends on the following lemma. 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 ( a , r 2 ) fs from ( a, b , r 1 ) fs yields the sequence ( b , r 1 ) 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. 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 R2 for Circus Time, similarly to Definition 5 where Φ(tr ) becomes ( , snd (last(tr ))) fs following Definitions 8 and 11, and tr − S tr is as given by Theorem 10. 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 Circus Time 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 Circus Time [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. Originally motivated by the goal of mechanising Circus Time [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 Circus Time [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 Circus Time [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 refusaltesting, 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. Unifying Theories of Programming Predicative programming part I Understanding Concurrent Systems A process algebraic framework for specification and validation of real-time systems Circus Time with reactive designs The COMPASS modelling language: timed semantics in UTP Slotted-circus: A UTP-family of reactive theories A denotational semantics for Handel-C Unifying theories of time with generalised reactive processes Probabilistic semantics for RoboChart Isabelle/UTP: a mechanised theory engineering framework Fundamentals of Semigroup Theory Proper two-sided restriction semigroups and partial actions A common framework for restriction semigroups and regular *-semigroups Using Z -Specification, Refinement, and Proof A stepwise approach to linking theories Communicating Sequential Processes A refusal testing model for CSP Refusal testing Unifying theories of programming that distinguish nontermination and abort On timed models and full abstraction Denotational semantics and its algebraic derivation for an event-driven system-level language A mathematical theory of synchronous communication A unifying theory of true concurrency based on CSP and lazy observation Unifying theories of reactive design contracts. Theor Hybrid relations in Isabelle/UTP The Esterel synchronous programming language: design, semantics, implementation Acknowledgements. This work is funded by the EPSRC grant EP/M025756/1. No new primary data was created as part of the study reported here. We are grateful to Ana Cavalcanti for comments on an earlier draft of this paper, and to the anonymous reviewers for their helpful and constructive feedback.