1 Introduction↩︎

A process is able to execute a set of actions with a predefined manner, while a truly concurrent process executes this set of actions with a manner with the flavour of true concurrency.

The so-called truly concurrent process algebras [1] [2] bridge the true concurrency (such as Petri nets [3] [4] [5], event structures [6], etc), and the interleaving concurrency (such as CCS [7], CSP [8] [9], ACP [10], etc).

In this paper, we give truly concurrent processes testing semantics followed by Hennessy’s great work [11], which inherits the trinity of operational semantics, axiomatic semantics and denotational semantics.

2 Preliminaries↩︎

For self-satisfactory, in this section, we introduce the preliminaries on set in 2.1 and multiset in 2.2.

2.1 Set↩︎

2.2 Multiset↩︎

We assume that the partial order \(\leq\) can be divided into two kinds: execution order \(\leq^{e}\) and communication \(\leq^{c}\). In the same parallel branch, the partial orders usually execution orders and communication usually exists among different parallel branches. Of course, parallel branches can be nested. Then, we can get the following definitions naturally.

It is easy to see that \(\sim\) is an equivalence and can be used to abstract from the carriers.

Concurrency includes parallelism and communication, then, we can get the following definitions of Pomsetc compositions.

The following definitions and conclusions are coming from [12], we retype them.

The definition of N-shape2 in Definition 27 is based on the assumption that partial orders (causalities) among different parallel branches are all communications.

So, in the following chapters, assume that all pomsets are series-parallel and all pomsetcs are series-communication-parallel. With a little of abuse of notions, we use \(\mathsf{Pom}\), \(\mathsf{Pomc}\), \(\mathsf{SP}\) and \(\mathsf{SCP}\) without distinctions.

3 The Algebras↩︎

In Scott-Strachey approach [13] of denotational semantics, domains are the key concepts. In this chapter, we introduce the related concepts of \(\Sigma\)-domain, which are coming from algebraic semantics [14] [15] [11].

Firstly, we introduce \(\Sigma\)-algebra related concepts in 3.1, then we introduce equational classes in 3.2 and inequational classes in 3.3. Finally, we introduce continuous algebras in 3.4.

3.1 \(\Sigma\)-algebra↩︎

3.2 Equational Classes↩︎

By allowing the occurrences of variables \(x,x_1,x_2\cdots\in X\) in a signature \(\Sigma\), we can get of the extended signature denoted \(\Sigma(X)\). Similarly, the term algebra \(T_{\Sigma}(X)\) is extended from \(T_{\Sigma}\), the elements of \(T_{\Sigma}\) are called closed terms (we often refer them as processes), while the ones of \(T_{\Sigma}(X)\) are called open terms. An \(A\)-assignment for \(X\) is a mapping \(\sigma_A:X\rightarrow A\), while a substitution \(\sigma(X)\) is a \(T_{\Sigma}(X)\)-assignment by mapping each \(x\in X\) to a term in \(T_{\Sigma}(X)\). For each \(x_i\) in a variable sequence \(\underline{x}\), if \(\sigma(x_i)\) is a closed term in \(T_{\Sigma}\), then \(\sigma\) is called a closed substitution. We write \(t\sigma\) for \(\sigma(t)\) and \(t(\sigma\circ\sigma')=(t\sigma')\sigma\) with \(t\in T_{\Sigma}(X)\), which is called an instantiation of \(t\).

3.3 Inequational Classes↩︎

3.4 Continuous Algebras↩︎

Recursion is used to capture infinite computations. \(\Sigma\)-algebras whose carrier are partial orders enjoying certain continuity constraints are called \(\Sigma\)-domains, which are sufficient to ensure that the recursive equations always have least solutions taken as the meaning of the recursive definitions.

3.4.1 Continuity↩︎

Recursive equations will be interpreted semantically by least fixpoints.

The compact elements are the semantic denotations of finite processes, and if an interpretation is algebraic, every recursive defined processes is semantically the limit of a directed set of finite processes. Let \(\mathrm{Fin}(A)\) to denote the set of finite or compact elements of \(A\), and for \(a\in A\) \(\mathrm{Fin}(a)=\{d\in\mathrm{Fin}(A)|d\leq a\}\), then the algebraicness requires \(a=\mathord{\scalebox{1.3}{\bigvee}}_A \mathrm{Fin}(a)\). If \(A,A'\) are algebraic cpos with \(\langle\mathrm{Fin}(A),\leq_A\rangle\) and \(\langle \mathrm{Fin}(A'),\leq_{A'}\rangle\) being isomorphic as partial orders, then \(A,A'\) are isomorphic as cpos.

3.4.2 \(\Sigma\)-domains↩︎

Let \(\mathscr{CC}(E)\) denote the class of \(\Sigma\)-domains satisfying the equations \(E\).

When \(E=\emptyset\), \(CI_E\) can not give syntax for the continuous objects, as the \(\Sigma\)-domain \(CT_{\Sigma}\) which can not be deemed as a language in the normal sense; but it can still give semantic domains. By introducing a new \(\Omega\)-rule to the proof system \(\mathbf{DED}(E)\), where \(t\in T_{\Sigma}(X)\): \[\frac{}{\Omega\leq t}\] we get the new proof system \(\mathbf{\Omega DED}(E)\), and \(t\leq_{E\Omega} t'\) if and only if \(\vdash_{E\Omega} t\leq t'\).

3.4.3 \(\Sigma\)-predomains↩︎

Let \(\mathscr{CP}(E)\) denote the class of \(\Sigma\)-predomains satisfying the equations \(E\).

\(t\leq_{E\Omega} t'\) if and only if \(\vdash_{E\Omega} t\leq t'\).

The following is related to generating \(\Sigma\)-domains from \(\Sigma\)-predomains by use of ideal completion.

Let \(\mathscr{I}(A)\) denote the set of ideals of \(A\).

\(in:A\rightarrow\mathscr{I}(A)\) is defined as \(in(a)=\{x|x\leq_A a,a\in A\}\), and the ideal completion \(\langle\mathscr{I}(A),\subseteq\rangle\) of the partial order \(\langle A,\leq_A\rangle\) is denoted \(\langle A,\leq_A\rangle^{\infty}\) or \(A^{\infty}\).

We write \(\langle A,\leq_{A},\Sigma_{A}\rangle^{\infty}\) or \(A^{\infty}\) to denote the \(\Sigma\)-domain \(\langle A^{\infty},\leq_{A^{\infty}}, \Sigma_{A^{\infty}}\rangle\).

4 Testing Semantics↩︎

In this chapter, we generalize the testing semantics [11] to the truly concurrent processes. Firstly, we introduce the testing preorders and testing equivalences in 4.1. Then we introduce pomset labelled transition system in 4.2. Finally, we introduce the operational semantics, axiomatic semantics and denotational semantics of the basic processes, recursion and abstraction in 5, 7 and 8, respectively.

4.1 Testing Preorders and Testing Equivalences↩︎

An experiment or test, i.e., the interactions between the experimenter \(e\in \mathsf{Exp}\) and \(p\in \mathsf{Proc}\), is a sequence of the form:

\[e\parallel_{EP}p\mapsto e_0\parallel_{EP}p_0\mapsto e_1\parallel_{EP}p_1\mapsto\cdots\mapsto e_k\parallel_{EP}p_k\mapsto\cdots\]

The above sequence is called a computation if it is maximal, i.e., it is infinite or finite with terminal element \(e_n\parallel_{EP}p_n\), and denoted \(Comp(e,p)\). The possible results \(Result(e,p)\) of \(Comp(e,p)\) is defined by \(Result(e,p)=\{\top,\bot\}\), where \(\top\) denotes a successful computation and \(\bot\) denotes an unsuccessful computation. There are the following natural relations between processes \(p,p'\in \mathsf{Proc}\), where \(e\in \mathsf{Exp}\):

1. \(p\bar{\sim}' p'\) if for every \(e\in \mathsf{Exp}\), \(Result(e,p)=Result(e,p')\).

2. \(p~\mathsf{may}~e\) if \(\top\in Result(e,p)\).

3. \(p~\mathsf{must}~e\) if \(\bot\notin Result(e,p)\).

This leads to the definitions of three kinds of preorders.

The kernels of \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}_{\mathrm{MAY}}\), \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}_{\mathrm{MUST}}\) and \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}\) are denoted \(\bar{\sim}_{\mathrm{MAY}}\), \(\bar{\sim}_{\mathrm{MUST}}\) and \(\bar{\sim}\), respectively.

4.2 Posmet Labelled Transition System↩︎

A pomset transition system specification is a collection of inductive proof rules to derive the pomset transitions over states in \(\mathsf{Proc}\).

Both the operational behaviours of processes and experimenters can be modelled by EPLTSs, and the EPLTS of experimenters can be defined as \(\langle\mathsf{Exp},\mathsf{Act}\cup\{\omega,\mu,\tau\},\{\xrightarrow{U}|U\in\mathsf{Pom}\},\mathsf{Pred},\rightarrowtail\rangle\), where \(\omega\) is special action and \(Success=\{e\in\mathsf{Exp}|e\xrightarrow{\omega}\}\); \(\tau\) is a special action, while \[\frac{e\xrightarrow{\tau}e'}{e\parallel_{EP}p\mapsto e'\parallel_{EP}p}\] for \(e,e'\in\mathsf{Exp}\) and \(p\in\mathsf{Proc}\); \(\mu\) is a special action, while \[\frac{e\xrightarrow{\mu}e'\quad p\surd}{e\parallel_{EP}p\mapsto e'\parallel_{EP}p}\] for \(\surd\) is the successful termination predicate, \(e,e'\in\mathsf{Exp}\) and \(p\in\mathsf{Proc}\). For \(e,e'\in\mathsf{Exp}\), \(p,p'\in\mathsf{Proc}\) and \(U\in\mathsf{Pom}\), we have the following compatible interaction between experimenters and processes:

\[\frac{e\xrightarrow{U}e'\quad p\xrightarrow{U}p'}{e\parallel_{EP}p\mapsto e'\parallel_{EP}p'}\] \[\frac{e\rightarrowtail e'}{e\parallel_{EP}p\mapsto e'\parallel_{EP}p}\] \[\frac{p\rightarrowtail p'}{e\parallel_{EP}p\mapsto e\parallel_{EP}p'}\]

5 Basic Processes↩︎

In this chapter, we introduce the basic processes. Because of the elementary properties of parallelism in true concurrency, we move the parallelism and concurrency related operators into the basic processes. Firstly, we introduce the basic signature in 5.1, then the operational semantics, denotational semantics and axiomatic semantics of the basic processes are introduced in 5.2, 5.3 and 5.4, respectively. Finally, we get the results on trinity of operational semantics, denotational semantics and axiomatic semantics in 5.5.

5.1 Basic Signature↩︎

5.2 Operational Semantics↩︎

In this section, we give the operational semantics of the language \(\mathbf{M}_1\). The predicate \(\surd\) represents successful termination, \(\xrightarrow{a}\surd\) represents successful termination after execution of the action \(a\in\mathsf{Act}\), \(\xrightarrow{U}\surd\) represents successful termination after execution of the action \(U\in\mathsf{Pom}\) and \(\xrightarrow{ }\surd\) represents successful termination without execution of the any action. The following are the PTSS of the language \(\mathbf{M}_1\), where \(p,q\in\mathsf{Proc}\).

The PTSS of action \(1\), \(a\in\mathsf{Act}\) and \(U\in\mathsf{Pom}\) is as follows. Note that, there is no any transition rules for \(0\).

\[\frac{}{1\xrightarrow{ }\surd}\quad\frac{}{a\xrightarrow{a}\surd}\quad\frac{}{U\xrightarrow{U}\surd}\]

The PTSS of sequential composition is as follows.

\[\frac{p\xrightarrow{U}\surd}{p\cdot q\xrightarrow{U} q}\quad\frac{p\xrightarrow{U}p'}{p\cdot q\xrightarrow{U} p'\cdot q}\]

The PTSS of alternative composition is as follows.

\[\frac{p\xrightarrow{U}\surd}{p+ q\xrightarrow{U}\surd} \quad\frac{p\xrightarrow{U}p'}{p+ q\xrightarrow{U}p'} \quad\frac{q\xrightarrow{U}\surd}{p+ q\xrightarrow{U}\surd} \quad\frac{q\xrightarrow{U}q'}{p+ q\xrightarrow{U}q'}\]

The PTSS of concurrent composition is as follows.

\[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'\between q'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\gamma(a,b)}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\gamma(a,b)}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\gamma(a,b)}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\gamma(a,b)}p'\between q'}\]

The PTSS of parallel composition is as follows.

\[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'\between q'}\]

The PTSS of communication merge is as follows.

\[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\mid q\xrightarrow{\gamma(a,b)}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\mid q\xrightarrow{\gamma(a,b)}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\mid q\xrightarrow{\gamma(a,b)}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\mid q\xrightarrow{\gamma(a,b)}p'\between q'}\]

The PTSS of encapsulation operator is as follows.

\[\frac{p\xrightarrow{a}\surd\quad a\notin H}{\partial_H(p)\xrightarrow{a}\surd}\quad\frac{p\xrightarrow{a}p'\quad a\notin H}{\partial_H(p)\xrightarrow{a}\partial_H(p')}\]

The PTSS of confliction, confliction eliminator and the auxiliary unless operator is as follows, where \(\leq\) is the execution order.

\[\frac{p\xrightarrow{a}\surd\quad a\sharp b}{\Theta(p)\xrightarrow{a}\surd} \quad\frac{p\xrightarrow{b}\surd\quad a\sharp b}{\Theta(p)\xrightarrow{b}\surd}\] \[\frac{p\xrightarrow{a}p'\quad a\sharp b}{\Theta(p)\xrightarrow{a}\Theta(p')} \quad\frac{p\xrightarrow{b}p'\quad a\sharp b}{\Theta(p)\xrightarrow{b}\Theta(p')}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad c\leq a}{p\triangleleft q\xrightarrow{c}\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad c\leq a}{p\triangleleft q\xrightarrow{c}p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\sharp b\quad b\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\sharp b\quad b\leq c}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad a\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad a\leq c}{p\triangleleft q\xrightarrow{ }p'}\]

The PTSS of internal confliction, confliction eliminator and the auxiliary unless operator is as follows.

\[\frac{p\xrightarrow{a}\surd\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{a}\surd} \quad\frac{p\xrightarrow{b}\surd\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{b}\surd}\] \[\frac{p\xrightarrow{a}p'\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{a}\Theta(p')} \quad\frac{p\xrightarrow{b}p'\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{b}\Theta(p')}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad c\leq a}{p\triangleleft q\xrightarrow{c}\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad c\leq a}{p\triangleleft q\xrightarrow{c}p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad b\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad b\leq c}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad a\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad a\leq c}{p\triangleleft q\xrightarrow{ }p'}\]

The PTSS of internal alternative composition is as follows.

\[\frac{}{1\rightarrowtail\surd}\] \[\frac{}{p\oplus q\rightarrowtail p} \quad\frac{}{p\oplus q\rightarrowtail q}\] \[\frac{p\rightarrowtail p'}{p\cdot q\rightarrowtail p'\cdot q}\] \[\frac{p\rightarrowtail p'}{p+q\rightarrowtail p'+q} \quad\frac{q\rightarrowtail q'}{p+q\rightarrowtail p+q'}\] \[\frac{p\rightarrowtail p'}{p\between q\rightarrowtail p'\between q} \quad\frac{q\rightarrowtail q'}{p\between q\rightarrowtail p\between q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\between q\rightarrowtail p'\between q'}\] \[\frac{p\rightarrowtail p'}{p\parallel q\rightarrowtail p'\parallel q} \quad\frac{q\rightarrowtail q'}{p\parallel q\rightarrowtail p\parallel q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\parallel q\rightarrowtail p'\parallel q'}\] \[\frac{p\rightarrowtail p'}{p\mid q\rightarrowtail p'\mid q} \quad\frac{q\rightarrowtail q'}{p\mid q\rightarrowtail p\mid q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\mid q\rightarrowtail p'\mid q'}\] \[\frac{p\rightarrowtail p'}{\partial_H(p)\rightarrowtail \partial_H(p')}\] \[\frac{p\rightarrowtail p'}{\Theta(p)\rightarrowtail \Theta(p')}\] \[\frac{p\rightarrowtail p'}{p\triangleleft q\rightarrowtail p'\triangleleft q} \quad\frac{q\rightarrowtail q'}{p\triangleleft q\rightarrowtail p\triangleleft q'}\]

If \(\mathscr{A},\mathscr{B}\) are Acceptance sets, we write \(\mathscr{A}\subset\subset\mathscr{B}\) if for every \(A\in\mathscr{A}\), there exists some \(B\in\mathscr{B}\) such that \(B\subseteq A\).

For \(U,U_1,\cdots,U_k,V_1,\cdots,V_n\in\mathsf{Stp}\), one essential type of test is of the form denoted \(e(s,U)\) where \(s\) is the sequence \(V_1\cdots V_n\):

\[\tau w+V_1(\tau w+\cdots+V_n(\tau w+U)\cdots)\]

Another essential type of test is of the form denoted \(e(s,A)\) where \(s\) is the sequence \(V_1\cdots V_n\) and \(A\) is the set of steps \(\{U_1,\cdots,U_k\}\):

\[\tau w+V_1(\tau w+V_2(\tau w+\cdots+V_n(U_1 w+\cdots+U_k w)\cdots))\]

Let \(T\) denote the set of all experiments of the form \(e(s,U)\) or \(e(s,A)\). For \(p,q\in\mathsf{Proc}\) and every \(e\in T\), \(p\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}_{\mathrm{MUST}}^T q\) if \(p~\mathsf{must}~e\) implies \(q~\mathsf{must}~e\).

By use of the following relations:

1. \(p\xRightarrow{U}p'\) if \(p\rightarrowtail^* q\xrightarrow{U}q'\rightarrowtail^* p'\) for some \(q,q'\).

2. \(p\xRightarrow{1}p'\) if \(p\rightarrowtail^* p'\).

3. \(p\xRightarrow{Us}\) if \(p\xRightarrow{U}q\xRightarrow{s}p'\) for some \(q\).

and the following definitions:

1. \(Im(p)=\{p'|p\rightarrowtail p'\}\).

2. \(D(p,s)=\{p'\in\mathsf{Proc}|p\xRightarrow{s}p'\}\), the \(s\)-derivatives of \(p\).

3. \(L(p)=\{s|p\xRightarrow{s}\}\), the language of \(p\).

4. \(D(p)=\{p'| for some U\in\mathsf{Pom},p\xRightarrow{U}p'\}\), the derivatives of \(p\).

5. \(S(p)=\{U|p\xRightarrow{U}\}\), the successors of \(p\).

6. \(S(p,s)=\{U|p\xRightarrow{s}p'\xRightarrow{U}\}\), the successors of \(p\) after \(s\).

7. \(\mathscr{A}(p,s)=\{S(p')|p\xRightarrow{s}p'\}\), the Acceptance sets of \(p\) after \(s\).

we can get the modified definition of the preorders \(\ll_{\mathrm{MUST}}\), \(\ll_{\mathrm{MAY}}\) and \(\ll\). The result theorem of alternative characterization of testing preorders in 29 still holds.

5.3 Denotational Semantics↩︎

In this section, we give the denotational semantics of the language \(\mathbf{M}_1\), the denotational interpretation of \(\mathbf{M}_1\) is finite Parallel Acceptance Tree (\(\mathbf{fPAT}\)), which is a parallelism generalization of Hennessy’s finite Acceptance Tree (\(\mathbf{fAT}\)) in [11]. In an \(\mathbf{fPAT}\), every node and every edge are labelled. Intuitively, every edge can be labelled by a single action. By this way, an \(\mathbf{fPAT}\) is usually unstructured, i.e., there are two kinds of branches: parallel ones and alternative ones, and there may exist communications or conflictions among actions located in different parallel branches. It is reasonable that all partial orders between actions in different parallel branches are communications. In the example of \(\mathbf{fPAT}\) in 1, there exist parallel branches denoted by \(\parallel\), alternative branches denoted by \(+\), communications between parallel branches denoted by lines with arrows, and conflictions between parallel branches denoted by dashed lines. Communications and conflictions between actions in different parallel branches are the causes of the unstructuredness.

The \(\mathbf{fPAT}\) in 1 can be expressed by a truly concurrent process term of the language \(\mathbf{M}_1\) with two unstructured constraints: \[(a_1\cdot((a_2\cdot a_3\cdot a_4)\between(a_5\cdot a_6\cdot a_7\cdot a_8)+(a_9\cdot a_{10})\between(a_{11}\cdot a_{12})))\between(a_{13}\cdot a_{14}\cdot a_{15}\cdot a_{16})\quad(a_3\leq^c a_6,a_{12}\sharp a_{16})\]

In the following, we define functions over \(\mathbf{fPAT}\) for every function symbol in \(\Sigma^1\): \(0_{\mathbf{fPAT}}\), \(1_{\mathbf{fPAT}}\), \(U_{\mathbf{fPAT}}\), \(\cdot_{\mathbf{fPAT}}\), \(+_{\mathbf{fPAT}}\), \(\oplus_{\mathbf{fPAT}}\), \(\parallel_{\mathbf{fPAT}}\), \(\gamma(a,b)_{\mathbf{fPAT}}\), \(\mid_{\mathbf{fPAT}}\), \(\between_{\mathbf{fPAT}}\), \(\partial_H(p)_{\mathbf{fPAT}}\), \(\sharp_{\mathbf{fPAT}}\), \(\Theta(p)_{\mathbf{fPAT}}\), \(\triangleleft_{\mathbf{fPAT}}\), \(\mathbin{\mathpalette\make@circled{\#}}_{\mathbf{fPAT}}\).

(1) \(0_{\mathbf{fPAT}}\).

Let \(0_{\mathbf{fPAT}}\) denote the trivial tree \(\bullet\{\emptyset\}\), which consists of only one node, labelled by the set of the empty set \(\emptyset\) with no successor branches, and rendered as \(\bullet\).

(2) \(1_{\mathbf{fPAT}}\).

Let \(1_{\mathbf{fPAT}}\) denote the trivial tree \(\bullet\{\{\}\}\), which consists of one node, labelled by the set of the empty set \(\{\}\), and rendered as \(\mathbin{\mathpalette\make@circled{\bullet}}\). Note that, \(1_{\mathbf{fPAT}}\) can have successor branches.

(3) \(U_{\mathbf{fPAT}}\).

Let \(U_{\mathbf{fPAT}}\) denote the trivial tree:

Formally, the tree \(U_{\mathbf{fPAT}}\) is the tree \(t\) determined by:

1. \(L(t)=\{1\}\cup\{U\}\).

2. \(\mathscr{A}(t(1))=\{\{U\}\}\), \(\mathscr{A}(t(U))=\{\{\}\}\).

(4) \(\cdot_{\mathbf{fPAT}}\).

The function \(\cdot_{\mathbf{fPAT}}\) maps the trees

to the tree

Formally, the tree \(t\cdot_{\mathbf{fPAT}}t'\) is the tree \(t''\) determined by:

1. \(L(t'')=\{1\}\cup\{ss'|s\in L(t),s'\in L(t')\}\).

2. \(\mathscr{A}(t''(1))=\mathscr{A}(t(1))\), \(\mathscr{A}(t''(\{\}_ss'))=\mathscr{A}(t(s'))\) where \(\{\}_s\) is the leaf of \(s\).

(5) \(+_{\mathbf{fPAT}}\).

The function \(+_{\mathbf{fPAT}}\) maps the trees

to the tree

Let \(\mathscr{B}\) be any finite collection of finite subsets of \(\mathsf{Pom}\) and \(A(\mathscr{B})\) be the set of actions which appear in \(\mathscr{B}\). Though in general \(\mathscr{B}\) is not an \(A(\mathscr{B})\)-set, it is always possible to extend \(\mathscr{B}\) to become an \(A(\mathscr{B})\)-set. Let \(c(\mathscr{B})\) be the least set such that:

1. \(\mathscr{B}\subseteq c(\mathscr{B})\).

2. (\(\cup\)-closed) \(X,Y\in c(\mathscr{B})\) implies \(X\cup Y\in c(\mathscr{B})\).

3. (Convex-closed) \(X,Y\in c(\mathscr{B})\), \(X\subseteq Z\subseteq Y\) implies \(Z\in c(\mathscr{B})\).

So, \(B\in c(\mathscr{B})\) if and only if it can be derived from the following rules:

1. \(B\in \mathscr{B}\) implies \(B\in c(\mathscr{B})\).

2. \(X,Y\in c(\mathscr{B})\) implies \(X\cup Y\in c(\mathscr{B})\).

3. \(X,Y\in c(\mathscr{B})\), \(X\subseteq Z\subseteq Y\) implies \(Z\in c(\mathscr{B})\).

If \(\mathscr{B}_1\), \(\mathscr{B}_2\) are set of sets, their pointwise union is defined as: \[\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_2=\{B_1\cup B_2|B_1\in\mathscr{B}_1,B_2\in\mathscr{B}_2\}\]

Then the operators \(c\) and \(\mathop{\mathrm{\mathcal{U}}}\) have the following properties.

c1. If \(\mathscr{B}\) is an \(S\)-set then \(c(\mathscr{B})=\mathscr{B}\).

c2. If \(\mathscr{B}\subseteq\mathscr{B}'\) then \(c(\mathscr{B})\subseteq c(\mathscr{B}')\).

c3. \(c(\mathscr{B})=c(c(\mathscr{B}))\).

c4. \(c(\mathscr{B}_1\cup c(\mathscr{B}_2\cup\mathscr{B}_3))=c(\mathscr{B}_1\cup\mathscr{B}_2\cup\mathscr{B}_3)\).

c5. \(c(\mathscr{B}_1\cup\mathscr{B}_2)=c(c(\mathscr{B}_1)\cup c(\mathscr{B}_2))\).

c6. If \(A\in c(\mathscr{B})\) then \(B\subseteq A\) for some \(B\in\mathscr{B}\).

du1. \((\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_2)\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_3=\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}(\mathscr{B}_2\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_3)\).

du2. \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_2=\mathscr{B}_2\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_1\).

du3. If \(\mathscr{B}\) is saturated, then \(\mathscr{B}\mathop{\mathrm{\mathcal{U}}}\mathscr{B}=\mathscr{B}\).

du4. \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}(\mathscr{B}_2\cup \mathscr{B}_3)=(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_2)\cup(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_3)\).

c7. If \(\mathscr{B}_1,\mathscr{B}_2\) are saturated, \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_2\) is saturated.

c8. \(c(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}\mathscr{B}_2)=c(\mathscr{B}_1)\mathop{\mathrm{\mathcal{U}}}c(\mathscr{B}_2)\).

Then, formally, the tree \(t+_{\mathbf{fPAT}}t'\) is the tree \(t''\) determined by:

1. \(L(t'')=L(t)\cup L(t')\).

2. \(\mathscr{A}(t'')=\mathscr{A}(t)\mathop{\mathrm{\mathcal{U}}}\mathscr{A}(t')\).

3. \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\cup\mathscr{A}(t'(s)))\) where \(s\neq 1\), and if \(s\notin L(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

(6) \(\oplus_{\mathbf{fPAT}}\).

The function \(\oplus_{\mathbf{fPAT}}\) maps the trees

to the tree

Formally, the tree \(t\oplus_{\mathbf{fPAT}}t'\) is the tree \(t''\) determined by:

1. \(L(t'')=L(t)\cup L(t')\).

2. \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\cup\mathscr{A}(t'(s)))\) for every \(s\in L(t'')\), and if \(s\notin L(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

(7) \(\parallel_{\mathbf{fPAT}}\), \(\gamma(a,b)_{\mathbf{fPAT}}\), \(\mid_{\mathbf{fPAT}}\), \(\between_{\mathbf{fPAT}}\) and \(\partial_H(p)_{\mathbf{fPAT}}\).

The function \(\parallel_{\mathbf{fPAT}}\) maps the trees

to the tree

The function \(\mid_{\mathbf{fPAT}}\) maps the trees

to the tree

The function \(\between_{\mathbf{fPAT}}\) maps the trees

to the tree

Firstly, we define the parallelism of sets. In this book, every element of a set is a pomset \(U\in\mathsf{Pom}\), for two such sets \(B_1,B_2\), their parallelism is defined as: \[B_1\parallel B_2=\{U_1\parallel U_2|U_1\in B_1,U_2\in B_2\}\] where \(U_1\parallel U_2\) is the parallel composition of pomsets defined in 2.2. Similarly, we can define the communication of sets and the concurrency of sets: \(B_1\mid B_2\) and \(B_1\between B_2\), respectively.

If \(\mathscr{B}_1\), \(\mathscr{B}_2\) are set of sets, their pointwise parallelism is defined as: \[\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel}\mathscr{B}_2=\{B_1\parallel B_2|B_1\in\mathscr{B}_1,B_2\in\mathscr{B}_2\}\]

Similarly, we can define their pointwise communication and pointwise concurrency as: \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid}\mathscr{B}_2\) and \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between}\mathscr{B}_2\).

Then the operators \(\mathop{\mathrm{\mathcal{U}}}_{\parallel}\), \(\mathop{\mathrm{\mathcal{U}}}_{\mid}\) and \(\mathop{\mathrm{\mathcal{U}}}_{\between}\) have the following properties.

dp1. \((\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_2)\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_3=\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel}(\mathscr{B}_2\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_3)\).

dp2. \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_2=\mathscr{B}_2\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_1\).

dp3. \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel} (\mathscr{B}_2\cup \mathscr{B}_3)=(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_2)\cup(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_3)\).

dp4. If \(\mathscr{B}_1,\mathscr{B}_2\) are saturated, \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_2\) is saturated.

dp5. \(c(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\parallel} \mathscr{B}_2)=c(\mathscr{B}_1)\mathop{\mathrm{\mathcal{U}}}_{\parallel} c(\mathscr{B}_2)\).

dp6. \((\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_2)\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_3=\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid}(\mathscr{B}_2\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_3)\).

dp7. \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_2=\mathscr{B}_2\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_1\).

dp8. \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid} (\mathscr{B}_2\cup \mathscr{B}_3)=(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_2)\cup(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_3)\).

dp9. If \(\mathscr{B}_1,\mathscr{B}_2\) are saturated, \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_2\) is saturated.

dp10. \(c(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\mid} \mathscr{B}_2)=c(\mathscr{B}_1)\mathop{\mathrm{\mathcal{U}}}_{\mid} c(\mathscr{B}_2)\).

dp11. \((\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_2)\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_3=\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between}(\mathscr{B}_2\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_3)\).

dp12. \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_2=\mathscr{B}_2\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_1\).

dp13. \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between} (\mathscr{B}_2\cup \mathscr{B}_3)=(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_2)\cup(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_3)\).

dp14. If \(\mathscr{B}_1,\mathscr{B}_2\) are saturated, \(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_2\) is saturated.

dp15. \(c(\mathscr{B}_1\mathop{\mathrm{\mathcal{U}}}_{\between} \mathscr{B}_2)=c(\mathscr{B}_1)\mathop{\mathrm{\mathcal{U}}}_{\between} c(\mathscr{B}_2)\).

Then, formally, the tree \(t\parallel_{\mathbf{fPAT}}t'\) is the tree \(t''\) determined by:

1. \(L(t'')=L(t)\parallel L(t')\).

2. \(\mathscr{A}(t'')=\mathscr{A}(t)\mathop{\mathrm{\mathcal{U}}}_{\parallel}\mathscr{A}(t')\).

3. \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\parallel\mathscr{A}(t'(s)))\) where \(s\neq 1\), and if \(s\notin L(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

The tree \(t\mid_{\mathbf{fPAT}}t'\) is the tree \(t''\) determined by:

1. \(L(t'')=L(t)\mid L(t')\).

2. \(\mathscr{A}(t'')=\mathscr{A}(t)\mathop{\mathrm{\mathcal{U}}}_{\mid}\mathscr{A}(t')\).

3. \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\mid\mathscr{A}(t'(s)))\) where \(s\neq 1\), and if \(s\notin L(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

The tree \(t\between_{\mathbf{fPAT}}t'\) is the tree \(t''\) determined by:

1. \(L(t'')=L(t)\between L(t')\).

2. \(\mathscr{A}(t'')=\mathscr{A}(t)\mathop{\mathrm{\mathcal{U}}}_{\between}\mathscr{A}(t')\).

3. \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\between\mathscr{A}(t'(s)))\) where \(s\neq 1\), and if \(s\notin L(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

According to the definitions of parallel composition, communication composition and concurrent composition of pomsets in 2.2, the tree

is equivalent to the tree

Formally the tree \(t\between_{\mathbf{fPAT}}t'\) is the tree \(t''\) determined by:

1. \(L(t'')=L(t)\between L(t')=(L(t)\parallel L(t'))\cup (L(t)\mid L(t'))\).

2. \(\mathscr{A}(t'')=\mathscr{A}(t)\mathop{\mathrm{\mathcal{U}}}_{\between}\mathscr{A}(t')=(\mathscr{A}(t)\mathop{\mathrm{\mathcal{U}}}_{\parallel}\mathscr{A}(t'))\mathop{\mathrm{\mathcal{U}}}(\mathscr{A}(t)\mathop{\mathrm{\mathcal{U}}}_{\mid}\mathscr{A}(t'))\).

3. \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\between\mathscr{A}(t'(s)))=(c(\mathscr{A}(t(s))\parallel\mathscr{A}(t'(s))))\cup (c(\mathscr{A}(t(s))\mid\mathscr{A}(t'(s))))\) where \(s\neq 1\), and if \(s\notin L(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

For \(a\in\mathsf{Act}(t)\) and \(b\in\mathsf{Act}(t')\), \(a,b\) in the tree \(t\mid_{\mathbf{fPAT}}t'\) are merged into \(\gamma(a,b)\) if \(a\leq^c b\); into \(0\), otherwise.

For \(H\subseteq\mathsf{Act}(t\parallel_{\mathbf{fPAT}}t')\), \(\partial_H(t\parallel_{\mathbf{fPAT}}t')\) renames every \(a\in H\) into \(0\); and remains themselves unchanged for all \(a\notin H\) and \(a\in\mathsf{Act}(t\parallel_{\mathbf{fPAT}}t')\).

Note that, in a tree \(t\in\mathbf{fPAT}\), arbitrary \(1\)’s can be padded in the alternative branches and parallel branches, but, we leave the padding of \(1\)’s as the privilege of the modelling phase to explicitly present the existences of \(1\)’s.

(8) \(\sharp_{\mathbf{fPAT}}\), \(\Theta(p)_{\mathbf{fPAT}}\), \(\triangleleft_{\mathbf{fPAT}}\) and \(\mathbin{\mathpalette\make@circled{\#}}_{\mathbf{fPAT}}\).

For \(a\in\mathsf{Act}(t)\) and \(b\in\mathsf{Act}(t')\), there exists a confliction relation \(a\sharp b\) in the tree \(t\parallel_{\mathbf{fPAT}}t'\) (resp. \(t\mid_{\mathbf{fPAT}}t'\)), \(\Theta(t\parallel_{\mathbf{fPAT}}t')_{\mathbf{fPAT}}\) (resp. \(\Theta(t\mid_{\mathbf{fPAT}}t')_{\mathbf{fPAT}}\)) and \(\triangleleft_{\mathbf{fPAT}}\) rename \(\{s'|t(1)\xrightarrow{s}\xrightarrow{a}t(s')\}\) to \(1\)’s and remain \(t'\) unchanged, or rename \(\{s'|t'(1)\xrightarrow{s}\xrightarrow{b}t'(s')\}\) to \(1\)’s and remain \(t\) unchanged. This is reflected that the tree

is equivalent to the tree

For \(a\in\mathsf{Act}(t)\) and \(b\in\mathsf{Act}(t')\), there exists an internal confliction relation \(a\mathbin{\mathpalette\make@circled{\#}}b\) in the tree \(t\parallel_{\mathbf{fPAT}}t'\) (resp. \(t\mid_{\mathbf{fPAT}}t'\)), \(\Theta(t\parallel_{\mathbf{fPAT}}t')_{\mathbf{fPAT}}\) (resp. \(\Theta(t\mid_{\mathbf{fPAT}}t')_{\mathbf{fPAT}}\)) and \(\triangleleft_{\mathbf{fPAT}}\) rename \(\{s'|t(1)\xrightarrow{s}\xrightarrow{a}t(s')\}\) to \(1\)’s and remain \(t'\) unchanged, or rename \(\{s'|t'(1)\xrightarrow{s}\xrightarrow{b}t'(s')\}\) to \(1\)’s and remain \(t\) unchanged. This is reflected that the tree

is equivalent to the tree

5.4 Axiomatic Semantics↩︎

The proof system \(\mathbf{DED}(E^1)\) of inequations of \(\mathbf{M}_1\) is shown in 1.

If \(P\) is a finite set of terms \(p_1,\cdots,p_k\), let \(\sum\{p|p\in P\}\) denote the term \[p_1+p_2+\cdots+p_k\] If \(P\) is a nonempty finite set of terms \(p_1,\cdots,p_k\), let \(\mathop{ \mathchoice { \begin{tikzpicture}[baseline=(char.base), inner sep=0, outer sep=0] \draw (-0.3ex,0) circle (0.1); \node (char) at (0,0) {\displaystyle\sum}; \end{tikzpicture}} { \begin{tikzpicture}[baseline=(char.base), inner sep=0, outer sep=0] \draw (-0.3ex,0) circle (0.075); \node (char) at (0,0) {\textstyle\sum}; \end{tikzpicture}} { \begin{tikzpicture}[baseline=(char.base), inner sep=0, outer sep=0] \draw (-0.3ex,0) circle (0.075); \node (char) at (0,0) {\scriptstyle\sum}; \end{tikzpicture}} { \begin{tikzpicture}[baseline=(char.base), inner sep=0, outer sep=0] \draw (-0.3ex,0) circle (0.075); \node (char) at (0,0) {\scriptscriptstyle\sum}; \end{tikzpicture}} }\displaylimits \{p|p\in P\}\) denote the term \[p_1\oplus p_2\oplus \cdots\oplus p_k\]

5.5 The Trinity↩︎

By adding the following axiom \[A19\quad x\oplus y\leq x\] into the proof system \(\mathbf{DED}(E^1)\) in 1 to get the proof system \(\mathbf{DED}(E^1_{\mathbf{S}})\).

By adding the following axiom \[A20\quad x\leq x\oplus y\] into the proof system \(\mathbf{DED}(E^1)\) in 1 to get the proof system \(\mathbf{DED}(E^1_{\mathbf{W}})\).

6 \(\Omega\)↩︎

In this chapter, we introduce the basic processes with \(\Omega\). Firstly, we introduce the \(\Omega\) signature in 6.1, then the operational semantics, denotational semantics and axiomatic semantics of the \(\Omega\) processes are introduced in 6.2, 6.3 and 6.4, respectively. Finally, we get the results on trinity of operational semantics, denotational semantics and axiomatic semantics in 6.5.

6.1 \(\Omega\) Signature↩︎

6.2 Operational Semantics↩︎

In this section, we give the operational semantics of the language \(\mathbf{M}_2\). The predicate \(\surd\) represents successful termination, \(\xrightarrow{a}\surd\) represents successful termination after execution of the action \(a\in\mathsf{Act}\), \(\xrightarrow{U}\surd\) represents successful termination after execution of the action \(U\in\mathsf{Pom}\) and \(\xrightarrow{ }\surd\) represents successful termination without execution of the any action. The following are the PTSS of the language \(\mathbf{M}_2\), where \(p,q\in\mathsf{Proc}\).

The PTSS of action \(1\), \(a\in\mathsf{Act}\) and \(U\in\mathsf{Pom}\) is as follows. Note that, there is no any transition rules for \(0\) and \(\Omega\).

\[\frac{}{1\xrightarrow{ }\surd}\quad\frac{}{a\xrightarrow{a}\surd}\quad\frac{}{U\xrightarrow{U}\surd}\]

The PTSS of sequential composition is as follows.

\[\frac{p\xrightarrow{U}\surd}{p\cdot q\xrightarrow{U} q}\quad\frac{p\xrightarrow{U}p'}{p\cdot q\xrightarrow{U} p'\cdot q}\]

The PTSS of alternative composition is as follows.

\[\frac{p\xrightarrow{U}\surd}{p+ q\xrightarrow{U}\surd} \quad\frac{p\xrightarrow{U}p'}{p+ q\xrightarrow{U}p'} \quad\frac{q\xrightarrow{U}\surd}{p+ q\xrightarrow{U}\surd} \quad\frac{q\xrightarrow{U}q'}{p+ q\xrightarrow{U}q'}\]

The PTSS of concurrent composition is as follows.

\[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'\between q'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\gamma(a,b)}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\gamma(a,b)}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\gamma(a,b)}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\gamma(a,b)}p'\between q'}\]

The PTSS of parallel composition is as follows.

\[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'\between q'}\]

The PTSS of communication merge is as follows.

\[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\mid q\xrightarrow{\gamma(a,b)}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\mid q\xrightarrow{\gamma(a,b)}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\mid q\xrightarrow{\gamma(a,b)}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\mid q\xrightarrow{\gamma(a,b)}p'\between q'}\]

The PTSS of encapsulation operator is as follows.

\[\frac{p\xrightarrow{a}\surd\quad a\notin H}{\partial_H(p)\xrightarrow{a}\surd}\quad\frac{p\xrightarrow{a}p'\quad a\notin H}{\partial_H(p)\xrightarrow{a}\partial_H(p')}\]

The PTSS of confliction, confliction eliminator and the auxiliary unless operator is as follows, where \(\leq\) is the execution order.

\[\frac{p\xrightarrow{a}\surd\quad a\sharp b}{\Theta(p)\xrightarrow{a}\surd} \quad\frac{p\xrightarrow{b}\surd\quad a\sharp b}{\Theta(p)\xrightarrow{b}\surd}\] \[\frac{p\xrightarrow{a}p'\quad a\sharp b}{\Theta(p)\xrightarrow{a}\Theta(p')} \quad\frac{p\xrightarrow{b}p'\quad a\sharp b}{\Theta(p)\xrightarrow{b}\Theta(p')}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad c\leq a}{p\triangleleft q\xrightarrow{c}\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad c\leq a}{p\triangleleft q\xrightarrow{c}p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\sharp b\quad b\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\sharp b\quad b\leq c}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad a\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad a\leq c}{p\triangleleft q\xrightarrow{ }p'}\]

The PTSS of internal confliction, confliction eliminator and the auxiliary unless operator is as follows.

\[\frac{p\xrightarrow{a}\surd\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{a}\surd} \quad\frac{p\xrightarrow{b}\surd\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{b}\surd}\] \[\frac{p\xrightarrow{a}p'\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{a}\Theta(p')} \quad\frac{p\xrightarrow{b}p'\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{b}\Theta(p')}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad c\leq a}{p\triangleleft q\xrightarrow{c}\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad c\leq a}{p\triangleleft q\xrightarrow{c}p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad b\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad b\leq c}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad a\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad a\leq c}{p\triangleleft q\xrightarrow{ }p'}\]

The PTSS of internal alternative composition is as follows.

\[\frac{}{1\rightarrowtail\surd}\] \[\frac{}{p\oplus q\rightarrowtail p} \quad\frac{}{p\oplus q\rightarrowtail q}\] \[\frac{p\rightarrowtail p'}{p\cdot q\rightarrowtail p'\cdot q}\] \[\frac{p\rightarrowtail p'}{p+q\rightarrowtail p'+q} \quad\frac{q\rightarrowtail q'}{p+q\rightarrowtail p+q'}\] \[\frac{p\rightarrowtail p'}{p\between q\rightarrowtail p'\between q} \quad\frac{q\rightarrowtail q'}{p\between q\rightarrowtail p\between q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\between q\rightarrowtail p'\between q'}\] \[\frac{p\rightarrowtail p'}{p\parallel q\rightarrowtail p'\parallel q} \quad\frac{q\rightarrowtail q'}{p\parallel q\rightarrowtail p\parallel q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\parallel q\rightarrowtail p'\parallel q'}\] \[\frac{p\rightarrowtail p'}{p\mid q\rightarrowtail p'\mid q} \quad\frac{q\rightarrowtail q'}{p\mid q\rightarrowtail p\mid q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\mid q\rightarrowtail p'\mid q'}\] \[\frac{p\rightarrowtail p'}{\partial_H(p)\rightarrowtail \partial_H(p')}\] \[\frac{p\rightarrowtail p'}{\Theta(p)\rightarrowtail \Theta(p')}\] \[\frac{p\rightarrowtail p'}{p\triangleleft q\rightarrowtail p'\triangleleft q} \quad\frac{q\rightarrowtail q'}{p\triangleleft q\rightarrowtail p\triangleleft q'}\]

6.3 Denotational Semantics↩︎

For a tree \(t\in\mathbf{PAT}_{\mathbf{S}}\), let \(CL(t)\subseteq L(t)\) determine closed nodes, which is prefix-closed and may be empty. For any tree \(t\in\mathbf{PAT}_{\mathbf{S}}\) and \(s\in\mathsf{Pom}^*\), we write \(t\downarrow s\) if \(s'\in L(t)\) then \(s'\in CL(t)\) for every prefix \(s'\) of \(s\).

In the following, we define functions over \(\mathbf{PAT}_{\mathbf{S}}\) for every function symbol in \(\Sigma^2\): \(0_{\mathbf{PAT}_{\mathbf{S}}}\), \(1_{\mathbf{PAT}_{\mathbf{S}}}\), \(U_{\mathbf{PAT}_{\mathbf{S}}}\), \(\cdot_{\mathbf{PAT}_{\mathbf{S}}}\), \(+_{\mathbf{PAT}_{\mathbf{S}}}\), \(\oplus_{\mathbf{PAT}_{\mathbf{S}}}\), \(\parallel_{\mathbf{PAT}_{\mathbf{S}}}\), \(\gamma(a,b)_{\mathbf{PAT}_{\mathbf{S}}}\), \(\mid_{\mathbf{PAT}_{\mathbf{S}}}\), \(\between_{\mathbf{PAT}_{\mathbf{S}}}\), \(\partial_H(p)_{\mathbf{PAT}_{\mathbf{S}}}\), \(\sharp_{\mathbf{PAT}_{\mathbf{S}}}\), \(\Theta(p)_{\mathbf{PAT}_{\mathbf{S}}}\), \(\triangleleft_{\mathbf{PAT}_{\mathbf{S}}}\), \(\mathbin{\mathpalette\make@circled{\#}}_{\mathbf{PAT}_{\mathbf{S}}}\). They are continuous operations on the algebra cpo \(\mathbf{PAT}_{\mathbf{S}}\) and mild extensions of those in \(\mathbf{fPAT}\).

(1) \(\Omega_{\mathbf{PAT}_{\mathbf{S}}}\).

Let \(\Omega_{\mathbf{PAT}_{\mathbf{S}}}\) denote the trivial tree \(\circ\), which consists of only one node, with no successor branches, and rendered as \(\circ\).

(2) \(0_{\mathbf{PAT}_{\mathbf{S}}}\).

Let \(0_{\mathbf{PAT}_{\mathbf{S}}}\) denote the trivial tree \(\bullet\{\emptyset\}\), which consists of only one node, labelled by the set of the empty set \(\emptyset\) with no successor branches, and rendered as \(\bullet\).

(3) \(1_{\mathbf{PAT}_{\mathbf{S}}}\).

Let \(1_{\mathbf{PAT}_{\mathbf{S}}}\) denote the trivial tree \(\bullet\{\{\}\}\), which consists of one node, labelled by the set of the empty set \(\{\}\), and rendered as \(\mathbin{\mathpalette\make@circled{\bullet}}\). Note that, \(1_{\mathbf{PAT}_{\mathbf{S}}}\) can have successor branches.

(4) \(U_{\mathbf{PAT}_{\mathbf{S}}}\).

Formally, the tree \(U_{\mathbf{PAT}_{\mathbf{S}}}\) is the tree \(t\) determined by:

1. \(L(t)=\{1\}\cup\{U\}\).

2. \(\mathscr{A}(t(1))=\{\{U\}\}\), \(\mathscr{A}(t(U))=\{\{\}\}\).

(5) \(\cdot_{\mathbf{PAT}_{\mathbf{S}}}\).

Formally, the tree \(t\cdot_{\mathbf{PAT}_{\mathbf{S}}}t'\) is the tree \(t''\) determined by:

1. \(L(t'')=\{1\}\cup\{ss'|s\in L(t),s'\in L(t')\}\).

2. \(\mathscr{A}(t''(1))=\mathscr{A}(t(1))\), \(\mathscr{A}(t''(\{\}_ss'))=\mathscr{A}(t(s'))\) where \(\{\}_s\) is the closed leaf of \(s\).

(6) \(+_{\mathbf{PAT}_{\mathbf{S}}}\).

Formally, the tree \(t+_{\mathbf{PAT}_{\mathbf{S}}}t'\) is the tree \(t''\) determined by:

1. \(CL(t'')=\{s|s\in L(t)\cup L(t'),for every prefix s' of s if s'\in L(t) then s'\in CL(t),\linebreak and for every prefix s' of s if s'\in L(t') then s'\in CL(t')\}\).

2. \(L(t'')=\{s|s\in L(t)\cup L(t'), s=s'U implies s'\in CL(t'')\}\).

3. \(\mathscr{A}(t''(1))=c(\mathscr{A}(t(1))\mathop{\mathrm{\mathcal{U}}}\mathscr{A}(t'(1)))\), \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\cup\mathscr{A}(t'(s)))\) for every \(s\in CL(t'')\), and if \(s\notin CL(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

(7) \(\oplus_{\mathbf{PAT}_{\mathbf{S}}}\).

Formally, the tree \(t\oplus_{\mathbf{PAT}_{\mathbf{S}}}t'\) is the tree \(t''\) determined by:

1. \(CL(t'')=\{s|s\in L(t)\cup L(t'),for every prefix s' of s if s'\in L(t) then s'\in CL(t),\linebreak and for every prefix s' of s if s'\in L(t') then s'\in CL(t')\}\).

2. \(L(t'')=\{s|s\in L(t)\cup L(t'), s=s'U implies s'\in CL(t'')\}\).

3. \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\cup\mathscr{A}(t'(s)))\) for every \(s\in CL(t'')\), and if \(s\notin CL(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

(8) \(\parallel_{\mathbf{PAT}_{\mathbf{S}}}\), \(\gamma(a,b)_{\mathbf{PAT}_{\mathbf{S}}}\), \(\mid_{\mathbf{PAT}_{\mathbf{S}}}\), \(\between_{\mathbf{PAT}_{\mathbf{S}}}\) and \(\partial_H(p)_{\mathbf{PAT}_{\mathbf{S}}}\).

Then, formally, the tree \(t\parallel_{\mathbf{PAT}_{\mathbf{S}}}t'\) is the tree \(t''\) determined by:

1. \(CL(t'')=\{s|s\in L(t)\parallel L(t'),for every prefix s' of s if s'\in L(t) then s'\in CL(t),\linebreak and for every prefix s' of s if s'\in L(t') then s'\in CL(t')\}\).

2. \(L(t'')=\{s|s\in L(t)\parallel L(t'), s=s'U implies s'\in CL(t'')\}\).

3. \(\mathscr{A}(t''(1))=c(\mathscr{A}(t(1))\mathop{\mathrm{\mathcal{U}}}_{\parallel}\mathscr{A}(t'(1)))\), \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\parallel\mathscr{A}(t'(s)))\) for every \(s\in CL(t'')\), and if \(s\notin CL(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

The tree \(t\mid_{\mathbf{PAT}_{\mathbf{S}}}t'\) is the tree \(t''\) determined by:

1. \(CL(t'')=\{s|s\in L(t)\mid L(t'),for every prefix s' of s if s'\in L(t) then s'\in CL(t),\linebreak and for every prefix s' of s if s'\in L(t') then s'\in CL(t')\}\).

2. \(L(t'')=\{s|s\in L(t)\mid L(t'), s=s'U implies s'\in CL(t'')\}\).

3. \(\mathscr{A}(t''(1))=c(\mathscr{A}(t(1))\mathop{\mathrm{\mathcal{U}}}_{\mid}\mathscr{A}(t'(1)))\), \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\mid\mathscr{A}(t'(s)))\) for every \(s\in CL(t'')\), and if \(s\notin CL(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

Formally the tree \(t\between_{\mathbf{PAT}_{\mathbf{S}}}t'\) is the tree \(t''\) determined by:

1. \(CL(t'')=(CL(t)\parallel CL(t'))\cup (CL(t)\mid CL(t'))\).

2. \(L(t'')=(L(t)\parallel L(t'))\cup (L(t)\mid L(t'))\).

3. \(\mathscr{A}(t''(1))=c(\mathscr{A}(t(1))\mathop{\mathrm{\mathcal{U}}}_{\parallel}\mathscr{A}(t'(1)))\cup c(\mathscr{A}(t(1))\mathop{\mathrm{\mathcal{U}}}_{\mid}\mathscr{A}(t'(1)))\), \(\mathscr{A}(t''(s))=c(\mathscr{A}(t(s))\parallel\mathscr{A}(t'(s)))\cup c(\mathscr{A}(t(s))\mid\mathscr{A}(t'(s)))\) for every \(s\in CL(t'')\), and if \(s\notin CL(t)\) then \(\mathscr{A}(t(s))=\emptyset\).

For \(a\in\mathsf{Act}(t)\) and \(b\in\mathsf{Act}(t')\), \(a,b\) in the tree \(t\mid_{\mathbf{PAT}_{\mathbf{S}}}t'\) are merged into \(\gamma(a,b)\) if \(a\leq^c b\); into \(0\), otherwise.

For \(H\subseteq\mathsf{Act}(t\parallel_{\mathbf{PAT}_{\mathbf{S}}}t')\), \(\partial_H(t\parallel_{\mathbf{PAT}_{\mathbf{S}}}t')\) renames every \(a\in H\) into \(0\); and remains themselves unchanged for all \(a\notin H\) and \(a\in\mathsf{Act}(t\parallel_{\mathbf{PAT}_{\mathbf{S}}}t')\).

(9) \(\sharp_{\mathbf{PAT}_{\mathbf{S}}}\), \(\Theta(p)_{\mathbf{PAT}_{\mathbf{S}}}\), \(\triangleleft_{\mathbf{PAT}_{\mathbf{S}}}\) and \(\mathbin{\mathpalette\make@circled{\#}}_{\mathbf{PAT}_{\mathbf{S}}}\).

For \(a\in\mathsf{Act}(t)\) and \(b\in\mathsf{Act}(t')\), there exists a confliction relation \(a\sharp b\) in the tree \(t\parallel_{\mathbf{PAT}_{\mathbf{S}}}t'\) (resp. \(t\mid_{\mathbf{PAT}_{\mathbf{S}}}t'\)), \(\Theta(t\parallel_{\mathbf{PAT}_{\mathbf{S}}}t')_{\mathbf{PAT}_{\mathbf{S}}}\) (resp. \(\Theta(t\mid_{\mathbf{PAT}_{\mathbf{S}}}t')_{\mathbf{PAT}_{\mathbf{S}}}\)) and \(\triangleleft_{\mathbf{PAT}_{\mathbf{S}}}\) rename \(\{s'|t(1)\xrightarrow{s}\xrightarrow{a}t(s')\}\) to \(1\)’s and remain the open nodes unchanged, and remain \(t'\) unchanged, or rename \(\{s'|t'(1)\xrightarrow{s}\xrightarrow{b}t'(s')\}\) to \(1\)’s and remain the open nodes unchanged, and remain \(t\) unchanged.

For \(a\in\mathsf{Act}(t)\) and \(b\in\mathsf{Act}(t')\), there exists an internal confliction relation \(a\mathbin{\mathpalette\make@circled{\#}}b\) in the tree \(t\parallel_{\mathbf{PAT}_{\mathbf{S}}}t'\) (resp. \(t\mid_{\mathbf{PAT}_{\mathbf{S}}}t'\)), \(\Theta(t\parallel_{\mathbf{PAT}_{\mathbf{S}}}t')_{\mathbf{PAT}_{\mathbf{S}}}\) (resp. \(\Theta(t\mid_{\mathbf{PAT}_{\mathbf{S}}}t')_{\mathbf{PAT}_{\mathbf{S}}}\)) and \(\triangleleft_{\mathbf{PAT}_{\mathbf{S}}}\) rename \(\{s'|t(1)\xrightarrow{s}\xrightarrow{a}t(s')\}\) to \(1\)’s and remain the open nodes unchanged, and remain \(t'\) unchanged, or rename \(\{s'|t'(1)\xrightarrow{s}\xrightarrow{b}t'(s')\}\) to \(1\)’s and remain the open nodes unchanged, and remain \(t\) unchanged.

6.4 Axiomatic Semantics↩︎

The proof system \(\mathbf{\Omega DED}(E^2_{\mathbf{S}})\) contains the inequations denoted \(E^2_{\mathbf{S}}\), which include \(E^1_{\mathbf{S}}\) in 5.5 and the inequations in 2. Note that, since the inequation \(\Omega\leq x\) is inherited from any proof system containing \(\Omega\) \(\mathbf{\Omega DED}\), the inequation \(\Omega2\) is redundant.

6.5 The Trinity↩︎

The proof system \(\mathbf{\Omega DED}(E^2)\) contains the inequations denoted \(E^2\), which include \(E^1\) in 5.4 and the inequations in 2.

The proof system \(\mathbf{\Omega DED}(E^2_{\mathbf{W}})\) contains the inequations denoted \(E^2_{\mathbf{W}}\), which include \(E^1_{\mathbf{W}}\) in 5.5 and the inequations in 2.

7 Recursion↩︎

In this chapter, we introduce the basic processes with recursion. Firstly, we introduce the recursive signature in 7.1, then the operational semantics and axiomatic semantics of the recursive processes are introduced in 7.2 and 7.3, respectively. Finally, we get the results on trinity of operational semantics, denotational semantics and axiomatic semantics in 7.4.

7.1 Recursive Signature↩︎

The set of recursive terms over \(\Sigma^3\) is denoted \(REC_{\Sigma^3}(X)\), sometimes we only write \(REC_{\Sigma}(X)\). We write \(FREC_{\Sigma}(X)\) to denote the subset of terms in \(REC_{\Sigma}(X)\) without occurrences of \(rec~x.\). We use \(FV(t)\) to denote the set of variables which occur free in term \(t\) and \(BV(t)\) to denote the set of variables which occur bound in \(t\). We use \(REC_{\Sigma}\) to denote the set of closed terms and \(FREC_{\Sigma}\) to denote the set of finite closed terms.

A substitution \(\sigma\) will mean a mapping from \(X\) to \(REC_{\Sigma}(X)\), i.e., \(\sigma[x\rightarrow t]\) is a substitution which maps \(x\) to \(t\), and \(I\) denotes the identity substitution which maps every variable \(x\) to itself. We write \(t\sigma\) to denote the result of applying \(\sigma\) to \(t\). If \(x\) is a variable, \(t\) a term, \(\sigma\) a substitution, let \(new~xt\sigma\) denote the least variable \(y\) in the enumeration of \(X\) such that for every \(z\in FV(t)\) which is different from \(x,y\notin FV(\sigma(z))\).

The meaning in a \(\Sigma\)-domain of a term is taken to be the limit of the meaning of its finite approximations. These approximations are defined by progressively expanding out recursive subterms as follows.

Let \(\mathrm{App}(t)=\{t^{n}|n\geq 0\}\), these approximations are related via the syntactic preorder \(\preceq\).

Let \(A\) be a \(\Sigma\)-domain and \(\sigma_A\) an \(A\)-assignment, which is a mapping from each variable \(x\in X\) to an element \(\sigma_A(x)\) of \(A\). Let \(ENV_{A}\) denote the collection of \(A\)-assignments. Sometimes, we only write \(\sigma\) for \(\sigma_A\) and \(ENV\) for \(ENV_A\). \(ENV_A\) can be ordered pointwise via: \(\sigma\leq\sigma'\) if for every \(x\in X\), \(\sigma(x)\leq_A\sigma'(x)\). If \(A\) is a domain, \(ENV_A\) under this ordering is a domain. For \(Y\subseteq X\), we write \(\sigma_A=_{Y}\sigma'_{A}\) if \(\sigma_A(y)=_{A}\sigma'_{A}(y)\) for every \(y\in Y\) and \(\sigma_A\leq_{Y}\sigma'_{A}\) if \(\sigma_A(y)\leq_{A}\sigma'_{A}(y)\) for every \(y\in Y\).

Let \(A\llbracket \rrbracket:T_{\Sigma}(X)\rightarrow(ENV_{A}\rightarrow A)\) which is a function be defined by:

1. \(A\llbracket x\rrbracket\sigma=\sigma(x)\).

2. \(A\llbracket f(\underline{t})\rrbracket\sigma=f_{A}(A\llbracket \underline{t}\rrbracket\sigma)\).

Let \(A\llbracket \rrbracket:REC_{\Sigma}(X)\rightarrow(ENV_{A}\rightarrow A)\) which is well-defined be extended by:

1. \(A\llbracket x\rrbracket\sigma=\sigma(x)\).

2. \(A\llbracket f(\underline{t})\rrbracket\sigma=f_{A}(A\llbracket \underline{t}\rrbracket\sigma)\).

3. \(A\llbracket rec~x.t\rrbracket\sigma=Y\lambda a.A\llbracket t\rrbracket\sigma[a/x]\), where \(a\in A\), \(Y\) is the least fixpoint operator.

A function \(\varphi:REC_{\Sigma}(X)\rightarrow[ENV_{A}\rightarrow A]\) is reasonable if:

1. \(\varphi(rec~x.t)=\varphi(t[rec~x.t/x])\).

2. \(\varphi(t[u/x])\sigma=\varphi(t)\sigma[\varphi(u)\sigma/x]\).

7.2 Operational Semantics↩︎

In this section, we give the operational semantics of the language \(\mathbf{M}_3\). The predicate \(\surd\) represents successful termination, \(\xrightarrow{a}\surd\) represents successful termination after execution of the action \(a\in\mathsf{Act}\), \(\xrightarrow{U}\surd\) represents successful termination after execution of the action \(U\in\mathsf{Pom}\) and \(\xrightarrow{ }\surd\) represents successful termination without execution of the any action. The divergence predicate \(p\uparrow\) represents that \(p\) is divergent, i.e., \(p\) has an infinite internal computation, \[p\rightarrowtail p_0\rightarrowtail p_1\rightarrowtail\cdots\rightarrowtail p_k\rightarrowtail\cdots\] While the convergence predicate \(p\downarrow\) represents that \(p\) is not divergent \(p\nuparrow\), i.e., convergent, \(p\) has no infinite internal computation. The following are the PTSS of the language \(\mathbf{M}_3\), where \(p,q\in\mathsf{Proc}\).

The PTSS of \(\Omega\) is as follows.

\[\frac{}{\Omega\uparrow}\] \[\frac{}{\Omega\rightarrowtail\Omega}\]

The PTSS of action \(1\), \(a\in\mathsf{Act}\) and \(U\in\mathsf{Pom}\) is as follows. Note that, there is no any transition rules for \(0\).

\[\frac{}{0\downarrow}\quad\frac{}{1\downarrow}\quad \frac{}{a\downarrow} \quad\frac{}{U\downarrow}\] \[\frac{}{1\xrightarrow{ }\surd}\quad\frac{}{a\xrightarrow{a}\surd}\quad\frac{}{U\xrightarrow{U}\surd}\]

The PTSS of sequential composition is as follows.

\[\frac{p\downarrow\quad q\downarrow}{p\cdot q\downarrow}\] \[\frac{p\xrightarrow{U}\surd}{p\cdot q\xrightarrow{U} q}\quad\frac{p\xrightarrow{U}p'}{p\cdot q\xrightarrow{U} p'\cdot q}\]

The PTSS of alternative composition is as follows.

\[\frac{q\downarrow\quad q\downarrow}{p+q\downarrow}\] \[\frac{p\xrightarrow{U}\surd}{p+ q\xrightarrow{U}\surd} \quad\frac{p\xrightarrow{U}p'}{p+ q\xrightarrow{U}p'} \quad\frac{q\xrightarrow{U}\surd}{p+ q\xrightarrow{U}\surd} \quad\frac{q\xrightarrow{U}q'}{p+ q\xrightarrow{U}q'}\]

The PTSS of concurrent composition is as follows.

\[\frac{p\downarrow\quad q\downarrow}{p\between q\downarrow}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'\between q'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\gamma(a,b)}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\between q\xrightarrow{\gamma(a,b)}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\gamma(a,b)}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\between q\xrightarrow{\gamma(a,b)}p'\between q'}\]

The PTSS of parallel composition is as follows.

\[\frac{p\downarrow\quad q\downarrow}{p\parallel q\downarrow}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\parallel q\xrightarrow{\langle\mskip-4mu|a,b|\mskip-4mu\rangle}p'\between q'}\]

The PTSS of communication merge is as follows.

\[\frac{p\downarrow\quad q\downarrow}{p\mid q\downarrow}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}\surd}{p\mid q\xrightarrow{\gamma(a,b)}\surd} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}\surd}{p\mid q\xrightarrow{\gamma(a,b)}p'}\] \[\frac{p\xrightarrow{a}\surd\quad q\xrightarrow{b}q'}{p\mid q\xrightarrow{\gamma(a,b)}q'} \quad\frac{p\xrightarrow{a}p'\quad q\xrightarrow{b}q'}{p\mid q\xrightarrow{\gamma(a,b)}p'\between q'}\]

The PTSS of encapsulation operator is as follows.

\[\frac{p\downarrow}{\partial_H(p)\downarrow}\] \[\frac{p\xrightarrow{a}\surd\quad a\notin H}{\partial_H(p)\xrightarrow{a}\surd}\quad\frac{p\xrightarrow{a}p'\quad a\notin H}{\partial_H(p)\xrightarrow{a}\partial_H(p')}\]

The PTSS of confliction, confliction eliminator and the auxiliary unless operator is as follows, where \(\leq\) is the execution order.

\[\frac{p\downarrow}{\Theta(p)\downarrow}\quad\frac{p\downarrow\quad q\downarrow}{p\triangleleft q\downarrow}\] \[\frac{p\xrightarrow{a}\surd\quad a\sharp b}{\Theta(p)\xrightarrow{a}\surd} \quad\frac{p\xrightarrow{b}\surd\quad a\sharp b}{\Theta(p)\xrightarrow{b}\surd}\] \[\frac{p\xrightarrow{a}p'\quad a\sharp b}{\Theta(p)\xrightarrow{a}\Theta(p')} \quad\frac{p\xrightarrow{b}p'\quad a\sharp b}{\Theta(p)\xrightarrow{b}\Theta(p')}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad c\leq a}{p\triangleleft q\xrightarrow{c}\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad c\leq a}{p\triangleleft q\xrightarrow{c}p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\sharp b\quad b\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\sharp b\quad b\leq c}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad a\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\sharp b\quad a\leq c}{p\triangleleft q\xrightarrow{ }p'}\]

The PTSS of internal confliction, confliction eliminator and the auxiliary unless operator is as follows.

\[\frac{p\downarrow}{\Theta(p)\downarrow}\quad\frac{p\downarrow\quad q\downarrow}{p\triangleleft q\downarrow}\] \[\frac{p\xrightarrow{a}\surd\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{a}\surd} \quad\frac{p\xrightarrow{b}\surd\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{b}\surd}\] \[\frac{p\xrightarrow{a}p'\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{a}\Theta(p')} \quad\frac{p\xrightarrow{b}p'\quad a\mathbin{\mathpalette\make@circled{\#}}b}{\Theta(p)\xrightarrow{b}\Theta(p')}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad c\leq a}{p\triangleleft q\xrightarrow{c}\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad c\leq a}{p\triangleleft q\xrightarrow{c}p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{a}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad b\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{a}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{c}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad b\leq c}{p\triangleleft q\xrightarrow{ }p'}\] \[\frac{p\xrightarrow{c}\surd \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad a\leq c}{p\triangleleft q\xrightarrow{ }\surd} \quad\frac{p\xrightarrow{c}p' \quad q \ext@arrow 0055{ \slashedarrowfill@\relbar\relbar/\rightarrow}{}{b}\quad a\mathbin{\mathpalette\make@circled{\#}}b\quad a\leq c}{p\triangleleft q\xrightarrow{ }p'}\]

The PTSS of internal alternative composition is as follows.

\[\frac{p\downarrow\quad q\downarrow}{p\oplus q\downarrow}\] \[\frac{}{1\rightarrowtail\surd}\] \[\frac{}{p\oplus q\rightarrowtail p} \quad\frac{}{p\oplus q\rightarrowtail q}\] \[\frac{p\rightarrowtail p'}{p\cdot q\rightarrowtail p'\cdot q}\] \[\frac{p\rightarrowtail p'}{p+q\rightarrowtail p'+q} \quad\frac{q\rightarrowtail q'}{p+q\rightarrowtail p+q'}\] \[\frac{p\rightarrowtail p'}{p\between q\rightarrowtail p'\between q} \quad\frac{q\rightarrowtail q'}{p\between q\rightarrowtail p\between q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\between q\rightarrowtail p'\between q'}\] \[\frac{p\rightarrowtail p'}{p\parallel q\rightarrowtail p'\parallel q} \quad\frac{q\rightarrowtail q'}{p\parallel q\rightarrowtail p\parallel q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\parallel q\rightarrowtail p'\parallel q'}\] \[\frac{p\rightarrowtail p'}{p\mid q\rightarrowtail p'\mid q} \quad\frac{q\rightarrowtail q'}{p\mid q\rightarrowtail p\mid q'} \quad\frac{p\rightarrowtail p'\quad q\rightarrowtail q'}{p\mid q\rightarrowtail p'\mid q'}\] \[\frac{p\rightarrowtail p'}{\partial_H(p)\rightarrowtail \partial_H(p')}\] \[\frac{p\rightarrowtail p'}{\Theta(p)\rightarrowtail \Theta(p')}\] \[\frac{p\rightarrowtail p'}{p\triangleleft q\rightarrowtail p'\triangleleft q} \quad\frac{q\rightarrowtail q'}{p\triangleleft q\rightarrowtail p\triangleleft q'}\]

The PTSS of recursion is as follows.

\[\frac{t[rec~x.t/x]\downarrow}{rec~x.t\downarrow}\] \[\frac{}{rec~x.t\rightarrowtail t[rec~x.t/x]}\]

The divergence predicate and the convergence predicate can be relativized to sequences of pomsets by:

1. \(p\downarrow 1\) if \(p\downarrow\).

2. \(p\downarrow Us\) if \(p\downarrow\) and \(p\xRightarrow{U}p'\) implies \(p'\downarrow s\).

While \(p\uparrow s\) if \(p\ndownarrow s\).

7.3 Axiomatic Semantics↩︎

The following is the definition of \(\omega\)-Induction. The proof system \(\mathbf{rDED}(E)\)+\(\omega\)-Induction is denoted \(\mathbf{\omega DED}(E)\).

\[\omega-Induction\quad \frac{for every d\in\mathrm{App}(t),d\leq t'}{t\leq t'}\]

We use \(t\leq_{E}t'\), \(t\leq_{Er}t'\) and \(t\leq_{E\omega}t'\) to mean that \(t\leq t'\) is derivable in the appropriate proof system. And we use \(\vdash_{r}\) and \(\vdash_{\omega}\) for \(\vdash_{\mathbf{rDED}(\emptyset)}\) and \(\vdash_{\mathbf{\omega DED}(\emptyset)}\) respectively.

The following is the definition of Recursion Induction (RI).

\[RI\quad \frac{t[u/x]\leq u}{rec~x.t\leq u}\]

Let \(\underline{z}=\langle z_1,\cdots,z_k\rangle\) be \(k\) distinct variables and \(\underline{u}=\langle u_1,\cdots,u_k\rangle\) be \(k\) terms in \(REC_{\Sigma}(X)\) with the property that if \(z_i\in FV(u_j)\) then \(i=j\), i.e., \(\underline{u}\) is called noninterfering with respect to \(\underline{z}\). And we use \(rec~\underline{z}.\underline{u}\) to denote the sequence \(\langle rec~z_1.u_1,\cdots,rec~z_k.u_k\rangle\).

The following is the definition of Scott Induction (SI).

SI: Suppose \(\underline{u}\) is noninterfering with respect to \(\underline{z}\) which is a sequence of distinct variables, If:

1. \(\vdash t[\underline{\Omega}/\underline{z}]\leq t'[\underline{\Omega}/\underline{z}]\).

2. \(t\leq t'\vdash t[\underline{u}/\underline{z}]\leq t'[\underline{u}\leq\underline{z}]\).

then,

\(\vdash t[rec~\underline{z}.\underline{u}/\underline{z}]\leq t'[rec~\underline{z}.\underline{u}/\underline{z}]\).

Let \(\mathbf{PS}\) and \(\mathbf{PS}'\) be two proof systems, we say that \(\mathbf{PS}\) is at least as powerful as \(\mathbf{PS}'\), written \(\mathbf{PS}'\leq\mathbf{PS}\), if for every \(t,t'\in REC_{\Sigma}(X)\),

\(\vdash_{\mathbf{PS}'}t\leq t'\) implies \(\vdash_{\mathbf{PS}}t\leq t'\).

The following is the definition called Unique Fixpoint Induction (UFI).

\[UFI\quad \frac{t[u/x]=u}{rec~x.t=u}\]

UFI is unsound in general because it assumes every recursive equation always has a unique fixpoint. The guarded recursion has a unique fixpoint. In the guarded recursive equation \(x=t\), every occurrence of \(x\) in \(t\) is with a prefix \(U\cdot\).

7.4 The Trinity↩︎

8 Abstraction↩︎

In this chapter, we introduce abstraction. Firstly, we introduce the whole signature of this book in 8.1, then the operational semantics, axiomatic semantics and denotational semantics of the processes are introduced in 8.2, 8.3 and 8.4, respectively. Finally, we get the results on trinity of operational semantics, denotational semantics and axiomatic semantics in 8.5.

8.1 Whole Signature↩︎

8.2 Operational Semantics↩︎

The PTSSs of \(0\), \(1\), \(\Omega\), \(U\), \(\cdot\), \(+\), \(\sharp\), \(\oplus\), \(\mathbin{\mathpalette\make@circled{\#}}\), \(\parallel\), \(\mid\), \(\between\), \(\Theta\), \(\triangleleft\) and \(rec~x.p\) are same as the ones in 7.2. The PTSS of \(\mathrm{Abs}_I\) is as follows.

\[\frac{p\downarrow}{\mathrm{Abs}_I(p)\downarrow}\] \[\frac{p\rightarrowtail\surd}{\mathrm{Abs}_I(p)\rightarrowtail\surd}\quad\frac{p\rightarrowtail p'}{\mathrm{Abs}_I(p)\rightarrowtail \mathrm{Abs}_I(p')}\] \[\frac{p\xrightarrow{a}\surd\quad a\notin I}{\mathrm{Abs}_I(p)\xrightarrow{a}\surd}\quad\frac{p\xrightarrow{a}p'\quad a\notin I}{\mathrm{Abs}_I(p)\xrightarrow{a} \mathrm{Abs}_I(p')}\]

We continue to use the preorders \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}_{\mathrm{MUST}}\), \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}_{\mathrm{MAY}}\), \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}\) and \(\ll_{\mathrm{MUST}}\), \(\ll_{\mathrm{MAY}}\), \(\ll\), and we can get the alternative characterization theorem for \(\mathbf{M}_4\).

8.3 Axiomatic Semantics↩︎

Let \(\Sigma\) be an arbitrary signature containing \(\Sigma^1\), then \(REC_{\Sigma}\) contains \(\mathbf{M}_3\), which is given an operational semantics by extending that of \(\mathbf{M}_3\). We continue to use the preorders \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}_{\mathrm{MUST}}\), \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}_{\mathrm{MAY}}\), \(\mathrel{\ooalign{\raise 0.13ex\sqsubset\cr\hidewidth\raise-0.6ex\scalebox{0.9}{\sim}\hidewidth\cr}}\) and \(\ll_{\mathrm{MUST}}\), \(\ll_{\mathrm{MAY}}\), \(\ll\), and we can get the alternative characterization theorem like \(\mathbf{M}_4\) in 8.2. And \(E^2_{\mathbf{S}}\) is augmented to a new set of inequations \(E\), in the following way, the extended proof system \(\mathbf{\omega DED}(E)\) is sound and complete, i.e., by eliminating all occurrences of function symbols in \(\Sigma\) which are not in \(\Sigma^1\).

Now, let us apply the reduction theorem to \(\mathbf{M}_4\).

The proof system \(\mathbf{\omega DED}(E^4_{\mathbf{S}})\) contains the inequations denoted \(E^4_{\mathbf{S}}\), which include \(E^2_{\mathbf{S}}\) in 6.4 and the inequations in 3.

8.4 Denotational Semantics↩︎

Let \(\langle \mathbf{PAT}_{\mathbf{S}},\leq_{\mathbf{PAT}_{\mathbf{S}}},\Sigma^4\rangle\) be a domain, we need to show for each \(f\in\Sigma^4\) there is a continuous function \(f_{\Sigma^4}\) over \(\mathbf{PAT}_{\mathbf{S}}\). Such a domain is called an extension of \(\mathbf{PAT}_{\mathbf{S}}\) if for every \(f\in \Sigma^1\), \(f_{\Sigma^4}\) coincides with \(f_{\mathbf{PAT}_{\mathbf{S}}}\) defined in 6.

So, we only consider the new function symbols in \(\Sigma^4\), i.e., \(\mathrm{Abs}_I\).

\(\mathrm{Abs}_I(1)=1\)

\(\mathrm{Abs}_I(\langle\mskip-4mu|a,s|\mskip-4mu\rangle)=\begin{cases} \mathrm{Abs}_I(s), & a\in I;\\ \langle\mskip-4mu|a,\mathrm{Abs}_I(s)|\mskip-4mu\rangle, & otherwise. \end{cases}\)

\(\mathrm{Abs}_I(as)=\begin{cases} \mathrm{Abs}_I(s), & a\in I;\\ a\mathrm{Abs}_I(s), & otherwise. \end{cases}\)

Let \(\mathrm{Abs}_I(L)=\{\mathrm{Abs}_I(s)|s\in L\}\), \(\mathrm{Abs}_I(U)=U\setminus I\) for \(U\in\mathsf{Pom}\), \(\mathrm{Abs}_I(A)=A\setminus I\) for \(A\subseteq\mathsf{Act}\), and \(\mathrm{Abs}_I(\mathscr{A})=\{\mathrm{Abs}_I(A)|A\in\mathscr{A}\}\) for \(\mathscr{A}\) a collection of such sets \(A\).

Then the tree \(\mathrm{Abs}_I(t)\) is defined as:

1. \(L(\mathrm{Abs}_I(t))=\mathrm{Abs}_I(L(t))\).

2. \(CL(\mathrm{Abs}_I(t))=\mathrm{Abs}_I(CL(t))\).

3. \(\mathscr{A}(\mathrm{Abs}_I(t)(s))=\mathrm{Abs}_I(\mathscr{A}(t(s)))\).

8.5 The Trinity↩︎

The proof system \(\mathbf{\omega DED}(E^4)\) contains the inequations denoted \(E^4\), which include \(E^2\) in 6.5 and the inequations in 3.

The proof system \(\mathbf{\omega DED}(E^4_{\mathbf{W}})\) contains the inequations denoted \(E^4_{\mathbf{W}}\), which include \(E^2_{\mathbf{W}}\) in 6.5 and the inequations in 3.

References↩︎