The notion of Reactive Turing machine (RTM) was proposed as an orthogonal extension of Turing machines with interaction. RTMs are used to define the notion of executable transition system in the same way as Turing machines are used to define the notion of computable function on natural numbers. RTMs inherited finiteness of all sets involved from Turing machines, and as a consequence, in a single step, an RTM can only communicate elements from a finite set of data. Some process calculi, such as the $\pi$-calculus, essentially depend on an infinite alphabet of actions, and hence it immediately follows that transition systems specified in these calculi are not executable. On closer inspection, however, the $\pi$-calculus does not appear to use the infinite data in a non-computable manner.

In this paper, we investigate several ways to relax the finiteness requirement. We start by considering a variant of RTMs in which all sets are allowed to be countable, and we get a notion of infinitary RTM. Infinitary RTMs are extremely expressive such that we can hardly use them as a expressiveness criterion. Then, we refine the model by adding extra restrictions. As a result, we define a notion of RTM with atoms. It is a more restricted variant of RTMs in which the sets of actions and data symbols are still allowed to be infinite. We propose a notion of of nominal executability based on RTMs with atoms, and show that every effective transition system with atoms is nominally executable. It will follow that processes definable in the $\pi$-calculus are nominally executable. In contrast, in the process specification language mCRL2 it is possible to specify processes that are not nominally executable. Thus, nominal executability provides a new expressiveness criterion for process calculi.

§ INTRODUCTION

We should not literally copy (this much) text from another paper. Moreover, this is another paper, written with another goal and for another venue, so it should have another introduction.

I think we should rewrite as follows:

* Briefly introduce RTMs as a model that serves to define which behaviours (labelled transition systems) are executable. We can refer to [2] for more elaborate explantations and motivations. It is probably necessary to explain that the notion of executability is parameterised by the choice of a behavioural equivalence.

* Say that RTMs can be used to characterise the absolute expressiveness of process calculi. There are two interesting questions one might ask about a process calculus: (1) Is it possible to specify every executable behaviour in the process calculus?; and (2) Is every behaviour specified in the calculus executable. In [2], a one-to-one correspondence was established between the executable behaviours and the behaviours finitely definable (with a guarded recursive specification) in a process calculus with deadlock, a constant denoting successful termination, action prefix, non-deterministic choice, and parallel composition with handshaking communication; the result is up to divergence-preserving branching bisimilarity. In [16], it was established that every executable behaviour can be specified in the $\pi$-calculus.

* But it was also observed that $\pi$-calculus processes are generally not executable: The $\pi$-calculus presupposes an infinite set of names, which gives rise to an infinite set of action labels. It is straightforward to define $\pi$-calculus processes that, in fact, execute an unbounded number of distinct actions. The infinity of the set of names is essential in the $\pi$-calculus both for the mechanism by which input of data is modelled, and for the mechanism by which the notion of private link between processes is modelled. But, one may also argue that these reasons are more syntactic than semantic; the mechanisms themselves are not essentially infinitary. In [16] it was already argued that if one abstracts, to some extent, from the two aspects for which the infiniteness is needed, then behaviour defined in the $\pi$-calculus are executable, at least up to branching bisimilarity.

* Then we can explain the goal of this paper: We want to explore a generalised notion of executability that allows an infinite alphabet of actions.

* First, we shall observe that allowing an infinite alphabet only makes sense if we also allow the set of data symbols (or, equivalently, the set of states) to be infinite. Putting no restrictions at all yields a notion of executability that is not discriminating at all: every countable transition system is executable by an infinitary RTM. The result has two immediate corollaries: Every effective transition system is executable up to divergence-preserving branching bisimilarity by an infinitary RTM with an effective transition relation, and every computable transition system is executable up to divergence-preserving branching bisimilarity by an infinitary RTM with a computable transition relation.

* Then, we shall consider a more restricted notion of infinitary executability. We define RTMs with atoms as an extension of Turing machines with atoms [7]. RTMs with atoms allow the sets involved in the definition to be infinite, but in a limited way; intuitively, the infinity can only be exploited to implement the notions of freshness. We characterise the associated notion of executability.

* Finally (and some of the conclusions should still be drawn), we apply the results to draw conclusions about the executability of process calculi. We shall prove that all $\pi$-calculus processes are executable by RTMs with atoms up to branching bisimilarity. On the other hand, in mCRL2 it is possible to define behaviours that are not executable by RTMs with atoms. (It is important to contrast the two, because it shows the usefulness of the notion of RTM with atoms.)

The Turing machine [21] is a machine model that formalizes which functions from natural numbers to natural numbers are effectively computable. For a long time, computing functions in a stand-alone fashion was the primary task of computers, but nowadays modern computing systems continuously interact with their environment, and their operations are not supposed to terminate. However, Turing machines lack facilities to adequately deal with the above two important ingredients of modern computing: interaction and non-termination. In recent decades, quite a number of extended models of computation have been proposed to study the combination of computation and interaction (see, e.g., the collection [13]).

The notion of Reactive Turing machine [2] was proposed as an orthogonal extension of classical Turing machines with a facility to model interaction in the style of concurrency theory. It subsumes some other concurrent computation models such as the interactive Turing machines [17].

Reactive Turing machines serve to define which behaviours (labelled transition systems) can be executed by a computing system. We say that a transition system is executable if it is behaviourally equivalent to the transition system of a reactive Turing machine. Note that the notion of executability is parameterised by the choice of a behavioural equivalence: if a behaviour specified in a transition system is not executable up to some fine notion of behavioural equivalence (e.g., divergence-preserving branching bisimilarity), it may still be executable up to some coarser notion of behavioural equivalence (e.g., the divergence-insensitive variant of branching bisimilarity). The entire spectrum of behavioural equivalences [10] is at our disposal to draw precise conclusions.

RTMs can be used to characterise the absolute expressiveness of process calculi. In the theory of executability, we ask two interesting questions about a process calculus.

* Is it possible to specify every executable behaviour in the process calculus?

* Is every behaviour specified in the calculus executable?

A one-to-one correspondence was established between the executable behaviours and the behaviours finitely definable (with a guarded recursive specification) in a process calculus with deadlock, a constant denoting successful termination, action prefix, non-deterministic choice, and parallel composition with handshaking communication; the result is up to divergence-preserving branching bisimilarity [2]. It was established that every executable behaviour can be specified in the $\pi$-calculus up to divergence-preserving branching bisimilarity [16].

But it was also observed that $\pi$-calculus processes are generally not executable: The $\pi$-calculus presupposes an infinite set of names, which gives rise to an infinite set of action labels. It is straightforward to define $\pi$-calculus processes that, in fact, execute an unbounded number of distinct actions. The infinity of the set of names is essential in the $\pi$-calculus, both for the mechanism by which input of data is modelled, and for the mechanism by which the notion of private link between processes is modelled. But, one may also argue that these reasons are more syntactic than semantic; the mechanisms themselves are not essentially infinitary. It was already argued that if one abstracts, to some extent, from the two aspects for which the infiniteness is needed, then behaviour defined in the $\pi$-calculus are executable, at least up to branching bisimilarity [16].

Moreover, a notable number of process calculi leading to transition systems with infinite sets of labels were proposed for various purposes, for instance, the psi-calculus [4], the value-passing calculus [8] and mCRL2 [14]. We extend the formalism of reactive Turing machines to adapt to the behaviour with infinite sets of labels such as the transition systems of the models mentioned above.

In this paper, we shall first explore a generalised notion of executability based on Reactive Turing Machines that allows an infinite alphabet of actions. First, we shall observe that allowing an infinite alphabet only makes sense if we also allow the set of data symbols (or, equivalently, the set of states) to be infinite. Putting no restrictions at all yields a notion of executability that is not discriminating at all: every countable transition system is executable by an infinitary RTM. The result has two immediate corollaries: Every effective transition system is executable modulo divergence-preserving branching bisimilarity by an infinitary RTM with an effective transition relation, and every computable transition system is executable modulo divergence-preserving branching bisimilarity by an infinitary RTM with a computable transition relation.

Then, we shall consider a more restricted notion of infinitary executability. Following the research about nominal sets for variable binding with infinite alphabets [9], the notion of Turing machine with atoms was introduced [7]. We define RTMs with atoms as an extension of Turing machines with atoms. RTMs with atoms allow the sets involved in the definition to be infinite, but in a limited way; intuitively, the infinity can only be exploited to generate fresh names in an execution. By using the notion of legal and orbit-finite set, the Turing machines with atoms are allowed to have infinite alphabets, and while keeping the transition relation finitely definable and finite up to atom automorphism. We say a transition system is nominally executable if it is branching bisimilar to a transition system associated with an RTM with atoms.

To characterise the notion of nominal executability, we propose a notion of transition system with atoms as a restricted version of transition systems. We show that every effective transition system with atoms is nominally executable. Moreover, we also conclude that the transition systems associated with an  is an effective transition system with atoms. Therefore, nominally executable transition systems exactly equals to the effective transition systems with atoms.

Finally, we apply the results to draw conclusions about the executability of process calculi. We shall prove that all $\pi$-calculus processes are nominally executable. On the other hand, in mCRL2 it is possible to define behaviours that are not nominally executable.We also show that behaviours definable in mCRL2 are executable by infinitary RTMs, but the RTMs do not necessarily have an effective transition relation. Therefore, nominal executability provides a new expressiveness criterion for process calculi involving infinite alphabets.

The paper is organized as follows. In Section <ref>, the basic definitions of executability are recapitulated, and we also recall some theorems in [2, 16]. In Section <ref>, we investigate reactive Turing machines with infinite sets of labels, data symbols and transitions. In Section <ref>, we review the notion of set with atoms from [6, 7], propose the reactive Turing machines with atoms, and characterise the class of the transition systems that are nominally executable. In Section <ref>, the nominal executability of some process calculi involving infinite alphabets is discussed.
The paper concludes in Section <ref>, in which a hierarchy of executable transition systems with infinite sets is proposed.

We provide an Appendix with the definitions from other works, detailed examples and proofs. A full version of this submission is available on arxiv <cit.>.

§ PRELIMINARIES

In this section, we briefly recap the theory of executability [2], which is based on RTMs in which all sets involved are finite. We shall generalise the finiteness condition for the sets in later sections.

*The behaviour of discrete-event systems

We use the notion of transition system to represent the behaviour of discrete-event systems. It is parameterised by a set $\A$ of action symbols, denoting the observable events of a system. We shall later impose extra restrictions on $\A$, e.g., requiring that it be finite or have a particular structure, but for now we let $\A$ be just an arbitrary abstract set. We extend $\A$ with a special symbol $\tau$, which intuitively denotes unobservable internal activity of the system. We shall abbreviate $\A \cup\{\tau\}$ by $\Atau$.

An $\Atau$-labelled transition system is a triple $(\Sta,\step{},\uparrow)$, where,

* $\Sta$ is a set of states,

* ${\step{}}\subseteq\Sta\times\Atau\times\Sta$ is an $\Atau$-labelled transition relation (we write $s\step{a} t$ for$(s,a,t)\in{\step{}}$), and

* ${\uparrow}\in\Sta$ is the initial state.

In this paper, we shall use the notion of (divergence-preserving) branching bisimilarity [12, 11], which is the finest behavioural equivalence in van Glabbeek's linear time - branching time spectrum [10]. (We put the definition in Appendix <ref>.) We denote branching bisimilarity by $\bbisim$ and divergence-preserving branching bisimilarity by $\bbisimd$.

In the definition of (divergence-preserving) branching bisimilarity we need the following notation: let $\step{}$ be an $\Atau$-labelled transition relation on a set $\Sta$, and let $a\in\Atau$; we write $s\step{(a)}t$ for “$s\step{a}t$ or $a=\tau$ and $s=t$”. Furthermore, we denote the transitive closure of $\step{\tau}$ by $\step{}^{+}$ and the reflexive-transitive closure of $\step{\tau}$ by $\step{}^{*}$.

Let $T_1=(\Sta_1,\step{}_1,\uparrow_1)$ and $T_2=(\Sta_2,\step{}_2,\uparrow_2)$ be $\Atau$-labelled transition systems. A branching bisimulation from $T_1$ to $T_2$ is a binary relation $\R\subseteq\Sta_1\times\Sta_2$ such that for all states $s_1$ and $s_2$, $s_1\R s_2$ implies

* if $s_1\step{a}_1s_1'$, then there exist $s_2',s_2''\in\Sta_2$, such that $s_2\step{}_2^{*}s_2''\step{(a)}s_2'$, $s_1\R s_2''$ and $s_1'\R s_2'$;

* if $s_2\step{a}_2s_2'$, then there exist $s_1',s_1''\in\Sta_1$, such that $s_1\step{}_1^{*}s_1''\step{(a)}s_1'$, $s_1''\R s_2$ and $s_1'\R s_2'$.

The transition systems $T_1$ and $T_2$ are branching bisimilar (notation: $T_1\bbisim T_2$) if there exists a branching bisimulation $\R$ from $T_1$ to $T_2$ s.t. $\uparrow_1\R\uparrow_2$.

A branching bisimulation $\R$ from $T_1$ to $T_2$ is divergence-preserving if, for all states $s_1$ and $s_2$, $s_1\R s_2$ implies

* if there exists an infinite sequence $(s_{1,i})_{i\in\mathbb{N}}$ such that $s_1=s_{1,0},\,s_{1,i}\step{\tau}s_{1,i+1}$ and $s_{1,i}\R s_2$ for all $i\in\mathbb{N}$, then there exists a state $s_2'$ such that $s_2\step{}^{+}s_2'$ and $s_{1,i}\R s_2'$ for some $i\in\mathbb{N}$; and

* if there exists an infinite sequence $(s_{2,i})_{i\in\mathbb{N}}$ such that $s_2=s_{2,0},\,s_{2,i}\step{\tau}s_{2,i+1}$ and $s_1\R s_{2,i}$ for all $i\in\mathbb{N}$, then there exists a state $s_1'$ such that $s_1\step{}^{+}s_1'$ and $s_1'\R s_{2,i}$ for some $i\in\mathbb{N}$.

The transition systems $T_1$ and $T_2$ are divergence-preserving branching bisimilar (notation: $T_1\bbisimd T_2$) if there exists a divergence-preserving branching bisimulation $\R$ from $T_1$ to $T_2$ such that $\uparrow_1\R\uparrow_2$.

*A theory of executability

The notion of reactive Turing machine (RTM) [1, 2] was put forward to mathematically characterise which behaviours are executable by a conventional computing system. In this section, we recall the definition of RTMs and the ensued notion of executable transition system. The definition of RTMs is parameterised with the set $\Atau$, which we  now assume to be a finite set. Furthermore, the definition is parameterised with another finite set $\D$ of data symbols. We extend $\D$ with a special symbol $\Box\notin\D$ to denote a blank tape cell, and denote the set $\D\cup\{\Box\}$ of tape symbols by $\Dbox$.

A reactive Turing machine (RTM) is a triple $(\Sta,\step{},\uparrow)$, where

* $\Sta$ is a finite set of states,

* ${\step{}}\subseteq \Sta\times\Dbox\times\Atau\times\Dbox\times\{L,R\}\times\Sta$ is a finite collection of $(\Dbox\times\Atau\times\Dbox\times\{L,R\})$-labelled transition relation (we write $s\step{a[d/e]M}t$ for $(s,d,a,e,M,t)\in{\step{}}$),

* ${\uparrow}\in\Sta$ is a distinguished initial state.

Intuitively, the meaning of  a transition $s\step{a[d/e]M}t$ is that whenever the RTM is in state $s$, and $d$ is the symbol currently read by the tape head, then it may execute the action $a$, write symbol $e$ on the tape (replacing $d$), move the read/write head one position to the left or to the right on the tape (depending on whether $M=L$ or $M=R$), and then end up in state $t$. To formalise this intuitive understanding of the operational behaviour of RTMs, we associate with every RTM $\M$ an $\Atau$-labelled transition system  $\T(\M)$. The states of $\T(\M)$ are the
configurations of $\M$, which consist of a state from $\Sta$, its tape contents, and the position of the read/write head.
We denote by $\check{\Dbox}=\{\check{d}\mid d\in\Dbox\}$ the set of marked symbols; a tape instance is a sequence $\delta\in(\Dbox\cup\check{\Dbox})^{*}$ such that $\delta$ contains exactly one element of the set of marked symbols $\check{\Dbox}$, indicating the position of the read/write head.
We adopt a convention to concisely denote an update of the placement of the tape head marker. Let $\delta$ be an element of $\Dbox^{*}$. Then by $\tphdL{\delta\,}$ we denote the element of $(\Dbox\cup\check{\Dbox})^{*}$ obtained by placing the tape head marker on the right-most symbol of $\delta$ (if it exists), and $\check{\Box}$ otherwise.
Similarly $\tphdR{\,\delta}$ is obtained by placing the tape head marker on the left-most symbol of $\delta$ (if it exists), and $\check{\Box}$ otherwise.

Let $\M=(\Sta,\step{},\uparrow)$ be an RTM. The transition system $\T(\M)$ associated with $\M$ is defined as follows:

* its set of states is the set $\Conf[\M]=\{(s,\delta)\mid s\in\Sta,\ \text{$\delta$ a tape instance}\}$ of all configurations of $\M$;

* its transition relation ${\step{}}\subseteq{\Conf[\M]\times\Atau\times\Conf[\M]}$ is the least relation satisfying, for all $a\in\Atau,\,d,e\in\Dbox$ and $\delta_L,\delta_R\in\Dbox^{*}$:

* $(s,\delta_L\check{d}\delta_R)\step{a}(t,\tphdL{\delta_L}e\delta_R)$ iff $s\step{a[d/e]L}t$, and

* $(s,\delta_L\check{d}\delta_R)\step{a}(t,\delta_L e{}\tphdR{\delta_R})$ iff $s\step{a[d/e]R}t$, and

* its initial state is the configuration $(\uparrow,\check{\Box})$.

Turing introduced his machines to define the notion of effectively computable function [21]. By analogy, the notion of RTM can be used to define a notion of executable behaviour. Usually, we shall be interested in the executability modulo (divergence-preserving) branching bisimilarity.

A transition system is executable modulo (divergence-preserving) branching bisimilarity if it is (divergence-preserving) branching bisimilarity to a transition system associated with some RTM.

A characterisation of executability modulo (divergence-preserving) branching bisimilarity is given that is independent of the notion of RTM [9].

In order to be able to recapitulate some results from our previous work [2, 16], we need the following definitions, pertaining to the recursive complexity and branching degree of transition systems.
Let $T=(\Sta,\step{},\uparrow)$ be a transition system. We say that $T$ is effective if ${\step{}}$ is a recursively enumerable set with respect to some suitable encoding (Gödel numbering). The mapping $\mathalpha{out}:\Sta\rightarrow 2^{\A_{\tau}\times\Sta}$ associates with every state its set of outgoing transitions, i.e., for all $s\in\Sta$, $\mathalpha{out}(s)=\{(a,t)\mid s\step{a}t\}$. We say that $T$ is computable if $\mathalpha{out}$ is a recursive function, again with respect to some suitable encoding. We call a transition system finitely branching if $\mathalpha{out}(s)$ is finite for every state $s$, and boundedly branching if there exists $B\in\mathbb{N}$ such that $|\mathalpha{out}(s)|\leq B$ for all $s\in \Sta$.

The following results were established to characterise the notion of executability [2].

* For every finite set $\Atau$ and every boundedly branching computable $\Atau$-labelled transition system $T$, there exists an RTM $\M$ such that $T\bbisimd \T(\M)$.

* For every finite set  $\Atau$ and every effective $\Atau$-labelled transition system $T$ there exists an RTM $\M$ such that $T\bbisim \T(\M)$.

Moreover, if a transition system without divergence is executable modulo $\bbisimd$, then it is necessarily boundedly branching [16].

If a transition system $T$ has no divergence up to $\bbisimd$ and is unboundedly branching up to $\bbisimd$, then it is not executable modulo $\bbisimd$.

§ INFINITARY REACTIVE TURING MACHINES

In this section, we shall investigate the effect of lifting one or more of the finiteness conditions imposed on RTMs on the ensued notion of executability. We start with lifting the finiteness condition on the alphabet of actions and the transition relation only. We shall argue by means of an example that this extension is hardly useful, because it is not possible to associate a different effect with each action. The next step is, therefore, to also allow an infinite set of data symbols. This, in turn, yields a notion of executability that is too expressive. Finally, we provide two intermediate notions of executability by restricting the transition relations associated with infinitary reactive Turing machines to be effective or computable. In this section, we allow $\A$ to be a countably infinite set of action labels.

*Infinitely many states or data symbols

Recall from Definition <ref> that an RTM has a finite set of states $\Sta$ and a finite transition relation. If we allow RTMs to have infinitely many actions, then, inevitably, we should at least also allow them to have an infinite transition relation. The following example illustrates that we then also either need infinitely many states or infinitely many data symbols.

Consider an $\Atau$-labelled transition system $T=(\Sta_T,\step{}_T,\uparrow_T)$, where

* ${\Sta_T}=\{\uparrow_T,\downarrow_T\}\cup\{s_x\mid x\in\A\}$, and

* ${\step{}_T}=\{(\uparrow_T,x,s_x)\mid x\in\A\}\cup\{(s_x,x,\downarrow_T)\mid x\in\A\}$.

There does not exist an RTM with finitely many states and data symbols that simulates $T$ modulo branching bisimilarity.

Suppose $\M=(\Sta,\step{},\uparrow)$ is an RTM such that $\T(\M)\bbisim T$, and we let $\A=\{x_1,x_2,\ldots\}$.

The transitions $\uparrow_T\step{x_1}s_{x_1},\,\uparrow_T\step{x_2}s_{x_2},\ldots$ lead to infinitely many states $s_{x_1},s_{x_2},\ldots$, which are all mutually distinct modulo branching bisimilarity.

Let $C=(\uparrow,\tphd{\Box})$ be the initial configuration of $\M$. Assume that we have $C\bbisim \uparrow_T$, so $C$ admits the following transition sequences: $C\step{}^{*}\step{x_1}\step{}^{*}C_1\step{x_1},\,C\step{}^{*}\step{x_2}\step{}^{*}C_2\step{x_2},\ldots$, where $C_1\bbisim s_{x_1},\,C_2\bbisim s_{x_2},\ldots$.

The transitions of an RTM are of the form $(s,a,d,e,M,t)$, where $s,\,t\in\Sta$, and $d,\,e\in\Dbox$; we call the pair $(s,d)$ the trigger of the transition. A configuration $(s',\delta_L\tphd{d'}\delta_R)$ satisfies the trigger $(s,d)$ if $s=s'$ and $d=d'$. Now we observe that a transition $(s,a,d,e,M,t)$ gives
rise to an $a$-transition from every configuration satisfying its trigger $(s,d)$. Since $\Sta$ and $\Dbox$ are finite sets, there are finitely many triggers.

So, in the infinite list of configurations $C_1,C_2,\ldots$, there are at least two configurations $C_i$ and $C_j$, satisfying the same trigger $(s,d)$; these configurations must have the same outgoing transitions.

Now we argue that we cannot have $C_i\bbisim s_{x_i}$ and $C_j\bbisim s_{x_j}$. Since $C_j\step{x_j}$, a transition labelled by $x_j$ is triggered by $(s,d)$. As $C_i$ also satisfies the trigger $(s,d)$, we have the transition $C_i\step{x_j}$. Hence $C_i\not\bbisim s_{x_i}$, and we get a contradiction to $\T(\M)\bbisim T$.

*Infinitary reactive Turing machines

If we allow the set of control states or the set of data symbols to be infinite too, the expressiveness of RTMs is greatly enhanced. We introduce a notion of infinitary RTM as follows.

An infinitary reactive Turing machine () is a triple $(\Sta,\step{},\uparrow)$, where

* $\Sta$ is a countable set of states,

* ${\step{}}\subseteq \Sta\times\Dbox\times\Atau\times\Dbox\times\{L,R\}\times\Sta$ is a countable collection of $(\Dbox\times\Atau\times\Dbox\times\{L,R\})$-labelled transition relation (we write $s\step{a[d/e]M}t$ for $(s,d,a,e,M,t)\in{\step{}}$),

* ${\uparrow}\in\Sta$ is a distinguished initial state.

*Executability by an

By analogy to Definition <ref>, we define the executability with respect to s.

A transition system is executable by an  modulo (divergence-preserving) branching bisimilarity if it is (divergence-preserving) branching bisimilar to a transition system associated with some .

The following theorem illustrates the expressiveness of s, showing that every countable transition system is executable by an  modulo $\bbisimd$. (We put the proof in Appendix <ref>.)

For every countable set $\Atau$ and every countable $\Atau$-labelled transition system $T$, there exists an  $\M$ such that $T\bbisimd \T(\M)$.

Let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be an $\Atau$-labelled countable transition system, and let $\encode{\_}: \Sta_T\rightarrow \mathbb{N}$ be an injective function encoding its states as natural numbers. Then, an RTM with infinite sets of action symbols and data symbols $\M(T)=(\Sta,\step{},\uparrow)$ is defined as follows.

* $\Sta=\{s,t,\uparrow\}$ is the set of control states.

* $\step{}$ is a finite $(\Dbox\times\A\times\Dbox\times\{L,R\})$-labelled transition relation, and it consists of the following transitions:

* $(\uparrow,\tau,\Box,\encode{\uparrow_T},R,s)$,

* $(s,\tau,\Box,\Box,L,t)$, and

* $(t,a,\encode{s_1},\encode{s_2},R,s)$ for every transition $s_1\step{a}_T s_2$.

* ${\uparrow}\in\Sta$ is the initial state.

Note that a transition step $s_1\step{a}s_2$ is simulated by a sequence

\begin{equation*}
\enskip.
\end{equation*}

Then one can verify that $\T(\M(T))\bbisimd T$.

So s are very expressive, and they certainly do not yield a useful model to distinguish between processes that can and cannot be executed. Note that the transition relation used to define s need not even be computable or effective. As a compromise, we provide two intermediate models by making requirements on the transition relation of s.

We say that a transition relation is effective, if for every pair of a control state and a data symbol $(s,d)$, the set of subsequent transitions is recursively enumerable, i.e., the set $\{(a,e,M,t)\mid s\step{a[d/e]M}t\}$ is recursively enumerable with respect to some encoding. By the proof of Theorem <ref>, if the transition system is effective, then the set of transitions $\{(t,a,\encode{s_1},\encode{s_2},R,s)\mid s_1\step{a} s_2\}$ is recursively enumerable. One may trivially verify that all the other transitions are also recursively enumerable. Hence, we get an effective transition relation. We derive the following corollary for the executability of effective transition systems from Theorem <ref>.

For every countable set $\Atau$ and every effective $\Atau$-labelled transition system $T$, there exists an  $\M$ with an effective transition relation such that $T\bbisimd \T(\M)$.

We say that a transition relation is computable if for every pair of a control state and a data symbol $(s,d)$ the set of subsequent transitions is computable, i.e., the set $\{(a,e,M,t)\mid s\step{a[d/e]M}t\}$ is recursive with respect to some encoding. By analogy to Corollary <ref>, we derive the following result.

By the proof of Theorem <ref>, if the transition system is computable, then the set of transitions $\{(t,a,\encode{s_1},\encode{s_2},R,s)\mid s_1\step{a} s_2\}$ becomes recursive. For the other transitions, they are also trivially recursive. Hence, we get a computable transition relation. Then from Theorem <ref> we also derive a corollary for the executability of computable transition systems.

For every countable set $\Atau$ and every computable $\Atau$-labelled transition system $T$, there exists an  $\M$ with a computable transition relation such that $T\bbisimd \T(\M)$.

§ REACTIVE TURING MACHINES WITH ATOMS

In this section, we introduce a notion of reactive Turing machine with atoms () as a natural intermediate between RTMs and s. On the one hand, s will be more expressive than RTMs, since they will admit infinite alphabets, whereas RTMs do not. On the other hand, s will be less expressive than s, because there will be restrictions imposed that, intuitively, make the alphabets finitely representable. We introduce a notion of effective transition system with atoms to characterise the transition systems associated with s modulo branching bisimilarity. We then have a proper model to investigate the executability of process calculi with infinite alphabets (such as the $\pi$-calculus).

*Sets with atoms

We adopt the definition of sets with atoms from Bojańczyk et al. [6, 7]. We fix for the remainder of this section a countable infinite set $\Atom$; we call its elements atoms. An atom automorphism is a bijection (permutation) on $\Atom$. A set with atoms is any set that contains atoms or other sets with atoms, in a well-founded way. Every set in the traditional sense thus is a set with atoms. The atoms will allow us to formulate certain finiteness restrictions that are slightly more liberal than simply requiring that sets are finite. To this end we proceed to introduce legal and orbit-finite sets with atoms.

For a set with atoms $X$ and an atom automorphism $\pi$, by $\pi(X)$ we denote the set obtained by application of $\pi$ to every atom in $X$, in elements of $X$, in elements of elements of $X$, etc., recursively. For a set of atoms $S\subseteq\Atom$, if an atom automorphism $\pi$ is the identity on $S$, then we call it an $S$-automorphism. We say that $S$ supports a set with atoms $X$ if $X=\pi(X)$ for every $S$-automorphism $\pi$. A set with atoms is called legal if it has a finite support, each of its elements has a finite support, and so on recursively. A set with atoms may contain infinitely many atoms, but legality restricts the extent. For instance, a finite set is legal (with itself as support), and also a co-finite set is legal (with its finite complement as support). On the other hand, the set of all odd natural numbers is not legal (its support necessarily includes all odd numbers, or all even numbers).

Now we proceed to introduce the notion of orbit-finite set.  Let $x$ be an element in a set with atoms $X$, the orbit of $x$ is the set
\begin{equation*}
\{y\in X\mid y=\pi(x)\mbox{ for some atom automorphism }\pi\}
\enskip.
\end{equation*}

A set with atoms $X$ is partitioned into disjoint orbits: elements $x$ and $y$ are in the same orbit iff $\pi(x)=y$ for some atom automorphism $\pi$. For example $\Atom^{2}$ decomposes into two orbits, the diagonal and its complement; and $\Atom^{*}$ has infinitely many orbits as the elements from $\Atom,\,\Atom^{2},\ldots$ all fall into disjoint orbits. A set with atoms that is partitioned into finitely many orbits is called an orbit-finite set. Orbit-finiteness restricts the number of partitions of a set with atoms with respect to atom automorphism.

*Reactive Turing machines with atoms

Bojańczyk et al. [7] defined a notion of Turing machine with atoms based on sets with atoms. Now we generalize this notion by defining a notion of reactive Turing machine with atoms. We assume that the sets of action symbols $\Atau$ and data symbols $\Dbox$ are legal and orbit-finite sets with atoms.

A reactive Turing machine with atoms () $\M$ is a triple $(\Sta,\step{},\uparrow)$, where

* $\Sta$ is a legal and orbit-finite set of states,

* ${\step{}}\subseteq \Sta\times\Dbox\times\Atau\times\Dbox\times\{L,R\}\times\Sta$ is a legal and orbit-finite $(\Dbox\times\Atau\times\Dbox\times\{L,R\})$-labelled transition relation (we write $s\step{a[d/e]M}t$ for $(s,d,a,e,M,t)\in{\step{}}$),

* ${\uparrow}\in\Sta$ is a distinguished initial state.

By analogy to Definition <ref>, we associate with every  a labelled transition system, and define a notion of executability with respect to . In this paper, we shall only consider executability modulo branching bisimilarity.

A transition system is nominally executable if it is branching bisimilar to a transition system associated with some .

s give rise to a less liberal notion of executability compared to the one induced by s. The following example give us an insight in the effect of the legality restriction.

Assume that the set of atoms is the set of natural numbers. We consider a transition system only with the following transitions: $s_1\step{1}s_3\step{3}\ldots s_{2n+1}\step{2n+1}\ldots$. It can be simulated by an  with the following transition relation:

\begin{equation*}
\{(s,n,n,n+2,R,t)\mid n=2i+1\,\mbox{and}\, i\in \mathbb{N}\}
\enskip.
\end{equation*}

Either the set of odd numbers or the set of even numbers supports the above set, however, neither of them is finite. The above transition relation therefore cannot define an . Moreover, s cannot define any transition system with an illegal set of labels, since it is inevitable to introduce an illegal transition relation.

Besides legality, orbit-finiteness also restricts the notion of executability. The transitions are restricted to finitely many different orbits up to atom automorphism. As a result, s cannot make transitions labelled with tuples of atoms of arbitrary lengths, nevertheless, such transitions can be realized by an .

Consider an  with the following transition relation:

\begin{equation*}
\{(s,\bar{a},\Box,\bar{a},R,t)\mid \bar{a}\mbox{ is a tuple of atoms of arbitrary length}\}
\enskip.
\end{equation*}

The labels of the above transition relation are not orbit-finite, so it does not defines an .

*Transition systems with atoms

Next, we investigate the class of transition systems that are nominally executable. By Example <ref> and Example <ref>, we can easily exclude the transition systems with an illegal or a non-orbit-finite set of labels. We let $\Atau$ be a legal and orbit-finite set of labels for the remaining of this section. We define the notion of transition system with atoms as follows:

An $\Atau$-labelled transition system $T=(\Sta_T,\step{}_T,\uparrow_T)$ is a transition system with atoms if $\Sta_T$ and $\step{}_T$ are legal sets with atoms. We say that a transition system with atoms is $K$-supported if $K\subset\Atom$ and $K$ is a support of the sets $\Sta_T$ and $\step{}_T$.

We observe that a transition system with atoms $T=(\Sta_T,\step{}_T,\uparrow_T)$ is $K$-supported iff for every $(s,a,t)\in{\step{}_T}$ and for every $K$-automorphism $\pi_K$ we have $\pi_K(s,a,t)\in{\step{}_T}$, where $\pi_K(s,a,t)=(\pi_K(s),\pi_K(a),\pi_K(t))$.

* $\Rightarrow$: We suppose that $K$ is a support of $\step{}_T$, then by the definition of support, for every $K$-automorphism $\pi_K$, we have $\pi_K(\step{}_T)=\step{}_T$. Therefore, for every $(s,a,t)\in{\step{}_T}$, we have $\pi_K(s,a,t)\in{\step{}_T}$.

* $\Leftarrow$: We suppose that for every $(s,a,t)\in{\step{}_T}$ and for every $K$-automorphism $\pi_K$, we have $\pi_K(s,a,t)\in{\step{}_T}$ then we have $\pi_K(\step{}_T)=\step{}_T$, Therefore $K$ is a support of $\step{}_T$.

For example, the transition systems associated with $\pi$-calculus terms are transition systems with atoms by the structural operational semantics in Figure <ref>  in Appendix <ref>. We consider the set of names as the set of atoms and hence all the $\pi$-terms and transitions are sets with atoms. The support of the union of the transition systems associated with $\alpha$-equivalence class of the individual $\pi$-terms is the empty set. The support of the transition system associated with the $\alpha$-equivalence class of an individual $\pi$-term is the set of free names. Note that the set of free names does not grow by transition [20].

*Effective transition systems with atoms

In order to define the class of transition systems that can be simulated by s, we need a notion of effectiveness that ensures that the transitions of an effective transition system can be enumerated by an . A difficulty we face when defining an RTM with atoms that simulates a legal transition system with atoms
is that s are not capable, in general, of decoding an encoded set with atoms. In particular, if the  produces the code of a transition, then it cannot always compute the label of that transition. We illustrate this idea with a simple example.

Let $\encode{\_}:\Atom\rightarrow\mathbb{N}$ be an encoding from the set of atoms to natural numbers. Consider the a transition system with a sequence of transitions $\uparrow\step{\encode{x}}s_x\step{x}$ for every $x\in\Atom$, where $\step{\encode{x}}$ denotes a sequence of transitions with the encoding of $x$ as their labels.
There does not exist an  to simulate this transition system.

We suppose that an  $\M$ simulates the above transition system. Note that there are infinitely many $x\in\Atom$ that are not in the support of the $\M$. We choose an $x$ that is not in the support, then for any transition that writes $x$ on the tape or does an $x$-labelled transition from a configuration that does not involve $x$ on the tape, every $\pi(x)$ is created by another transition from that configuration, where $\pi$ is an arbitrary atom automorphism preserving the support of $\M$. Hence, $\M$ is not the required .

Rather than encoding the states and transitions of a transition system with atoms, orbits of states and transitions will be encoded. Effectiveness is defined on functions over natural numbers. In order to define the notion of effectiveness, we encode the structures (orbits) of sets with atoms into natural numbers by using the terminology of definable sets introduced by Bojańczyk [5].

Let $V$ be an countably infinite set of variables. We let $\bar{x}$ be a tuple of variables. An $\bar{x}$-valuation is a function that maps each variable in $\bar{x}$ to an element in $\Atom$. The notion of set builder expression is inductively defined as follows:

* The empty set $\emptyset$ is a set builder expression.

* A variable is a set builder expression.

* Let $\bar{x}$ and $\bar{y}$ be disjoint tuples of variables and let $\alpha$ be a set builder expression with free variables contained in $\bar{x}\bar{y}$, and let $\phi$ be a first-order formula over $\Atom$ and with free variables contained in $\bar{x}\bar{y}$. Then $\{\alpha(\bar{x}\bar{y})\mid\mbox{ for }\bar{y} \mbox{ such that }\phi(\bar{x}\bar{y})\}$ is a set builder expression with free variables $\bar{x}$ and bound variables $\bar{y}$. (This expression equals to the set $\{\alpha(\bar{x},\bar{a}) \mid \bar{a}\mbox{ is a tuple of atoms such that }\phi(\bar{x},\bar{a})\}$).

* If $\alpha_1,\ldots,\alpha_n$ are set builder expressions, then so is $\alpha_1\cup\cdots\cup\alpha_n$.

We use $\mathbb{B}$ to denote the set of all set builder expressions. For a set builder expression $\alpha$ with free variables $\bar{x}$, we define $\setb{\alpha}$ to be the function which inputs a valuation of $\bar{x}$ and outputs the corresponding set (or set of sets, etc.).

A set with atoms is definable if it is of the form $\setb{\alpha}(\bar{a})$, where $\alpha$ is a set builder expression and $\bar{a}$ denotes an assignment of atoms to the free variables in $\alpha$.

We have the following lemma [5]:

Every legal set of $n$-tuples of atoms and every orbit-finite set with atoms is definable.

Taking the $\pi$-calculus as an example, the set of all $\pi$-terms is not definable, since it is not orbit-finite, in other words, infinitely many distinct structures are involved. However, the $\alpha$-equivalence class of a $\pi$-term is definable since it has only one orbit.

The transition systems associated mCRL2 expression is not necessarily definable. Consider a term that is able to input a string with arbitrary length, this term involves infinitely many distinct structures.

We introduce the encodings of set builder expressions.  We let $\encode{\_}: \mathbb{B}\rightarrow \mathbb{N}$ be an encoding from set builder expressions to natural numbers. Now we consider an arbitrary legal and orbit-finite set with atoms $x$. We let $\sete{x}$ be a set builder expression of $x$, and $\tup{x}$ be the tuple of atoms satisfying $\setb{\sete{x}}(\tup{x})=x$. In an , we use a pair of a natural number and a tuple of atoms to represent a set with atoms $x$, i.e., $x$ is represented by $\encode{\sete{x}}$ and $\tup{x}$.

To characterise the class of executable transition systems with atoms, we define a notion of effectiveness on transition systems with atoms on orbits of states and transitions up to atom automorphism.

Recall the notion of effective transition system: a transition system is effective, if, for every state, the set of its outgoing transitions is recursively enumerable. For transition systems with atoms, however, sets with atoms cannot be enumerated by s directly since the operation of enumerating atoms is not legal. Hence, we define the effectiveness on orbits of states and transitions up to atom automorphism.

Let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be a transition system with atoms. We say that $T$ is effective if it satisfies the following conditions:

* Every $s\in\Sta_T$ and every $(s,a,t)\in{\step{}_T}$ is orbit-finite.

* There exists a recursively enumerable function $\mathit{out}:\mathbb{N}\rightarrow\mathbb{N}$ satisfying:

\begin{equation*}
\forall s\in\Sta_T,\,\mathit{out}(\encode{\sete{s}})=\{\encode{\sete{(s,a,t)}}\mid s\step{a}_T t\}
\enskip.
\end{equation*}

Intuitively, a transition system with atoms is effective if there is an effective algorithm to enumerate the set builder expression of the set of outgoing transitions given the set builder expression of a state as the input. Moreover, it is necessary to enumerate the structure of the triple $(s,a,t)$  rather than $(a,t)$, since some variables in $\sete{s}$ might also appear in $\sete{a}$ and $\sete{t}$; the same atoms should be assigned to the variables in $e_s$, $e_a$, and $e_t$ in order to obtain a correct transition.

*Encoding sets with atoms

In order to simulate a transition system with atoms with an , we need to use an  to enumerate the transitions from every state of a transition system with atoms. To implement the procedure of enumeration, we need a schema to encode sets with atoms into natural numbers. Let $X$ be a countable set with atoms; an encoding is an injection $\encode{\_}: X\rightarrow \mathbb{N}$.

Now we consider an arbitrary legal set with atoms $X$, and fix a minimal support $K$ of $X$. Let $x\in X$ be an element of $X$. The $x$-orbit is the set $[x]=\{\pi_K(x)\mid \pi_K \mbox{ is a }K\mbox{-automorphism}\}$. Note that all the elements in the $x$-orbit are in the same equivalence class with $x$ up to atom automorphism.

We will encode an element of a set with atoms by its orbit and the atoms it uses. We presuppose that there exist a function $\atom$ and a set of functions $\{\orb_{[x]}\mid x\in X\}$ satisfying the properties below:

\begin{eqnarray*}
&\atom: X\rightarrow\Atom^{*},\,
\orb_{[x]}:\Atom^{*}\rightarrow [x],\, \mbox{satisfying that}:\\
&\forall y\in[x],\,
\orb_{[x]}(\atom(y))=y
\enskip.
\end{eqnarray*}

$\atom(x)$ associates with $x$ the atoms that are used in $x$. $\orb_{[x]}$ associates with a sequence of atoms $\atom(y)$ an element $y$ of the $x$-orbit. Note that we have:

\begin{equation*}
\forall x\in X,\,\forall K\mbox{-automorphism}\,\pi_K,
\orb_{[x]}(atom(\pi_K(x)))=\pi_K(x)
\enskip.
\end{equation*}

We can number every equivalence class (orbit) in $X$ by a natural number as $X$ is countable. We encode $\orb_{[x]}$ by an injection from the equivalence class of $x$ to the natural number that numbers $[x]$. We assume that there is an encoding from $\Atom$ to $\mathbb{N}$, and there is an encoding of lists. We encode $\atom(x)$ by the encoding of lists of encodings of atoms.
We define the encoding of an element $x$ by a pair consisting of the encoding of the function of $\orb_{[x]}$, and the encoding of the list of atoms $\atom(x)$ as follows:

\begin{equation*}
\encode{x}=\encode{(\encode{orb_{[x]}},\encode{atom(x)})}
\enskip.
\end{equation*}

We remark that if $X$ is, e.g., the set of labels of a $\pi$-calculus process, then one may derive $\atom$ and $\{\orb_{[x]}\mid x\in X\}$ as well as their encodings trivially.

Let us consider the transition relation, it could be interpreted as follows:

\begin{equation*}
\trans: \mathbb{N}\times\Atom^{*}\rightarrow\mathbb{N}\times\Atom^{*}\times\mathbb{N}\times\Atom^{*}
\enskip.
\end{equation*}

We formalise the following condition $\star$ for the $\Atau$-labelled transition system $T=(\Sta,\step{},\uparrow)$. The condition satisfies if there is a function $\supp:\Sta\rightarrow M$ where $M$ is a finite subset of $\Atom$, and we denote $\supp(s)$ by $M_s$. $\forall s\step{a} s_1$ the following properties holds:

\begin{equation*}
\forall M_s\mbox{-automorphism }\pi_{M_s},\,\exists s\step{\pi_{M_s}(a)} s_2,\,M_{s_2}=\pi_{M_s}(M_{s_1})
\enskip.
\end{equation*}

* Let $N(a)$ be the set of atoms appeared in $a$

\begin{equation*}
\forall M_s\cup N(a)\mbox{-automorphism }\pi_{M_s\cup N(a)},\,\exists s\step{\pi_{M_s\cup N(a)}(a)} s_3,\,M_{s_3}=\pi_{M_s\cup N(a)}(M_{s_1})
\enskip.
\end{equation*}

As we assign a set of atoms $M_s$ to every state $s$. We first investigate to what extent, an  can manipulate these sets.

Suppose that there is already a set of atoms $M_s$ written on the tape, and we design an  to create a new set $M_s'$ and write it on the tape. Then it may add either an atom from $M_s$ or an atom which is not from $M_s$. We discuss the two cases:

*Nominal executability

Now we show that every effective transition system with atoms is nominally executable.

The simulation of a transition from a state $s$ consists of three stages. In the initial stage, we suppose that the representation of the state $\encode{\sete{s}}\tup{s}$ is written on the tape. Then, the  enumerates the structure of an outgoing transition $\encode{\sete{(s,a,t)}}$ on the tape. In the second stage, the  compress from $\encode{\sete{(s,a,t)}}$ and $\tup{s}$ appropriate assignments to the variables in $\tup{a}$ and $\tup{t}$. Fresh atoms are created in this stage if necessary. In the final stage, the  uses $\encode{\sete{a}}$ and $\tup{a}$ to produce an $a$-labelled transition, leading to a configuration representing state $t$, or it returns to the initial stage and enumerates another transition. Note that an  cannot enumerate the outgoing transitions directly, rather, it enumerates the orbit of the transition and nondeterministically produces one of the elements in that orbit.

We use the encodings of set builder expressions to represent the structures of the sets with atoms, moreover, we also need a tuple of atoms to instantiate the free variables. Now we introduce some gadgets of s to manipulate tuples of atoms.

Let $\M=(\Sta_{\M},\step{}_{\M},\uparrow_{\M})$ be an . Then there exists a finite set of atoms $K\subset\Atom$ such that,
for every $(s,a,d,e,M,t)\in{\step{}_{\M}}$, and for every $K\mbox{-automorphism}\,\pi_K$, we have

As $\step{}_{\M}$ is a legal set. We take $K$ to be its the minimal support. Then we conclude the lemma from the definition of the support.

Let $\bar{a}$ and $\bar{b}$ be two tuples of atoms. We define an  (We put the details in Appendix <ref>.) $\M$ with $\bar{a}\bar{b}$ as its tape instance, and within finitely many steps of execution, it changes its tape instance by either:

* duplicating an atom $x$ from $\bar{a}$, and adding it to $\bar{b}$, or

* nondeterministically creating a fresh atom $x$ which is not in $\bar{a}$, and adding it to $\bar{b}$.

We denote the current tape instance by $\bar{a}\bar{b}$, and we show the two ways to add a new atom to $\bar{b}$.

For the first case, we suppose that $x$ is the atom in $\bar{a}$ to be duplicated, and the first empty cell after $\bar{b}$ is the destination of the duplication. The machine could accomplish the task by the transitions $\cop\step{\tau[x/x]R}\cop_x\step{\tau[y/y]R}{}^{*}\step{\tau[\Box/x]}\finish$, which is realized by the following set of transitions.

\begin{eqnarray*}
&\{(\cop,\tau,x,x,R,\cop_x)\mid x\in\Atom\}\\
&\cup\{(\cop_x,\tau,y,y,R,\cop_x)\mid x,y\in\Atom\}\\
&\cup\{(\cop_x,\tau,\Box,x,R,\finish)\mid x\in\Atom\}
\enskip.
\end{eqnarray*}

This is a legal and orbit-finite set of transitions.

For the second case, the machine creates a fresh atom, by the following set of transitions,

\begin{eqnarray*}
&\{(\fresh,\tau,\Box,x,L,\chec_x)\mid x\in\Atom\}\\
&\cup\{(\chec_x,\tau,y,y,L,\chec_x)\mid x\neq y\wedge y\neq \Box\wedge x,y\in\Atom\}\\
&\cup\{(\chec_x,\tau,x,x,L,\refresh_x)\mid x\in\Atom\}\\
&\cup\{(\refresh_x,\tau,y,y,R,\refresh_x)\mid x\neq y\wedge x,y\in\Atom\}\\
&\cup\{(\refresh_x,\tau,x,y,L,\chec_y)\mid x\neq y\wedge x,y\in\Atom\}\\
&\cup\{(\chec_x,\tau,\Box,\Box,R,\finish)\mid x\in\Atom\}
\enskip.
\end{eqnarray*}

The machine first creates an arbitrary atom $x$, and then it checks every atom on the tape whether it is identical with $x$. We suppose that $\Box$ indicates the end of the sequence of atoms on tape. If the check procedure succeeds, the creation is finished, otherwise, the machine creates another atom and checks again.
We also verify that the above transitions form a legal and orbit-finite set.

Next, we illustrate that an  is able to produce an $x$-labelled transition from the encoding of the its structure and the atoms used in $x$, if $x$ is from an orbit-finite set $X$.

Let $X$ be an arbitrary legal and orbit-finite set with atoms. We define an  (We put the details in Appendix <ref>.)  such that for any arbitrary $x\in X$, if $\encode{\sete{x}}$ and $\tup{x}$ are written on the tape in a configuration, then there is one and only one labelled transition reachable from that configuration, and the transition is labelled by $x$.

We define an  $M=(\Sta_M,\step{}_M,\uparrow_M)$, and we show that $M$ suffices the requirement.

According to the assumption, we suppose that in the state $\start$, the tape instance is $\encode{\sete{x}}\tup{x}$. It suffices to show that within finitely many steps, the machine is able to write $x$ as one symbol on the tape.

Note that $X$ is an orbit-finite set, which means that there are finitely many distinct orbits that construct the set $X$. Therefore, there are finitely many distinct values of $\encode{\sete{x}}$ for all the elements in $X$. The machine associates with each value a program that calculates $\setb{\sete{x}}(\tup{x})$, which produces the elements from that specific orbit according to the valuation of $\bar{x}$. The machine enters the programme by entering the state $\encode{\sete{x}}$.

\begin{equation*}
\{(\start,\tau,\encode{\sete{x}},\encode{\sete{x}},R,\encode{\sete{x}})\mid x\in X\}
\enskip.
\end{equation*}

As $X$ is orbit-finite, there is an upper-bound for the length of the tuple $\bar{x}$ for every $x\in X$. The machine can represent a tuple as a data symbol.
We suppose that every element in $x$-orbit uses $n$ free variables in its structure, then $\bar{x}$ is a tuple of $n$ atoms. Now we consider the following set of transitions:

\begin{equation*}
\{(\encode{\sete{x}},\setb{\sete{x}}(\tup{x}),\tup{x},\setb{\sete{x}}(\tup{x}),R,\finish\mid a_1\ldots a_n\in \Atom\}
\enskip.
\end{equation*}

These transitions will create $x$ by $\setb{\sete{x}}(\tup{x})$. We suppose that $\tup{x}$ is of the form $(a_1,\ldots,a_n)$. The above set of transitions is orbit-finite, since there is an upper bound of $n$,

Moreover, we show that the machine is able to create a tuple $\tup{x}$ as one symbol, given that each atom in $\tup{x}$ is written on one tape cell, and ordered from left to right as the order of the atoms in the tuple.

The machine constructs $\bar{x}$ by duplicating the elements from each tape cell to the tuple one by one, using the transitions as follows:

\begin{eqnarray*}
&\{(\encode{\sete{x}},\tau,a,a,R,(\encode{\sete{x}},a))\mid a\in\Atom\}\\
&\cup\{((\encode{\sete{x}},a),\tau,b,b,R,(\encode{\sete{x}},a))\mid a,b\in\Atom\}\\
&\cup\{((\encode{\sete{x}},a),\tau,\Box,(a),L,(\encode{\sete{x}},a)')\mid a\in\Atom\}\\
&\cup\{((\encode{\sete{x}},a_i),\tau,(a_1,\ldots,a_{i-1}),(a_1,\ldots,a_{i-1},a_i),L,(\encode{\sete{x}},a_i)')\mid a_1,\ldots, a_i\in \Atom, 2 \leq i\leq n\}\\
&\cup\{((\encode{\sete{x}},a)',\tau,b,b,L,(\encode{\sete{x}},a)')\mid a,b\in \Atom,\, a\neq b\}\\
&\cup\{((\encode{\sete{x}},a)',\tau,a,a,R,\encode{\sete{x}})\mid a\in\Atom\}\\
\enskip.
\end{eqnarray*}

The machine first finds the atom to duplicate, and uses a state $(\encode{\sete{x}},a)$ to register the atom $a$. Then it moves the tape head to the tuple and adds the atom to that tuple. If the tuple is empty, then the machine produces $(a)$, otherwise, the machine adds $a$ to an existed tuple $(a_1,\ldots,a_{i-1})$, and enters the state $(\encode{\sete{x}},a)'$. Finally, the tape goes back to the atom it duplicated and enters state $\encode{\sete{x}}$ again to start the duplication of the next atom. This procedure ends by finishing the duplication of all the atoms in $\bar{x}$, and entering the state $\encode{\sete{x}}$ with $\tup{x}$ written under the tape head. Hence, the machine is ready to produce $\setb{\sete{x}}(\tup{x})$.

Since there is an upper bound of the length of the atom, this set of transitions is legal and orbit-finite. Moreover, there are finitely many orbits for the set $X$, which means that the machine needs finitely many such programs.
Hence, we have obtained an  $M$ that meets the requirement.

By applying a $\pi_K$-automorphism on the element $x$, we derive the following corollary.

For every legal and orbit-finite set with atoms $X$, there exists an , such that for every $x\in X$, and for every $K$-automorphism $\pi_K$, it produces an $\pi_K(x)$ labelled transition, and writes $\pi_K(x)$ on the tape in the resulting configuration, given that $\atom(\pi_K(x))$ and $\encode{\orb_{[x]}}$ are written on the tape.

However, the machine could check the atoms from the finite support and the atoms already on the tape. Therefore, at least all the atoms not in the finite support and on the tape have the possibility to be produced in the same configuration of the machine.

Now we take the labels into consideration. As $\Atau$ has finitely many orbits, we only need to consider finitely many set theoretical structures that may construct a label. For the simplicity of the analysis, we consider tuples of atoms.

We suppose there are $n$ orbits. The $k$-th orbit is a tuple $(x_1,x_2,\ldots,x_{m_k})$, where $x_i$ is either an atom from the minimal support $M$ (we call it a constant), or an atom not from the support (and we call it a variable). Note that, we only distinguish atoms with equality. Hence, we only distinguish from pairs $x_i$ and $x_j$ referring to the same element, or not. If $x_i$ and $x_j$ refer to the same element, we assign them to the same variable.

Since $\Atau$ is orbit-finite, we assign a special representative element for every orbit.

* If the elements in this orbit the elements only consists of tuples of atoms from $M$. Then for an element $x$, $\pi(x)=x$ for every $M$-automorphism. We choose $x$ itself as the representative.

* Otherwise, the elements consists of tuples like $(x_1,x_2,\ldots,a_1,a_2\ldots)$, where $x_1,x_2,\ldots \in M$ and $a_1,a_2,\ldots\notin M$. Then for every distinct atom $a_i$, we introduce a new symbol $a_i'$ not in $M$ for it. Hence, an representative for this orbit is $(x_1,x_2,\ldots,a_1',a_2',\ldots)$. If we denote this representative by $x$, then for every element $y$ in this orbit, there is a $M$-automorphism $\pi$, such that $\pi(x)=y$.

When the machine needs to produce a label, it is able makes several operations.
There are finitely many representatives, we use $R$ to denote the set of representatives.

* It first selects a structure of the label, i.e., it produces a representative of the orbit.

* It assigns a variable with an atom from the support or the tape if necessary.

* It assigns a variable with a fresh atom (neither in the support nor on the tape) if necessary.

We show that these operations could be accomplished with an .

The following lemma shows that effective labelled transition systems with atoms are nominally executable. (We put a proof in Appendix <ref>.)

For every legal and orbit-finite set $\Atau$ and every effective $\Atau$-labelled transition system with atoms $T$, there exists an  $\M$ such that $T\bbisim \T(\M)$.

We let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be an effective $\Atau$-labelled transition system with atoms, and let $K\subset\Atom$ be the minimal support of $T$. We show that there exists an  $\M=(\Sta_{\M},\step{}_{\M},\uparrow_{\M})$ such that $\T(\M)\bbisim T$.

As $T$ is effective, for every state $s\in\Sta_T$, the set $\mathalpha{out}(\encode{\sete{s}})=\{\encode{\sete{(s,a,t)}}\mid s\step{a}_T t\}$ is recursively enumerable. We use this fact to simulate the transition system. We describe the simulation in $3$ stages.

* Initially, the tape is empty. Hence the initial configuration is $(\uparrow_{\M},\tphd{\Box})$. For simplicity, we do not denote the position of the tape head in the tape instances. The machine first writes the representation of the initial state $\uparrow_T$, i.e., $\encode{\sete{\uparrow_T}}\tup{\uparrow_T}$ on the tape, satisfying $\setb{\sete{\uparrow_T}}(\tup{\uparrow_T})=\uparrow_T$. As $T$ is legal, $\tup{\uparrow_T}$ consists of finitely many atoms. The initialization procedure is represented as follows,

\begin{equation*}
\enskip.
\end{equation*}

In the control state $\enu$, we assume that the tape instance is $\encode{\sete{s}}\tup{s}$, satisfying $\setb{\sete{s}}(\tup{s})=s$. As the transition system is effective, the machine is able to enumerate the structure of the outgoing transitions of $s$ as follows,

\begin{equation*}
\enskip.
\end{equation*}

For state $s$, its subsequent transitions are $\{(s,a,t)\in \step{}_T\}$ and by the proposition of transition system with atoms, the set of transitions from $\pi_K(s)$ is $\pi_K{\{(s,a,t)\in \step{}_T\}}$. We use this fact to enumerate the transitions from $s$ and take a $\pi_K$ automorphism by the the atoms $\atom(\pi_K(s))$ which is already on the tape, and hence we obtained the transitions from $\pi_K(s)$.

Then the machine enumerates $\mathalpha{out}(s)$,  and writes $(\encode{a},\encode{t})$ (which are represented by $\encode{\orb_{[a]}},\encode{\atom(a)},\encode{\orb_{[t]}},\encode{\atom(t)}$ respectively) on the tape whenever a transition $(s,a,t)$ is enumerated.

The step of enumeration is represented as follows,

\begin{eqnarray*}
\enskip.
\end{eqnarray*}

* In the second stage, the  produces the tuples of atoms $\tup{a}$ and $\tup{t}$ that valuates the free variables of $a$ and $t$. The valuation creates fresh atoms when necessary and preserves atoms from $K$ and $\tup{s}$.

We denote the tuple of free variables of $\sete{(s,a,t)}$ by $\bar{x}$, and tuples of free variables of $\sete{s}$, $\sete{a}$ and $\sete{t}$ by $\bar{x_s}$, $\bar{x_a}$ and $\bar{x_t}$ respectively. Note that all the variables in $\bar{x_s}$, $\bar{x_a}$ and $\bar{x_t}$ are also in $\bar{x}$. Since $\encode{\sete{(s,a,t)}}$ is already on the tape, the following terms are computable:

* the set builder expressions of $a$ and $t$: $\encode{\sete{a}}$ and $\encode{\sete{t}}$;

* the tuples of free variables: $\bar{x}$, $\bar{x_s}$, $\bar{x_a}$ and $\bar{x_t}$;

We show the above statements as follows. We define a triple $(s,a,t)$ by $\{\{s\},\{s,a\},\{s,a,t\}\}$. We use the standard Gödel numbering on sets and variables. The encoding $\encode{\sete{(s,a,t)}}$ is equal to $\encode{\{\{\sete{s}\},\{\sete{s},\sete{a}\},\{\sete{s},\sete{a},\sete{t}\}\}}$. $\encode{\sete{a}}$ and $\encode{\sete{t}}$ are all computable because the projection operation is computable in Gödel encoding of ordered triples. Moreover, the projection from $\encode{\sete{x}}$ to the free variables used in each elements are computable.

Then we evaluate $\bar{x}$ to tuples of atoms. $\tup{s}$ is a valuation of $\bar{x_s}$. We evaluate $\bar{x}$ by distinguishing two cases:

* if a variable $y$ in $\bar{x}$ also appears in $\bar{x_s}$, then we duplicate the valuation of that variable from $\tup{s}$ to valuate $y$;

* otherwise, we create a fresh atom to valuate $y$.

By Example <ref>, the above two operations are valid by s.
Since $\bar{x_a}$ and $\bar{x_t}$ are both sub-tuples of $\bar{x}$, the machine duplicates the valuation from $\bar{x}$ to create $\tup{a}$ and $\tup{t}$.

Hence, we get $\encode{\sete{a}}$, $\encode{\sete{t}}$, $\tup{a}$ and $\tup{t}$ satisfying that $\setb{\sete{a}}(\tup{a})=a'$, $\setb{\sete{t}}(\tup{t})=t'$, and there exists an $K\cup\tup{s}$-automorphism $\pi$ which preserves all the atoms in $K\cup\tup{s}$, such that $\pi(s,a',t')=(s,a,t)$. By the property of transition system with atoms, $(s,a',t')\in\step{}_T$. Moreover, by Example <ref>, during the generation of fresh variables, every fresh variable from the universe of $\Atom$ can be generated, the  is able to create all the transitions which are equivalent to $(s,a,t)$ up to $K\cup\tup{s}$-automorphism. We denote this stage as follows:

\begin{equation*}
\enskip.
\end{equation*}

We use $\pi_{K\cup s}$ to denote some arbitrary atom automorphism that preserves the support $K$ and the atoms from the state $\pi_K(s)$, and $\pi_{K\cup s\cup a}$ to denote some arbitrary atom automorphism that preserves $K$, $\pi_K(s)$ and $\atom(\pi_{K\cup s}(a))$. Then the machine nondeterministically produces $\atom(\pi_{K\cup s}(a))$ and $\atom(\pi_{K\cup s\cup a}(t))$ according to $\atom(s)$, $\encode{\atom(s)}$, $\encode{\atom(a)}$ and $\encode{\atom(t)}$, for some arbitrary $\pi_{K\cup s}$ and $\pi_{K\cup s\cup a}$.

The machine first generates $\atom(\pi_{K\cup s}(a))$. For every element $\encode{x}\in\encode{\atom(a)}$, we distinguish with two cases:

* if $\encode{x}$  also in $\encode{\atom(s)}$, then the machine find the the corresponding element from $\atom(\pi_K(s))$ and duplicate that one to fills the position of $\encode{x}$ in $\atom(\pi_{K\cup s}(a))$;

* if $\encode{x}$ not in $\encode{\atom(s)}$, then the machine create a fresh atom and fills the position of $\encode{x}$ in $\atom(\pi_{K\cup s}(a))$.

Then the machine then generates $\atom(\pi_{K\cup s\cup a}(t))$. For every element $\encode{x}\in\encode{\atom(t)}$, we also distinguish with two cases:

* if $\encode{x}$ is also in $\encode{\atom(s)}$ or $\encode{\atom(a)}$ , then the machine find the the corresponding element from $\atom(\pi_K(s))$ or $\atom(\pi_{K\cup s}(a))$ and duplicate that one to fills the position of $\encode{x}$ in $\atom(\pi_{K\cup s\cup a }(t))$;

* if $\encode{x}$ is not in $\encode{\atom(s)}$ nor in $\encode{\atom(a)}$ , then the machine create a fresh atom and fills the position of $\encode{x}$ in $\atom(\pi_{K\cup s\cup a}(t))$.

By Example <ref>, duplication and creating of atoms are valid operations for .

We denote this step as follows,

\begin{eqnarray*}
&(\act,\encode{\orb_{[s]}}\encode{\orb_{[a]}}\encode{\orb_{[t]}}\encode{\atom(s)}\encode{\atom(a)}\encode{\atom(t)}\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t)))
\enskip.
\end{eqnarray*}

* In the third stage, the  generates the action label $a'$ and chooses to execute the transition or to continue the enumeration.

As $\Atau$ is a legal and orbit-finite set, by Example <ref>, the  is able to create a symbol $a'$ such that $\setb{\sete{a}}\tup{a}=a'$.

\begin{equation*}
\enskip.
\end{equation*}

Then the  has two choices: executing the $a'$-labelled transition and starting the next round of simulation or returning to the first stage.

\begin{eqnarray*}
\end{eqnarray*}

Hence, the machine will produce a label $\pi_{K\cup s}(a)$ from $\atom(\pi_{K\cup s}(a))$ and $\encode{\orb_{[a]}}$. By Corollary <ref>, this step is computable by an . According to the property of transition systems with atoms, the transition to be simulated $(\pi_K(s),\pi_{K\cup s}(a),\pi_{K\cup s\cup a}(t))\in\step{}_T$. Moreover, the procedure of generating fresh atoms, it is guaranteed that every transition $(\pi_K(s),a',t')\in\step{}_T$ satisfying that there exists some $\pi_{K\cup s}$ such that $\pi_{K\cup s}(\pi_K(s),a,t)=(\pi_K(s),a',t')$ are produced in the previous step.

This procedure of producing the action label is represented as follows,

\begin{eqnarray*}
&\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t)))\step{}^{*}\\
&\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t))\pi_{K\cup s}(a))
\enskip.
\end{eqnarray*}

* $\tran\Rightarrow\enu$:

Finally the machine simulates the transition or continues the enumeration.

\begin{eqnarray*}
&\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t))\pi_{K\cup s}(a))\step{\pi_{K\cup s}(a)}\step{}^{*}\\
&(\enu,\encode{\orb_{[t]}}\encode{\atom(t)}\atom(\pi_{K\cup s\cup a}(t)))\\
&\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t))\pi_{K\cup s}(a))
\step{}^{*}\\
\enskip.
\end{eqnarray*}

We can verify that before the $a'$-labelled transition, the transition system of the machine preserves its states modulo $\bbisim$ by a sequence of $\tau$-transitions which leads back to the configuration $(\enu,\encode{\sete{s}}\tup{s})$. Moreover, from the above analysis, we have $(s,a',t')\in\step{}_T$; and every transition obtained by an $K\cup\tup{s}$-automorphism from $(s,a,t)$ can be simulated by the  $M$. Therefore, we conclude that $T\bbisim \T(\M)$.

Let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be an effective $\Atau$-labelled transition system with a minimal support $M\in\Atom$ satisfying condition $\star$. We show that there exists an  $\M=(\Sta,\step{},\uparrow)$ such that $\T(\M)\bbisim T$.

As $T$ is effective, for every state $s\in\Sta_T$, the set $\mathit{Next}(s)=\{(a,t)\mid s\step{a}_T t\}$ is recursively enumerable. We use this fact to simulate the transition system. Note that, the operations we mention are based on the encodings of the elements of sets with atoms unless we actually write or execute elements from sets with atoms.

In the initial state, the machine writes the encoding of $\uparrow_T$ on the tape.

\begin{equation*}
\enskip.
\end{equation*}

In the $\mathit{State}$ state, the machine start to enumerate the encodings of the elements in $\mathit{Next}$. When it gets a label $a_0$, it starts to enumerate the $M$-automorphisms $\pi$, until we get $\pi(a_0)\in R$, namely $x_0$. As there are finitely many representatives, we can write $x_0$ on the tape.

\begin{equation*}
\enskip.
\end{equation*}

Now the machine nondeterministically chooses a renaming operation on $x_0$, using the following set of transitions:

\begin{equation*}
\{\mathit{Rename}\step{\tau[x/\pi_M(x)]R}\mathit{Next}\mid \forall M\mbox{-automorphism }\pi_M\}
\enskip.
\end{equation*}

This set is legal and orbit-finite. With these transitions, we can rewrite $x_0$ by any element in its own orbit, namely $x_1$. Then the machine nondeterministically chooses one of the transitions with that label and get the subsequent state.

\begin{equation*}
\end{equation*}

Then, the machine has three choices, continue to enumerate a new transition, go back to the configuration $(\mathit{State},\encode{s})$, or simulate the transition.

\begin{eqnarray*}
\enskip.
\end{eqnarray*}

In state $\mathit{Dest}$, the machine would prepare for the next step of transition.

\begin{equation*}
\enskip.
\end{equation*}

The following set of transitions are used to simulate any labelled the transitions.

\begin{equation*}
\{\mathit{Step}\step{x[x/x]R}\mathit{Dest}\mid x\in\Atau\}
\enskip.
\end{equation*}

Obviously, it is a legal and orbit-finite set, as every element of this set only consists of a tuple with three atoms and several constants.

Note that all the computations are either using transitions which are legal and orbit-finite sets with atoms, or just using encodings (which are based on finite sets of transitions). Hence, $\M$ uses a legal and orbit-finite set of transitions.

We also show that the requirements of effective transition systems with atoms are necessary to prove that a transition system is nominally executable. (We put a proof in Appendix <ref>.)

For every  $\M$, the associated transition system $\T(\M)$ is an effective transition system with atoms.

It is obvious that $\T(\M)$ is effective.

Let $\M=(\Sta_{\M},\step{}_{\M},\uparrow_{\M})$, then there exists a finite set of atoms $K\subset\Atom$ such that, for every $(s,a,d,e,M,t)\in{\step{}_{\M}}$, and for every $K\mbox{-automorphism}\,\pi_K$, we have $\pi_K(s,a,d,e,M,t)\in{\step{}_{\M}}$. It follows that the transition system $\T(\M)$ is legal.

To conclude, we have the following theorem stating that the class of nominally executable transition systems are exactly the set of effective transition systems with atoms.

A transition system $T$ is nominally executable iff there exists a legal and orbit-finite set $\Atau$ and an effective $\Atau$-labelled transition system with atoms $T'$ such that $T\bbisim T'$.

Ignore the following parts!
The above simulation introduces divergence during the procedure of generating new atoms as well as the enumeration of transitions. We also consider the transition systems that can be simulated by  modulo $\bbisimd$. We propose the following requirements:

* the transition system is computable, i.e. the set $\mathit{Next}$ is computable;

* the set of states should be legal sets with atoms, i.e. there is a finite support $K$ for $\Sta_T\cup\Atau$.

Now we proceed to consider computable transition systems. As a counterparts for boundedly branching transition systems, we define the transition systems that branching with boundedly many orbits. For an orbit-finite set with atoms $A$, we define a function $\orb$, such that $\orb(A)$ is the number of orbits of $A$. For a set of states $S$, we define a function $\num_{\bbisimd}$, such that $\num_{\bbisimd}(S)$ is the number of equivalence classes modulo $\bbisimd$ in $S$.

We formalise another condition $\square$ for the $\Atau$-labelled transition system $T=(\Sta,\step{},\uparrow)$.

* $\forall s\in\Sta$ it satisfies that:

\begin{equation*}
s\step{a} \iff \forall M\mbox{-automorphism }\pi_M,\,s\step{\pi_M(a)}
\enskip.
\end{equation*}

* There exists a universal bound $p$ for all the pair of states and labels $(s,a)$, that bounds the number of equivalence classes modulo $\bbisimd$ from an $a$-labelled transitions from $s$, i.e.,

\begin{equation*}
\exists p\in\mathbb{N}.\,\forall (s,a)\in\Sta\times\Atau,\,\num_{\bbisimd}(\{t\mid s\step{a}t\})\leq p
\enskip.
\end{equation*}

We first show that the above conditions are sufficient for executability of  modulo $\bbisimd$.

For every legal and orbit-finite set $\Atau$ and every computable $\Atau$-labelled transition system $T$ satisfying condition $\square$, there exists an  $\M$ such that $T\bbisimd \T(\M)$.

Let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be a computable $\Atau$-labelled transition system with a minimal support $M\in\Atom$ satisfying condition $\star$. We show that there exists an  $\M=(\Sta,\step{},\uparrow)$ such that $\T(\M)\bbisim T$.

Note that $\Atau$ is orbit-finite, and we assume $\orb(\Atau)=k$. We have that there are at most $k$ representatives.

Hence, we conclude that there exists a universal bound $k$ for all the states, that bounds the number of orbits of the sets of labels of the transitions, i.e.,

\begin{equation*}
\forall s\in\Sta,\, orb(\{a\mid s\step{a}\})\leq k
\enskip.
\end{equation*}

As $T$ is computable, for every state $s\in\Sta_T$, the set $\mathit{Next}(s)=\{(a,t)\mid s\step{a}_T t\}$ is recursive. We use this fact to simulate the transition system. Note that, the operations we mention are based on the encodings of the elements of sets with atoms unless we actually write or execute elements from sets with atoms.

In the initial state, the machine writes the encoding of $\uparrow_T$ on the tape.

\begin{equation*}
\enskip.
\end{equation*}

In the $\mathit{State}$ state, the machine start to compute the representatives of the labels in $\mathit{Next}$. As there are at most $q$ representatives, the machine only needs to verify all the $q$ representatives whether it is a label in $\mathit{Next}$. As $T$ is computable, this procedure is also computable. Finally, the machine writes a the tuples of representatives as symbol $(x_1,x_2,\ldots,x_i)\in R^i$ on the tape, where $(i\leq k)$. Note that there are at most $k$ representatives, we need to introduce at most $k^k$ such symbols.

\begin{equation*}
\enskip.
\end{equation*}

Then the machine nondeterministically chooses one of the labels and one of the subsequent states.

\begin{equation*}
\enskip.
\end{equation*}

Where $1\leq j\leq i\leq k$, and $0\leq l \leq p$.

This step is achieved by the following transitions,

\begin{equation*}
\{\mathit{Step}\step{\pi_M(x_j)[(x_1,x_2,\ldots,x_i)/(\pi_M(x_j),l)]}\mathit{Dest}\mid 1\leq j\leq i\leq k,\,0\leq l \leq p,\,\forall M\mbox{-automorphism }\pi_M\}
\enskip.
\end{equation*}

This is a legal and obit-finite set.

We denote $\pi_M(x_j)$ by $y$, then the machine proceed to compute the $l$-th reachable state by a $y$-labelled transition from $s$, if there are less then $l$ distinct reachable state, then the machine take the first state as the destination state. We denote the result state by $s'$.

\begin{equation*}
\enskip.
\end{equation*}

We can verify that the set of transitions are legal and orbit-finite.

We also show that it is a necessary condition.
This is not correct! I will fix it

For every  $\M$, $\T(\M)$ is computable and satisfies condition $\square$.

By the above lemmas, we have the following theorem.

A transition system $T$ is executable by an  modulo $\bbisimd$ iff there exists a legal and orbit-finite set $\Atau$ and a computable $\Atau$-labelled transition system $T'$  satisfying condition $\square$, and $T\bbisimd T'$.

For every legal and orbit-finite set $\Atau$ and every effective $\Atau$-labelled transition system $T$, there exists an  $\M$ such that $T\bbisim \T(\M)$.

The proof sketch below is unclear and should be improved. You
seem to be adapting the proof in [2], but this is only clear
to me because I am an author of that paper. Readers less familiar
with [2] will not understand this. You should, therefore,
briefly summarise the proof in [2] here (also explicitly
say that this is what you do!), and then explain
how this proof can be adapted and why the resulting sets are all legal
and orbit-finite.

Let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be an $\Atau$-labelled effective transition system. We show that there exists an  $\M=(\Sta,\step{},\uparrow)$ such that $\T(\M)\bbisim T$.

As $T$ is effective, for every state $s\in\Sta_T$, the set $\mathit{Next}(s)=\{(a,t)\mid s\step{a}_T t\}$ is recursively enumerable. We use this fact to simulate the transition system.

In the initial state, the machine writes the encoding of $\uparrow_T$ on the tape.

\begin{equation*}
\enskip.
\end{equation*}

In the $\mathit{State}$ state, the machine start to enumerate the elements in $\mathit{Next}$, and write them on the tape. Suppose $(a_0,s_0)$ is the first element enumerated from $\mathit{Next}$.

\begin{equation*}
\enskip.
\end{equation*}

Then, the machine has three choices, continue to enumerate a new transition, go back to the configuration $(\mathit{State},\encode{s})$, or simulate the transition.

\begin{eqnarray*}
\enskip.
\end{eqnarray*}

In state $\mathit{Dest}$, the machine would prepare for the next step of transition.

\begin{equation*}
\enskip.
\end{equation*}

We only illustrate the following set of transitions which are used to simulate any labelled the transitions.

\begin{equation*}
\{\mathit{Step}\step{a[a/a]R}\mathit{Dest}\mid a\in\Atau\}
\enskip.
\end{equation*}

Obviously, it is a legal and orbit-finite set, as every element of this set only consists of a tuple with three atoms and several constants.

For all the other steps, one can verify that they are computable by a
Turing machine with atoms, and hence by an . Which other
steps? Explain why you need the full power of Turing machines with
atoms, and why a finitary Turing machine would not do the job. Also,
there should be a more complete argument that the sets involved are
legal and orbit-finite. I can see that the set of transitions
stemming from $\mathit{Step}$ is legal and orbit-finite. But a
reader would like to understand why this is the only interesting case.
Hence we have designed an  $\M$, satisfying $\T(\M)\bbisim T$.

By analogy to the results of RTMs, we also investigate the transition systems that are executable by  modulo $\bbisimd$. A naive requirement for the transition system is let it to be computable and boundedly branching. For a transition system if the cardinality of the set $\mathit{Next}(s)$ is bounded, we call it a boundedly branching transition system, and the maximum cardinality is the branching degree of the transition system. Moreover, if $\mathit{Next}(s)=\{(a,t)\mid s\step{a}_T t\}$ is computable, we call it a computable transition system. For boundedly branching computable transition systems, we have the following theorem.

Remove the following theorem. Instead, explain that in
[2] a refinement of the above theorem in the finitary
case is obtained showing that boundedly branching computable
transition systems are executable up to divergence-preserving
branching bisimilarity. We shall obtain a similar refinement for
RTMs with atoms.

For every legal and orbit-finite set $\Atau$ and every boundedly branching computable $\Atau$-labelled transition system $T$, there exists an  $\M$ such that $T\bbisimd \T(\M)$.

We omit the proof since the theorem is actually a corollary of Theorem <ref>. Actually, even if divergence-preserving branching bisimilarity is required, the transition systems associated with  are more than boundedly branching computable transition systems. Consider the transition system $T$ in Lemma <ref>, it is an infinitely branching transition system. Nevertheless, there is an  such that its transition system is divergence-preserving branching bisimilar to $T$.

We design an  $\M=(\Sta,\step{},\uparrow)$ as follows,

* $\Sta=\{\uparrow, s_1,s_2,s_3\}$

* $\step{}=\{\uparrow\step{x[\Box/x]R}s_1\mid x\in\A\}\cup\{s_1\step{\tau[\Box/\Box]L}s_2\}\cup\{s_2\step{x[x/\Box]R}s_3\mid x\in\A\}$.

Obviously, we have $\T(\M)\bbisimd T$.

Now we proceed to figure out the exact class of transition systems that are executable by  modulo $\bbisimd$. By analogy to the boundedly branching transition system, we define the transition systems with transition relations that have boundedly many orbits.

From our assumption, the sets of labels are from legal and orbit-finite sets with atoms, thus we may apply an atom automorphism $\pi$ on any label. Moreover, we introduce the notion of atom automorphism $\pi$ on a transition system $T$ by applying $\pi$ on the labels of every transition of $T$. We denote by $\pi(s)$ for applying an atom automorphism $\pi$ on a transition system with $s$ as its initial state.

For an labelled transition system $T=(\Sta_T,\step{}_T,\uparrow_T)$, we partition the transitions from every state $s\in\Sta_T$ into disjoint orbits. We say two transitions $s\step{a_1}_T s_1$ and $s\step{a_2}_T s_2$ are in the same orbit if there is an atom automorphism $\pi$ such that $\pi(a_1)=a_2$ and $\pi(s_1)=s_2$. If there exists a natural number $k$ such that for every state $s\in\Sta_T$, the transitions from $s$ are partitioned into at most $k$ orbits, then we say that $T$ has a transition relation with boundedly many orbits.

For every legal and orbit-finite set $\Atau$ and every computable $\Atau$-labelled transition system $T$ that has a transition relation with boundedly many orbits, there exists an  $\M$ such that $T\bbisimd \T(\M)$.

Let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be an $\Atau$-labelled computable transition system that has a transition relation with at most $k$ orbits. We show that there exists an  $\M=(\Sta,\step{},\uparrow)$ such that $\T(\M)\bbisimd T$.

In the initial state, the machine writes the encoding of $\uparrow_T$ on the tape.

\begin{equation*}
\enskip.
\end{equation*}

As the transition relation is computable and has boundedly many orbits, the machine computes and writes a representative for all the orbits of the subsequent transitions on the tape.

\begin{equation*}
\enskip.
\end{equation*}

Note that we have $i\leq k$. Then, the machine writes a data symbol as a tuple of $(a_0,\ldots,a_i)$ on the tape.

\begin{equation*}
\enskip.
\end{equation*}

The machine then chooses one of the transitions to simulate,

\begin{equation*}
\enskip.
\end{equation*}

Note that we have $0\leq j\leq i$. $\pi$ is an atom automorphism that maps $a_j$ to any elements from its orbit. Finally, the machine prepares for the simulation for the next state. As the transition relation is computable, the encoding of the next state $\encode{\pi(s_j)}$ is also computable.

\begin{equation*}
\enskip.
\end{equation*}

needs the following set of transitions to generate the step of $\pi(a_j)$ labelled transition, which is a legal and orbit-finite set.

\begin{equation*}
\{\mathit{Step'}\step{\pi(a_j)[(a_0\ldots,a_i)/(\pi(a_j),j)]R}\mathit{Dest}\mid a_0,\ldots,a_j\in\Atau,\, 0\leq j\leq k,\,\pi\mbox{ is an atom automorphism}\}
\enskip.
\end{equation*}

Moreover, one can verify that all the other steps are computable by a Turing machine with atoms, and hence by an .
Hence we have designed an  $\M$, satisfying $\T(\M)\bbisimd T$.

We also show that, the set of transition systems that are executable by  modulo $\bbisimd$ does not exceeds the above criterion. Followed by the proof about RTMs with finite sets in [16], we first establish some auxiliary facts.

For every  $\M$, the transition relation of $\T(\M)$ has boundedly many orbits.

As the transition relation of $\M$ is orbit-finite, it has boundedly many orbits. It follows that the transition relation of $\T(\M)$ has boundedly many orbits.

If $s\bbisimd t$, then the transition relation from $s$ and $t$ has the same number of orbits.

Then we have the following theorem of negative result.

For every legal and orbit-finite set $\Atau$ and every computable $\Atau$-labelled transition system $T$ that has a transition relation with unboundedly many orbits and has no divergence up to $\bbisimd$, then there does not exist an  $\M$ such that $T\bbisimd \T(\M)$.

§ APPLICATIONS

The $\pi$-calculus was proposed by Milner, Parrow and Walker [18] as a language to specify processes with link mobility. In this paper, we shall consider the version presented in the textbook by Sangiorgi and Walker [20], excluding the match prefix.

We presuppose a countably infinite set $\N$ of names; we use strings of lower case letters for elements of $\N$.
The prefixes, processes and summations of the $\pi$-calculus are, respectively, defined by the following grammar:

\begin{align*}
\pi\      & \coloneqq\ \outcap{x}{y}\ \mid\ \incap{x}{z}\ \mid\ \taucap \qquad (x,y,z\in \N)\\
P\    & \coloneqq\ M\ \mid\  P\parc P\ \mid\ \restr{z}{P}\ \mid\ \repl{P}\\
M\   & \coloneqq\ \nil\ \mid\ \pref{\pi}P \mid\ M \altc M\enskip.
\end{align*}

We use $P\{z/y\}$ to denote a $\pi$-term obtained by substituting every occurrence of $y$ to $z$ in $P$.

An $\alpha$-conversion between $\pi$-terms is defined in [20] as a finite number of renaming of bound names. We write $P\aeq Q$ if $P$ and $Q$ are two $\pi$-terms that are $\alpha$-convertible.

We define the operational behaviour of $\pi$-terms by means of the structural operational semantics in Fig. <ref>, in which $\piact{}$ ranges over the set of actions of the $\pi$-calculus.

The transition system associated with a $\pi$-term is defined as follows:

Let $P$ be a $\pi$-term. $\T(P)=(\Sta_{P},\step{}_{P},\uparrow_{P})$ is the transition system associated with $P$, where

* $\Sta_{P}$ is the set of $\alpha$-equivalence classes of all reachable $\pi$-terms from $P$ by the operational semantics;

* $\step{}_{P}$ is the set of transitions between $\alpha$-equivalence classes of all reachable $\pi$-terms; and

* $\uparrow_{P}$ is the $\alpha$-equivalence class of $P$.

$\mathrm{PREFIX}\quad\inference{\,}{\tau.P\step{\tau}P}\quad \inference{}{\overline{x}y.P\step{\overline{x}y}P}\quad\inference{}{x(y).P\step{xz}P\{z/y\}}$

%%$\mathrm{MISMATCH}\quad\inference{P\step{\alpha}P',\,x\neq y}{if\,x\neq y\,then\,P\step{\alpha}P'}$\\
\quad\mathrm{PAR_L}\quad\inference{P\step{\piact{}}P'}{P\parc{Q}\step{\piact{}}P'\parc{Q}}\,\bn{\piact{}}\cap \fn{Q}=\emptyset$

\mathrm{CLOSE_L}\quad\inference{P\step{\overline{x}(z)}P',\,Q\step{xz}Q'}{P\parc{Q}\step{\tau}\restr{z}{(P'\parc{Q'})}}\,z\notin \fn{Q}$

\mathrm{OPEN}\quad\inference{P\step{\overline{x}z}P'}{(z)P\step{\overline{x}(z)}P'}\,z\neq x$

%  \quad\inference{P\mid !P\step{\piact{}}P'}{!P\step{\piact{}}P'}
\quad\inference{P\step{\piact{}}P'}{\repl{P}\step{\piact{}}P'\parc\repl{P}}
\quad\inference{P\step{\outact{x}{y}}P',\,P\step{\inact{x}{y}}P''}{\repl{P}\step{\tauact{}}(P'\parc P'')\parc\repl{P}}
\quad\inference{P\step{\boutact{x}{z}}P',\,P\step{\inact{x}{z}}P''}{\repl{P}\step{\tauact}\restr{z}{(P'\parc P'')}\parc\repl{P}}$

$\mathrm{ALPHA}\quad\inference{P\step{\piact{}}P'}{Q\step{\piact{}}P'}\,Q\aeq P$.

Operational rules for the $\pi$-calculus

The motivation for introducing the notion of RTM with infinite alphabets comes from the discussion of the executability of the $\pi$-calculus [16].
We show that the transition systems that the $\pi$-calculus associates with are nominally executable.
We consider the set of names $\N$ of a $\pi$-calculus process as the set of atoms. The transition system associated with a $\pi$-term (We put a detailed introduction in Appendix <ref>.) is actually an effective transition system with atoms. We get the following result as a corollary to Theorem <ref>. (We prove this result in Appendix <ref>.)

Note that, trivially, $\N$ itself is then a legal and orbit-finite set with atoms. Moreover, a label from the transition system of a $\pi$-calculus process is a pair two names or $\tau$. Hence the set of labels $\Atau$ for every $\pi$-calculus process is a legal and orbit-finite set with atoms. Moreover, the transition relations of all $\pi$-calculus processes are preserved under $\alpha$-conversion. As mentioned in [20], the set of free variables of a $\pi$-calculus process is invariant under execution. We consider the set of free names in a $\pi$-term as the support of the associated transition system. The set of free names is finite, thus we get a finite support of the transition system. We conclude that the transition systems associated with $\pi$-calculus processes are legal transition systems with atoms. By using the fact that the operational semantics of the $\pi$-calculus leads to an effective transition relation,

For every $\pi$-calculus process $P$, the transition system $\T(P)$ is nominally executable.

We use $\N$ to denote the countable set of names used in the $\pi$-calculus, and we suppose that $\N=\Atom$. We suppose that $P$ is an arbitrary $\pi$-calculus process. We use $\fn{P}$ to denote the set of free names involved in $P$ and $\bn{P}$ to denote the set of bound names involved in $P$.

By Theorem <ref>, it is sufficient to show that for every $\pi$-calculus process $P$, the transition system $\T(P)$ is an effective legal transition system with atoms. The transition system is effective by the effectiveness of structural operational semantics of the $\pi$-calculus. Therefore, by Definition <ref>, it is sufficient to show that there is a finite set $K\subset\N$ such that $K$ is a support of $\T(P)$. We let $\T(P)=(\Sta_{\pi},\step{}_{\pi},P)$ be an $\Atau$ labelled transition system, and we take $K=\fn{P}\cup\{\tau\}$. Note that $\Sta_P$ is the set of $\pi$-terms and $\Atau$ is the set of labels, and hence $\Sta_{\pi}$ is a set with atoms and $\Atau$ is an orbit-finite set with atoms. To show that $K$ is a support of $\T(P)$, we only need to show that for every $(s,a,t)\in\step{}_{\pi}$, and for every $K$-automorphism $\pi_K$, $\pi_K(s,a,t)\in\step{}_{\pi}$.

We let $\pi_K$ be an arbitrary $K$-automorphism, and we show that $\pi_K(P)$ is an $\alpha$-conversion of $P$, i.e., $\pi_K(P)\aeq P$. We show it by a structural induction on $P$.
In the base case, $P=\nil$, then it is trivial that $\pi_K(P)=\nil\aeq P$.

For the step case, we distinguish with 7 cases.

* If $P=\pref{\tau}P'$, by induction hypothesis, we have $\pi_K(P')\aeq P'$. Hence, we have $\pi_K(\pref{\tau}P')=\pref{\tau}\pi_K(P')\aeq \pref{\tau}P'=P$.

* If $P=\pref{\outcap{x}{y}}P'$, by induction hypothesis, we have $\pi_K(P')\aeq P'$. Moreover, $x,y\in\fn{P}\in K$. Hence, we have $\pi_K(\pref{\outcap{x}{y}}P')=\pref{\outcap{x}{y}}\pi_K(P')\aeq \pref{\outcap{x}{y}}P'=P$.

* If $P=\pref{\incap{x}{y}}P'$, by induction hypothesis, we have $\pi_K(P')\aeq P'$. Moreover, $x\in\fn{P}\in K$. Hence, we have $\pi_K(\pref{\incap{x}{y}}P')=\pref{\incap{x}{\pi_K(y)}}\pi_K(P')\aeq\pref{\incap{x}{y}}P'=P$.

* If $P=P_1+P_2$, by induction hypothesis, we have $\pi_K(P_1)\aeq P_1,\,\pi_K(P_2)\aeq P_2$. Hence, we have $\pi_K(P_1+P_2)=\pi_K(P_1)+\pi_K(P_2)\aeq P_1+P_2=P$.

* If $P=P_1\parc P_2$, by induction hypothesis, we have $\pi_K(P_1)\aeq P_1,\,\pi_K(P_2)\aeq P_2$. Hence, we have $\pi_K(P_1\parc P_2)=\pi_K(P_1)\parc \pi_K(P_2)\aeq P_1\parc P_2=P$.

* If $P=\restr{z}{P'}$, by induction hypothesis, we have $\pi_K(P')\aeq P'$. Moreover, $\pi_K(z)=z'\notin K$. Hence, we have $\pi_K(\restr{z}{P'})=\restr{z'}{\pi_K(P')}\aeq \restr{z}{P'}=P$.

* If $P=\repl{P'}$, by induction hypothesis, we have $\pi_K(P')\aeq P$. Hence, we have $\pi_K(\repl{P'})=\repl{\pi_K(P')}\aeq \repl{P'}=P$.

By structural induction, we have shown that for every $K$-automorphism $\pi_K$, $\pi_K(P)\aeq P$. Therefore, we have $\pi_K(P)\in\Sta_{\pi}$. Hence, $K$ is a support of $\Sta_{\pi}$.

Next we still let $\pi_K$ be an arbitrary $K$-automorphism, and we show that for every transition $P\step{\piact}_{\pi}Q\in\step{}_{\pi}$, it satisfies that $\pi_K(P\step{\piact}_{\pi}Q)\in\step{}_{\pi}$ by an induction on the structural operational semantics of the $\pi$ calculus.

We construct a proof tree according to the structural operational semantics in Figure <ref> for every transition $(P,\piact,Q)\in\step{}_{\pi}$. The induction hypothesis is that, if $(P,\piact,Q)$ is induced from a set of transitions $\mathit{Pre}(P,\piact,Q)\subset\step{}_{\pi}$ , then for every transition $(P_i,\piact_i,Q_i)\in\mathit{Pre}(P,\piact,Q)$, there is $\pi_K(P_i,\piact_i,Q_i)\in\step{}_{\pi}$.

For the base case, the $\nil$ process cannot do any transition, then the property trivially holds. For the step case, we distinguish with several cases as follows.

* If the transition is $\pref{\tauact}P\step{\tauact}_{\pi}P$, then we have $\pi_K(\pref{\tauact}P)\step{\pi_K(\tauact)}_{\pi}\pi_K(P)$.

* If the transition is $\pref{\outcap{x}{y}}P\step{\outact{x}{y}}_{\pi}P$, then we have $\pi_K(\pref{\outcap{x}{y}}P)\step{\pi_K(\outact{x}{y})}_{\pi}\pi_K(P)$.

* If the transition is $\pref{\incap{x}{y}}P\step{\outact{x}{z}}_{\pi}P\{z/y\}$, then we have $\pi_K(\pref{\incap{x}{y}}P)\step{\pi_K(\inact{x}{z})}_{\pi}\pi_K(P\{z/y\})$.

* If the transition is $P_1+P_2\step{\piact}_{\pi}Q$, then there are two cases

* if $P_1\step{\piact}_{\pi}Q$. By induction hypothesis, we have $\pi_K(P_1)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$. Hence, we have $\pi_K(P_1+P_2)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$.

* If $P_2\step{\piact}_{\pi}Q$. The proof is symmetric with the previous case.

* If the transition is $P_1\parc P_2\step{\piact}_{\pi}Q_1\parc P_2$, then we have $P_1\step{\piact}_{\pi}Q_1$ and $\bn{\piact}\cap\fn{P_2}=\emptyset$. By induction hypothesis, we have $\pi_K(P_1)\step{\pi_K(\piact)}_{\pi}\pi_K(Q_1)$. Moreover, there is $\bn{\pi_K(\piact)}\cap\fn{\pi_K(P_2)}=\emptyset$. Hence we have $\pi_K(P_1\parc P_2)\step{\pi_K(\piact)}_{\pi}\pi_K(Q_1\parc P_2)$.

* If the transition is $P_1\parc P_2\step{\piact}_{\pi}P_1\parc Q_2$. The  proof is symmetric with the previous case.

* If the transition is $P_1\parc P_2\step{\tauact}_{\pi}Q_1\parc Q_2$, then we have $P_1\step{\outact{x}{y}}_{\pi}Q_1,\,P_2\step{\inact{x}{y}}_{\pi}Q_2$ (or the symmetrical case). By induction hypothesis, we have $\pi_K(P_1)\step{\pi_K(\outact{x}{y})}_{\pi}\pi_K(Q_1)$ and $\pi_K(P_2)\step{\pi_K(\inact{x}{y})}_{\pi}\pi_K(Q_2)$. Hence we have $\pi_K(P_1\parc P_2)\step{\pi_K(\tauact)}_{\pi}\pi_K(Q_1\parc Q_2)$.

* If the transition is $P_1\parc P_2\step{\tauact}_{\pi}\restr{z}{(Q_1\parc Q_2)}$, then we have $P_1\step{\boutact{x}{z}}_{\pi}Q_1$, $P_2\step{\inact{x}{z}}_{\pi}Q_2$, and $z\notin\fn{P_2}$ (or the symmetrical case). By induction hypothesis, we have $\pi_K(P_1)\step{\pi_K(\boutact{x}{z})}_{\pi}\pi_K(Q_1)$ and $\pi_K(P_2)\step{\pi_K(\inact{x}{z})}_{\pi}\pi_K(Q_2)$. Moreover, there is $\pi_K(z)\notin\fn{\pi_K(P_2)}$. Hence, we have $\pi_K(P_1\parc P_2)\step{\pi_K(\tauact)}_{\pi}\pi_K(\restr{z}{(Q_1\parc Q_2)})$.

* If the transition is $\restr{z}{P}\step{\piact}_{\pi}\restr{z}{Q}$, then we have $P\step{\piact}_{\pi} Q$ and $z\notin \piact$. By induction hypothesis, we have $\pi_K(P)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$. Moreover, there is $\pi_K(z)\notin\pi_K(\piact)$. Hence, we have $\pi_K(\restr{z}{P})\step{\pi_K(\piact)}_{\pi}\pi_K(\restr{z}{Q})$.

* If the transition is $\restr{z}{P}\step{\boutact{x}{z}}_{\pi}Q$, then we have $P\step{\outact{x}{z}}Q$, and $z\neq x$.  By induction hypothesis, we have $\pi_K(P)\step{\pi_K(\outact{x}{z})}_{\pi}\pi_K(Q)$. Moreover, there is $\pi_K(z)\neq\pi_K(x)$. Hence, we have $\pi_K(\restr{z}{P})\step{\pi_K(\boutact{x}{z})}_{\pi}\pi_K(Q)$.

* If the transition is $\repl{P}\step{\piact}_{\pi}Q\parc \repl{P}$, then we have $P\step{\piact}_{\pi}Q$. By induction hypothesis, we have $\pi_K(\repl{P})\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$. Hence we have  $\pi_K(P)\step{\pi_K(\piact)}_{\pi}\pi_K(Q\parc \repl{P})$.

* If the transition is $\repl{P}\step{\tauact}_{\pi}(Q_1\parc Q_2)\parc \repl{P}$, then we have $P\step{\outact{x}{y}}_{\pi}Q_1$, and $P\step{\inact{x}{y}}_{\pi}Q_2$. By induction hypothesis, we have $\pi_K(P)\step{\pi_K(\outact{x}{y})}_{\pi}\pi_K(Q_1)$, and $\pi_K(P)\step{\pi_K(\inact{x}{y})}_{\pi}\pi_K(Q_2)$. Hence we have  $\pi_K(P)\step{\pi_K(\tauact)}_{\pi}\pi_K((Q_1\parc Q_2)\parc \repl{P})$.

* If the transition is $\repl{P}\step{\tauact}_{\pi}\restr{z}{(Q_1\parc Q_2)}\parc \repl{P}$, then we have $P\step{\boutact{x}{z}}_{\pi}Q_1$, and $P\step{\inact{x}{z}}_{\pi}Q_2$. By induction hypothesis, we have $\pi_K(P)\step{\pi_K(\boutact{x}{z})}_{\pi}\pi_K(Q_1)$, and $\pi_K(P)\step{\pi_K(\inact{x}{z})}_{\pi}\pi_K(Q_2)$. Hence we have  $\pi_K(P)\step{\pi_K(\tauact)}_{\pi}\pi_K(\restr{z}{(Q_1\parc Q_2)}\parc \repl{P})$.

* If the transition is $P\step{\piact}_{\pi} Q$, and $P\aeq P_1$, then $P_1\step{\piact}_{\pi} Q$. By induction hypothesis $\pi_K(P_1)\step{\pi_K(\piact)}_{\pi} \pi_K(Q)$. Moreover, using the statement $\pi_K(P)\aeq P$, we have $\pi_K(P)\aeq P\aeq P_1\aeq\pi_K(P_1)$. Hence, we have $\pi_K(P)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$.

Using the induction on the depth of the proof tree of the transition, we have shown that for every transition $P\step{\piact}_{\pi}Q$, we have $\pi_K(P)\step{\pi_K(\piact)}_{\pi}\pi_K(Q)$. We conclude that $K$ is a support of $\step{}_{\pi}$. Therefore, the transition system $\T(P)$ is an effective legal transition system with atoms.

As a consequence of Theorem <ref>, for every $\pi$-calculus process $P$, the transition system $\T(P)$ is nominally executable.

The formal specification language mCRL2 [14, 15] is widely used to specify and analyze the behaviour of distributed systems. The question arises to what extent the transition systems specified by mCRL2 are executable. The actions in an mCRL2 specification may contain a tuple of integers of any arbitrary lengths, which leads to a set of actions with infinitely many orbits. Moreover, we can also specify transition systems that do not have a finite support in mCRL2. Therefore, we conclude that such transition systems are not nominally executable. (We prove this result in Appendix <ref>.)

There exists an mCRL2 specification $P$, such that the transition system $\T(P)$ is not nominally executable.

Consider the following mCRL2 specification:

\begin{eqnarray*}
&&\mathit{act\, num:\, Nat};\\
&&\mathit{init\,sum\, v:\, Nat\, .\, num(2 * v)};
\end{eqnarray*}

It defines a transition system that includes a set of transitions from the initial state labelled by all even natural numbers as follows:

\begin{equation*}
\{(\uparrow,2n,\downarrow)\mid n\in\mathbb{N}\}
\enskip.
\end{equation*}

This transition system does not have a finite support, therefore, it is not nominally executable.

Moreover, the transition systems specified in mCRL2 are countable but not necessarily effective, therefore, we have the following corollary.

* For every mCRL2 specification $P$, the transition system $\T(P)$ is executable by an  modulo $\bbisimd$.

* There exists an mCRL2 specification $P$, such that the transition system $\T(P)$ is not executable by any  with an effective/computable transition relation modulo $\bbisimd$.

§ CONCLUSIONS

In this paper, we investigated the executable transition systems associated with s and s.
We summarize the executable transition systems associated with s, s and RTMs as a hierarchy in Figure <ref>. Note that all the inclusion relations over the above sets of transition systems are interpreted as the inclusion of the regions in Figure <ref>.

[very thick] (6.6,0) – (-5.6,0);

(3.2,0) parabola bend (2,0.9) (0.8,0);
at (2,0.3) RTM $\bbisimd$;

(4,0) parabola bend (-0.5,1.5) (-0.5,0);
at (0.3,1.1) RTM $\bbisim$;

(-2,0) parabola bend (-2,2.1) (4.5,0);
at (-1,1.8)  $\bbisim$;

(0,0) parabola bend (6,2.8) (6,0);
at (4.1,1.5) Computable  $\bbisimd$;

(-4.7,0) parabola bend (6,5) (6,0);
[anchor=north] at (4.1,4) Effective  $\bbisimd$;

[very thick] (-5.2,0) parabola bend (6,6) (6,0);
at (4.7,5.3)  $\bbisimd$;

A Hierarchy of Executability

We summarize the corresponding transition system of each notion of executability as follows:

* by Theorem <ref>, the class of executable transition systems by RTMs modulo $\bbisimd$ is the boundedly branching computable transition system with a finite set of labels;

* the class of executable transition systems by RTMs modulo $\bbisim$ is the effective transition system with a finite set of labels;

* by Theorem <ref>, the class of nominally executable transition systems is the effective transition system with atoms;

* by Corollary <ref>, the class of executable transition systems by s with a computable transition relation modulo $\bbisimd$ is the computable transition system;

* by Corollary <ref>,the class of executable transition systems by s with an effective transition relation modulo $\bbisimd$ is the effective transition system; and

* by Theorem <ref>, the class of executable transition systems by s modulo $\bbisimd$ is the countable transition system.

Finally, we propose some future work on this issue.

* The precise characterisation of the transition systems executable by s modulo $\bbisimd$ is still open. Further restrictions should be imposed to make it possible to generate all possible transitions of an arbitrary state in the transition system from a single configuration of an .

* It would be interesting to show the existence of a universal , such that it is able to simulate the behaviour of every  with its encoding.

* Psi-calculi [4] were introduced as to characterise transition systems with nominal data types for data structures and with logical assertions representing facts about data. The adoption of nominal data types provides a natural characterisation of the behaviour executed by . An encoding of the $\pi$-calculus was proposed in the psi-calculus [3], proving that the psi-calculus is at least as expressive as the $\pi$-calculus. It would be interesting to figure out the relationship between the transition systems associated with the psi-calculus and the transition systems associated with . We conjecture that as long as the logical assertions used in psi-calculus are semi-decidable, the transition systems of the psi-calculus processes are nominally executable.

* A notion of nominal transition system was proposed by Parrow et al. [19]. Nominal transition systems satisfy the requirements of transition systems with atoms naturally. We did not use the notion of nominal transition system since the predicates for states in Hennessy-Milner logic is ignored in proving the executability. By assuming a appropriate definition of effectiveness, we conjecture that the effective nominal transition systems are nominally executable.

* The value-passing calculus [8] is a process calculus in which the contents of communications are values chosen from natural numbers. It can be used to specify transition systems that are not nominally executable (such as the one we used in the proof of Corollary <ref>). It would be interesting to impose some structures on the sets of atoms, e.g., by considering the natural numbers. Moreover, we could investigate a notion of RTM with natural numbers, and make a comparison to the value-passing calculus.

[very thick] (9.5,0) – (-9.5,0);

(2.8,0) parabola bend (0,2.8) (-2.8,0);
at (0,0.5)

Boundedly Branching
Computable LTS

(3.5,0) parabola bend (-3.5,7) (-5.5,0);
[rotate=45] at (-3.7,5) Effective LTS;

(-3.5,0) parabola bend (1.5,5.5) (4.8,0);
[rotate=-45] at (2.3,3.5)
Boundedly Branching
Computable LTSA
(-4.5,0) parabola bend (2.5,6.5) (6.5,0);
[rotate=-45] at (3.5,5)
Boundedly Orbit
Computable LTSA

(-7,0) parabola bend (-1.5,10) (7.5,0);
[rotate=45] at (-3.5,7.5) Effective LTSA;

(-5,0) parabola bend (1.5,10) (8,0);
[rotate=-45] at (3.5,7.5) Computable LTSI;

(-8.5,0) parabola bend (0,11.5) (8.5,0);
[anchor=north] at (0,11) Effective LTSI;

[very thick] (-9,0) parabola bend (0,12.5) (9,0);
at (0,12) Countable LTSI;

(2.8,0) parabola bend (0,-1.5) (-2.8,0);
at (0,-0.5) RTM $\bbisimd$;

(3.5,0) parabola bend (-3.2,-3.2) (-5.5,0);
[rotate=-45] at (-3.7,-2.2) RTM $\bbisim$;

(-4.5,0) parabola bend (2.5,-2.5) (6.5,0);
[rotate=45] at (3.5,-1.5) RTMA $\bbisimd$;

(-7,0) parabola bend (-2.5,-5) (7.5,0);
[rotate=-45] at (-3.7,-4) RTMA $\bbisim$;

(-5,0) parabola bend (2.5,-5) (8,0);
[rotate=45] at (4.2,-3.5) Computable RTMI $\bbisimd$;

(-8.5,0) parabola bend (0,-6.5) (8.5,0);
[anchor=north] at (0,-5.5) Effective RTMI $\bbisimd$;

[very thick] (-9,0) parabola bend (0,-7.5) (9,0);
at (0,-7) RTMI $\bbisimd$;

A Hierarchy of Executability

[1]
Baeten, J.C.M., Cuijpers, P., Luttik, B., van Tilburg, P.: A process-theoretic
look at automata. In: International Conference on Fundamentals of Software
Engineering. pp. 1–33. Springer (2009)

[2]
Baeten, J.C.M., Luttik, B., van Tilburg, P.: Reactive Turing Machines.
Inform. Comput.  231,  143–166 (2013)

[3]
Bengtson, J., Johansson, M., Parrow, J., Victor, B., et al.: Psi-calculi: a
Framework for Mobile Processes with Nominal Data and Logic. arXiv preprint
arXiv:1101.3262  (2011)

[4]
Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: Mobile
Processes, Nominal Data, and Logic. In: Logic In Computer Science, 2009.
LICS'09. 24th Annual IEEE Symposium on. pp. 39–48. IEEE (2009)

[5]
Bojańczyk, M.: Slightly infinite sets  (2016),
<https://www.mimuw.edu.pl/ bojan/upload/main4.pdf>

[6]
Bojańczyk, M., Klin, B., Lasota, S.: Automata with group actions. In: Logic
in Computer Science (LICS), 2011 26th Annual IEEE Symposium on. pp. 355–364.
IEEE (2011)

[7]
Bojańczyk, M., Klin, B., Lasota, S., Toruńczyk, S.: Turing machines with
atoms. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science,
LICS 2013, New Orleans, LA, USA, June 25-28, 2013. pp. 183–192. IEEE
Computer Society (2013)

[8]
Fu, Y.: The Value-Passing Calculus. In: Theories of Programming and Formal
Methods, pp. 166–195. Springer (2013)

[9]
Gabbay, J.M., Pitts, M.A.: A new approach to abstract syntax with variable
binding. Formal Aspects of Computing  13(3),  341–363 (2002),

[10]
van Glabbeek, R.J.: The linear time — branching time spectrum II. In:
CONCUR'93. pp. 66–81. Springer (1993)

[11]
van Glabbeek, R.J., Luttik, B., Trčka, N.: Branching bisimilarity with
explicit divergence. Fundamenta Informaticae  93(4),  371–392 (2009)

[12]
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in
bisimulation semantics. Journal of the ACM (JACM)  43(3),  555–600 (1996)

[13]
Goldin, D., Smolka, S.A., Wegner, P.: Interactive computation: The new
paradigm. Springer Science & Business Media (2006)

[14]
Groote, J.F., Mathijssen, A., Reniers, M., Usenko, Y., van Weerdenburg, M.:
The Formal Specification Language mCRL2. In: Brinksma, E., Harel, D.,
Mader, A., Stevens, P., Wieringa, R. (eds.) Methods for Modelling Software
Systems (MMOSS). No. 06351 in Dagstuhl Seminar Proceedings, Internationales
Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss
Dagstuhl, Germany, Dagstuhl, Germany (2007),

[15]
Groote, J.F., Mousavi, M.R.: Modeling and analysis of communicating systems.
MIT press (2014)

[16]
Luttik, B., Yang, F.: Executable behaviour and the \(\pi\)-calculus (extended
abstract). In: Knight, S., Lanese, I., Lluch-Lafuente, A., Vieira, H.T.
(eds.) Proceedings 8th Interaction and Concurrency Experience, ICE 2015,
Grenoble, France, 4-5th June 2015. EPTCS, vol. 189, pp. 37–52 (2015),

[17]
Luttik, B., Yang, F.: On the Executability of Interactive Computation. In:
Beckmann, A., Bienvenu, L., Jonoska, N. (eds.) Pursuit of the Universal -
12th Conference on Computability in Europe, CiE 2016, Paris, France, June 27
- July 1, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9709,
pp. 312–322. Springer (2016)

[18]
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I & II.
Information and computation  100(1),  1–77 (1992)

[19]
Parrow, J., Borgström, J., Eriksson, L., Gutkovas, R., Weber, T.: Modal
logics for nominal transition systems. In: Aceto, L., de Frutos-Escrig, D.
(eds.) 26th International Conference on Concurrency Theory, CONCUR 2015,
Madrid, Spain, September 1.4, 2015. LIPIcs, vol. 42, pp. 198–211. Schloss
Dagstuhl - Leibniz-Zentrum fuer Informatik (2015),

[20]
Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes.
Cambridge University Press (2001)

[21]
Turing, A.M.: On computable numbers, with an application to the
Entscheidungsproblem. J. of Math  58,  345–363 (1936)

§ BRANCHING BISIMILARITY

In the definition of (divergence-preserving) branching bisimilarity we need the following notation: let $\step{}$ be an $\Atau$-labelled transition relation on a set $\Sta$, and let $a\in\Atau$; we write $s\step{(a)}t$ for “$s\step{a}t$ or $a=\tau$ and $s=t$”. Furthermore, we denote the transitive closure of $\step{\tau}$ by $\step{}^{+}$ and the reflexive-transitive closure of $\step{\tau}$ by $\step{}^{*}$.

Let $T_1=(\Sta_1,\step{}_1,\uparrow_1)$ and $T_2=(\Sta_2,\step{}_2,\uparrow_2)$ be $\Atau$-labelled transition systems. A branching bisimulation from $T_1$ to $T_2$ is a binary relation $\R\subseteq\Sta_1\times\Sta_2$ such that for all states $s_1$ and $s_2$, $s_1\R s_2$ implies

* if $s_1\step{a}_1s_1'$, then there exist $s_2',s_2''\in\Sta_2$, such that $s_2\step{}_2^{*}s_2''\step{(a)}s_2'$, $s_1\R s_2''$ and $s_1'\R s_2'$;

* if $s_2\step{a}_2s_2'$, then there exist $s_1',s_1''\in\Sta_1$, such that $s_1\step{}_1^{*}s_1''\step{(a)}s_1'$, $s_1''\R s_2$ and $s_1'\R s_2'$.

The transition systems $T_1$ and $T_2$ are branching bisimilar (notation: $T_1\bbisim T_2$) if there exists a branching bisimulation $\R$ from $T_1$ to $T_2$ s.t. $\uparrow_1\R\uparrow_2$.

A branching bisimulation $\R$ from $T_1$ to $T_2$ is divergence-preserving if, for all states $s_1$ and $s_2$, $s_1\R s_2$ implies

* if there exists an infinite sequence $(s_{1,i})_{i\in\mathbb{N}}$ such that $s_1=s_{1,0},\,s_{1,i}\step{\tau}s_{1,i+1}$ and $s_{1,i}\R s_2$ for all $i\in\mathbb{N}$, then there exists a state $s_2'$ such that $s_2\step{}^{+}s_2'$ and $s_{1,i}\R s_2'$ for some $i\in\mathbb{N}$; and

* if there exists an infinite sequence $(s_{2,i})_{i\in\mathbb{N}}$ such that $s_2=s_{2,0},\,s_{2,i}\step{\tau}s_{2,i+1}$ and $s_1\R s_{2,i}$ for all $i\in\mathbb{N}$, then there exists a state $s_1'$ such that $s_1\step{}^{+}s_1'$ and $s_1'\R s_{2,i}$ for some $i\in\mathbb{N}$.

The transition systems $T_1$ and $T_2$ are divergence-preserving branching bisimilar (notation: $T_1\bbisimd T_2$) if there exists a divergence-preserving branching bisimulation $\R$ from $T_1$ to $T_2$ such that $\uparrow_1\R\uparrow_2$.

§ SUPPLEMENTARY MATERIAL FOR

*Proof of Theorem <ref>

Let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be an $\Atau$-labelled countable transition system, and let $\encode{\_}: \Sta_T\rightarrow \mathbb{N}$ be an injective function encoding its states as natural numbers. Then, an RTM with infinite sets of action symbols and data symbols $\M(T)=(\Sta,\step{},\uparrow)$ is defined as follows.

* $\Sta=\{s,t,\uparrow\}$ is the set of control states.

* $\step{}$ is a finite $(\Dbox\times\A\times\Dbox\times\{L,R\})$-labelled transition relation, and it consists of the following transitions:

* $(\uparrow,\tau,\Box,\encode{\uparrow_T},R,s)$,

* $(s,\tau,\Box,\Box,L,t)$, and

* $(t,a,\encode{s_1},\encode{s_2},R,s)$ for every transition $s_1\step{a}_T s_2$.

* ${\uparrow}\in\Sta$ is the initial state.

Note that a transition step $s_1\step{a}s_2$ is simulated by a sequence

\begin{equation*}
\enskip.
\end{equation*}

Then one can verify that $\T(\M(T))\bbisimd T$.

*Proof of Lemma <ref>

* $\Rightarrow$: We suppose that $K$ is a support of $\step{}_T$, then by the definition of support, for every $K$-automorphism $\pi_K$, we have $\pi_K(\step{}_T)=\step{}_T$. Therefore, for every $(s,a,t)\in{\step{}_T}$, we have $\pi_K(s,a,t)\in{\step{}_T}$.

* $\Leftarrow$: We suppose that for every $(s,a,t)\in{\step{}_T}$ and for every $K$-automorphism $\pi_K$, we have $\pi_K(s,a,t)\in{\step{}_T}$ then we have $\pi_K(\step{}_T)=\step{}_T$, Therefore $K$ is a support of $\step{}_T$.

*Proof of Lemma <ref>

As $\step{}_{\M}$ is a legal set. We take $K$ to be its the minimal support. Then we conclude the lemma from the definition of the support.

*Proof of Lemma <ref>

Suppose that there exists such an . If $x$ is in the support of the transitions of , then the function can be trivially realized. However, introducing infinitely many atoms to the support will lead to an illegal transition relation. Therefore, $x$ is not in the support of the transitions of .

As $x$ is not in the support, then for any transition that creates $x$, every $\pi(x)$ is created by another branch of execution, where $\pi$ is an arbitrary atom automorphism that preserves the support of the transitions of . Hence, whenever an $x$-labelled transition is produced, some $\pi(x)$-labelled transition can be produced in some other branch of execution. Hence, this is not the required .

§ SUPPLEMENTARY MATERIAL FOR

*Details of Example <ref>

We denote the current tape instance by $\bar{a}\bar{b}$, and we show the two ways to add a new atom to $\bar{b}$.

For the first case, we suppose that $x$ is the atom in $\bar{a}$ to be duplicated, and the first empty cell after $\bar{b}$ is the destination of the duplication. The machine could accomplish the task by the transitions $\cop\step{\tau[x/x]R}\cop_x\step{\tau[y/y]R}{}^{*}\step{\tau[\Box/x]}\finish$, which is realized by the following set of transitions.

\begin{eqnarray*}
&\{(\cop,\tau,x,x,R,\cop_x)\mid x\in\Atom\}\\
&\cup\{(\cop_x,\tau,y,y,R,\cop_x)\mid x,y\in\Atom\}\\
&\cup\{(\cop_x,\tau,\Box,x,R,\finish)\mid x\in\Atom\}
\enskip.
\end{eqnarray*}

This is a legal and orbit-finite set of transitions.

For the second case, the machine creates a fresh atom, by the following set of transitions,

\begin{eqnarray*}
&\{(\fresh,\tau,\Box,x,L,\chec_x)\mid x\in\Atom\}\\
&\cup\{(\chec_x,\tau,y,y,L,\chec_x)\mid x\neq y\wedge y\neq \Box\wedge x,y\in\Atom\}\\
&\cup\{(\chec_x,\tau,x,x,L,\refresh_x)\mid x\in\Atom\}\\
&\cup\{(\refresh_x,\tau,y,y,R,\refresh_x)\mid x\neq y\wedge x,y\in\Atom\}\\
&\cup\{(\refresh_x,\tau,x,y,L,\chec_y)\mid x\neq y\wedge x,y\in\Atom\}\\
&\cup\{(\chec_x,\tau,\Box,\Box,R,\finish)\mid x\in\Atom\}
\enskip.
\end{eqnarray*}

The machine first creates an arbitrary atom $x$, and then it checks every atom on the tape whether it is identical with $x$. We suppose that $\Box$ indicates the end of the sequence of atoms on tape. If the check procedure succeeds, the creation is finished, otherwise, the machine creates another atom and checks again.
We also verify that the above transitions form a legal and orbit-finite set.

*Details of Example <ref>
We define an  $M=(\Sta_M,\step{}_M,\uparrow_M)$, and we show that $M$ suffices the requirement.

According to the assumption, we suppose that in the state $\start$, the tape instance is $\encode{\sete{x}}\tup{x}$. It suffices to show that within finitely many steps, the machine is able to write $x$ as one symbol on the tape.

Note that $X$ is an orbit-finite set, which means that there are finitely many distinct orbits that construct the set $X$. Therefore, there are finitely many distinct values of $\encode{\sete{x}}$ for all the elements in $X$. The machine associates with each value a program that calculates $\setb{\sete{x}}(\tup{x})$, which produces the elements from that specific orbit according to the valuation of $\bar{x}$. The machine enters the programme by entering the state $\encode{\sete{x}}$.

\begin{equation*}
\{(\start,\tau,\encode{\sete{x}},\encode{\sete{x}},R,\encode{\sete{x}})\mid x\in X\}
\enskip.
\end{equation*}

As $X$ is orbit-finite, there is an upper-bound for the length of the tuple $\bar{x}$ for every $x\in X$. The machine can represent a tuple as a data symbol.
We suppose that every element in $x$-orbit uses $n$ free variables in its structure, then $\bar{x}$ is a tuple of $n$ atoms. Now we consider the following set of transitions:

\begin{equation*}
\{(\encode{\sete{x}},\setb{\sete{x}}(\tup{x}),\tup{x},\setb{\sete{x}}(\tup{x}),R,\finish\mid a_1\ldots a_n\in \Atom\}
\enskip.
\end{equation*}

These transitions will create $x$ by $\setb{\sete{x}}(\tup{x})$. We suppose that $\tup{x}$ is of the form $(a_1,\ldots,a_n)$. The above set of transitions is orbit-finite, since there is an upper bound of $n$,

Moreover, we show that the machine is able to create a tuple $\tup{x}$ as one symbol, given that each atom in $\tup{x}$ is written on one tape cell, and ordered from left to right as the order of the atoms in the tuple.

The machine constructs $\bar{x}$ by duplicating the elements from each tape cell to the tuple one by one, using the transitions as follows:

\begin{eqnarray*}
&\{(\encode{\sete{x}},\tau,a,a,R,(\encode{\sete{x}},a))\mid a\in\Atom\}\\
&\cup\{((\encode{\sete{x}},a),\tau,b,b,R,(\encode{\sete{x}},a))\mid a,b\in\Atom\}\\
&\cup\{((\encode{\sete{x}},a),\tau,\Box,(a),L,(\encode{\sete{x}},a)')\mid a\in\Atom\}\\
&\cup\{((\encode{\sete{x}},a_i),\tau,(a_1,\ldots,a_{i-1}),(a_1,\ldots,a_{i-1},a_i),L,(\encode{\sete{x}},a_i)')\mid a_1,\ldots, a_i\in \Atom, 2 \leq i\leq n\}\\
&\cup\{((\encode{\sete{x}},a)',\tau,b,b,L,(\encode{\sete{x}},a)')\mid a,b\in \Atom,\, a\neq b\}\\
&\cup\{((\encode{\sete{x}},a)',\tau,a,a,R,\encode{\sete{x}})\mid a\in\Atom\}\\
\enskip.
\end{eqnarray*}

The machine first finds the atom to duplicate, and uses a state $(\encode{\sete{x}},a)$ to register the atom $a$. Then it moves the tape head to the tuple and adds the atom to that tuple. If the tuple is empty, then the machine produces $(a)$, otherwise, the machine adds $a$ to an existed tuple $(a_1,\ldots,a_{i-1})$, and enters the state $(\encode{\sete{x}},a)'$. Finally, the tape goes back to the atom it duplicated and enters state $\encode{\sete{x}}$ again to start the duplication of the next atom. This procedure ends by finishing the duplication of all the atoms in $\bar{x}$, and entering the state $\encode{\sete{x}}$ with $\tup{x}$ written under the tape head. Hence, the machine is ready to produce $\setb{\sete{x}}(\tup{x})$.

Since there is an upper bound of the length of the atom, this set of transitions is legal and orbit-finite. Moreover, there are finitely many orbits for the set $X$, which means that the machine needs finitely many such programs.
Hence, we have obtained an  $M$ that meets the requirement.

*Proof of Lemma <ref>

We let $T=(\Sta_T,\step{}_T,\uparrow_T)$ be an effective $\Atau$-labelled transition system with atoms, and let $K\subset\Atom$ be the minimal support of $T$. We show that there exists an  $\M=(\Sta_{\M},\step{}_{\M},\uparrow_{\M})$ such that $\T(\M)\bbisim T$.

As $T$ is effective, for every state $s\in\Sta_T$, the set $\mathalpha{out}(\encode{\sete{s}})=\{\encode{\sete{(s,a,t)}}\mid s\step{a}_T t\}$ is recursively enumerable. We use this fact to simulate the transition system. We describe the simulation in $3$ stages.

* Initially, the tape is empty. Hence the initial configuration is $(\uparrow_{\M},\tphd{\Box})$. For simplicity, we do not denote the position of the tape head in the tape instances. The machine first writes the representation of the initial state $\uparrow_T$, i.e., $\encode{\sete{\uparrow_T}}\tup{\uparrow_T}$ on the tape, satisfying $\setb{\sete{\uparrow_T}}(\tup{\uparrow_T})=\uparrow_T$. As $T$ is legal, $\tup{\uparrow_T}$ consists of finitely many atoms. The initialization procedure is represented as follows,

\begin{equation*}
\enskip.
\end{equation*}

In the control state $\enu$, we assume that the tape instance is $\encode{\sete{s}}\tup{s}$, satisfying $\setb{\sete{s}}(\tup{s})=s$. As the transition system is effective, the machine is able to enumerate the structure of the outgoing transitions of $s$ as follows,

\begin{equation*}
\enskip.
\end{equation*}

For state $s$, its subsequent transitions are $\{(s,a,t)\in \step{}_T\}$ and by the proposition of transition system with atoms, the set of transitions from $\pi_K(s)$ is $\pi_K{\{(s,a,t)\in \step{}_T\}}$. We use this fact to enumerate the transitions from $s$ and take a $\pi_K$ automorphism by the the atoms $\atom(\pi_K(s))$ which is already on the tape, and hence we obtained the transitions from $\pi_K(s)$.

Then the machine enumerates $\mathalpha{out}(s)$,  and writes $(\encode{a},\encode{t})$ (which are represented by $\encode{\orb_{[a]}},\encode{\atom(a)},\encode{\orb_{[t]}},\encode{\atom(t)}$ respectively) on the tape whenever a transition $(s,a,t)$ is enumerated.

The step of enumeration is represented as follows,

\begin{eqnarray*}
\enskip.
\end{eqnarray*}

* In the second stage, the  produces the tuples of atoms $\tup{a}$ and $\tup{t}$ that valuates the free variables of $a$ and $t$. The valuation creates fresh atoms when necessary and preserves atoms from $K$ and $\tup{s}$.

We denote the tuple of free variables of $\sete{(s,a,t)}$ by $\bar{x}$, and tuples of free variables of $\sete{s}$, $\sete{a}$ and $\sete{t}$ by $\bar{x_s}$, $\bar{x_a}$ and $\bar{x_t}$ respectively. Note that all the variables in $\bar{x_s}$, $\bar{x_a}$ and $\bar{x_t}$ are also in $\bar{x}$. Since $\encode{\sete{(s,a,t)}}$ is already on the tape, the following terms are computable:

* the set builder expressions of $a$ and $t$: $\encode{\sete{a}}$ and $\encode{\sete{t}}$;

* the tuples of free variables: $\bar{x}$, $\bar{x_s}$, $\bar{x_a}$ and $\bar{x_t}$;

We show the above statements as follows. We define a triple $(s,a,t)$ by $\{\{s\},\{s,a\},\{s,a,t\}\}$. We use the standard Gödel numbering on sets and variables. The encoding $\encode{\sete{(s,a,t)}}$ is equal to $\encode{\{\{\sete{s}\},\{\sete{s},\sete{a}\},\{\sete{s},\sete{a},\sete{t}\}\}}$. $\encode{\sete{a}}$ and $\encode{\sete{t}}$ are all computable because the projection operation is computable in Gödel encoding of ordered triples. Moreover, the projection from $\encode{\sete{x}}$ to the free variables used in each elements are computable.

Then we evaluate $\bar{x}$ to tuples of atoms. $\tup{s}$ is a valuation of $\bar{x_s}$. We evaluate $\bar{x}$ by distinguishing two cases:

* if a variable $y$ in $\bar{x}$ also appears in $\bar{x_s}$, then we duplicate the valuation of that variable from $\tup{s}$ to valuate $y$;

* otherwise, we create a fresh atom to valuate $y$.

By Example <ref>, the above two operations are valid by s.
Since $\bar{x_a}$ and $\bar{x_t}$ are both sub-tuples of $\bar{x}$, the machine duplicates the valuation from $\bar{x}$ to create $\tup{a}$ and $\tup{t}$.

Hence, we get $\encode{\sete{a}}$, $\encode{\sete{t}}$, $\tup{a}$ and $\tup{t}$ satisfying that $\setb{\sete{a}}(\tup{a})=a'$, $\setb{\sete{t}}(\tup{t})=t'$, and there exists an $K\cup\tup{s}$-automorphism $\pi$ which preserves all the atoms in $K\cup\tup{s}$, such that $\pi(s,a',t')=(s,a,t)$. By the property of transition system with atoms, $(s,a',t')\in\step{}_T$. Moreover, by Example <ref>, during the generation of fresh variables, every fresh variable from the universe of $\Atom$ can be generated, the  is able to create all the transitions which are equivalent to $(s,a,t)$ up to $K\cup\tup{s}$-automorphism. We denote this stage as follows:

\begin{equation*}
\enskip.
\end{equation*}

We use $\pi_{K\cup s}$ to denote some arbitrary atom automorphism that preserves the support $K$ and the atoms from the state $\pi_K(s)$, and $\pi_{K\cup s\cup a}$ to denote some arbitrary atom automorphism that preserves $K$, $\pi_K(s)$ and $\atom(\pi_{K\cup s}(a))$. Then the machine nondeterministically produces $\atom(\pi_{K\cup s}(a))$ and $\atom(\pi_{K\cup s\cup a}(t))$ according to $\atom(s)$, $\encode{\atom(s)}$, $\encode{\atom(a)}$ and $\encode{\atom(t)}$, for some arbitrary $\pi_{K\cup s}$ and $\pi_{K\cup s\cup a}$.

The machine first generates $\atom(\pi_{K\cup s}(a))$. For every element $\encode{x}\in\encode{\atom(a)}$, we distinguish with two cases:

* if $\encode{x}$  also in $\encode{\atom(s)}$, then the machine find the the corresponding element from $\atom(\pi_K(s))$ and duplicate that one to fills the position of $\encode{x}$ in $\atom(\pi_{K\cup s}(a))$;

* if $\encode{x}$ not in $\encode{\atom(s)}$, then the machine create a fresh atom and fills the position of $\encode{x}$ in $\atom(\pi_{K\cup s}(a))$.

Then the machine then generates $\atom(\pi_{K\cup s\cup a}(t))$. For every element $\encode{x}\in\encode{\atom(t)}$, we also distinguish with two cases:

* if $\encode{x}$ is also in $\encode{\atom(s)}$ or $\encode{\atom(a)}$ , then the machine find the the corresponding element from $\atom(\pi_K(s))$ or $\atom(\pi_{K\cup s}(a))$ and duplicate that one to fills the position of $\encode{x}$ in $\atom(\pi_{K\cup s\cup a }(t))$;

* if $\encode{x}$ is not in $\encode{\atom(s)}$ nor in $\encode{\atom(a)}$ , then the machine create a fresh atom and fills the position of $\encode{x}$ in $\atom(\pi_{K\cup s\cup a}(t))$.

By Example <ref>, duplication and creating of atoms are valid operations for .

We denote this step as follows,

\begin{eqnarray*}
&(\act,\encode{\orb_{[s]}}\encode{\orb_{[a]}}\encode{\orb_{[t]}}\encode{\atom(s)}\encode{\atom(a)}\encode{\atom(t)}\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t)))
\enskip.
\end{eqnarray*}

* In the third stage, the  generates the action label $a'$ and chooses to execute the transition or to continue the enumeration.

As $\Atau$ is a legal and orbit-finite set, by Example <ref>, the  is able to create a symbol $a'$ such that $\setb{\sete{a}}\tup{a}=a'$.

\begin{equation*}
\enskip.
\end{equation*}

Then the  has two choices: executing the $a'$-labelled transition and starting the next round of simulation or returning to the first stage.

\begin{eqnarray*}
\end{eqnarray*}

Hence, the machine will produce a label $\pi_{K\cup s}(a)$ from $\atom(\pi_{K\cup s}(a))$ and $\encode{\orb_{[a]}}$. By Corollary <ref>, this step is computable by an . According to the property of transition systems with atoms, the transition to be simulated $(\pi_K(s),\pi_{K\cup s}(a),\pi_{K\cup s\cup a}(t))\in\step{}_T$. Moreover, the procedure of generating fresh atoms, it is guaranteed that every transition $(\pi_K(s),a',t')\in\step{}_T$ satisfying that there exists some $\pi_{K\cup s}$ such that $\pi_{K\cup s}(\pi_K(s),a,t)=(\pi_K(s),a',t')$ are produced in the previous step.

This procedure of producing the action label is represented as follows,

\begin{eqnarray*}
&\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t)))\step{}^{*}\\
&\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t))\pi_{K\cup s}(a))
\enskip.
\end{eqnarray*}

* $\tran\Rightarrow\enu$:

Finally the machine simulates the transition or continues the enumeration.

\begin{eqnarray*}
&\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t))\pi_{K\cup s}(a))\step{\pi_{K\cup s}(a)}\step{}^{*}\\
&(\enu,\encode{\orb_{[t]}}\encode{\atom(t)}\atom(\pi_{K\cup s\cup a}(t)))\\
&\atom(\pi_K(s))\atom(\pi_{K\cup s}(a))\atom(\pi_{K\cup s\cup a}(t))\pi_{K\cup s}(a))
\step{}^{*}\\
\enskip.
\end{eqnarray*}

We can verify that before the $a'$-labelled transition, the transition system of the machine preserves its states modulo $\bbisim$ by a sequence of $\tau$-transitions which leads back to the configuration $(\enu,\encode{\sete{s}}\tup{s})$. Moreover, from the above analysis, we have $(s,a',t')\in\step{}_T$; and every transition obtained by an $K\cup\tup{s}$-automorphism from $(s,a,t)$ can be simulated by the  $M$. Therefore, we conclude that $T\bbisim \T(\M)$.

*Proof of Lemma <ref>

It is obvious that $\T(\M)$ is effective.