A Formally Verified SMT Approach to True Concurrency? Juliana K. F. Bowles[0000−0002−5918−9114] and Marco B. Caminati[0000−0002−4529−5442] School of Computer Science, University of St Andrews St Andrews KY16 9SX, United Kingdom {jkfb|mbc8}@st-andrews.ac.uk Abstract. Many problems related to distributed and parallel systems, such as scheduling and optimisation, are computationally hard, thereby justifying the adoption of SMT solvers. The latter provide standard arithmetic as interpreted functions, naturally leading to express concur- rent executions as a linearly-ordered sequentialisation (or interleaving) of events, which have an obvious correspondence with integer segments and therefore permit to take advantage of such arithmetical capabilities. However, there are alternative semantic approaches (also known as true concurrent) not imposing the extra step of interleaving events, which brings the question of how to computationally exploit SMT solvers in these approaches. This paper presents a solution to this problem, and in- troduces a metric, made possible by adopting a true concurrent paradigm, which relates mutually distinct solutions of a family of distributed optimi- sation problems. We also contribute an original, computational definition of degree of parallelism, which we compare with the existing ones. Finally, we use theorem proving to formally certify a basic correctness property of our true concurrent approach. 1 Introduction and Related Work There are many possible models to capture the behaviour of distributed and parallel systems. Here we use labelled (prime) event structures [24], or event structures for short. Event structures have been widely studied in the literature, and have been used to give a true concurrent semantics to process calculi such as CCS, CSP, SCCS and ACP (e.g., [23]). The advantages of prime event structures include their underlying simplicity and how they naturally describe fundamental notions present in behavioural models including sequential, parallel and iterative behaviour (or the unfoldings thereof) as well as nondeterminism (cf. [14]), and are hence our model of choice. Event structures consist of sets of events and ? This research is supported by MRC grant MR/S003819/1 and Health Data Research UK, an initiative funded by UK Research and Innovation, Department of Health and Social Care (England) and the devolved administrations, and leading medical research charities. Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). binary relations over events to represent these notions. When used to capture the behaviour of a system, for example, event structures can be further equipped with labelling (total or partial) functions that associate information to these events, such as the action performed, action synchronisations, or any additional metric that may be relevant within the context. For instance, in a medical context an event may be associated with taking a particular medication, and a measure of interest may be the efficacy of the chosen medication for the underlying treatment. Event structures have well-defined composition operators (cf. e.g., [18]). How- ever, these composition mechanisms ignore labels and are hence inadequate for our use here. In practice we are not interested in computing the composition of models, but rather in finding optimal paths of execution in such a composition with respect to a certain measure of interest (usually a certain integer value which we want to maximise or minimise). Again, within a medical context this may be to maximise the efficacy of the medications given to patients following multiple treatment plans (which may be the case if patients have multimorbidi- ties, i.e., multiple ongoing chronic conditions). In this case, we are searching for optimal treatment plans which also avoid adverse drug reactions between chosen medications (i.e., maximise efficacy whilst minimising adverse reactions). When measures of interest can be quantified, we can make use of SMT (Satisfiability Modulo Theories) solvers to search for the optimal solution. We have used the SMT solver Z3 [17] in our earlier work (see for instance [5,6,7]). However, in that work we have ignored the true concurrent nature of event structures and treated the inherent parallelism within executions as interleaving. In this paper, we turn our attention to the problem of computing and se- lecting trace executions in a true-concurrent manner, as opposed to an implicit non-deterministic choice among allowed sequentialisations (or interleaving) of events. While work exists providing theoretical frameworks to characterise and reason about true-concurrency [1], [10], [15], true-concurrent approaches to the computational problem introduced above are rare. Other existing works we are aware of (see, for example, [12]) deal with notions of distance between different event structures, rather than between trace executions of one event structure. In [16] a problem similar to the one considered here is studied, but within the theoretical framework of Petri nets, and without including a numerical interaction between sets of concurrent events to influence the execution choice, as we do here: there, the focus is more on the theoretical study of the complexity associated with checking the optimality of a number of resources (concurrency threshold) for the execution of a given parallel process. Our work presents similar differ- ences with [9], where an encoding of timed BPMN models into rewriting logic is presented; this permits to use the rewriting logic implementation Maude [8] in order to reflect about a notion of parallelism degree. The contributions we provide are: an SMT-viable model for a true-concurrent handling of trace executions, a notion of metric to be able to choose among such executions, and, at the same time, to quantify the degree of concurrency of a trace execution; finally, a formal verification of a basic sanity property of our approach through the theorem prover Isabelle/HOL, where Isabelle is foundation-agnostic proof assistant and Isabelle/HOL is the strain based on higher-order logic (HOL) [19]1 This paper is structured as follows. Section 2 describes the formal model used, how configurations and paths/traces of executions are defined, as well as what resources we care to maximise/minimise when searching for the optimal path. Our SMT-based formulation of the problem is shown in Section 3 and how verification is done is described in Section 4. This is followed by concluding remarks in Section 5. 2 Formal Model In an event structure, we have a set of event occurrences together with binary relations for expressing causal dependency (called causality) and nondeterminism (called conflict). The causality relation implies a (partial) order among event occurrences, while the conflict relation expresses how the occurrence of certain events excludes the occurrence of others. From the two relations defined over the set of events, a further relation is derived, namely the concurrency relation co. Two events are concurrent if and only if they are completely unrelated, i.e., neither related by causality nor by conflict. The formal definition of an event structure, as in [14], is as follows. Definition 1. An event structure is a triple E = (Ev, →∗ , #) where Ev is a set of events and →∗ , # ⊆ Ev × Ev are binary relations called causality and conflict, respectively. Causality →∗ is a partial order. Conflict # is symmetric and 0 00 00 irreflexive, and propagates over causality, i.e., e#e ∧ e0 →∗ e ⇒ e#e for all 0 00 0 0 ∗ 0 0 e, e , e ∈ Ev. Two events e, e ∈ Ev are concurrent, e co e iff ¬(e → e ∨e →∗ 0 e ∨ e#e ). C ⊆ Ev is a configuration iff (1) C is conflict-free: ∀e, e ∈ C¬( e#e0 ) 0 and (2) downward-closed: e ∈ C and e0 →∗ e implies e0 ∈ C. We assume discrete event structures. Discreteness imposes a finiteness con- straint on the model, i.e., there are always only a finite number of causally related predecessors to an event, known as the local configuration of the event (written ↓ e). A further motivation for this constraint is given by the fact that every execution has a starting point or configuration. A maximal configuration is called a trace. An event e may have an immediate successor e0 according to the order →∗ , written e → e0 , where → denotes immediate causality iff there is no possible intermediate event. Fig. 1 shows a visual depiction of a simple event structure. Here, event e0 marks the initial event, and events e1 #e8 are in conflict. Ac- cording to conflict propagation, events e1 #e9 are also in conflict. Immediate causality is shown, and any events not related by causality or conflict are con- current. For instance, e2 co e6 are concurrent. Two configurations are shown surrounding some of the events: in red to the left (X1 ), and in green to the right (X2 ). X1 contains concurrency, whereas X2 does not. Moreover, X1 =↓e7 and X2 =↓e10 . 1 We will often write just Isabelle in lieu of Isabelle/HOL. Fig. 1. Example event structure. To make a connection between the semantic model (an event structure) and the syntactic model (ignored here) it is describing, we need to associate additional information to individual events. Let L be a given set of labels. Definition 2. A labelled event structure over L is a triple M = (Ev, µ, ν) where µ and ν are partial labelling functions µ : Ev → 2L and ν : Ev → N × N. Labelled event structures are event structures enriched with two labelling functions µ and ν. The function µ maps events onto a subset of elements of L. The labels in the set L either denote formulas (constraints over integer variables, e.g., x > 9 or y = 5), logical propositions (e.g., pro1) or actions (e.g., ma1). If for an event e ∈ Ev, µ(e) contains an action α ∈ L, then e denotes an occurrence of that action α. If µ(e) contains a formula or logical proposition ϕ ∈ L, then ϕ must hold when e occurs. The labelling function ν associates to each event its priority and duration, for instance, ν(e) = (p, d) indicates that p is the priority and d is the duration associated with e. The higher the value of p, the higher the priority associated to the event. The duration d indicates the time units spent at event e. Sometimes, we will write ν1 or ν2 for the function returning only the first or second component of the pair returned by ν. Giving different priority values to events is meaningful in the presence of alternatives (conflicting events), where the highest value can be used to determine the ideal configuration in a model. For instance, event e2 may have a higher priority than e8 . Further labels may be added to the framework as partial functions if required. We call a labelled event structure a model in what follows. In addition, we define a map Γ specifying the level of conflict between event labels as follows. Definition 3. Label conflicts are given by a (possibly partial) function Γ : 2L → Z. When we are interested to the value of Γ in a restricted subset of L, we use the notation (l1 , l2 , v), indicating that l1 and l2 are in conflict with an interaction score of value v. We consider that the lower the value of v the higher the severity of the label conflict. This permits to add further expressiveness to our model: for example, two events may not be in conflict, but the possible choice for their labels could have a bad interaction score, which could lead to alternative solutions. For the event structure in Fig. 1, we assume that µ(e4 ) = ma2 and µ(e3 ) = mb2 , and a label conflict such that Γ ({ma2 , mb2 }) = −100. Fig. 2. Possible executions of X1 with and without label conflicts. The labels of some of the events (e3 and e4 in the example) are conflicting according to Γ . When obtaining the optimal trace execution within the event structure above we need to make sure label inconsistencies are detected and avoided. A trace execution that avoids a label conflict is given by an execution of the configuration X2 . However, this is too restrictive since the priority of e2 is higher than e8 , and X1 may hence lead to an overall better trace execution. The label conflicts are only a problem if the events occur simultaneously. In our earlier approach [7], events in a configuration would be linearised and hence the label conflict automatically avoided. The loss of parallelism would, however, be too significant, and instead we want to choose trace executions for configurations that avoid label conflicts but achieve the best possible measure of concurrency. Consider a few options for traces execution for X1 shown in Fig. 2. We show a timeline from left to right and event durations, where overlapping events denote simultaneous execution. As highlighted, trace1 (shorthand name for execution number 1 of the trace) is problematic since the simultaneous execution of e3 and e4 would contribute to a label conflict. Both trace2 and trace3 avoid label conflicts, but trace2 has a higher degree of concurrency as it takes less time to execute (more events are executed in parallel). Because the notion of how many events are executed in parallel seems more complicated to define formally, we take the execution time as a definition of degree of parallelism. While the two notions are intuitively strongly correlated, this does not mean that this measure will pick an execution having the highest number of parallel events at all instants. Let us focus on a given subset of events C (which could be, for example, the events in a trace), and introduce the idea of how to associate to different executions of C a number measuring how parallel they are. The lowest degree of parallelism will correspond to the number Σe∈C ν2 (e) + τ, given by the sum of all event durations (yielded by the function ν2 ) and an additional parameter τ representing idle time in between events. τ is a parameter to describe optional slack in the execution, and can be set to zero when not needed. The highest possible (loose) upper bound to the degree of parallelism will correspond to the maximal duration of an event in C. In our example, let C1 = {e2 , e3 } and C2 = {e4 , e5 , e6 }. The degree of concurrency for different executions of C1 would be in the range [2, 3 + τ ], where ν2 (e2 ) = 1 and ν2 (e3 ) = 2; and for C2 in [2, 4 + τ ] where ν2 (e4 ) = ν2 (e6 ) = 1 and ν2 (e5 ) = 2. In Fig. 2, executions trace1 and trace2 have the highest degree of concurrency. In the sequel, we will give a precise definition to this idea of degree of concurrency, allowing us to compute its exact value for any execution, picked from the range introduced above. 3 An SMT-oriented Formulation The efficiency of SMT solvers comes at a price: first, one has to find a formulation of their problem which must be in first-order logic, because SMT-LIB (the standardised input format for SMT solvers [3]) is a first-order language, although with some added interpreted relations (whence the letters M and T in SMT). Secondly, the SMT-LIB code one obtains after managing to do that is typically very little readable for a human, as we will see in this section. We will deal with the first problem in this section, and with the second in Section 4. We will use the natural index i to range over (1, . . . , n) where n is the number of models (event structures) we are considering for composition. Since we will need to impose conditions on all of them, in the sequel we will often implicitly quantify over i. We denote by Gi the set of ordered pairs representing the immediate causality relation →i ; that is, given events e0 , e1 in the i-th event structure: (e0 , e1 ) ∈ Gi ↔ e0 →i e1 . This is the standard way of representing relations (such as →i ) in set theory. Gi can also be viewed as the set of edges of a directed graph (given by the transitive reduction of the partial order →∗i ): this graph-theoretical view will sometimes be useful and gives us the relevant jargon, allowing us to refer to nodes instead of events, etc. We also denote with G := ∪i Gi the union of all the immediate causality relations and with Evi := dom Gi ∪ ran Gi the set of all the events of the i-th event structure (dom and ran take the domain and the range set, respectively, of any given relation). Finally, [ Ev := Evi i is the set of all the events. 3.1 Trace Selection Recall that a configuration Xi for Evi is a set of events of Evi which is downward closed and conflict-free: ∀e0 , e1 ∈ Evi . e0 ∈ Xi ∧ e1 ∈ Xi → ¬(e0 #e1 ) (1) ^ ∀e1 ∈ ran (Gi ) .e1 ∈ Xi → e0 ∈ Xi (2) −1 → e0 ∈(Gi ) {e1 } Here R→ represents the function mapping a set to its image set through a given relation R. We note that, since Gi represents a relation as a set of ordered pairs, G−1 i is the inverse relation. Further, recall that a configuration Xi is a trace exactly when it is maximal, that is, ∀Y ⊆ Evi satisfying (1)–(2) , Y ⊆ Xi . (3) Now, the quantification appearing in (3) is not directly expressible, because a quantification over relations is second-order logic, and any SMT-LIB theory is within first-order logic. The mathematical language used in (1), (2) and 3 allows us to convey ideas to the reader in a more compact and, hopefully, more understandable way than crude SMT-LIB code would. However, it also hides difficulties such the one just explained, arising from the gap between the expressiveness of first-order logic and that of standard mathematical notation. This problem can have several solutions: in [6] we used bit-vectors to represent sets and, in [7] we showed condition (3) to be equivalent to the following, first-order ones: ∀e1 ∈ Evi \Xi . ∃e0 ∈ Evi . ((e0 #e1 ∧ e0 ∈ Xi ) ∨ (4) ((e0 , e1 ) ∈ Gi ∧ e0 ∈ / Xi )) This allows us to formulate the problem of trace finding in SMT-LIB. 3.2 Concurrent Execution of Traces The next step is to define a measure of concurrency which will allow us to execute a given trace (or configuration) without violating the constraints given by the causality and conflict relations. Since any configuration is conflict-free, we only need to focus on not violating the causality relation when executing it. 1. Consider that every event in the configuration has a start time and an end time, with the latter not smaller than the former; 2. Any two ordered events should not overlap; 3. Any successor (according to →∗ ) of an event should happen after it. These conditions normally leave quite some freedom in the arrangement of the events for an execution as shown in Fig. 2 for a configuration X1 . A conceptually simple approach (commonly referred to as interleaving or sequentialising) is to find a linear order respecting →∗ : this means finding an order morphism from the configuration (seen as equipped with the partial order →∗ ) to Z (equipped with its standard linear, total order). This way of handling execution is particularly well-suited to an SMT solver due to its awareness of integer arithmetics, and is the one we adopted in [7]. This approach is usually contrasted, in the literature, with the true concurrent one, whereby the restriction given by this linearisation is dropped, with an additional number of possible execution arrangements becoming possible which still comply with the three conditions above. This amounts to permitting to take advantage of possible parallelism, which gets lost in the interleaving process: in the latter approach, compliance with conditions (1)-(3) is attained by ruling out overlaps between any pair of distinct events, thereby including concurrent events (recall that two events are concurrent if they are not related by →∗ nor by #). We now introduce an SMT way of – modelling this increased choice of possible executions for the traces selected in the previous subsection and – ranking them according to their efficiency, that is, their degree of concurrency. It will rely on two functions, s and t, defined on all the events, and returning the time each of them starts and ends, respectively. The first constraint we impose on them is that any single event must respect time: ∀e ∈ Evi .t (e) − s (e) = ν2 (e) . (5) Let us recall that we assume that our event structures are finite so that, in particular, we can define a function pi over the set of non-source nodes for the directed graph ran Gi returning, for each such node, its parent node in the considered trace Xi which terminates last: → pi (e1 ) ∈ Xi ∩ G−1 ( i ({e1 }) ∀e1 ∈ ran Gi . −1 → (6) ∀e0 ∈ Xi ∩ Gi ({e1 }) . t (pi (e1 )) ≥ t (e0 ) . We have only one requirement to impose on p: ∀e ∈ ran Gi . s (e) ≥ t (p (e)) . (7) This last requirement can be tightened to ∀e ∈ ran Gi . s (e) = t (p (e)) in case we are seeking for executions without idle times between subsequent events. The formulas introduced in this section capture the linearly interleaved (or sequentialised) executions we described above, but add more possible executions. Intuitively, the former are the least possible concurrent execution, and in this sense they are also the least efficient ones. To make this kind of comparison more precise, we introduce a measure to rank all the different possible executions. This will give a metric, or distance, between executions according to their degree of concurrency. Consider, for a given Gi , the event which terminates last in a given execution of the trace Xi , denoted zi ; it can be described by the formulas zi ∈ Xi ∩ (ran Gi \ dom Gi ) (8) ∀e ∈ Xi ∩ (ran Gi \ dom Gi ) . t (zi ) ≥ t (e) . (9) We will consider an execution of Xi less concurrent than another whenever t (zi ) is larger for the former than for the latter. In this sense, we can use, e.g., an optimising SMT solver [17] to find the most concurrent execution by simply asking it to minimise the quantity t (zi ). In particular, this definition of amount of concurrency can be reconciled with the intuition that sequentialised executions are the least concurrent ones: the number above will not be maximum for such executions, given a fixed Xi . This fact is also practically useful: since we know that a linearised execution has maximal duration, and since such duration is obviously bounded by the sum of all the event durations, we can pass this bound as an assertion to the SMT solver to reduce its search space when computing a generic execution. Finally, among the several possible traces captured by the assertions of Section 3.1, we want to select the best one (see the example in Section 2). To do this, we consider one generic trace Xi for each Gi , and describe which labels are active at a given time y, via the function l: [ l (y) = b (ρ (e)) (y ∈ [s (e) , t (e)[). S e∈ i Xi Here, ρ (e) describes the selected label for the event e (which is imposed to be in the set of allowed labels through an assertion we omit here), and b(j) sets the j-th bit in a bit-vector of length equal to the overall number of all labels. Therefore, l(y) is a bit-vector whose 1-bits correspond exactly to the labels active at time y, because the term in the rightmost pair of brackets filters exactly the active events (note that our convention is that the when the ending time t (e) of an event ticks, we consider the event instantly off, so that the range in that term is right-open). We finally ask the SMT solver to maximise maxi {t(zi )} X Γ (l (t)) , t=0 where Γ is a function returning the interaction between the labels denoted by l (t). 4 Verification We have seen in Section 3.1 how the gap in expressiveness between standard mathematical notation and the first-order language of SMT solvers can cause difficulties when translating a mathematical problem for its computation in an SMT setting. In some cases, reformulations are needed (recall how we passed from (1) and (2) to (4) earlier). Even when the translation is more straightforward, several choices affect the final SMT code passed to the solver. One common choice is to instantiate universal quantifiers appearing in formulas exploiting the fact that they quantify over finite domains which are easy to compute separately, because this can considerably help the solver. For example, (9) features a universal quantifier ranging over a subset of the sinks of Gi , which is easily computed, for non-trivial graphs, as the set-theoretical difference between the set all children of some node of Gi and the set of all parents of some node of Gi . Performing this computation before invoking the SMT solver helps by removing a universal quantifier and by carefully restricting the possible cases over which it is instantiated; this kind of pre-processing is done often to obtain better performing SMT problems, but comes with a significant drawback: the SMT code thus obtained becomes exceedingly verbose, and, typically, difficult to peruse. In other words, the final SMT code usually looks extremely different (and extremely longer) than the original pen-and-paper mathematical formulation of the problem; in our case, we can compare the concise mathematical formulation in Section 3 with the final SMT code we effectively run for a simple example, a small (necessarily truncated) excerpt of which is in Listing 1.1, representing (6) and (7). Listing 1.1. SMT macro for (6) and (7), in the case of a small example (excerpt) ( define−fun trueConcurrencySMT ( ) Bool ( let ( ( $x206 ( and true (=> ( isSelected g0 ) (>= ( endTime ( lastParent g1 ) ) ( endTime g0 ) ) ) ) ) ) ( let ( ( $x212 ( and ( or false ( and ( isSelected g0 ) (= ( lastParent g1 ) g0 ) ) ) $x206 (= ( idleTime g1 ) (− ( startTime g1 ) ( endTime ( lastParent g1 ) ) ) ) (>= ( idleTime g1 ) 0 ) ) ) ) ( let ( ( $x165 ( isSelected g1 ) ) ) ( let ( ( $x195 ( and ( or false ( and $x165 (= ( lastParent g2 ) g1 ) ) ) ( and true (=> $x165 (>= ( endTime ( lastParent g2 ) ) ( endTime g1 ) ) ) ) (= ( idleTime g2 ) (− ( startTime g2 ) ( endTime ( lastParent g2 ) ) ) ) (>= ( idleTime g2 ) 0 ) ) ) ) ( let ( ( $x142 ( isSelected g2 ) ) ) ( let ( ( $x180 ( and ( or false ( and $x165 (= ( lastParent g3 ) g1 ) ) ) ( and true (=> $x165 (>= ( endTime ( lastParent g3 ) ) ( endTime g1 ) ) ) ) (= ( idleTime g3 ) (− ( startTime g3 ) ( endTime ( lastParent g3 ) ) ) ) (>= ( idleTime g3 ) 0 ) ) ) ) ( let ( ( $x146 ( isSelected g3 ) ) ) [ . . . ] The striking difference between them is clearly a problem when examining the SMT code and in particular when this code needs to have some degree of confidence in the result it produces. However, nobody prevents us from keeping two SMT codes: one (let us call it code A) closer to the mathematical formulation (and likely less efficient), and the other (code B) which underwent a series of transformations as hinted just above. If the SMT solver returns no models satisfying one code and not the other, then we can be confident about their equivalence, assuming correctness of the solver. But, more than that, code A is usually compact enough to be easily formulated within a theorem prover whose foundations entail the first-order logic (plus arithmetics) featured in an SMT solver, such as Isabelle/HOL [20]. And, if we manage to do that, we can use existing SMT code generators from within the theorem prover, which means that the definitions formulated in the theorem provers can be used both to prove their correctness and to generate code A. On top of that, we can arbitrarily introduce intermediate equivalent codes between A and B, if this eases the verification process. We now see a particular application of this general verification mechanism. In Isabelle/HOL, we can introduce the following function: abbreviation ” trueConcur01 ’ G X lastParent startTime endTime == ∀ child . ( X child & ( ∃ parent . G parent child ) ) → ( X ( lastParent child ) & ( G ( lastParent child ) child ) & ( ∀ parent . ( X parent & G parent child ) → endTime ( lastParent child ) ≥ endTime parent ) & startTime ( child ) ≥ endTime ( lastParent ( child ) ) ) ” It is carefully crafted to be equivalent, as the one in listing 1.1, to (6) and (7) and to only feature mathematical objects available in the first-order logic of an SMT solver; this means no sets, no higher-order functions, no lists, etc: everything is represented as functions and predicates (for example, instead of writing child ∈ X, we write X child, where X is a predicate, or boolean function). This allows us, on one hand, to export it to an SMT constant (let us call it trueConcurrencyIsabelle) taking advantage of the translator provided by Isabelle’s Sledgehammer tool [4], and to check its equivalence to trueConcurrencySMT inside an SMT solver (expecting the answer unsat): ( assert ( or ( and trueConcurrencySMT ( not trueConcurrencyIsabelle ) ) ( and ( not trueConcurrencySMT ) ( trueConcurrencyIsabelle ) ) ) ) On the other hand, the Isabelle definition can be proved correctness theorems about, thereby granting automatically that such correctness proofs carry over to trueConcurrencySMT. Let us focus on a basic property we expect from any execution, namely that expressed by requirements (2) and (3) of Section 3.2. The first step is usually to formulate the SMT-friendly Isabelle definition above into an equivalent one, but possibly more convenient when coming to formal proofs. This does not compromise the verification efforts because these new definitions can be provided with formal theorems proving their equivalence to the original ones. In this case, we will use abbreviation ” TrueConcur00 ’ P X lastParent startTime endTime == ∀ child ∈ X ∩ ( Range P ) . ( lastParent ( child ) ∈ X ∩ immediatePredecessors ’ P { child } & endTime ( lastParent ( child ) ) ≥ Max ( endTime ‘ ( X ∩ ( immediatePredecessors ’ P { child } ) ) ) & startTime ( child ) ge endTime ( lastParent ( child ) ) ) ” , all the relations have been expressed as sets of ordered pairs, the immediate causality relation G (corresponding to →) has been substituted by its transitive- reflexive closure P (corresponding to →∗ ), and the infix operator ‘ takes the image of a set through a function. We note that the custom-defined operator immediatePredecessors only makes sense for discrete relations; this is not a problem here, because we are in a finite setting. We omit the relevant equivalence proof, and only state the main correctness formal theorem: theorem fixes startTime : : ”_ => nat ” assumes ” wf ( strict P ) ” ” wf ( strict ( P ˆ −1))” ” atomicTimeArrow P startTime endTime ” ” isPo P” ” TrueConcur00 ’ P X lastParent startTime endTime ” shows ”{ e2 ∈ X ∩ events P . e2 | ( ∃ e0 ∈ X ∩ ( strict P )ˆ −1 ‘ ‘{ e2 } . startTime ( e2)