Frank S De Boer
email: f.s.de.boer@cwi.nl

MAHDI JAGHOORI b , COSIMO LANEVE c Gianluigi Zavattaro
email: gianluigi.zavattaro@unibo.it

M M Jaghoori
email: jaghoori@cwi.nl

C Laneve

DECIDABILITY PROBLEMS FOR ACTOR SYSTEMS *

Keywords: [Software and its engineering]: Software notations and tools-General programming languages-Language types-Concurrent programming languages; [Theory of computation]: Semantics and reasoning-Program reasoning-Program verification Actors, RESTful services, decidability problems, 2-Counter Machines, wellstructured transition systems, embedding relation

We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. This decidability result still holds for actors with states when the number of actors is bounded and the state is read-only.

ACM CCS:

Introduction

Since their introduction in [START_REF] Hewitt | Procedural embedding of knowledge in planner[END_REF], actor languages have evolved as a powerful computational model for defining distributed and concurrent systems [START_REF] Agha | The structure and semantics of actor languages[END_REF][START_REF] Agha | A foundation for actor computation[END_REF]. Languages based on actors have been also designed for modelling embedded systems [START_REF] Lee | Classes and inheritance in actor-oriented design[END_REF][START_REF] Lee | Actor-oriented design of embedded hardware and software systems[END_REF], wireless sensor networks [START_REF] Cheong | Viptos: a graphical development and simulation environment for tinyos-based wireless sensor networks[END_REF][START_REF] Razavi | Sysfier: Actor-based formal verification of systemc[END_REF], multi-core programming [START_REF] Karmani | Actor frameworks for the jvm platform: a comparative analysis[END_REF], and web services [START_REF] Chang | Supporting reconfigurable object distribution for customized web applications[END_REF][START_REF] Chang | Towards context-aware web applications[END_REF]. The underlying concurrent model of actor languages also forms the basis of the programming languages Erlang [START_REF] Armstrong | Erlang[END_REF] and Scala [START_REF] Haller | Scala actors: Unifying thread-based and event-based programming[END_REF] that have recently gained in popularity, in part due to their support for scalable concurrency.

In actor languages [START_REF] Agha | The structure and semantics of actor languages[END_REF][START_REF] Hewitt | Procedural embedding of knowledge in planner[END_REF][START_REF] Sirjani | Rebeca: Theory, applications, and tools[END_REF], actors use a queue for storing the invocations to their methods in a FIFO manner. The queued invocations are processed sequentially by executing the corresponding method bodies. The encapsulated memory of an actor is represented by a finite number of fields that can be read and set by its methods and as such exist throughout its life time.

In this paper we introduce a nominal actor-based language and study its expressive power. This language, besides dynamic creation of actors, also supports the dynamic creation of variable names that can be stored in fields and communicated in method calls. As such our nominal actor-based language gives rise to unboundedness in [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF] internal queues of the actors, (2) dynamic actor creation/activation and (3) dynamic creation of variable names.

Statelessness has recently been adopted as a basic principle of service oriented computing, in particular by RESTful services. Such services are designed to be stateless, and contextual information should be added to messages, so a service can customize replies simply by looking at the received request messages. In service oriented computing read-only fields (which are initialized upon activation) are used to provide configuration/deployment information that distinguishes the distinct instances of the same service. We have identified the presence/absence of fields as a crucial feature of our language: (1) and (3) in combination with fields gives rise to a Turing complete calculus. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination and process reachability are decidable. In order to preserve this decidability result to actors with states we have to restrict the number of actors to be finite and the state to be read-only.

More specifically, we model a system consisting of finitely many actors with read-only fields as a well-structured transition system [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] -henceforth termination and process reachability are decidable. Further, we show that an abstraction of systems of unboundedly many stateless actors (i.e., actors without fields) which preserves termination and process reachability is also an instance of well-structured transition system. It turns out that, in the context of unbounded actor creation, this restriction to stateless actors is necessary by a reduction to the halting problem for 2 Counter Machines.

To the best of our knowledge, the technique we use to establish the decidability results for the above languages is original since (i ) these systems respectively admit the creation of unboundedly many variables and actor names; (ii ) actors in general are sensitive to the identity of names because of the presence of a name-match operator. In particular, in the case of finitely many actors with read-only fields, we define an equivalence on process instances in terms of renamings of the variables that generate the same partition. This equivalence allows us to compute an upper bound to the instances of method bodies, which is the basic argument for the model being a well-structured transition system. In case of systems with unboundedly many stateless actors, the reasonable extensions of this equivalence on process instances have been unsuccessful because of the required abstraction of the identity of actor names. Therefore we decided to apply our arguments to an abstract operational model where messages may be enqueued in every actor of the same class. The above equivalence can be successfully used in this model, thus yielding again the upper bounds for the number of method body instances. Further, the abstract model still provides enough information to derive decidable properties of the language. Related Works. There exists a vast body of related work on decidability of infinite-state systems (see [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF]). However, to the best of our knowledge, the specific characteristics of the pure asynchronous mechanism of queued and dequeued method calls in actor-based languages has not been addressed. It is interesting to observe that the most expressive known fragment of the pi-calculus for which interesting verification problems are still decidable is the depth-bounded fragment [START_REF] Meyer | On boundedness in depth in the pi-calculus[END_REF]. In [START_REF] Wies | Forward analysis of depth-bounded processes[END_REF] the theory of well-structured transition systems is applied to prove the decidability of coverability problems for bounded depth pi-calculus. Our nominal actor language also features the creation and communication of new names. In our decidable fragments however, differently from the depth-bounded pi-calculus fragment, we do not restrict the creation and communication of names. For instance, in the queue of an actor we might have unboundedly many messages (representing process continuations) where each message shares one name with the previous message in the queue. Decidability of asynchronous communication via a shared data space, read operation and non-blocking test operators on the shared space of the coordination language Linda has been studied in [START_REF] Busi | On the expressiveness of linda coordination primitives[END_REF]. In [START_REF] Bouajjani | Context-bounded analysis of multithreaded programs with dynamic linked structures[END_REF] the authors introduce an algorithm for reachability analysis of multithreaded object-oriented programs. This algorithm requires both a bound on the number of context switches (between the threads) and the visible heap. Further their approach is specific to object-oriented programs and is not applicable to actor-based languages, which are based on a different concurrency model. As another final example, a system composed of finitely many actors can be easily modeled as a communicating finite state machine [START_REF] Brand | On communicating finite-state machines[END_REF], a formalism that is known to be Turing complete [START_REF] Brand | On communicating finite-state machines[END_REF][START_REF] Memmi | An introduction to fifo nets monogeneous nets: A subclass of fifo nets[END_REF]. However, this modelling does not scale to infinite actors and does not display the execution model of actors. Recent work on actor-based language focusses on deadlock analysis: In [START_REF] Giachino | Analysis of deadlocks in object groups[END_REF], a technique for the deadlock analysis has been introduced for a version of Featherweight Java which features asynchronous method invocations and a synchronization mechanism based on futures variables. The approach followed in [START_REF] De Boer | Termination detection for active objects[END_REF] for detecting deadlock in an actor-like subset of Creol [START_REF] Johnsen | An asynchronous communication model for distributed concurrent objects[END_REF] is based on suitable over-approximations.

The language Actor

Four disjoint infinite sets of names are used: actor classes, ranged over by C, D, • • • , method names, ranged over by m, m ′ , n, n ′ , • • • , field names, ranged over by f, g, • • • , and variables, ranged over by x, y, z, • • • . For notational convenience, we use x when we refer to a list of variables x 1 , . . . , x n (and similarly for other kinds of terms).

The syntax of the language Actor uses expressions E and processes P defined by the rules

E ::= f | x | new C( E) P ::= 0 | (f ← E).P | let x = E in P | x!m( E).P | [E = E]P ;P | P + P
An expression E either denotes a value stored in a field f, or a variable x, or a new actor of class C with fields initialized to the values of E. A process may be either the terminated one, denoted by 0, or a field update (f ← E).P , or the assignment let x = E in P of a value to a variable, or an invocation x!m( E).P of a method m of the actor x with arguments E, or a check [E = E ′ ]P ;P ′ of the identity of expressions with positive and negative continuations, or, finally a nondeterministic process P + P ′ . We never write the tailing 0 in processes; for example (f ← x).0 will be always shortened into (f ← x). We will also shorten [E = E ′ ]P ;0 into [E = E ′ ]P . Following the tradition of process calculi like CCS [START_REF] Milner | Communication and concurrency[END_REF], we model sequences of actions by exploiting the so-called prefix notation (like, e.g., in (f ← E).P ).

The operation let x = E in P is a binder of the occurrences of the variable x in the process P that are not already bound by a nested let operation of x; the occurrences of x in E are free. Let free(P ) be the set of variables of P that are not bound. As usual, we identify processes P and P ′ that are equal up-to alpha-conversion of bound names, written P = α P ′ . The substitution operation P [ y / x ] returns the process P where the free occurrences of x are replaced by y. The substitution operation P [ y / x ] returns the process P where the free occurrences of x are simultaneously replaced by y. In case, alpha-renaming is required for avoiding name clashes. For example

let z = x in new C(y, z)[ z, u / x, y ] returns let z ′ = z in new C(u, z ′ ).
In the following examples and encodings we shorten let x = f in x!m( E).P into f!m( E).P (we have preferred the simpler syntax to ease the descriptions).

A program is a main process P and a finite set of actor class definitions C.m( x) = P C,m , where P C,m may contain the special variable this (which can be seen as an implicit formal parameter of each method). In the following we restrict to programs that are (1) unambiguous, namely, every pair C, m has at most one definition;

(2) correct, namely, let fields(•) be a map that associates a tuple of field names to every actor class. Then, (i ) in every expression new C( E), the length of the tuples E and fields(C) are the same; (ii ) in every definition C.m( x) = P C,m , the field names occurring in P C,m are in the tuple fields(C). In this paper, we abstract from types and type-correctness because we are only interested in expressive power issues. However, it is straightforward to equip the above language with a type discipline.

2.1.

Examples. To illustrate the features of the actor language we discuss four examples.

Example 2.1. The merger service is an application that forwards to a back office server the values carried by two invocations of clients to methods first and second . The merger freezes the forward as long as there is no invocation of either first or second -in the process calculi community, the merger is modelled by a join pattern [START_REF] Fournet | The reflexive cham and the join-calculus[END_REF]. In our actor language the merger is modelled by a class actor Merger with six fields: t and f storing the values true and false, respectively; fst and snd storing true or false according to the method first and second have been invoked or not, respectively; g storing the argument of the invocation; srv storing the actor name of the back office server.

The class actor Merger includes the following three methods:

Merger.init (x) = (t ← tt).(f ← ff ).(fst ← ff ).(snd ← ff ).(srv ← x) Merger.first(a) = [snd = t] srv!m(a, g).(snd ← f); [fst = f] (fst ← t).(g ← a);this!first(a) Merger.second (a) = [fst = t] srv!m(g, a).(fst ← f); [snd = f] (snd ← t).(g ← a);this!second (a)
The method init manifests a basic feature of our actor language: the creation of new variables. In particular, tt and ff are free variables in the method definition of init. When init will be invoked, they will be replaced by two different fresh variables (said in pi-calculus jargon [START_REF] Milner | A calculus of mobile processes[END_REF], we are assuming an implicit (ν tt, ff )-at the beginning of the method body).

These variables are stored in the fields t and f, respectively and they will be used to update the fields fst and snd appropriately . The merger forwards two messages to the server, which is stored in the field srv. These messages have been received through invocations of first and second. No forward occurs if one of the two methods has not been invoked. In particular, first (the method second behaves in a similar way) performs the forward if second has been evaluated and its message has not been already forwarded (field snd equal to tt); in this case the parameter of the invocation of second has been stored into g. Otherwise, if there is no previous invocation to first, still to be forwarded, (field fst equal to ff ) then fst is set to tt and the parameter stored into g. There is a possibility that first is evaluated and a previous evaluation of first has still to be forwarded (field fst equal to tt). In this case, the invocation is bounced back (it is enqueued in the actor queue -see the operational semantics).

Example 2.2. As a second example we model the OpenID authentication protocol [START_REF]Openid specifications[END_REF]. Three actors are considered: a client, a server, and an authProvider. The client sends a login request to the server. The server generates two secure tokens clientToken and authToken, used for secure communication with the client and the authProvider, respectively, and then sends the two tokens to the corresponding actors. Subsequently, the client sends an authentication message to the authProvider that (after checking the correctness of the username and password) communicates to the server whether the authentication succeeds or fails. In the following, we abstract from the management of username and password and we simply assume that they are stored in the fields u and p of the client when it sends the authenticate message to the authServer. A.open(server , cToken, aToken) = (server ← server ).(ctoken ← cToken).

(atoken ← aToken) A.authenticate(u, p, cToken) = [ctoken = cT oken] server!succeeds(atoken); server!fails(atoken) The main program that instantiates the client, the server and the authProvider is as follows:

let client = new C in let server = new S in let authProvider = new A in client!init(server ).server !init(authProvider )

Example 2.3. We illustrate the modeling of a register that stores natural numbers and supports the operations of increment and decrement, when its value is positive. In the absence of data-types in our nominal actor language, we model a register by an actor and implement the value of the register by the number of invocations of the method item stored in its queue. Below we describe the corresponding class R, assuming a class Ctrl which encodes the control of the register machine. When an operation is performed, the register replies with an invocation run(pc, tt, ff ), where pc is a suitable continuation. The continuation is unique when the increment is invoked; the decrement has two possible continuations: a positive one, in case of success, and a negative one (the register was 0, no decrement is performed).

// R has a field called dec, Ctrl is an actor in the context R.inc(pc, tt, ff

) = R!item(tt, ff ).Ctrl !run(pc, tt, ff ) R.dec(pc, pc ′ , tt, ff ) = (dec ← tt).R!checkzero(pc, pc ′ , tt, ff ) R.checkzero(pc, pc ′ , tt, ff ) = [dec = tt]Ctrl !run(pc ′ , tt, ff ).(dec ← ff );Ctrl !run(pc, tt, ff ) R.init(tt, ff ) = (dec ← ff ) R.item(tt, ff ) = [dec = ff ]R!item(tt, ff );(dec ← ff )
Method inc simply gives rise to the storage of a new message item and a trigger of the continuation. Executing a message item, amounts to bouncing the invocation back if the value of the field dec is false. In this case the invocation is enqueued again. Otherwise the invocations is "consumed" because there was a pending decrement to perform (see below) and dec is set to true (indicating that there is no pending decrement anymore). Method dec is the tricky one: it sets dec to true and add an invocation of checkzero (we are assuming that the register queue always contains at most one invocation of dec). That is, we are postponing the triggering of the continuation to the evaluation of checkzero that will occur after the evaluation of any other method in the queue of the register. When checkzero will be evaluated either (i) the dec field is true, this means that the register did not contained any item message -its value was 0 -and the continuation pc ′ is triggered; or (ii) the dec field is false, that is the register has been decremented and the continuation pc is triggered. A refinement of the above register is used in Theorem 3.2 to demonstrate the Turing completeness of a sublanguage of Actor.

Example 2.4. In Sections 4 and 5 we will respectively prove decidability results for two fragments of our actor language: in the first fragment only the main program can create new actors (so boundedly many actors can be created) and fields are read-only, while in the second fragment actors have an empty state. To illustrate these two fragments we show how they can be used to model a system in which n workers are used to execute n distinct tasks indicated by a client.

In the fragment with bounded actors and read-only fields the model can be described by considering a class C for the client with an init method responsible for invoking the task manager, passing him the description of the n tasks to be executed:

// C has no fields C.init (TManager ) = TManager !tasksExec(t 1 , • • • , t n )
The task manager is an instance of a class providing a method called tasksExec able to pass to the workers the description of their relative tasks:

// T M has n fields called W1, • • • , Wn, T M.tasksExec(p 1 , • • • , p n ) = W1!exec(p 1 ). • • • .Wn!exec(p n )
Finally, a worker is an instance of a class W with one method exec able to execute the passed task (we leave this method unspecified):

// W has no fields and one method exec(p) The main program first instantiates the workers, then the task manager by storing in its state the reference to the workers, and finally the client; after the init method of the client is invoked passing him a reference to the task manager:

let w 1 = new W in • • • let w n = new W in let taskManager = new TMs(w 1 , • • • , w n ) in let client = new C in client!init(taskManager )
In the fragment with stateless actors we present an alternative specification of the system in which the classes for the client and the workers are as above, while the task manager is defined as follows:

// T M has no fields T M.tasksExec(p 1 , • • • , p n ) = this!nextTask (p 1 , • • • , p n , x 1 , x 2 , • • • , x n , x 1 ) T M.nextTask (p 1 , • • • , p n , v 1 , • • • , v n+1 ) = [v 1 = v 2 ]0;let w = new W in w!exec(p 1 ). this!nextTask (p 2 , • • • , p n , p 1 , v 2 , • • • , v n+1 , v 1 )
Upon reception of the n tasks to be executed, the task manager passes the task descriptions to the method nextTask. This method instantiates one new worker, passes to it the corresponding task, and then recursively invokes itself to continue with worker instantiations. In order to execute exactly n recursive calls, n + 1 additional parameters are considered: in the first call all such parameters are distinct excluding the first and the last one, at every call the parameters are circularly shifted, and when the first two parameters coincide the chain of calls is terminated.

2.2. The operational semantics. The operational semantics of the language Actor will use an infinite set of actor names, ranged over A, B, • • • . This set is partitioned by the actor classes in such a way that every partition retains infinitely many actor names. We write A ∈ C to say that A belongs to the partition of C. In the following, the (run-time) expressions will also include actor names and, with an abuse of notation, this extended set of expressions will be ranged over by E. The set of terms that are variables or actor names, called values, will be addressed by U , V , • • • . Similarly for processes that, at run-time, may also have actor names. The extended set will be addressed by P . We notice that free(P ), when P belongs to this extended set, may returns variables and actor names. We will also apply free(•) to tuples of (extended) expressions: free( E) returns the set of variables and actor names in E.

The semantics is defined in terms of a transition relation S -→ S ′ , where S, S ′ , called configurations, are sets of terms A ⊲ (P, ϕ, q) with A being an actor name, ϕ, the state of A, being a map from fields(C) to values, where A ∈ C, and q being a queue of terms m( U ). The empty queue will be denoted with ε. Configurations contain at most one A ⊲ (P, ϕ, q) for each actor name A. As usual, let -→ * be the transitive closure of -→ and -→ + be -→-→ * .

U ϕ U ; ∅ f ϕ ϕ(f) ; ∅ E ϕ U ; S f = fields(C) A = fresh(C) new C( E) ϕ A ; A ⊲ (0, [ f → U ], ε), S E i ϕ U i ; S i , for i ∈ 1..n E 1 , • • • , E n ϕ U 1 , • • • , U n ; S 1 , • • • , S n Table 1: The evaluation relation E ϕ U ; S
The operational semantics of Actor is defined in Table 2, where the evaluation function E ϕ U ; S is used (defined in Table 1). This function takes an expression E and a store ϕ and returns a value U and a possibly empty configuration S of terms A ⊲ (0, ϕ, ε). These terms represent actors created during the evaluation -the names A are fresh -and ϕ records the initial values of the fields of A. The auxiliary function fresh(•) used in the evaluation function takes a class actor and returns an actor name of that class that is fresh. In order to have a finitely branching transition system (see the remark at the end of this section), we assume actor names in classes are totally ordered and fresh(C) always returns the first unused name of the class C. In this way, fresh names are selected in a deterministic manner.

The same auxiliary function is used in rule (inst) on a tuple of variables. In this case it returns a tuple of the same length of variables that are fresh. Also in this case, we assume a total order of variables and fresh( x), where x has length n, returns the least n unused variables. For notational convenience, we always omit the standard curly brackets in the set notation and we use ", " both to separate elements inside sequences and for set union (the actual meaning is made clear by the context).

The initial configuration of a program with main process P is ℵ ⊲ (P, ∅, ε), where ℵ is a name of the root, an actor of a class without fields and methods. We assume that the class of ℵ does not belong to the classes of the program. Note that the root actor is guaranteed to terminate because its queue remains empty (no method invocation may be enqueued) and the main process (as any other one) terminates.

We finally remark that transition systems of the language Actor are finitely branching (every state has a finite number of successor states) because the choices of fresh actor names (in the evaluation of new C) and of fresh variables (in the instantiation of the bodies of methods) are deterministic.

2.3. Relevant sublanguages. We will consider the following fragments of Actor whose relevance has been already discussed in the Introduction:

Actor ba is the sublanguage where the new expression only occurs in the main process (the number of actor names that it is possible to create is bounded). Actor ro is the sublanguage without the field update operation (f ← E) (fields are read-only as they cannot be modified after the initialization). Actor ro ba is the intersection of Actor ba and Actor ro . Actor sl is the sublanguage with classes without fields (objects are stateless).

(upd)

E ϕ U ; S A ⊲ ((f ← E).P, ϕ, q) -→ A ⊲ (P, ϕ[f ← U ], q), S (let)
E ϕ U ; S A ⊲ (let x = E in P, ϕ, q) -→ A ⊲ (P [ U / x ], ϕ, q), S (invk-s) E ϕ U ; S A ⊲ (A!m( E).P, ϕ, q) -→ A ⊲ (P, ϕ, q • m( U )), S (invk)
E ϕ U ; S A ⊲ (A ′ !m( E).P, ϕ, q), A ′ ⊲ (P ′ , ϕ ′ , q ′ ) -→ A ⊲ (P, ϕ, q), A ′ ⊲ (P ′ , ϕ ′ , q ′ • m( U )), S (inst)
A In this section we establish the main undecidability results for the actor language in Section 2.

∈ C C.m( x) = P y = free(P ) \ x y ′ = fresh( y) A ⊲ (0, ϕ, m( U ) • q) -→ A ⊲ (P [ A / this ][ y ′ / y ][ U / x ], ϕ, q) (match) E, E ′ ϕ U, U ; S A ⊲ ([E = E ′ ]P ;Q, ϕ, q) -→ A ⊲ (P, ϕ, q), S (mmatch)
E, E ′ ϕ U, V ; S U = V A ⊲ ([E = E ′ ]P ;Q, ϕ, q) -→ A ⊲ (Q, ϕ, q), S (plus-l) A ⊲ (P + Q, ϕ, q) -→ A ⊲ (P, ϕ, q) (plus-r) A ⊲ (P + Q, ϕ, q) -→ A ⊲ (Q, ϕ, q) (context) S -→ S ′ S, S ′′ -→ S ′ , S ′′
In particular, we will prove the undecidability of termination and process reachability.

Definition 3.1. Consider an actor program. The termination problem is to decide whether it has no infinite computation; the process reachability problem is to decide, given a process P , whether there exists a computation of the program traversing a configuration having a term A ⊲ (P ′ , ϕ, q) with P ′ being equal to P up-to renaming of variables and actor names.

We will use a reduction technique from a Turing-complete model to our actor model. In particular, the Turing-complete models we consider are the 2 Counter Machines (2CMs) [START_REF] Minsky | Computation: finite and infinite machines[END_REF] and a faulty variation of them. A 2CM is a machine with two registers R 1 and R 2 holding arbitrary large natural numbers and a program P consisting of a finite sequence of numbered instructions of the following type:

• j : Inc(R i ): increments R i and goes to the instruction j + 1;

• j : DecJump(R i , l): if the content of R i is not zero, then decreases it by 1 and goes to the instruction j + 1, otherwise jumps to the instruction l; • j : Halt: stops the computation and returns the value in the register R 1 . A state of the machine is given by a tuple (i, v 1 , v 2 ) where i indicates the next instruction to execute (the program counter) and v 1 and v 2 are the contents of the two registers. The user has to provide the initial state of the machine. The transition relation of the 2CM will be denoted by =⇒.

The faulty variation of the 2CM we use are the "two Faulty Towers Machine" (2FTM, for short) [START_REF] Cleese | Fawlty towers. See en.wikipedia[END_REF]. These machines have two faulty registers R 1 and R 2 holding either arbitrary large natural numbers or the faulty value ⊥. The program of a 2FTM is a finite sequence of numbered instructions that are the same of those in 2CMs. However, in contrast with 2CMs, 2FTMs from a state (i, v 1 , v 2 ) may nondeterministically evolve into a faulty state (i, ⊥, v 2 ) or (i, v 1 , ⊥) or (i, ⊥, ⊥). If an instruction i is an Inc/DecJump that refers to the register R 1 (respectively, R 2 ) then (i, ⊥, v) (respectively, (i, v, ⊥)) evolves to (0, ⊥, v) (respectively, (0, v, ⊥)). In 2FTMs, the instruction numbered 0 is always assumed to be Halt. Let =⇒ F be the transition relation of the 2FTMs.

By definition, every 2CM program with a 0-numbered instruction Halt is a 2FTM program and conversely. If we restrict to 2CM with a 0-numbered instruction Halt, it is easy to verify that every such machine has an infinite computation with a 2CM-semantics if and only if it has an infinite computation with a 2FTM-semantics. Similarly for instruction reachability, if we consider any non 0-numbered instruction.

In the sequel, we consider 2FTMs and 2CMs whose initial state is (1, 0, 0).

3.1.

The language Actor ba . We encode the value n stored in a register as n messages (of the same type) that are enqueued in an actor -see Figure 1. Namely, let R 1 and R 2 be two actors of class R and let the number of messages item in R 1 and R 2 be their value.

The instruction Inc is implemented by inserting one item message in the queue of the corresponding register. In our formalism, this is done by invoking the method item whose execution has two possible outcomes: (i) the invocation is enqueued again; (ii) the invocation is discarded because we are in the presence of a residual of a DecJump operation, as described next. R // R has fields dec, ctr, loop and stop

R.item(tt, ff ) = [stop = ff ] [dec = ff ]this!item(tt, ff );(dec ← ff ) R.inc(pc, tt, ff ) = [stop = ff ](loop ← ff ).this!item(tt, ff ).ctr!run(pc, tt, ff ) R.decjump(pc, pc ′ , tt, ff ) = [stop = ff ](loop ← ff ).(dec ← tt).this!checkzero(pc, pc ′ , tt, ff ) R.checkzero(pc, pc ′ , tt, ff ) = [stop = ff ](loop ← ff ). [dec = tt]ctr!run(pc ′ , tt, ff ).(dec ← ff );ctr!run(pc, tt, ff ) R.init(tt, ff , Ctrl ) = (dec ← ff ).(ctr ← Ctrl ).(loop ← ff ).(stop ← ff ). this!bottom(tt, ff ) R.bottom(tt, ff ) = [loop = ff ](loop ← tt).this!bottom(tt, ff ); (stop ← tt) Ctrl // Ctrl has fields stm 1 , • • • , stm n and r 1 and r 2 Ctrl.run(pc, tt, ff ) = [pc = stm 1 ][[Instruction 1 ]] 1,tt,ff • • • [pc = stm n ][[Instruction n]] n,tt,ff Ctrl.init() = r 1 !init(tt, ff , this).r 2 !init(tt, ff , this).this!run(stm 1 , tt, ff ) Ctrl.halt () = 0 where [[Instruction i ]] i,tt,ff is equal to -r j !inc(stm i+1 , tt, ff ) if Instruction i = Inc(R j ); -r j !decjump(stm i+1 , stm k , tt, ff ) if Instruction i = DecJump(R j , k); -this!halt if Instruction i = Halt.
The main process is

let x = new Ctrl(x 1 , • • • , x n , new R( , , , ), new R( , , , )) in x!init().
Figure 1: Encoding a 2FTM in Actor ba (" " denotes an irrelevant initialization parameter)

In case (i), to avoid an infinite sequence of item dequeues and enqueues, we introduce fields stop and loop which are initialized to false and set to true by the bottom method in case the queue contains only item messages. This has as effect that the stored item messages are subsequently purged from the queue of the register. Note that differently from the example in Section 2 we have encoded the boolean values as fields (so that we do not need to pass them around).

In case (ii), registers have a field dec that is set to tt by a decjump method execution. This field means that the actual decrement of the register is delayed to the next execution of checkzero. Since in (ii) item is not enqueued, then the register is actually decremented and the field dec is set to ff . When checkzero will be executed, since dec = ff then the next instruction of the 2CM is simulated. On the contrary, when checkzero is executed with dec = tt then the decrement has not been performed (the register is 0) and the simulation jumps.

The Halt instruction is simulated by invoking a method halt that does nothing. As in the examples of Section 2, booleans are implemented by two variables -see the method Ctrl.init -that are distributed during the invocations. With a similar machinery, in the actor class Ctrl, the labels of the instructions are represented by the variables x 1 , • • • , x n , which are stored in the fields stm 1 , . . . , stm n of Ctrl . Theorem 3.2. Termination and process reachability are undecidable in Actor ba .

The undecidability of termination in Actor ba follows by the property that a 2FTM diverges if and only if the corresponding actor program has an infinite computation. As regards process reachability, we need a smooth refinement of the encoding in Figure 1 where the Halt instruction is simulated by a specific process.

Proof. Let us assume to have a fixed 2FTM and let [[Instruction i ]] i,tt,ff be defined in Figure 1. Let also

[[(i, v 1 , v 2 )]] tt ,ff def = ℵ ⊲ (0, ∅, ε), (v 1 = ⊥ and v 2 = ⊥) C ⊲ ([[Instruction i ]] i,tt,ff , ϕ ctrl , ε), R 1 ⊲ (0, ϕ reg , bottom(tt, ff ) • item(tt, ff ) v 1 ), R 2 ⊲ (0, ϕ reg , bottom(tt, ff ) • item(tt, ff ) v 2 ) [[(i, ⊥, v)]] tt ,ff def = ℵ ⊲ (0, ∅, ε), (v = ⊥) C ⊲ ([[Instruction i ]] i,tt,ff , ϕ ctrl , ε), R 1 ⊲ (0, ϕ ⊥ reg , ε), R 2 ⊲ (0, ϕ reg , bottom(tt, ff ) • item(tt, ff ) v ) [[(0, ⊥, v)]] tt ,ff def = ℵ ⊲ (0, ∅, ε), (v = ⊥) C ⊲ (0, ϕ ctrl , ε), R 1 ⊲ (0, ϕ ⊥ reg , ε), R 2 ⊲ (0, ϕ reg , bottom(tt, ff ) • item(tt, ff ) v ) where -ϕ ctrl def = [stm i → x i i∈1..n , r 1 → R 1 , r 2 → R 2 ]; -ϕ reg def = [stop → ff , loop → ff , dec → ff , ctr → C]; -ϕ ⊥ reg def = [stop → tt, loop → tt, dec → ff , ctr → C]; -item(tt, ff ) v def = item(tt, ff ) • • • item(tt, ff ) v times . (the definitions of [[(i, v, ⊥)]] tt ,ff and [[(0, v, ⊥)]] tt ,ff and [[(0, ⊥, ⊥)]] tt ,ff follow the same patterns). We first observe that ℵ ⊲ (P, ∅, ε) -→ * [[(1, 0, 0)]] tt ,ff
, where P is the main process in Figure 1. Then we demonstrate the following properties:

(1) if (i, v 1 , v 2 ) =⇒ F (j, v ′ 1 , v ′ 2 ) then [[(i, v 1 , v 2 )]] tt,ff -→ + [[(j, v ′ 1 , v ′ 2 )]] tt ,ff ; (2) if [[(i, v 1 , v 2 )]
] tt,ff has an infinite computation then the computation has infinitely many configurations like

ℵ ⊲ (0, ∅, ε), C ⊲ ([[Instruction i ]] i,tt,ff , ϕ ctrl , ε), R 1 ⊲ (P 1 , ϕ 1 , q 1 ), R 2 ⊲ (P 2 , ϕ 2 , q 2 ) (3.1) (3) if ℵ ⊲ (0, ∅, ε), C ⊲ ([[Instruction i ]] i,tt,ff , ϕ ctrl , ε), R 1 ⊲ (P 1 , ϕ 1 , q 1 ), R 2 ⊲ (P 2 , ϕ 2 , q 2 ) -→ * ℵ ⊲ (0, ∅, ε), C ⊲ ([[Instruction j ]] j,tt,ff , ϕ ctrl , ε), R 1 ⊲ (P ′ 1 , ϕ ′ 1 , q ′ 1 ), R 2 ⊲ (P ′ 2 , ϕ ′ 2 , q ′
2 ) is a computation with every intermediate configuration having the process of the actor C equal to 0 then there are two computations

ℵ ⊲ (0, ∅, ε), C ⊲ ([[Instruction i ]] i,tt,ff , ϕ ctrl , ε), R 1 ⊲ (P 1 , ϕ 1 , q 1 ), R 2 ⊲ (P 2 , ϕ 2 , q 2 ) -→ * [[(i, v 1 , v 2 )]] tt ,ff and ℵ ⊲ (0, ∅, ε), C ⊲ ([[Instruction j ]] j,tt,ff , ϕ ctrl , ε), R 1 ⊲ (P ′ 1 , ϕ ′ 1 , q ′ 1 ), R 2 ⊲ (P ′ 2 , ϕ ′ 2 , q ′ 2 ) -→ * [[(j, v ′ 1 , v ′ 2 )
]] tt ,ff where the actor C never moves such that

(i, v 1 , v 2 ) =⇒ F (j, v ′ 1 , v ′ 2 )
. The proof of ( 1) is a straightforward case analysis on the type of instruction i.

The proof of ( 2) uses an argument by contradiction. Assume that there are finitely many configurations like 3.1. Then, there is an infinite suffix of this computation in which the actor C does not perform actions. This means that at least one actor R i performs infinitely many actions by executing the methods item and bottom. But this is not possible because bottom blocks the actor if it is invoked twice without executing update actions on the register in between.

The proof of (3) simply considers two possible cases: either some fields stop is set to tt during the computation or not. In the first case the corresponding register of the 2FTM enters a faulty state ⊥. In the second case the instruction has been correctly executed.

The property [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF] guarantees that if a 2FTM has an infinite computation then also the corresponding encoding has an infinite computation. The opposite follows from (1) and ( 2): if the encoding has an infinite computation, it traverses infinitely many configurations representing configurations of the corresponding 2FTM, thus it also has an infinite computation. The undecidability result can be easily extended to the process reachability problem. It suffices to modify the process modeling an Halt (not numbered with 0) by replacing this!halt () with a process Q different from all the other processes in Figure 1. We have that Q is reachable if and only if the 2CM with the same program of the given 2FTM terminates.

3.2.

The language Actor ro . We show that Actor ro is Turing-complete by means of an encoding of a 2CM -see Figure 2. In this encoding the two registers are represented by two disjoint stacks of actors linked by the next field. The top elements of the two stacks are passed as parameters r 1 and r 2 of the run method of the controller. As before, this actor encodes the control of the 2CM.

The instruction Inc is implemented by pushing an element on top of the corresponding stack. This element is an actor of class R storing in its field the old pointer of the stack. The new pointer, i.e. the new actor name, is passed to the next invocation of the run method.

The instruction DecJump is implemented by popping the corresponding stack. In particular, the method run of the controller is invoked with the field next of the register being decreased. This pop operation is performed provided the register that is argument of run is different from nil. Otherwise a jump is performed. Note that the other top of the stack r j (i = j) and the next instruction to be executed are simply passed around and therefore they do not need to be stored in updatable fields. Theorem 3.3. Termination and process reachability are undecidable in Actor ro .

Proof. It is easy to verify that if a 2CM has a computation

(1, 0, 0) =⇒ (i 1 , v 1 , v ′ 1 ) =⇒ • • • =⇒ (i n , v n , v ′ n ) then there is a computation ℵ ⊲ (P, ∅, ε) -→ * ℵ ⊲ (0, ∅, ε), C ⊲ ([[Instruction 1 ]] nil ,nil , ϕ, ε) -→ * ℵ ⊲ (0, ∅, ε), C ⊲ ([[Instruction i 1 ]] r 1 ,r ′ 1 , ϕ, ε), R r 1 , R r ′ 1 , G 1 -→ * ℵ ⊲ (0, ∅, ε), C ⊲ ([[Instruction i n ]] rn,r ′ n , ϕ, ε), R rn , R r ′ n , G n where P is the main process of Figure 2, [[Instruction i j ]] r j ,r ′ j are defined in Figure 2, ϕ = [stm 1 → x 1 , • • • , stm n → x n , nil → nil], R r i and R r ′ i are stacks of register actors whose length is v i and v ′ i , respectively. For instance, R r 1 of length k is r 1 ⊲ (0, [next → r 2 ], ε), r 2 ⊲ (0, [next → r 3 ], ε), • • • , r k ⊲ (0, [next → nil], ε) .
The configurations G i only contain register terms r⊲(0, [next → r ′ ], ε) and represent garbage (they are inactive).

In contrast with Theorem 3.2, the converse implication (every computation of the Actor ro program in Figure 2 may be split in subcomputations of finite lengths that correspond to 2CM transitions) is not difficult because the program of Figure 2 is deterministic.

The above correspondence guarantees that the computation of the actor system terminates if and only if a Halt instruction is reached. The undecidability of process reachability is proved by using the same arguments of Theorem 3.2.

Decidability results for Actor ro ba

We demonstrate that programs in Actor ro ba are well-structured transition systems [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. This will allow us to decide a number of properties, such as termination. We begin with some background on well-structured transition systems.

A reflective and transitive relation is called quasi-ordering. A well-quasi-ordering is a quasi-ordering (X, ≤) such that, for every infinite sequence x 1 , x 2 , x 3 , • • • , there exist i, j with i < j and x i ≤ x j . Definition 4.1. A well-structured transition system is a finitely branching transition system (S, -→, ) where is a quasi-ordering relation on states such that [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF] is a well-quasi-ordering [START_REF] Agha | The structure and semantics of actor languages[END_REF] is upward compatible with -→, i.e., for every S 1 S ′ 1 and S 1 -→ S 2 , there exists S ′ 1 -→ * S ′ 2 such that S 2 S ′ 2 . Given a state s of a well-structured transition system, Pred (s) denotes the set of immediate predecessors of s (i.e., Pred (s) = {s ′ | s ′ -→ s}) while ↑ s denotes the set of states greater than s (i.e., ↑ s = {s ′ | s s ′ }). With abuse of notation we will denote with Pred ( ) also its natural extension to sets of states.

According to the theory of well-structured transition systems [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF], we have that several properties are decidable for such transition systems (under some conditions discussed below). We will consider the following properties.

R // R has a field next R.dec 1 (ctrl , r, stm) = ctrl !run(next, r, stm) R.dec 2 (ctrl , r, stm) = ctrl !run(r, next, stm) Ctrl // Ctrl has fields stm 1 , • • • , stm n and nil Ctrl.run(r 1 , r 2 , pc) = [pc = stm 1 ][[Instruction 1 ]] r 1 ,r 2 ; • • • [pc = stm n ][[Instruction n]] r 1 ,r 2 where [[Instruction i ]] r 1 ,r 2 is equal to -this!run(new R(r 1 ), r 2 , stm i+1 ) if Instruction i = Inc(R 1 ); -this!run(r 1 , new R(r 2 ), stm i+1 ) if Instruction i = Inc(R 2 ); -[r 1 = nil]this!run(r 1 , r 2 , stm k );r 1 !dec 1 (this, r 2 , stm i+1 ) if Instruction i = DecJump(R 1 , k); -[r 2 = nil]this!run(r 1 , r 2 , stm k );r 2 !dec 2 (this, r 1 , stm i+1 ) if Instruction i = DecJump(R 2 , k); -0 if Instruction i = Halt.
The main process is let x = new Ctrl(x 1 , • • • , x n , nil ) in x!run(nil , nil , x 1 ).

Figure 2: Encoding a 2CM in Actor ro Definition 4.2. Consider a well-structured transition system (S, -→, ). Given S ∈ S the termination problem is to decide whether S has an infinite computation; the control-state reachability problem is to decide, given T ∈ S, whether there is T ′ T such that S -→ * T ′ .

In well-structured transition systems termination is decidable when the transition relation -→ and the ordering are effectively computable. When it is also possible to effectively compute a finite-basis for the set of states Pred (↑ s) we have that control-state reachability is decidable as well.

In the following we assume given an actor program with its main process and its set of actor class definitions. The first relation we convey is • = that relates renamings, ranged over by ρ, ρ ′ , . . . that are functions mapping variables that are not free in the main process into either actor names or variables. Let

ρ • = ρ ′ def = for every x, y : (i) ρ(x) = ρ(y) if and only if ρ ′ (x) = ρ ′ (y) (ii) ρ(x) = ρ ′ (x) if ρ(x) or ρ ′ (x
) is an actor name or a free variable of the main process Namely, two renamings are in the relation • = if they identify the same variables, regardless the value they associate when such a value is a variable. For example, [x → y, y → z]

• = [x → x, y → z] and [x → y, y → y, z → A] • = [x → x ′ , y → x ′ , z → A]. However [x → y, y → z] • = [x → x, y → x] and [x → A] • = [x → B].
In general, if ρ and ρ ′ are injective renamings that always return variables then ρ

). From this also follows that the above renamings do not change the main process (because they do not apply to its free variables).

Let dom(ρ) be the domain of the renaming ρ. We denote by P ρ the result of P [ ρ( x) / x ], where x = x 1 , • • • , x n is a tuple containing the variables in dom(ρ) (without repetitions) and ρ( x

) = ρ(x 1 ), • • • , ρ(x n ).
Next, let ≃ be the least relation on terms m(U 1 , • • • , U n ) and on processes such that

ρ • = ρ ′ m(ρ(x 1 ), • • • , ρ(x k )) ≃ m(ρ ′ (x 1 ), • • • , ρ ′ (x k )) ρ • = ρ ′ P ρ ≃ P ρ ′
For example, it is easy to verify that m(x, y) ≃ m(x ′ , y ′ ) and that

[x = A]y!m(x, A, y) ≃ [z = A]y ′ !m(z, A, y ′ ). On the contrary [x = A]B!m(x, A, B) ≃ [z = A]y ′ !m(z, A, y ′ ).
The rationale behind ≃ is that it identifies processes that "behave in similar ways", namely they enqueue "similar invocations" in the same actor queue. Method invocations m(U 1 , • • • , U n ) of a given actor are identified if the processes they trigger "behave in similar ways".

). Let T = {T ρ 1 , T ρ 2 , T ρ 3 , • • • } be such that i = j implies T ρ i ≃ T ρ j . Then T is finite.
Proof. We demonstrate the lemma for processes, the argument is similar for method invocations. So, let P be a process. It is possible to count the number of renamings ρ on free(P ) that are different according to • =. In fact, the values of renamings on variables that are different from free(P ) do not play any role in the definition of T .

The basic remark is that a renaming ρ generates a partition of the set free(P ): two variables x and y are in the same partition if and only if ρ(x) = ρ(y). If we restrict to renamings that map variables to variables (and not actor names), then they are different according to • = if they yield different partitions. The number of such renaming is the Bell number of the cardinality of free(P ), let it be Bell(κ), where κ is the cardinality of free(P ). In addition, in our case, renamings may map a variable to an actor name into a finite set {A 1 , • • • , A ℓ }. In this case the identity of the actor name is relevant. If κ ≥ ℓ then The well-quasi-ordering relation on configurations relies on an (almost standard) embedding relation ≤ on queues (except the part about ≃, it is the one in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]):

(( κ ℓ ) × ℓ! + 1) × Bell(κ)
there exist i 1 < i 2 < • • • < i k ≤ h such that , for j ∈ 1..k, m j ( U j ) ≃ n ij ( V ij ) m 1 ( U 1 ) . . . m k ( U k ) ≤ n 1 ( V 1 ) . . . n h ( V h )
Then, let

P i ≃ P ′ i and q i ≤ q ′ i for i ∈ 1..ℓ A 1 ⊲ (P 1 , ϕ 1 , q 1 ), • • • , A ℓ ⊲ (P ℓ , ϕ ℓ , q ℓ ) A 1 ⊲ (P ′ 1 , ϕ 1 , q ′ 1 ), • • • , A ℓ ⊲ (P ′ ℓ , ϕ ℓ , q ′ ℓ )
It is worth noticing that the relation constraints corresponding elements A ⊲ (P, ϕ, q) and A ⊲ (P ′ , ϕ, q ′ ) to have the same states. In fact these states are defined by the main process using either its free variables or the actor names that it has created. For this reason there are finitely many of them and the relation is parametric with respect to them.

Theorem 4.4. Let (S, -→) be a transition system of a program of Actor ro ba . Then (S, -→ , ) is a well-structured transition system.

Proof. (1)

is a well-quasi-ordering. To prove that is a well-quasi-ordering, we reason by contradiction. Let S 1 , S 2 , S 3 , • • • be an infinite sequence of states in S such that, for every i < j, S i S j . Let y 1 ,• The set subterms(C) is finite, but all the -possibly infinitely many-processes that can be executed (or the messages that can be received) by an actor of class C are renamings P ρ (or m( y)ρ) of these terms. Notice that by Lemma 4.3, the number of terms P ρ (and m( y)ρ) which are different according to ≃ is finite as well. It is thus possible to extract a subsequence

S i 1 , S i 2 , S i 3 , • • • from S 1 , S 2 , S 3 ,
• • • such that, for every A, in the elements A ⊲ (P A i j ρ i j , ϕ A i j , q A i j ) and A⊲(P A i k ρ i k , ϕ A i k , q A i k ) of S i j and S i k , respectively, we have that P A i j ρ i j ≃ P A i k ρ i k . Moreover, as we are considering Actor ro ba the actor state cannot be modified, hence ϕ A i j = ϕ A i k . As we are considering Actor ro ba , the set of actor is bound. Let A 1 , • • • , A ℓ be such actor names. Due to the above arguments, the sequence S i 1 , S i 2 , S i 3 , • • • may be represented as a sequence of tuples of queues:

(q A 1 i 1 , • • • , q A ℓ i 1 ), (q A 1 i 2 , • • • , q A ℓ i 2 ), (q A 1 i 3 , • • • , q A ℓ i 3 ), • • • such that S i j S i k if and only if (q A 1 i j , • • • , q A ℓ i j ) ⊑ ℓ (q A 1 i k , • • • , q A ℓ i k )
, where ⊑ ℓ is the coordinatewise order defined by

(q 1 , • • • , q ℓ ) ⊑ ℓ (q ′ 1 , • • • , q ′ ℓ ) def = for every h : q h ≤ q ′ h
(≤ is the above embedding relation).

We are finally reduced to an infinite sequence of tuples of queues such that every tuple cannot be in relation according to ⊑ ℓ with any of the subsequent ones. This fact contradicts the Higman's Lemma [START_REF] Higman | Ordering by Divisibility in Abstract Algebras[END_REF]: if (X, ≤) is a well-quasi-ordering and (X * , ≤ * ) is the set of finite X-sequences ordered by the embedding relation ≤ * defined using ≤ as pointwise ordering, then (X * , ≤ * ) is a well-quasi-ordering. More precisely, the contradictions follows from the following consequence of the Higman's Lemma:

• if X is a finite set and (X * , ≤) is the set of finite X-sequences ordered by the embedding relation, then (X * , ≤) is a well-quasi-ordering. and from the following statement

• if (X, ≤) is a well-quasi-ordering then (X ℓ , ≤ ℓ ) is a well-quasi-ordering. (2)
is upward compatible with -→. A state ϕ is normed, if, for every field f, ϕ(f) is either a free variable in the main process or an actor name. A configuration is normed if the states of the actors are normed. We observe that the initial configuration is normed. We also let ( E)ρ ≃ ( E)ρ ′ whenever ρ

• = ρ ′ . We first demonstrate that, if E ϕ U ; S with ϕ normed, then (exp-i) if E ≃ E ′ and S = ∅ then E ′ ϕ U ′ ; ∅ and U ≃ U ′ ;
(exp-ii) if E (respectively P ) only contain free variables in the main process and actor names then E ≃ E ′ (respectively P ≃ P ′ ) implies E = E ′ (respectively P = α P ′ ) and E ∅ U ; S implies that U contain free variables in the main process and actor names and S is normed. (exp-i) is proved by induction on the hight of the proof-tree of E ϕ U ; ∅. There are two basic cases: (1) E = U and (2) E = f. As regards ( 1), E ′ = U ′ and the property is immediate by the hypothesis that E ≃ E ′ . As regards ( 2),

E ′ = f because E ≃ E ′ ;
henceforth the property (because E ′ is evaluated in the state ϕ as well). There is one inductive case (because the case of new is not possible, otherwise S cannot be empty), which is immediate.

(exp-ii) is an immediate consequence of the definition of

• = and ∅ .
Let S 1 -→ S 2 . We demonstrate that (i) if S 1 is normed then S 2 is normed as well (this means that the transition system (S, -→) of a program of Actor ro ba has normed configurations because the initial state is normed); (ii) if S 1 S ′ 1 then there exists S ′ 1 -→ * S ′ 2 such that S 2 S ′ 2 . As regards (i), it follows by remarking that in programs of Actor ro ba , there is no field update and the unique process that may create states is the one of ℵ (the main process). Then (i) derives from the property (exp-ii).

As regards (ii), its proof is a case analysis on the proof-tree of S 1 -→ S 2 where the cases correspond to the unique rule appearing in the tree that is not an instance of (context).

Let S 1 = A 1 ⊲ (P 1 ρ 1 , ϕ 1 , q 1 ), • • • , A ℓ ⊲ (P ℓ ρ ℓ , ϕ ℓ , q ℓ ). Since S 1 S ′ 1 then S ′ 1 = A 1 ⊲ (P 1 ρ ′ 1 , ϕ 1 , q ′ 1 ), • • • , A ℓ ⊲ (P ℓ ρ ′ ℓ , ϕ ℓ , q ′ ℓ ) such that, for every i, P i ρ i • = P i ρ ′ i and q i ≤ q ′ i .
The cases are discussed in order.

(1) S 1 -→ S 2 contains an instance of (let), namely

A ⊲ (let x = E in P, ϕ, q), -→ A ⊲ (P [ U / x ], ϕ, q), S 3 . where E ϕ U ; S. By S 1 S ′ 1 , S ′ 1 must contain A ⊲ (let x = E ′ in P ′ , ∅, ε) such that let x = E in P ≃ let x = E ′ in P ′ (
without loss of generality, we are assuming the two bound variables are the same) and q ≤ q ′ . There are two subcases: (1.1) A = ℵ and (1.2) A = ℵ. In (1.1), By (exp-ii), this is possible provided E = E ′ and P = α P ′ . It is easy to verify that S ′ 1 -→ S ′ 2 and S 2 S ′ 2 because their unique difference with S 1 and S ′ 1 is due to the two processes P and P ′ . In (1.2), S 3 = ∅ because no new can occur in E. Additionally, by definition of ≃, E ≃ E ′ and P ≃ P ′ . Let E ′ ϕ U ′ , ∅. By (exp-i) we have U ≃ U ′ and it is easy to verify that P

[ U / x ] ≃ P ′ [ U ′ / x ]. Henceforth S ′ 1 -→ S ′ 2
and S 2 S ′ 2 because their unique difference with S 1 and S ′ 1 is due to the two processes P [ U / x ] and

P ′ [ U ′ / x ].
(2) S 1 -→ S 2 contains an instance of (invk-s), namely A ⊲ (A!m( E).P, ϕ, q), -→ A ⊲ (P, ϕ, q • m( U )) .

Since S 1 S ′ 1 then S ′ 1 contains A ⊲ (A!m( E ′ ).P ′ , ϕ, q ′ ) with E ≃ E ′ , P ≃ P ′ , and q ≤ q ′ . We observe that A = ℵ and if E ϕ U , ∅ and

E ′ ϕ U ′ , ∅ then U ≃ U ′ by (exp-i). Therefore q • m( U ) ≤ q ′ • m( U ′ ) and S ′ 1 -→ S ′ 2 with S 2 S ′
2 because their unique difference with S 1 and S ′ 1 is due to the two terms A ⊲ (P, ϕ, q • m( U )) and A ⊲ (P ′ , ϕ, q ′ • m( U ′ )).

(3) S 1 -→ S 2 contains an instance of (invk), namely

A ⊲ (B!m( E).P, ϕ, q), B ⊲ (Q, ψ, p) -→ A ⊲ (P, ϕ, q), B ⊲ (Q, ψ, p • m( U )), S 3 .
There are two subcases: either A = ℵ or A = ℵ. When A = ℵ the proof is similar to the above case (1.1); when A = ℵ the proof is similar to case (2). ( 4) S 1 -→ S 2 contains an instance of (inst), namely

A ⊲ (0, ϕ, m( U ) • q) -→ A ⊲ (P [ A / this ][ y ′ / y ][ U / x ], ϕ, q) ,
where C.m( x) = P , C being the class of A, y = free(P ) \ x and y ′ = fresh( y). Therefore

S 1 = A ⊲ (0, m( U ) • q), T 1 and S 2 = A ⊲ (P [ A / this ][ y ′ / y ][ U / x ], q), T 1 . Since S 1 S ′ 1 then S ′ 1 = A ⊲ (0, ϕ, n 1 ( V 1 ) • • • n h ( V h ) • m( V ) • q ′ ), T ′ 1 and m( U ) ≃ m( V ) and q ≤ q ′ and T 1 T ′ 1 .
By the operational semantics rules, we get S ′ 1 -→ * A⊲(0, ϕ, m( V )•q ′ •q ′′ ), T ′′ 1 by performing transitions of the actor A, with T ′ 1 T ′′ 1 and, by definition, q ≤ q ′ •q ′′ . At this stage, we notice that A ⊲ (0, ϕ, m( V )

• q ′ • q ′′ ), T ′′ 1 -→ A ⊲ (P [ A / this ][ z / y ][ V / x ], ϕ, q ′ • q ′′ ), T ′′ 1 . We notice that P [ A / this ][ y ′ / y ][ U / x ] = P [ A / this ][ y → y ′ , x → U ] and P [ A / this ][ z / y ][ V / x ] = P [ A / this ][ y → z, x → V ] and [ y → y ′ , x → U ] • = [ y → z, x → V ]. Therefore P [ A / this ][ z / y ][ V / x ] ≃ P [ A / this ][ z / y ][ V / x ]
which implies that S ′ 1 -→ * -→ S ′ 2 and S 2 S ′ 2 because their unique difference with S 1 and S ′ 1 is due to the two above processes. (5) S 1 -→ S 2 contains an instance of (match), namely A ⊲ ([E = E ′ ]P ;Q, ϕ, q) -→ A ⊲ (P, ϕ, q), S 3 .

We discuss the case A = ℵ because the other one is similar to (1.1). There are three subcases (5.1) both E and E ′ are variables; (5.2) E is a variable and E ′ is a field; (5.3) E and E ′ are both fields. In case (5.1), let

E = x = E ′ . Since S 1 S ′ 1 , then S ′ 1 must contain A ⊲ ([z = z]P ′ ;Q ′ , ϕ, q ′ ) with [x = x]P ;Q ≃ [z = z]P ′ ;Q ′ and q ≤ q ′ . Therefore we may use (match) to derive S ′ 1 -→ S ′ 2 with S 2 S ′ 2 .
In case (5.2), let E = U and E ′ = f. There are two subcases: (5.2.1) U is a variable or (5.2.2) U is an actor name. In (5.2.1), U has to be a free variable in the main process because we are using (match) (f may contain either such variables or actor names, additionally, renamings never return free variables in the main process). Therefore, by S 1 S ′ 1 , we have that S ′

1 contains A ⊲ ([U = f]P ′ ;Q ′ , ϕ, q ′ ) with [U = f]P ;Q ≃ [U = f]P ′ ;Q ′ and q ≤ q ′ . The consequence is that S ′ 1 -→ S ′ 2 with S 2 S ′
2 because their unique difference with S 1 and S ′ 1 is due to the two either the pair of processes P , P ′ or Q, Q ′ . Similarly for (5.2.2). The case (5.3) is obvious. ( 6) S 1 -→ S 2 contains an instance of (mmatch). Similar to (5). ( 7) S 1 -→ S 2 contains an instance of (plus-l) or of (plus-r). Straightforward.

We notice that the well-structured transition system (S, -→, ) has decidable algorithms for computing and for computing the next states. Then decidability of termination directly follows from the above mentioned results of the theory of well-structured transition systems that we have previously recalled. Theorem 4.5. In programs of Actor ro ba the termination problem is decidable. We now move to the definition of an appropriate algorithm for the computation of a finite basis for the predecessors of a given configuration, so to conclude also the decidability of control-state reachability.

Lemma 4.6. Let (S, -→, ) be a well-structured transition system of a program in Actor ro ba , and let S ∈ S. Then there is a finite set X ⊆ Pred (S) such that, for every S ′ ∈ Pred (S), there is T ∈ X with T S ′ . X can be effectively computed.

Proof. We show how to compute X . Let S = A ⊲ (P, ϕ, q), S ′ . The predecessor processes of P are the following ones: (i ) let x = E in P ′ , with P = P ′ [ U / x ], for some U and some x;

(ii ) x!m(E 1 , • • • , E n ).P ; (iii ) [U = U ] P ;Q; (iv ) [U = V ] Q;P ; (v ) P + Q; (vi ) Q + P ;
(vii ) P is an instance of a method body of the actor class of A. If A is of actor class C then we take all the method bodies of C with a suffix matching one of the cases (i )-(vi ) above (in this case, the expressions in (ii ) are either variables or actor names). If A = ℵ then we look for a matching suffix of the main process. The above six cases are demonstrated in the presence of such suffixes.

We only discuss case (i ), the other ones are similar. In case (i ), if A is of actor class C, then E = y, for some y. If x ∈ free(P ′ ) then X contains the configuration A ⊲ (let x = y in P ′ , ϕ, q), S ′ with P = P ′ [ y / x ]. Otherwise X contains the configuration A ⊲ (let x = z in P ′ , ϕ, q), S ′ , for z ∈ free(P ′ ) and for a unique z / ∈ free(P ′ ). When A = ℵ then E may be new C (orherwise the argument is as before). If x ∈ free(P ′ ) and S ′ = A ′ ⊲ (0, ϕ, ε), S ′′ with A ′ ∈ C then X contains the configuration A ⊲ (let x = new C in P ′ , q), S ′′ (and this for every possible

A ′ ∈ C such that A ′ ⊲ (0, ε) is in S ′ ).
Lemma 4.6 and the above mentioned results on well-structured transition systems allow us to decide the control-state reachability problem. Theorem 4.7. In programs of Actor ro ba the control-state reachability problem is decidable.

Proof. Let ↑ S = {S ′ ∈ S | S S ′ }. Let also Pred (↑ S) = {T | T -→ S ′ and S ′ S}. By definition of , Pred (↑ S) ⊆ Pred (S). Therefore ↑ Pred (↑ S) ⊆ ↑ Pred (S) ⊆ ↑ X ,
where X is the finite set of Lemma 4.6 that is effectively computable.

Next we discuss the process reachability problem -see Definition 3.1 -in Actor ro ba . To this aim, we use a simpler version of the (classical) diamond property. Proposition 4.8. Let (S, -→) be a transition system of a program of Actor ro ba and let ℵ ⊲ (P, ∅, ε), S -→ ℵ ⊲ (P, ∅, ε), S ′ (ℵ does not move) and ℵ ⊲ (P, ∅, ε), S ′ -→ ℵ ⊲ (P ′ , ∅, ε), S ′′ with P ′ = P (ℵ moves). Then there exists S ′′′ such that ℵ ⊲ (P, ∅, ε), S -→ ℵ ⊲ (P ′ , ∅, ε), S ′′′ -→ ℵ ⊲ (P ′ , ∅, ε), S ′′ .

It is worth noticing that the language Actor also owns the more classical diamond property: if in a configuration there are two transitions inferred by two distinct actors, then it is possible to perform them in any order reaching the same configurations up-to bijective renaming. We omit the formalization of this property since it is not needed in the rest of the paper.

Corollary 4.9. The process reachability problem is decidable in Actor ro ba . Proof. In order to verify whether a configuration A ⊲ (P ′ , ϕ, q), S is reachable with P ′ equal to P up-to renaming of variables and actor names, we proceed as follows.

First, by Proposition 4.8 it is not restrictive to consider the set of configurations T reachable by completely executing the actor ℵ only. The cardinality of T is bounded by 2 k , where k is the maximal nesting of + in the main process. If one of the processes in the configurations reached by executing ℵ is equal to P , up-to renaming of variables and actor names, then we are done. Otherwise, let u be the free variables in the main process. For each of

T = ℵ ⊲ (0, ∅, ε), A 1 ⊲ (0, ϕ 1 , q 1 ), • • • , A ℓ ⊲ (0, ϕ ℓ , q ℓ )
in T , we check control-state reachability from T to at least one of the states in the following finite set:

{ ℵ ⊲ (0, ∅, ε), A 1 ⊲ (Q 1 [ A1 / this ][ z1 / y1 ][ U1 / x1 ], ϕ 1 , ε), • • • , A ℓ ⊲ (Q ℓ [ A ℓ / this ][ z ℓ / y ℓ ][ U ℓ / x ℓ ], ϕ ℓ , ε) | for every 1 ≤ i ≤ ℓ, Q i is a suffix of the body of m i in C i , where A i ∈ C i ,
formal parameters and free variables of m i are x i and

y i U i is a tuple in {A 1 , . . . , A ℓ , u, z} ( z, z 1 , • • • , z ℓ are fresh) there exists 1 ≤ j ≤ ℓ such that Q j is equal to P up-to renaming }
Then the corollary follows by Theorem 4.7.

We conclude this section by recalling that we have already proved the undecidability of termination in programs with unboundedly many actors and read-only fields. Note that if we remove from Actor ro ba the constraint on bounded actor names then the relation is no longer a well-quasi-ordering. Consider, for instance, an actor (with empty state) having a method that first creates a new instance of the same class and then invokes on this new instance the same method. Among the reachable configurations it is possible to select a sequence S 1 , S 2 , S 3 , • • • such that the configuration S n is defined as follows:

S n def = A 1 ⊲ (0, ∅, ε) , • • • , A n ⊲ (0, ∅, ε)
It is easy to see that, for every i < j, S i S j .

Decidability results for Actor sl

We prove that in Actor sl termination and process reachability are decidable, too. As discussed at the end of Section 4, the ordering defined for Actor ro ba is not appropriate for Actor sl because in the latter it is possible to dynamically produce unboundedly many actors. Therefore, in order to compute an upper bound to the instances of method bodies, which is the basic argument for the model of Section 4 to be a well-structured transition system, we need to abstract from the identity of these names -as we have done with variables. However, in case of actor names, the abstractions we have devised all break the delivering of messages. Therefore we decided to apply our arguments to an abstraction of the operational model where the delivery of messages is inexact: it may be enqueued in every actor of the same class. Yet, this abstract model allows us to derive decidability of termination and process reachability for the original language.

In order to formalize the correspondence between the concrete and the abstract operational semantics, we need to add decorations to processes and transitions at the concrete level. Such decorations are used to keep track of the causal dependencies among processes. The decorated syntax adds a sequence of natural numbers in front of the process of an actor, namely, we use A ⊲ (σ : P, ∅, q) where σ has the following meaning: if σ = σ ′ • n, then σ ′ The decorated evaluation relation E d U ; S:

U d U ; ∅ E d U ; S A = fresh(C) new C( E) d A ; A ⊲ (ε : 0, ∅, ε), S E i d U i ; S i , for i ∈ 1..n E 1 , • • • , E n d U 1 , • • • , U n ; S 1 , • • • , S n
The decorated transition relation S σ -→ S ′ :

(let d ) E d U ; S A ⊲ (σ • n : let x = E in P, ∅, q) σ•n+1 -→ A ⊲ (σ • n + 1 : P [ U / x ], ∅, q), S (invk-s d ) E d U ; S A ⊲ (σ • n : A!m( E).P, ∅, q) σ•n+1|m( U ,A) -→ A ⊲ (σ • n + 1 : P, ∅, q • m( U , σ • n + 1)), S (invk d ) E d U ; S A ⊲ (σ • n : A ′ !m( E).P, ∅, q), A ′ ⊲ (σ ′ : P ′ , ∅, q ′ ) σ•n+1|m( U ,A ′ ) -→ A ⊲ (σ • n + 1 : P, ∅, q), A ′ ⊲ (σ ′ : P ′ , ∅, q ′ • m( U , σ • n + 1)), S (inst d )
A ∈ C C.m( x) = P y = free(P ) \ x y ′ = fresh( y)

A ⊲ (σ ′ : 0, ∅, m( U , σ) • q)

σ•0 -→ A ⊲ (σ • 0 : P [ A / this ][ y ′ / y ][ U / x ], ∅, q) (match d ) E, E ′ d U, U ; S A ⊲ (σ • n : [E = E ′ ]P ;Q, ∅, q) σ•n+1 -→ A ⊲ (σ • n + 1 : P, ∅, q), S (mmatch d ) E, E ′ d U, V ; S U = V A ⊲ (σ • n : [E = E ′ ]P ;Q, ∅, q) σ•n+1 -→ A ⊲ (σ • n + 1 : Q, ∅, q), S (plus-l d ) A ⊲ (σ • n : P + Q, ∅, q) σ•n+1 -→ A ⊲ (σ • n + 1 : P, ∅, q) (plus-r d ) A ⊲ (σ • n : P + Q, ∅, q) σ•n+1 -→ A ⊲ (σ • n + 1 : Q, ∅, q) (context d ) S σ -→ S ′ S, S ′′ σ -→ S ′ , S ′′
Table 3: The decorated operational semantics of the language Actor sl identifies the action of emission of the message that caused the method instantiation from which P was generated, and n is a counter indicating that P is actually generated by the method instantiation after n steps. Notice that for the main process executed by the actor ℵ the sequence σ ′ is empty, and that when a method is instantiated the counter n is initialized

(invk-sa) E d U ; S A, A ′ ∈ C A ⊲ (σ • n : A ′ !m( E).P, ∅, q) σ•n+1|m( U,A ′ ) -→ a A ⊲ (σ • n + 1 : P, ∅, q • m( U , σ • n + 1, A ′ )), S (invka)
E d U ; S A ′ , A ′′ ∈ C A ⊲ (σ • n : A ′ !m( E).P, ∅, q), A ′′ ⊲ (σ ′ : P ′ , ∅, q ′ ) σ•n+1|m( U,A ′ ) -→ a A ⊲ (σ • n + 1 : P, ∅, q), A ′′ ⊲ (σ ′ : P ′ , ∅, q ′ • m( U , σ • n + 1, A ′ )), S (insta)
A ∈ C C.m( x) = P y = free(P ) \ x y ′ = fresh( y)

A ⊲ (0, ∅, m( U , σ, A ′ ) • q) σ•0 -→ a A ⊲ (σ • 0 : P [ A ′ / this ][ y ′ / y ][ U / x ], ∅, q)
Table 4: Abstract transition rules for method invocations and instantiations to 0. In order to transfer the sequence from the message emitter to the receiving actor, we add σ at the end of messages. Namely, messages are now denoted with m( U , σ). The decorated operational semantics S α -→ S ′ is defined in Table 3, where the label α can be either a sequence σ or a pair σ|m( U , A) where the second element identifies the message issued during the transition. The decorated operational semantics increments the last number of the sequence of a process every time it performs an action, adds to messages the current sequence of the emitter, and use the sequences inside messages to initialize the sequence of the method instantiations (by extending it with 0).

It is trivial to see that the operational semantics in Table 3 and the decorated semantics coincide, in the sense that given one configuration S 1 of Actor sl we have S 1 -→ S 2 if and only if there exist a label α and two decorations S ′ 1 and S ′ 2 of S 1 and S 2 , respectively, such that S ′ 1 α -→ S ′ 2 . As discussed at the beginning of this Section, we need a more abstract semantics with inexact message deliveries. This is obtained by changing the operational semantics in Table 3 by decoupling the evaluation of the body of a method from the actor name of that method. Let S α -→ a S ′ be the abstract transition relation defined as S α -→ S ′ in Table 3 except the two rules (invk-s d ) and (invk d ) for method invocation and the rule (inst d ) for the instantiation of method bodies, which are replaced by those in Table 4. In the abstract transition relation, a message is added in a queue of an actor nondeterministically selected among those belonging to the same class of the target actor. The item m( U , σ) is enqueued with an additional argument -the actor name of the target actor. This additional argument is used when the method body is instantiated. In fact it replaces the variable this, thus making the execution of a body invariant regardless the actor that actually performs it.

As an example, consider the task manager specified in Actor sl in the Example 2.4. Also under the abstract semantics n distinct workers are instantiated, but it is possible for two distinct tasks to be delivered to the same worker.

We now introduce few notations: -Let Ω() be a map from "concrete" to "abstract" configurations: given a configuration S, we denote with Ω(S) the configuration obtained from S by replacing each of its actors A ⊲ (σ : P, ∅, q) with A ⊲ (σ : P, ∅, q ′ ) where q ′ is obtained from q by adding to each method invocation the parameter A. -Given a decorated configuration S and a label α, such that α = σ or α = σ|m( U , A), we use S⇂ α to denote the process decorated with σ in S: S⇂ α = P if S contains the actor A ⊲ (σ : P, ∅, q), for some A and q. -Let • = a be the following relation on variable renamings (not applied to variables that are free in the main process) ρ m in which they can be embedded. Proposition 5.1. Let S and S 0 be a decorated configuration and an initial decorated configuration ℵ ⊲ (0 : P, ∅, ε) of Actor sl , respectively.

• = a ρ ′ def = for every x, y : (i) ρ(x) = ρ(y) if and only if ρ ′ (x) = ρ ′ (y) (ii) ρ(x) ∈ C if and only if ρ ′ (x) ∈ C (iii) ρ(x) = ρ ′ (x) if ρ(x) or ρ ′ (x)
(1) If S α -→ S ′ then Ω(S) α -→ a Ω(S ′ ); (2) if S 0 α 1 -→ a . . . αn -→ a S n then there exists a computation S ′ 0 α ′ 1 -→ S ′ 1 . . . α ′ m -→ S ′ m and an injection I such that, for all 1 ≤ i ≤ n, we have α i ≃ a α ′ I(i) and S i ⇂ α i ≃ a S ′ I(i) ⇂ α ′ I(i)
.

Proof. The first item trivially holds because the new rules used in the definition of α -→ a are (strictly) more general than the corresponding rules used in the definition of α -→. The second item is proved by induction on the length of the computation S 0

α 1 -→ a . . . αn -→ a S n . If n = 1 then S 0 α 1 -→ a S 1 with α 1 = 1 or α 1 = 1|m( U , A)
and S 1 ⇂ α = P ′ , where P ′ is an immediate derivative of the main process P . It is trivial to see that the same transition is present in the concrete decorated semantics: namely, ℵ ⊲ (0 : P, ∅, ε)

α ′ 1 -→ S ′ 1 with α 1 ≃ a α ′ 1 and S ′ 1 ⇂ α ′ 1 ≃ a P ′ . If n > 1 we consider S 0 α 1 -→ a . . . αn -→ a S n α n+1 -→ a S n+1
≤ i ≤ n, we have α i ≃ a α ′ I(i) and S i ⇂ α i ≃ a S ′ I(i) ⇂ α ′ I(i)
. We now proceed by case analysis on the last number of the sequence in α n+1 .

If the number is 0, then α n+1 = σ • 0 and the transition is obtained by applying rule (inst a ) on a message m( U , σ, A ′ ). The presence of this message in one of the queues in S n guarantees the existence of 1 ≤ j ≤ n such that α j = σ|m( U , A ′ ). In the concrete computation we have α ′ I(j) ≃ a σ|m( U , A ′ ). This means that the same message (up-to ≃ a ) is in the queue of an actor A ′′ such that A ′ , A ′′ ∈ C in the concrete state S ′ I(j) . We have two subcases: either such method invocation is instantiated by the actor A ′′ during the concrete computation

S ′ 0 α ′ 1 -→ . . . α ′ m -→ S ′
m or not. In the first case, there exists I(j) < l ≤ m such that α ′ l = σ • 0 that instantiates the method. The thesis is proved simply by extending the injection I with I(n + 1) = l and observing that S n+1 ⇂ σ•0 ≃ a S ′ l ⇂ σ•0 . If the method invocation was not instantiated, it is in the queue of the actor A ′′ in the configuration S ′ m . It is sufficient to apply the same reasoning on an extension of the concrete computation that consumes the messages in front of the method invocation with sequence σ and that finally instantiates it. Such extension exists because processes are finite and non-blocking.

If the number is not 0, we discuss only the case in which α n+1 = σ • k (with k > 0) because the case α = σ • k|m( U , A) is treated similarly. In the computation S 0 α 1 -→ a . . . αn -→ a S n is guaranteed the presence of a label containing σ • k -1, i.e. there exists 1 ≤ j ≤ n such that the label α j contains σ • k -1. The process S j ⇂ α j is the process that has just performed the action labeled with σ • k -1 and that performs the action in the transition

S n α n+1 -→ a S n+1 because α n+1 = σ • k. By inductive hypothesis S j ⇂ α j ≃ a S ′ I(j) ⇂ α ′ I(j)
hence a process ready to execute an action labeled with the sequence σ • k occurs also in the concrete state S ′ I(j) . We now consider two subcases.

• There exists no label α ′ l containing σ • k. In this case the process

S ′ I(j) ⇂ α ′ I(j)
still occurs in

S ′ m . Hence it is possible to extend the computation S ′ 0 α ′ 1 -→ . . . α ′ m -→ S ′ m with S ′ m σ•k -→ S ′ m+1 in such a way that S ′ m+1 ⇂ σ•k ≃ a S n+1 ⇂ σ•k .
The thesis is proved simply by extending the injection I with I(n + 1) = m + 1.

• There exists I(j) < l ≤ m such that α ′ l contains σ • k. In this case it is not guaranteed that S ′ l ⇂ α ′ l ≃ a S n+1 ⇂ σ•k , due to nondeterminism. For this reason we construct from

S ′ 0 α ′ 1 -→ . . . α ′ m -→ S ′
m another concrete computation that satisfies our thesis. The first transformation that we apply to S

′ 0 α ′ 1 -→ . . . α ′ m -→ S ′
m consists of the cancellation of the transition α ′ l and of all the other transitions that depends on it. Namely, there are two kinds of transitions that must be removed: (i) those labeled with a sequence having a prefix σ • r such that r ≥ k and (ii) those causally dependent on the instantiation of messages that are in S ′ l inside the queue of the actor containing the process decorated with σ

• k. Let S ′ 0 α ′ 1 -→ . . . α ′ l-1 -→ S ′ l-1 α ′′ l -→ S ′′ l . . . α ′′ s -→ S ′′
s be the concrete computation obtained after this elimination of transitions. We now extend such computation by letting the process labeled with σ • k -1 to execute the expected action labeled with σ • k. Namely, we add the transition

S ′′ s σ•k -→ S ′′ s+1 such that S ′′ s+1 ⇂ σ•k ≃ a S n+1 ⇂ σ•k .
Then, we extend the computation by performing at least all the transitions removed for the reason (ii) above. This extension exists because all processes are finite and nonblocking and because the considered transitions causally depend on messages that are in S ′′ s+1 inside the queue of the actor containing the process decorated with σ

• k. Let S ′ 0 α ′ 1 -→ . . . α ′ l-1 -→ S ′ l-1 α ′′ l -→ S ′′ l . . . α ′′ s -→ S ′′ s α ′′ s+1 -→ . . . α ′′ t
-→ S ′′ t be the obtained computation. The thesis is proved by considering this last concrete computation, a rearrangement of the injection I that maps to their new positions the transitions in its codomain that belong to the group (ii), and by extending it with I(n + 1) = l.

As a direct consequence we have that the abstract semantics preserves both termination and control-state reachability. It remains to prove that termination and process reachability is decidable for the abstract semantics. To this aim, we consider a transition system -→ a obtained by removing the labels from the transitions α -→ a . On this transition system we define a as a variant of the ordering defined in the previous section in such a way that (S, -→ a , a ) turns out to be a well-structured transition system (for configurations of stateless programs). Let: -Let ≤ a be the following relation on message queues:

there exist i 1 < i 2 < • • • < i k ≤ h s.t . for j ∈ 1..k, m j ( U j , σ j , A j ) ≃ a n ij ( V ij , σ ′ ij , A ′ ij ) m 1 ( U 1 , σ 1 , A 1 ) . . . m k ( U k , σ k , A k ) ≤ a n 1 ( V 1 , σ ′ 1 , A ′ 1 ) . . . n h ( V h , σ ′ h , A ′ h )
-Let a be the ordering:

A i , A ′ j i ∈ C i P i ≃ a P ′ j i and q i ≤ a q ′ j i for i ∈ 1..ℓ, 1 ≤ j 1 < j 2 < • • • < j ℓ ≤ κ A 1 ⊲ (σ 1 : P 1 , ∅, q 1 ), • • • , A ℓ ⊲ (σ ℓ : P ℓ , ∅, q ℓ ) a A ′ 1 ⊲ (σ ′ 1 : P ′ 1 , ∅, q ′ 1 ), • • • , A ′ κ ⊲ (σ ′ κ : P ′ κ , ∅, q ′ κ )
Next, we observe that Lemma 4.3 can be adapted to the case of unbounded actors by using ≃ a instead of ≃. Namely, let T be either a process or a method invocation m(U 1 , • • • , U n , σ, A) of a stateless program and let T = {T ρ 1 , T ρ 2 , T ρ 3 , • • • } be such that i = j implies T ρ i ≃ a T ρ j . Proceeding as in the proof of Lemma 4.3, we prove that T is finite.

Theorem 5.2. Given a stateless program S we have that (S, -→ a , a ) is a well-structured transition system.

Proof. The proof is as in Theorem 4.4 with few differences that are discussed below.

In part (1) the unique difference is in the last part where the coordinatewise order ⊑ ℓ on sequences (of length ℓ) of queues of terms is used. As we now consider configurations with an unbounded number of actors, instead of configurations with a bounded number ℓ of actors, we need to resort to the embedding ⊑ a defined as follows:

q i ≤ a q ′ j i for i ∈ 1..ℓ, 1 ≤ j 1 < j 2 < • • • < j ℓ ≤ κ (q 1 , • • • , q ℓ ) ⊑ a (q ′ 1 , • • • , q ′ κ )
The final contradiction of part (1) is now reached by observing that by Highman's lemma, also ⊑ a is a well-quasi-ordering, as a consequence of the well-quasi-ordering ≤ a .

In part (2) the unique difference is for the monotonicity transitions due to rules (invka) and (invk-sa). The greater configuration is guaranteed to have a program ready to perform a corresponding method invocation, but this could be addressed to a different actor. In fact, the ordering a does not preserve actor names as it was for in the proof of Theorem 4.4. But a preserves at least actor classes. As the abstract transition system -→ a allows a term m( U , σ, A) to be introduced in the queue of any of the actor belonging to the same class of A, the method invocation executed by the greater configuration can be introduced in the queue of the actor corresponding to the target of the method invocation executed by the smaller configuration.

In the light of the results on well-structured transition systems recalled at the beginning of Section 4, this theorem proves the decidability of termination for the abstract semantics. To prove the decidability of process reachability we need to prove that a finite basis for predecessors is effectively computable. Lemma 5.3. Let (S, -→ a , a ) be a well-structured transition system of a program in Actor sl , and let S ∈ S. Then there is a finite set X such that, for every S ′ a S and S ′′ ∈ Pred (S ′ ), there is T ∈ X with T a S ′′ . X can be effectively computed.

Proof. The computation of X must extend the construction presented in the proof of Lemma 4.6 in two ways.

The first extension derives from the fact that, differently from the ordering considered in Lemma 4.6, if S a S ′ it could be possible for S ′ to have strictly more actors than S. In these case, it is possible that the predecessor differs from its successor S ′ for actors that are not present in S. We can cope with this problem by applying the procedure described in the proof of Lemma 4.6 not only to the configuration S, but to all the configurations that can be obtained by extending S with one or two additional actors belonging to one of the finite classes of the considered program. In fact, at most two actors are modified by one transition. Each of these additional actors executes a process obtained by applying a renaming ρ to a suffix of one of the method definitions of the corresponding class. As observed above, there are finitely many processes that can be obtained up-to ≃ a . Finally, the additional actors have a queue including at most one method invocation (in fact, at most one message can be consumed in one transition). Also in this case, by considering the method definitions of the actor class, it is easy to see that there are finitely many different method invocations up-to ≃ a .

The second extension is trivial and deals with the fact that in the abstract semantics a method invocations can be introduced in the queue of any of the actors belonging to the same class of the expected target actor. So the procedure of the proof of Lemma 4.6 for computing X must be extended to consider also this kind of transitions.

From Theorem 5.2, this last Lemma and the results on well-structured transition systems recalled at the beginning of Section 4, we can conclude that also control-state reachability, besides termination as already commented above, is decidable for the abstract semantics. From Proposition 5.1 we have already concluded that the abstract semantics preserves termination and control-state reachability w.r.t. the concrete semantics. Hence, we have that termination and control-state reachability are decidable for stateless actor program.

The decidability of control-state reachability entails the decidability of process reachability. In fact, given a process P , the reachability of a configuration A ⊲ (P ′ , ϕ, q), S with P ′ equal to P up-to renaming of variables and actor names can be solved in the abstract transition system simply by checking the control-state reachability of at least one of the following states. Let C 1 , . . . , C n be the actor classes of the considered actor system and let A 1 , • • • , A n be such that A i ∈ C i . We consider the following finite set of states:

S = { A i ⊲ (Q i , ∅, ε) | 1 ≤ i ≤ n, Q i is a suffix of a method definition
in the class C i and it is equal to P up-to renaming }

Conclusions

To the best of our knowledge this paper contains a first systematic study on the computational power of Actor-based languages. We have focussed on the pure asynchronous FIFO queueing and dequeuing of method calls between actors in the context of a nominal calculus which features the dynamic creation of variable names that can be passed around. The results proved in this paper can be summarized as follows:

• we identified two small but Turing powerful fragments of our Actor language: the fragment in which only boundedly many actors can be created, and the fragment in which fields cannot be updated; • we have proved that the fragment obtained as intersection of the two above sublanguages is not Turing complete, as properties like termination and control-state reachability turn out to be decidable; • if Actors are stateless, the language has decidable termination and control-state reachability even if we consider unboundedly many Actors. We conclude by mentioning relevant lines for future research. Recent work have identified more expressive Actor interaction mechanisms based an asynchronous method calls implemented by means of the so-called future variables [START_REF] De Boer | A complete guide to the future[END_REF]: we plan to investigate the impact of this Actor-based synchronization mechanism on our (un)decidability results. We also plan to extend our study of expressiveness to primitives like the release statements in [START_REF] Johnsen | An asynchronous communication model for distributed concurrent objects[END_REF]. These statements support the so-called cooperative shceduling of method invocations: method executions can release the control of the Actor in such a way that other method executions can be instantiated or resumed.

  The class C of the client includes the following two definitions: C.init(server ) = server !login(this) C.token(authServer , clientToken) = authServer !authenticate (u, p, clientToken) The class S of the server includes the following four definitions: S.init(authServer ) = (auth ← authServer ) S.login(client) = auth!open(this, clientToken, authToken). client!token(auth, authToken) S.succeeds(authToken) = . . . S.fails(authToken) = . . . The class A of the authServer includes the following two definitions (we leave unspecified the check of the correctness of username and password):

•

  = ρ ′ . The requirements of • = are stronger for actor names: in this case the two renamings should be identical. By definition, renamings in relation according to • = never apply to free variables of the main process. This because these variables are possibly stored in fields of actors and their renaming might change the behaviours of actors in a way that breaks the upward compatibility of the following relation and -→ (c.f. proof of Theorem 4.4, part

Lemma 4 . 3 .

 43 Let T be either a method invocation m(U 1 , • • • , U n ) or a process of a program in Actor ba (and therefore in Actor ro ba

  is an upper bound to the different renamings according • =. If κ < ℓ then the upper bound is (ℓ!/κ! + 1) × Bell(κ). In any case the number of different renamings according to • = is finite. Henceforth the set T is finite as well.

1 -

 1 is a free variable of the main process Differently from the definition of • =, • = a does not care of the identity of actor names (it is sufficient that they belong to the same class).-Let ≃ a be the relation defined as ≃ in Section 4, with• = a instead of • =.We extend it to messages containing sequences and actor names as follows:m( U , σ, A) ≃ a m( U ′ , σ ′ , A ′ ) iff m( U ) ≃ a m( U ′ ), σ = σ ′and there exists C such that A, A ′ ∈ C. We extend it also to labels: σ ≃ a σ and σ|m( U , A)≃ a σ|m( U ′ , A ′ ) iff m( U ) ≃ a m( U ′) and there exists C such that A, A ′ ∈ C. The following Proposition formalizes the correspondence between α -→ and α -→ a : 1. all α -→ transitions are present also in α -→ a (up-to application of the abstraction function Ω() to configurations) and 2. all the abstract computations S 0 α → a . . . αn -→ a S n have a corresponding concrete computation S ′

′ 1 -

 1 . The inductive hypothesis guarantees the existence of the concrete computation S ′ 0 α → . . .

  ′ m and of the injection I such that, for all 1

Table 2 :

 2

The transition relation S -→ S ′ 3. Undecidability results for Actor ba and Actor ro

  • • ,y m be a sequence of variables not free in the main process.

Consider: subterms(C) = {P | there exists a method m s.t. P is a subterm of C.m( x)} ∪ {m(y 1 , • • • , y g ) | there exists a method m s.t. C.m( x) with | x| = g}

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany

Project No. FP7-231620 (Highly Adaptable and Trustworthy Software using Formal Models) and by the ENVISAGE Project No. FP7-610582 (Engineering Virtualized Services) of the EC.