Schedulers and Finishers: On Generating the Behaviours of an Event Structure

Abstract

It is well known that every trace of a transition system can be generated using a scheduler. However, this basic completeness result does not hold in event structure models. The reason for this failure is that, according to its standard definition, a scheduler chooses which action to schedule and, at the same time, finishes the one scheduled last. Thus, scheduled events will never be able to overlap. We propose to separate scheduling from finishing and introduce the dual notion of finishers which, together with schedulers, are enough to regain completeness back. We then investigate all possible interactions between schedulers and finishers, concluding that simple alternating interactions are enough to express complex ones. Finally, we show how finishers can be used to filter behaviours to the extent to which they capture intrinsic system characteristics.

This research was supported by an iMQRES from Macquarie University, the ARC Discovery Grant DP1092464 and the EPSRC Grant EP/J003727/1.

Appendices

A   Proof of Proposition 1

Let ${\mathcal E}$ be an event structure and $\alpha {\in }{\mathcal T}$ be an event trace. We write $\overline{\alpha }$ for the set of events occurring in $\alpha$, which is a configuration of ${\mathcal E}$.

Lemma 1

Let $\alpha {\in }{\mathcal T}$ and $x{\in }{\mathcal C}$ such that $x{\subseteq }\overline{\alpha }$, then the restriction $\alpha |_{x}$ of $\alpha$ to events in x is an event trace.

Proof

Let $\alpha = e_1e_2\cdots e_n$, $x{\in }{\mathcal C}$ and write $\alpha |_{x} = e_{i_1}e_{i_2}\cdots e_{i_m}$. Let us show that $\alpha |_x$ is an event trace of ${\mathcal E}$. Let $e_{i_k}{\in } x$ and $z{\mapsto } e_{i_k}$ be a bundle of ${\mathcal E}$. Since $\alpha$ is an event trace, there exists an event $e_j$ such that $e_j{\in } z$ and $j<i_k$. Since x is a configuration and $e_{i_k}{\in } x$, there exists $e_{i_l}{\in } z$ and $l{<}k$. By definition, the bundle set z contains mutually conflicting events only and since $\overline{\alpha }$ is conflict free, $e_{i_l} = e_j$. That is, $z{\cap }\{e_{i_1},\dots , e_{i_{k-1}}\}\ne \emptyset$ for every bundle $z{\mapsto } e_{i_k}$. Hence, $\alpha |_{x}$ is an event trace (it is already conflict free). $\square$

Lemma 2

Let $x,y{\in }{\mathcal C}$ such that $x{\subseteq } y$. For every event trace $\alpha$ such that $\overline{\alpha } = x$, there exists an event trace $\alpha '$ satisfying $\overline{\alpha '} = y$ and $\alpha '|_{x} = \alpha$.

Proof

Let $\alpha ,\beta$ be event traces such that $\overline{\alpha }= x$, $\overline{\beta } = y$ and $x{\subseteq } y$. Let $\beta '$ be the concatenation of two sequences $\beta _1\beta _2$, where events in $\beta _1$ are exactly those of x ordered with ${\le }_\beta$ and $\beta _2$ is composed of events from $y{\setminus }x$ (set difference) ordered again with ${\le }_\beta$. We now show that the concatenation $\alpha ' = \alpha \beta _2$ is an event trace. That $\alpha '$ is conflict-free comes from the configuration y. To show the second property of an event trace, we need to show that every bundle pointing to an event $e_2$ in $\beta _2$ has to intersect $\overline{\alpha }{\cup }\overline{\beta }_2$ at an event occurring before $e_2$ with respect to the order $\le _\beta$. That is clear because $\beta$ is an event trace (notice that if $z{\mapsto } e_2$ holds, it is possible that the sole event in $z{\cap }\overline{\beta }$ belongs to $\overline{\alpha }$). Moreover, it is enough to show the property for events in $\beta _2$ only because $\alpha$ is already an event trace. Hence $\alpha '$ is an event trace and $\alpha '|_{x} = \alpha$.$\square$

With the help of these two lemmas, we now prove the envisaged characterisation of prefixing with configuration inclusion.

Proposition 8

If $x,y{\in }{\mathcal C}$ and $x{\subseteq } y$, then $(x,{\le }_x,\lambda _x)\trianglelefteq (y,{\le }_y,\lambda _y)$.

Proof

Let $x{\subseteq } y$. Let us first show that ${\le }_x = {\le }_y{\cap }(x{\times } x)$. Let $e,e'{\in } x$. We need to show that $e{{\le }_x}e'$ iff $e{{\le }_y}e'$. Assume $e{{\le }_x}e'$, then Lemma 1 implies that $e{{\le }_y} e'$ because every event trace for y restricts to an event trace for x. For the converse implication, let $e,e'{\in } x$ such that $e{{\le }_y}e'$. Lemma 2 implies that every event trace for x can be obtained as a restriction of some event trace for y. Hence, $e{{\le }_x} e'$. Therefore ${\le }_x = {\le }_y{\cap }(x{\times } x)$.

It remains to show that Property 1 holds. Let $e,e'{\in } y$, $e{{\le }_y} e'$ and $e'{\in } x$. It is enough to show that $e{\in } x$ because, once that is established, we use ${\le }_x = {\le }_y{\cap }(x{\times } x)$ to deduce that $e{\le _x} e'$. For a contradiction, assume that $e{\notin } x$. Then there exists an event trace $\beta ' = \beta _1\beta _2$ as specified in the proof of Lemma 2, that is, $\overline{\beta '} = y$, $\overline{\beta _1} = x$ and $e{\in }\overline{\beta _2}$. Thus, $e{{\not \le }_{\beta '}} e'$ which contradicts the fact that $e{\le }_ye'$. $\square$

B   Proof of Proposition 5

Proposition 9

For every $(u,v){\in }{\downarrow }{{\mathcal L}}^2$ such that $v\trianglelefteq u$, if $v\trianglelefteq \varphi (u)$ then $v_{m}^n\trianglelefteq \varphi (u_{m}^n)$ where $(u_{m}^n,v_{m}^n) = (\overline{\sigma }^m{\circ }\overline{\varphi })^n(u,v)$ and $m,n{\in }{\mathbb N}$.

Proof

Let m be a fixed natural number and let us reason by induction on n.

• For $n {=} 0$, we have $(u_m^0,v_m^0) {=} (\overline{\sigma }^m{\circ }\varphi )^0(u,v) {=} (u,v)$ and thus $v_m^0 {=} v \trianglelefteq \varphi (u) {=} u_m^0$.

• Let us assume $v_m^n\trianglelefteq \varphi (u_m^n)$. We have

  $$ (u_m^{n+1},v_m^{n+1})=(\overline{\sigma }^m{\circ }\overline{\varphi })^{n+1}(u,v)=(\overline{\sigma }^m{\circ }\overline{\varphi })(u_m^n,v_m^n)=\overline{\sigma }^m(u_m^n,\varphi (u_m^n))~. $$

  Since $\overline{\sigma }$ only operates on the first component of the state, we have $v_m^{n+1} = \varphi (u_m^n)$ and

  $$\begin{aligned} u_m^{n+1}=\underbrace{\sigma [\sigma [\dots \sigma [u_m^n{\leftarrow }v_m^n]\dots {\leftarrow }v_m^n]{\leftarrow }v_m^n]}_{m \text { times}}~. \end{aligned}$$

  (4)

  The induction hypothesis implies $v_m^n\trianglelefteq u_m^{n}$, thus Eq. 4 is well defined and implies $u_m^n\trianglelefteq u_m^{n+1}$. It follows from the monotonicity of $\varphi$ that $v_m^{n+1} = \varphi (u_m^n)\trianglelefteq \varphi (u_m^{n+1})$.$\square$

C   Proof of Proposition 7

Proposition 10

If $f{:}{\downarrow }{{\mathcal L}}{\rightharpoondown }{\downarrow }{{\mathcal L}}$ is a partial function defined on a increasing sequence of lposets $\emptyset =u_0\trianglelefteq u_1\trianglelefteq \cdots$ and satisfies the two properties of a finisher, i.e. $u\trianglelefteq f(u)$ for all u and f is monotonic, then there exists a finisher $\varphi$ (i.e. totally defined) such that $\varphi (u_i) = f(u_i)$ for every i.

Proof

Let ${\mathcal E}$ be an event structure and f be a function satisfying the hypothesis of the proposition. We construct $\varphi$ as follows

$$\begin{aligned} \varphi (u) = {\left\{ \begin{array}{ll} f(u_i) &{} \text {if there is a maximal } i \text { such that } u_i\trianglelefteq u\\ u &{} \text {if } u_i\trianglelefteq u\text { for every } i\\ \emptyset &{} \text {otherwise} \end{array}\right. } \end{aligned}$$

Firstly, we show the prefixing property of finishers. Let $u{\in }{\downarrow }{{\mathcal L}}$:

• If there exists a maximal i such that $u_i\trianglelefteq u$ then $\varphi (u) = f(u_i)\trianglelefteq u_i\trianglelefteq u$.

• If $u_i\trianglelefteq u$ for all i, then $\varphi (u) = u\trianglelefteq u$.

• Otherwise, $\varphi (u) = \emptyset \trianglelefteq u$.

Secondly, we show that $\varphi$ is monotonic. Let $u\trianglelefteq v$.

• If there exists a maximal i such that $u_i\trianglelefteq u$, then $\varphi (u) = f(u_i)$. There are three cases based on the value of $\varphi (v)$.

  • – There exists a maximal j such that $u_j\trianglelefteq v$ and $\varphi (v)=f(u_j)$. Since $u\trianglelefteq v$, maximality of j implies that $u_i\trianglelefteq u_j$ and hence $\varphi (u)=f(u_i)\trianglelefteq f(u_j)=\varphi (v)$, by monotonicity of f.

  • – For all j, $u_j\trianglelefteq v$ and therefore $\varphi (u) = f(u_i)\trianglelefteq u_i\trianglelefteq v = \varphi (v)$.

  • – The case $\varphi (v) = \emptyset$ cannot happen, unless $f(u_i) = \emptyset$ because $u_i\trianglelefteq v$ for every i.

• If $u_i\trianglelefteq u$ for all i, then $u_i\trianglelefteq v$ for all i because $u\trianglelefteq v$. Hence $\varphi (u) = u\trianglelefteq v = \varphi (v)$.

• Otherwise, $\varphi (u) = \emptyset \trianglelefteq \varphi (v)$, whatever $\varphi (v)$ is.$\square$

D   Proof of Theorem 2

Theorem 3

For every scheduler $\sigma$ and finisher $\varphi$, there exists a (countable) family of finishers $\varphi _0,\varphi _1,\dots$ such that the full resolution $(\sigma {*}\varphi )^*$ is the union of the family of resolutions $(\sigma \varphi _0)^*,(\sigma \varphi _1)^*,\dots$.

Proof

Let $\sigma$ and $\varphi$ be some scheduler and finisher on the event structure ${\mathcal E}$. The full resolution $(\sigma {*}\varphi )^*$ is depicted in Fig. 4.

Given a path $\pi$ in the directed acyclic graph of Fig. 4, we generate a partial function $f_{\pi }$ such that $f(u) = v$ iff $(u,v){\in }\pi$. Therefore, $f_\pi$ satisfies the first property of a finisher because each node of the tree is a state of ${\mathcal E}$ and it is monotonic because if $(u_i,v_i),(u_j,v_j){\in }\pi$ such that $u_i\trianglelefteq u_j$, then there exist two indices $k_i,k_j$ such that $f(u_i) = \varphi (u_{k_i})$ and $f(u_j) = \varphi (u_{k_j})$ and $u_{k_i}\trianglelefteq u_{k_j}$. Hence $f(u_i)\trianglelefteq f(u_j)$ and it extends to a finisher $\varphi _\pi$ by Proposition 7. Since the directed acyclic graph can be recovered from the union of all paths, we deduce that

$$(\sigma {*}\varphi )^* = \cup _{\pi }(\sigma \varphi _\pi )^*$$

where $\pi$ ranges over all paths in $(\sigma {*}\varphi )^*$ (which is of course countable).$\square$

Fig. 4.

Full resolution where unlabelled arrows are added for unchanging states.