Reward Testing Equivalences for Processes

TL;DR

This paper introduces reward testing to process semantics, providing a finer equivalence that captures conditional liveness properties beyond traditional safety and liveness properties.

Contribution

It proposes reward testing as a new semantic equivalence that refines existing testing equivalences and captures conditional liveness properties.

Findings

Reward testing is strictly finer than may- and must-testing equivalences.

Reward testing captures conditional liveness properties.

It extends the semantic framework for process equivalences.

Abstract

May and must testing were introduced by De Nicola and Hennessy to define semantic equivalences on processes. May-testing equivalence exactly captures safety properties, and must-testing equivalence liveness properties. This paper proposes reward testing and shows that the resulting semantic equivalence also captures conditional liveness properties. It is strictly finer than both the may- and must-testing equivalence.

Equations

$$P{⊑}_{\mathrm{may}}Q\text{mbox}iff\forall T\in \text{mathbbm}T\forall \text{Pass}\in \text{mbox}{P}^{\uparrow }(\text{mathbbm}O)(P\text{may}\text{Pass}T\Rightarrow Q\text{may}\text{Pass}T)$$

$$P{⊑}_{\mathrm{must}}Q\text{mbox}iff\forall T\in \text{mathbbm}T\forall \text{Pass}\in \text{mbox}{P}^{\uparrow }(\text{mathbbm}O)(P\text{must}\text{Pass}T\Rightarrow Q\text{must}\text{Pass}T)$$

$$\mathcal{A}\it pply(T,P):=\{\bot\mid\exists\mbox{ catastrophic $\pi\in\textit{Comp}(T,P)$}\}\cup\{\top\mid\exists\mbox{ uncatastrophic $\pi\in\textit{Comp}(T,P)$}\}.\vspace{-1pt}$$

$$C_{\_}1:=\tau C_{\_}2:=\tau .c+\tau C_{\_}3:=\tau .c$$

$$\underset{\_}{\inf }n\to \infty \sum _{\_}{i=1}^n{r}_{\_}i\in \text{mathbbm}R\cup \{-\infty ,\infty \}.$$

Full text

Introduction

The idea behind semantic equivalences $\equiv$ and refinement preorders $\sqsubseteq$ on processes is that $P\equiv Q$ says, essentially, that for practical purposes processes $P$ and $Q$ are equally suitable, i.e. one can be replaced for by the other without untoward side effects. Likewise, $P\sqsubseteq Q$ says that for all practical purposes under consideration, $Q$ is at least as suitable as $P$, i.e. it will never harm to replace $P$ by $Q$. To this end, $Q$ must have all relevant good properties that $P$ enjoys. Among the properties that ought to be so preserved, are safety properties, saying that nothing bad will even happen, and liveness properties, saying that something good will happen eventually.

In the setting of the process algebra CCS, refinement preorders $\sqsubseteq_{\rm{may}}$ and $\sqsubseteq_{\rm{must}}$, and associated semantic equivalences $\equiv_{\rm{may}}$ and $\equiv_{\rm{must}}$, were proposed by De Nicola & Hennessy in [DH84]. In [vG10] I argue that $\equiv_{\rm{may}}$ and $\equiv_{\rm{must}}$ are the coarsest equivalences that enjoy some basic compositionality requirements111Namely being congruences for injective renaming and partially synchronous interleaving operators, or equivalently all operators of CSP, or equivalently the CCS operators parallel composition, restriction and relabelling. and preserve safety and liveness properties, respectively. Yet neither preserves so-called conditional liveness properties.

This is illustrated in Figure 1, showing two processes that are identified under both may and must testing. From a practical point of view, the difference between these two processes may be enormous. It could be that the action $c$ comes with a huge cost, that is only worth making when the good action $g$ happens afterwards. Only the right-hand side process is able to incur the cost without any benefits, and for this reason it lacks an important property that the left-hand process has. I call such properties conditional liveness properties. A conditional liveness property says that

under certain conditions something good will eventually happen.

This paper introduces a stronger form of testing that preserves conditional liveness properties.

1 General setting

It is natural to view the semantics of processes as being determined by their ability to pass tests [DH84, henn]; processes $P_{\_}1$ and $P_{\_}2$ are deemed to be semantically equivalent unless there is a test which can distinguish them. The actual tests used typically represent the ways in which users, or indeed other processes, can interact with $P_{\_}i$. This idea can be formulated in the following general testing scenario [DGHMZ07], of which the testing scenarios of [DH84, henn] are instances. It assumes

• •

a set of processes $\mathbbm{P}$,

• •

a set of tests $\mathbbm{T}$, which can be applied to processes,

• •

a set of outcomes $\mathbbm{O}$, the possible results from applying a test to a process, and

• •

a function $\mathcal{A}\it pply:\mathbbm{T}\times\mathbbm{P}\rightarrow\Pow^{+}(\mathbbm{O})$, representing the possible results of applying a specific test to a specific process.

Here $\Pow^{+}(\mathbbm{O})$ denotes the collection of non-empty subsets of $\mathbbm{O}$; so the result of applying a test $T$ to a process $P$, $\mathcal{A}\it pply(T,P)$, is in general a set of outcomes, representing the fact that the behaviour of processes, and indeed tests, may be nondeterministic.

Moreover, some outcomes are considered better then others; for example the application of a test may simply succeed, or it may fail, with success being better than failure. So one can assume that $\mathbbm{O}$ is endowed with a partial order, in which $o_{\_}1\leq o_{\_}2$ means that $o_{\_}2$ is a better outcome than $o_{\_}1$.

When comparing the result of applying tests to processes one needs to compare subsets of $\mathbbm{O}$. There are two standard approaches to make this comparison, based on viewing these sets as elements of either the Hoare or Smyth powerdomain [Hen82, AJ94] of $\mathbbm{O}$. For $O_{\_}1,O_{\_}2\in\Pow^{+}(\mathbbm{O})$ let

1. (i)

$O_{\_}1\sqsubseteq_{\rm Ho}O_{\_}2$ if for every $o_{\_}1\in O_{\_}1$ there exists some $o_{\_}2\in O_{\_}2$ such that $o_{\_}1\leq o_{\_}2$ 2. (ii)

$O_{\_}1\sqsubseteq_{\rm Sm}O_{\_}2$ if for every $o_{\_}2\in O_{\_}2$ there exists some $o_{\_}1\in O_{\_}1$ such that $o_{\_}1\leq o_{\_}2$.

Using these two comparison methods one obtains two different semantic preorders for processes:

1. (i)

For $P,Q\in\mathbbm{P}$ let $P\mathbin{\sqsubseteq_{\rm{may}}}Q$ if $\mathcal{A}\it pply(T,P)\mathbin{\sqsubseteq_{\rm Ho}}\mathcal{A}\it pply(T,Q)$ for every test $T$ 2. (ii)

Similarly, let $P\sqsubseteq_{\rm{must}}Q$ if $\mathcal{A}\it pply(T,P)\sqsubseteq_{\rm Sm}\mathcal{A}\it pply(T,Q)$ for every test $T$.

Note that $\sqsubseteq_{\rm{may}}$ and $\sqsubseteq_{\rm{must}}$ are reflexive and transitive, and hence preorders. I use $P\equiv_{\rm{may}}Q$ and $P\equiv_{\rm{must}}Q$ to denote the associated equivalences.

The terminology may and must refers to the following reformulation of the same idea. Let ${\it Pass}\subseteq\mathbbm{O}$ be an upwards-closed subset of $\mathbbm{O}$, i.e. satisfying $o^{\prime}\geq o\in{\it Pass}\Rightarrow o^{\prime}\in{\it Pass}$, thought of as the set of outcomes that can be regarded as passing a test. Then one says that a process $P$ may pass a test $T$ with an outcome in Pass, notation “$P$ may ${\it Pass}~{}T$”, if there is an outcome $o\in\mathcal{A}\it pply(P,T)$ with $o\in\textit{Pass}$, and likewise $P$ must pass a test $T$ with an outcome in Pass, notation “$P$ must ${\it Pass}~{}T$”, if for all $o\in\mathcal{A}\it pply(P,T)$ one has $o\in\textit{Pass}$. Now

[TABLE]

where $\mbox{P}^{\uparrow}\kern-1.00006pt(\mathbbm{O})$ is the set of upwards-closed subsets of $\mathbbm{O}$.

The original theory of testing [DH84, henn] is obtained by using as the set of outcomes $\mathbbm{O}$ the two-point lattice

\bot$$\top

with $\top$ representing the success of a test application, and $\bot$ failure.

2 CCS: The Calculus of Communicating Systems

CCS [ccs] is parametrised with a set $\Ch$ of names; $Act:=\Ch\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\bar{\Ch}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\{\tau\}$ is the set of actions, where $\tau$ is a special internal action and $\bar{\Ch}:=\{\bar{c}\mid c\in\Ch\}$ is the set of co-names. Complementation is extended to $\bar{\Ch}$ by setting \bar{\bar{\mbox{c}}}=c. Below, $a$ ranges over $\A:=\Ch\cup\bar{\Ch}$ and $\alpha$ over $Act$. A relabelling is a function $f\!:\Ch\mathbin{\rightarrow}\Ch$; it extends to $Act$ by $f(\bar{c})\mathbin{=}\overline{f(c)}$ and $f(\tau):=\tau$. Let $\V$ be a set $X$, $Y$, …of process variables. The set $\mathbbm{E}_{\_}{\rm CCS}$ of CCS expressions is the smallest set including:

[TABLE]

The expression $\sum_{\_}{i\in\{1,2\}}\!\alpha_{\_}i.E_{\_}i$ is often written as $\alpha_{\_}1.E_{\_}1{+}\alpha_{\_}2.E_{\_}2$, $\sum_{\_}{i\in\{1\}}\!\alpha_{\_}i.E_{\_}i$ as $\alpha_{\_}1.E_{\_}1$, and $\sum_{\_}{i\in\emptyset}\!\alpha_{\_}i.E_{\_}i$ as ${\bf 0}$. Moreover, one abbreviates $\alpha.{\bf 0}$ by $\alpha$, and $P\backslash\{c\}$ by $P\backslash c$. A partial function $S\!:\V\mathbin{\rightharpoonup}\mathbbm{E}_{\_}{\rm CCS}$ is called a recursive specification, and traditionally written as $\{Y\stackrel{{\scriptstyle{\it def}}}{{=}}S(Y)\mid Y\mathbin{\in}{\it dom}(S)\}$. A CCS expression $E$ is closed if each occurrence of a process variable $Y$ in $E$ lays within a subexpression ${\bf fix}\llparenthesis X{:}S\rrparenthesis$ of $E$ with $Y\mathbin{\in}{\it dom}(S)$; $\mathbbm{P}_{\_}{\rm CCS}$, ranged over by $P,Q,\dots$, denotes the set of closed CCS expressions, or processes.

The semantics of CCS is given by the labelled transition relation $\mathord{\rightarrow}\subseteq\mathbbm{P}_{\_}{\rm CCS}\times Act\times\mathbbm{P}_{\_}{\rm CCS}$, where transitions P\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha$\hskip 2.5pt}\hfil}}}}}Q are derived from the rules of Table 1. Here ${\bf fix}\llparenthesis S_{\_}X{:}S\rrparenthesis$ denotes the expression $S(X)$ (written $S_{\_}X$) with ${\bf fix}\llparenthesis Y{:}S\rrparenthesis$ substituted for each free occurrence of $Y\!$, for all $Y\in{\it dom}(S)$, while renaming bound variables in $S_{\_}X$ as necessary to avoid name-clashes.

The process $\alpha.P$ performs the action $\alpha$ first and subsequently acts as $P$. The choice operator $\sum_{\_}{i\in I}P_{\_}i$ may act as any of its arguments $P_{\_}i$, depending on which of these processes is able to act at all. The parallel composition $P|Q$ executes an action from $P$, an action from $Q$, or in the case where $P$ and $Q$ can perform complementary actions $a$ and $\bar{a}$, the process can perform a synchronisation, resulting in an internal action $\tau$. The restriction operator $P\backslash L$ inhibits execution of the actions from $L$ and their complements. The relabelling $P[f]$ acts like process $P$ with all labels $\alpha$ replaced by $f(\alpha)$. Finally, the rule for recursion says that a recursively defined process ${\bf fix}\llparenthesis X{:}S\rrparenthesis$ behaves exactly as the body $S_{\_}X$ of the recursive equation $X\stackrel{{\scriptstyle{\it def}}}{{=}}S_{\_}X$, but with recursive calls ${\bf fix}\llparenthesis Y{:}S\rrparenthesis$ substituted for the variables $Y\in{\it dom}(S)$.

3 Classical may and must testing for CCS

Let $Act^{\omega}:=Act\cup\{\omega\}$, where $\omega\notin Act$ is a special action reporting success. A CCS test $T\in\mathbbm{T}_{\_}{\rm CCS}$ is defined just like a CCS process, but with $\alpha$ ranging over $Act^{\omega}$. So a CCS process is a special kind of CCS test, namely one that never performs the action $\omega$. To apply the test $T$ to the process $P$ one runs them in parallel; that is, one runs the combined process $T|P$—which is itself a CCS test.

Definition 3.1**.**

computation A computation $\pi$ is a finite or infinite sequence $T_{\_}0,T_{\_}1,T_{\_}2,\dots$ of tests, such that (i) if $T_{\_}n$ is the final element in the sequence, then $T_{\_}n\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}T$ for no $T$, and (ii) otherwise $T_{\_}n\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}T_{\_}{n+1}$.

A computation $\pi$ is successful if it contains a state $T$ with $T\stackrel{{\scriptstyle\omega}}{{\longrightarrow}}T^{\prime}$ for some $T^{\prime}$.

For $T\in\mathbbm{T}_{\_}{\rm CCS}$, $P\in\mathbbm{P}_{\_}{\rm CCS}$, let $\textit{Comp}(T,P)$ be the set of computations whose initial element is $T|P$.

Let \mathcal{A}\it pply(T,P):=\{\top\mid\exists\mbox{ successful \pi\in\textit{Comp}(T,P)}\}\cup\{\bot\mid\exists\mbox{ unsuccessful \pi\in\textit{Comp}(T,P)}\}.

Using this definition of $\mathcal{A}\it pply$ it follows that $P\sqsubseteq_{\rm{may}}Q$ holds unless there is a test $T$ such that $T|P$ has (that is, is the initial state of) a successful computation but $Q$ has not. Likewise $P\sqsubseteq_{\rm{must}}Q$ holds unless there is a test $T$ such that $T|P$ has only successful computations but $Q$ has not.

4 Dual may and must testing

A liveness property [Lam77] is a property that says that something good will eventually happen. In the context of CCS, any test $T$ can be regarded to specify a liveness property; a process $P$ is defined to have this property iff all computations of $T|P$ are successful. Now $P\sqsubseteq_{\rm{must}}Q$ holds iff all liveness properties $T\in\mathbbm{T}_{\_}{\rm CCS}$ that are enjoyed by $P$ also hold for $Q$.

A safety property [Lam77] is a property that says that something bad will never happen. When thinking of the special action $\omega$ as reporting that something bad has occurred, rather than something good, any test $T$ can also be regarded to specify a safety property; a process $P$ is defined to have this property iff none of the computations of $T|P$ are catastrophic; here catastrophic is simply another word for “successful”, when reversing the connotation of $\omega$. Now $Q\sqsubseteq_{\rm{may}}P$ holds iff all safety properties $T\in\mathbbm{T}_{\_}{\rm CCS}$ that are enjoyed by $P$ also hold for $Q$.

A labelled transition system (LTS) over a set $Act$ is a pair $(\mathbbm{P},\rightarrow)$ where $\mathbbm{P}$ is a set of processes or states and ${\rightarrow}\subseteq\mathbbm{P}\times Act\times\mathbbm{P}$ a set of transitions. In [vG10] preorders $\sqsubseteq_{\_}{\it liveness}$ and $\sqsubseteq_{\_}{\it safety}$ are defined on LTSs. Specialised to the LTS $(\mathbbm{P}_{\_}{\rm CCS},\rightarrow)$ induced by CCS, $\sqsubseteq_{\_}{\it liveness}$ coincides with $\sqsubseteq_{\rm{must}}$, and $\sqsubseteq_{\_}{\it safety}$ is exactly the reverse of $\sqsubseteq_{\rm{may}}$, in accordance with the reasoning above.

To explain the reversal of $\sqsubseteq_{\rm{may}}$ when dealing with safety properties, I propose a variant of CCS testing where in Definition LABEL:df:computation the word “catastrophic” is used for “successful” and $\mathcal{A}\it pply$ is redefined by

[TABLE]

An equivalent alternative to redefining $\mathcal{A}\it pply$ is to simply invert the order between $\bot$ and $\top$. Let $\sqsubseteq_{\rm{may}}^{\rm dual}$ and $\sqsubseteq_{\rm{must}}^{\rm dual}$ be the versions of the may- and must-testing preorders obtained from this alternative definition. It follows immediately from the definitions that $P\sqsubseteq_{\rm{may}}^{\rm dual}Q$ iff $Q\sqsubseteq_{\rm{must}}P$ and that $P\sqsubseteq_{\rm{must}}^{\rm dual}Q$ iff $Q\sqsubseteq_{\rm{may}}P$. Based on this, it may be more accurate to say that $\sqsubseteq_{\_}{\it safety}$ coincides with $\sqsubseteq_{\rm{must}}^{\rm dual}$.

A possibility property [Lam98] is a property that says that something good might eventually happen. A test $T$ can be regarded to specify a possibility property; a process $P$ is defined to have this property iff some computation of $T|P$ is successful. Now $P\sqsubseteq_{\rm{may}}Q$ holds iff all possibility properties $T\in\mathbbm{T}_{\_}{\rm CCS}$ that are enjoyed by $P$ also hold for $Q$. Lamport argues that “verifying possibility properties tells you nothing interesting about a system” [Lam98]. As an example, consider the following models of coffee machines:

[TABLE]

where $c$ is the act of dispensing coffee. The machine $C_{\_}1$ surely will not make coffee, $C_{\_}2$ makes a nondeterministic choice between making coffee or not, and $C_{\_}3$ surely makes coffee. Under may testing, systems $C2$ and $C_{\_}3$ are equivalent—both have the possibility of making coffee—and each of them is better than $C_{\_}1$: $C_{\_}1\sqsubset_{\_}{\rm may}C_{\_}2\equiv_{\rm{may}}C_{\_}3$. The relevance of this indeed is questionable. It takes must testing to formalise that $C_{\_}3$ is better than $C_{\_}2$: only $C_{\_}3$ guarantees that coffee will eventually be dispensed.

When employing dual testing, the same example applies, but with $c$ denoting a catastrophe. Now $C_{\_}1$ is safe, whereas $C_{\_}2$ and $C_{\_}3$ are not: $C_{\_}1\sqsupset^{\rm dual}_{\_}{\rm must}C_{\_}2\equiv^{\rm dual}_{\_}{\rm must}C_{\_}3$. Dual may testing would argue that $C_{\_}2$ is better than $C_{\_}3$ because a catastrophe might be avoided. This however, can be deemed a weak argument.

In view of these considerations, I will focus on the preorders $\sqsubseteq_{\rm{must}}$ and $\sqsubseteq_{\rm{must}}^{\rm dual}$ (or $\sqsubseteq_{\_}{\it safety}$). The (dual) may preorders simply arise as their inverses, and hence do not require explicit treatment.

5 Reward testing for CCS

A CCS reward test is defined just like a CCS process, but with $\alpha$ ranging over $Act\times\mathbbm{R}$, the valued actions. A valued action is an action tagged with a real number, the reward for executing this action. A negative reward can be seen as a penalty. Let $\mathbbm{T}^{R}_{\_}{\rm CCS}$ be the set of CCS reward tests. The structural operational semantics for CCS reward tests has the following modified rules:

\begin{array}[]{c@{\qquad}c@{\qquad}c}\displaystyle\frac{P\mathrel{\mathrel{\hbox{\mathop{\hbox to15.66374pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a,r$\hskip 2.5pt}}}}}P^{\prime},~{}Q\mathrel{\mathrel{\hbox{\mathop{\hbox to18.06363pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\bar{a},r^{\prime}$\hskip 2.5pt}}}}}Q^{\prime}}{P|Q\mathrel{\mathrel{\hbox{\mathop{\hbox to28.80948pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\tau,r+r^{\prime}$\hskip 2.5pt}}}}}P^{\prime}|Q^{\prime}}\hypertarget{lab:Comm'}{\ \mbox{{\scriptsize\sc(Comm{}^{\prime})}}}&\displaystyle\frac{P\mathrel{\mathrel{\hbox{\mathop{\hbox to16.44153pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha,r$\hskip 2.5pt}}}}}P^{\prime}}{P\backslash L\mathrel{\mathrel{\hbox{\mathop{\hbox to16.44153pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha,r$\hskip 2.5pt}}}}}P^{\prime}\backslash L}~{}~{}(\alpha,\bar{\alpha}\not\in L)\hypertarget{lab:Res'}{\ \mbox{{\scriptsize\sc(Res{}^{\prime})}}}&\displaystyle\frac{P\mathrel{\mathrel{\hbox{\mathop{\hbox to16.44153pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha,r$\hskip 2.5pt}}}}}P^{\prime}}{P[f]\mathrel{\mathrel{\hbox{\mathop{\hbox to26.06656pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle f(\alpha),r$\hskip 2.5pt}}}}}P^{\prime}[f]}\hypertarget{lab:Rel'}{\ \mbox{{\scriptsize\sc(Rel{}^{\prime})}}}\end{array}

Thus, in synchronising two actions one reaps the rewards of both. In all other rules of Table 1, $\alpha$ is simply replaced by $\alpha,r$, with $r\in\mathbbm{R}$. A valued action $\alpha,0$ is simply denoted $\alpha$, so that a CCS process can be seen as a special CCS reward test, namely one in which all rewards are [math]. To apply a reward test $T$ to a process $P$ one again runs them in parallel.

Definition 5.1**.**

reward computation A reward computation $\pi$ is a finite or infinite sequence $T_{\_}0,r_{\_}1,T_{\_}1,r_{\_}2,T_{\_}2\dots$ of reward tests, such that (i) if $T_{\_}n$ is the final element in $\pi$, then T_{\_}n\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\tau,r$\hskip 2.5pt}\hfil}}}}}T for no $r$ and $T$, and (ii) otherwise T_{\_}n\mathrel{\mathrel{\hbox{\mathop{\hbox to30.61424pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\tau,r_{\_}{n+1}$\hskip 2.5pt}}}}}T_{\_}{n+1}.

The reward of a finite computation $\pi$ ending in $T_{\_}n$ is $\sum_{\_}{i=1}^{n}r_{\_}i$. The reward of an infinite computation $T_{\_}0,r_{\_}1,T_{\_}1,r_{\_}2,T_{\_}2\dots$ is

[TABLE]

*For $T\in\mathbbm{T}^{R}_{\_}{\rm CCS}$, $P\in\mathbbm{P}_{\_}{\rm CCS}$, let $\textit{Comp}^{R}(T,P)$ be the set of reward computations with initial element $T|P$.

Let $\mathcal{A}\it pply(T,P):=\{\textit{reward}(\pi)\mid\pi\in\textit{Comp}^{R}(T,P)\}$.*

This defines reward preorders $\sqsubseteq^{\rm may}_{\_}{\rm reward}$ and $\sqsubseteq^{\rm must}_{\_}{\rm reward}$ on $\mathbbm{P}_{\_}{\rm CCS}$. It will turn out that $P\sqsubseteq^{\rm may}_{\_}{\rm reward}Q$ iff $Q\sqsubseteq^{\rm must}_{\_}{\rm reward}P$. As a consequence I will focus on $\sqsubseteq^{\rm must}_{\_}{\rm reward}$, and simply call it $\sqsubseteq_{\_}{\rm reward}$.

6 Characterising reward testing

Assuming a fixed LTS $(\mathbb{P},\rightarrow)$, labelled over a set $Act=\A\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\{\tau\}$, the ternary relation \mathord{\mathrel{\stackrel{{\scriptstyle\_\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}}\subseteq\mathbb{P}\times\A^{*}\times\mathbb{P} is the least relation satisfying

P\mathrel{\stackrel{{\scriptstyle\epsilon\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}P , \rule{0.0pt}{17.07164pt}\begin{array}[]{c}P\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}Q\\[0.43057pt] \hline\cr\rule{0.0pt}{11.62494pt}P\mathrel{\stackrel{{\scriptstyle\epsilon\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}Q\end{array} , \rule{0.0pt}{17.07164pt}\begin{array}[]{c}P\stackrel{{\scriptstyle a}}{{\longrightarrow}}Q,~{}a\not=\tau\\[0.43057pt] \hline\cr\rule{0.0pt}{11.62494pt}P\mathrel{\stackrel{{\scriptstyle a\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}Q\end{array} and \rule{0.0pt}{17.07164pt}\begin{array}[]{c}P\mathrel{\stackrel{{\scriptstyle\sigma\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}Q\mathrel{\stackrel{{\scriptstyle\rho\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}r\\[0.43057pt] \hline\cr\rule{0.0pt}{11.62494pt}P\mathrel{\stackrel{{\scriptstyle\sigma\rho\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}r\end{array}  .

For $\sigma\in\A^{*}$ and $\nu\in\A^{*}\cup\A^{\infty}$ write $\sigma\leq\nu$ for “$\sigma$ is a prefix of $\rho$”, i.e. “$\exists\rho\;.\sigma\rho=\nu$”.

Definition 6.1**.**

traces Let $P\in\mathbb{P}$.

• •

$a_{\_}1a_{\_}2a_{\_}3\cdots\in\A^{\infty}$* is an infinite trace of $P$ if there are $P_{\_}1,P_{\_}2,\ldots$ such that P\mathrel{\stackrel{{\scriptstyle a_{\_}1\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}P_{\_}1\mathrel{\stackrel{{\scriptstyle a_{\_}2\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}P_{\_}2\mathrel{\stackrel{{\scriptstyle a_{\_}3\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}\cdots.*

• •

${\it inf}(P)$* denotes the set of infinite traces of $P$.*

• •

$P$* diverges, notation $P{\Uparrow}$, if there are $P_{\_}i\in\mathbb{P}$ for all $i>0$ such that $P\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P_{\_}1\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P_{\_}2\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\cdots$.*

• •

{\it divergences}(P):=\{\sigma\in\A^{*}\mid\exists Q.\;P\mathrel{\stackrel{{\scriptstyle\sigma\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}Q{\Uparrow}\}* is the set of divergence traces of $P$.*

• •

${\it initials}(P):=\{\alpha\in\A\mid\exists Q.\;P\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q\}$**.

• •

{\it deadlocks}(P):=\{\sigma\in\A^{*}\mid\exists Q.\;P\mathrel{\stackrel{{\scriptstyle\sigma\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}Q\wedge{\it initials}(Q)=\emptyset\}* is the set of deadlock traces of $P$.*

• •

${\it CT}(P):={\it inf}(P)\cup{\it divergences}(P)\cup{\it deadlocks}(P)$* is the set of complete traces of $P$.*

• •

{\it ptraces}(P):=\{\sigma\in\A^{*}\mid\exists Q.\;P\mathrel{\stackrel{{\scriptstyle\sigma\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}Q\}* is the set of partial traces of $P$.*

• •

{\it failures}(P):=\{\langle\sigma,X\rangle\in\A^{*}\times\Pow(\A)\mid\exists Q.\;P\mathrel{\stackrel{{\scriptstyle\sigma\ }}{{\raisebox{0.0pt}[4.0pt][0.0pt]{\Longrightarrow}}}}Q\wedge{\it initials}(Q)\cap(X\cup\{\tau\})=\emptyset\}**.

• •

${\it failures\!}_{d}(P):={\it failures}(P)\cup\{\langle\sigma,X\rangle\mid\sigma\in{\it divergences}(P)\wedge X\subseteq\A\}$.

• •

${\it inf\!\!}_{d}(P):={\it inf}(P)\cup\{\nu\in\A^{\infty}\mid\forall\sigma{<}\nu\;\exists\rho\in{\it divergences}(P).\;\sigma\leq\rho<\nu\}$.

• •

${\it divergences\!}_{\bot}(P):=\{\sigma\rho\mid\sigma\in{\it divergences}(P)\wedge\rho\in\A^{*}\}$.

• •

${\it inf\!\!}_{\bot}(P):={\it inf}(P)\cup\{\sigma\nu\mid\sigma\in{\it divergences}(P)\wedge\nu\in\A^{\infty}\}$.

• •

${\it failures\!}_{\bot}(P):={\it failures}(P)\cup\{\langle\sigma\rho,X\rangle\mid\sigma\in{\it divergences}(P)\wedge\rho\in\A^{*}\wedge X\subseteq\A\}$.

Note that ${\it ptraces}(R)=\{\sigma\mid\langle\sigma,\emptyset\rangle\in{\it failures\!}_{d}(R)\}$ for any $R\in\mathbbm{P}$. (*)

A path of a process $P\in\mathbbm{P}$ is an alternating sequence $P_{\_}0\,\alpha_{\_}1\,P_{\_}1\,\alpha_{\_}2\,P_{\_}2\cdots$ of processes/states and actions, starting with a state and either being infinite or ending with a state, such that P_{\_}i\mathrel{\mathrel{\hbox{\mathop{\hbox to23.83395pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha_{\_}{i+1}$\hskip 2.5pt}}}}}P_{\_}{i+1} for all relevant $i$. Let $l(\pi):=\alpha_{\_}1\alpha_{\_}2\cdots$ be the sequence of actions in $\pi$, and $\ell(\pi)$ the same sequence after all $\tau$s are removed. Now $\sigma\in{\it inf}(P)\cup{\it divergences}(P)$ iff $P$ has an infinite path $\pi$ with $\ell(\pi)=\sigma$. Likewise, $\sigma\in{\it ptraces}(P)$ iff $P$ has a finite path $\pi$ with $\ell(\pi)=\sigma$. Finally, $\sigma\in{\it inf}(P)\cup{\it ptraces}(P)$ iff $P$ has an path $\pi$ with $\ell(\pi)=\sigma$.

Any transition P|Q\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha$\hskip 2.5pt}\hfil}}}}}R derives, through the rules of Table 1, from

• •

a transition P\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha$\hskip 2.5pt}\hfil}}}}}P^{\prime} and a state $Q$, where $R=P^{\prime}|Q$ ,

• •

two transitions P\mathrel{\mathrel{\hbox{\mathop{\hbox to15.20012pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle a_{\_}1$\hskip 2.5pt}}}}}P^{\prime} and Q\mathrel{\mathrel{\hbox{\mathop{\hbox to16.50002pt{\rightarrowfill}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\bar{a}_{\_}2$\hskip 2.5pt}}}}}Q^{\prime}, where $R=P^{\prime}|Q^{\prime}$ ,

• •

or from a state $P$ and a transition Q\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha$\hskip 2.5pt}\hfil}}}}}Q^{\prime}, where $R=P|Q^{\prime}$.

This transition/state, transition/transition or state/transition pair is called a decomposition of P|Q\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt$\scriptstyle\alpha$\hskip 2.5pt}\hfil}}}}}R; it need not be unique. Now a decomposition of a path $\pi$ of $P|Q$ into paths $\pi_{\_}1$ and $\pi_{\_}2$ of $P$ and $Q$, respectively, is obtained by decomposing each transition in the path, and concatenating all left-projections into a path of $P$ and all right-projections into a path of $Q$—notation $\pi\in\pi_{\_}1|\pi_{\_}2$ [GH15a]. Here it could be that $\pi$ is infinite, yet either $\pi_{\_}1$ or $\pi_{\_}2$ (but not both) are finite. Again, decomposition of paths need not be unique.

Theorem 6.2**.**

reward characterisation Let $P,Q\in\mathbbm{P}_{\_}{\rm CCS}$. Then P\sqsubseteq_{\_}{\rm reward}Q~{}~{}\Leftrightarrow~{}~{}\begin{array}[t]{@{}r@{~\supseteq~}l@{}}{\it divergences}(P)~{}\supseteq~{}&{\it divergences}(Q)\wedge\mbox{}\\ {\it inf}(P)~{}\supseteq~{}&{\it inf}(Q)\wedge\mbox{}\\ {\it failures\!}_{d}(P)~{}\supseteq~{}&{\it failures\!}_{d}(Q).\end{array}

Proof 6.3**.**

Let $\sqsubseteq_{\_}{\it NDFD}$ be the preorder defined by: $P\sqsubseteq_{\_}{\it NDFD}Q$ iff the right-hand side of

7 Weaker notions of reward testing

Finite-penalty reward testing doesn’t allow computations that incur infinitely many penalties. A test $T\in\mathbbm{T}^{R}_{\_}{\rm CCS}$ has finite penalties if each infinite path $T\alpha_{\_}1^{r_{\_}1}T_{\_}1\alpha_{\_}2^{r_{\_}2}T_{\_}2\cdots$ has only finitely many transitions $i$ with $r_{\_}i<0$. Let $P\sqsubseteq_{\_}{\rm\textrm{\scriptsize fp-reward}}Q$ iff $\mathcal{A}\it pply(T,P)\sqsubseteq_{\rm Sm}\mathcal{A}\it pply(T,Q)$ for every finite-penalty reward test $T\!$.

Theorem 7.1**.**

finite-penalty reward characterisation Let $P,Q\in\mathbbm{P}_{\_}{\rm CCS}$. Then P\sqsubseteq_{\_}{\textrm{\scriptsize fp-reward}}Q~{}~{}\Leftrightarrow~{}~{}\begin{array}[t]{@{}r@{~\supseteq~}l@{}}{\it divergences}(P)~{}\supseteq~{}&{\it divergences}(Q)\wedge\mbox{}\\ {\it inf\!\!}_{d}(P)~{}\supseteq~{}&{\it inf\!\!}_{d}(Q)\wedge\mbox{}\\ {\it failures\!}_{d}(P)~{}\supseteq~{}&{\it failures\!}_{d}(Q).\end{array}

Proof 7.2**.**

Let $\sqsubseteq_{\_}{\it FDI}^{d}$ be the preorder defined by: $P\sqsubseteq_{\_}{\it FDI}^{d}Q$ iff the right-hand side of

Single penalty reward testing doesn’t allow computations that incur multiple penalties. A test $T\in\mathbbm{T}^{R}_{\_}{\rm CCS}$ has the single penalty property if each path $T\alpha_{\_}1^{r_{\_}1}T_{\_}1\alpha_{\_}2^{r_{\_}2}T_{\_}2\cdots$ has at most one transition $i$ with $r_{\_}i<0$. Let $P\sqsubseteq_{\_}{\textrm{\scriptsize sp-reward}}Q$ iff $\mathcal{A}\it pply(T,P)\sqsubseteq_{\rm Sm}\mathcal{A}\it pply(T,Q)$ for every single penalty reward test $T\!$. Obviously, $\sqsubseteq_{\_}{\textrm{\scriptsize sp-reward}}$ coincides with $\sqsubseteq_{\_}{\textrm{\scriptsize fp-reward}}$. This follows because all test used in the proof of

Theorem 6**.**

finite-penalty reward characterisation have the single penalty property.

Analogously one might weaken reward testing and/or single penalty reward testing by requiring that in each computation only finitely many, or at most one, positive reward can be reaped. This does not constitute a real weakening, as the tests used in Theorems LABEL:thm:reward_characterisation and LABEL:thm:finite-penalty_reward_characterisation already allot at most a single positive reward per computation only.

Nonnegative reward testing* requires all rewards to be nonnegative. Let $P\sqsubseteq_{\_}{+\textrm{\scriptsize reward}}Q$ iff $\mathcal{A}\it pply(T,P)\linebreak[1]\sqsubseteq_{\rm Sm}\mathcal{A}\it pply(T,Q)$ for every nonnegative reward test $T\!$. Likewise $\sqsubseteq_{\_}{-\textrm{\scriptsize reward}}$ requires all rewards to be [math] or negative.*

Theorem 7.3**.**

nonnegative reward characterisation Let $P,Q\in\mathbbm{P}_{\_}{\rm CCS}$. Then P\sqsubseteq_{\_}{+\textrm{\scriptsize reward}}Q~{}~{}\Leftrightarrow~{}~{}\begin{array}[t]{@{}r@{~\supseteq~}l@{}}{\it divergences\!}_{\bot}(P)~{}\supseteq~{}&{\it divergences\!}_{\bot}(Q)\wedge\mbox{}\\ {\it inf\!\!}_{\bot}(P)~{}\supseteq~{}&{\it inf\!\!}_{\bot}(Q)\wedge\mbox{}\\ {\it failures\!}_{\bot}(P)~{}\supseteq~{}&{\it failures\!}_{\bot}(Q).\end{array}

Proof 7.4**.**

Let $\sqsubseteq_{\_}{\it FDI}^{\bot}$ be the preorder defined by: $P\sqsubseteq_{\_}{\it FDI}^{\bot}Q$ iff the right-hand side of

One might weaken nonnegative reward testing by requiring that in each computation only finitely many, or at most one, reward can be reaped. This does not constitute a real weakening, as the tests used in