Juan Francisco

Director Díaz Frias

Del Proyecto

Jurado Jurado

Nota de Aceptación

The π-calculus is one of the most important formalisms for analyzing and modelling concurrent systems. It is a simple but powerful tool for specifying and checking several properties in this kind of systems. An interesting property of any system is the ability to reach some special state where it has a particular behavior. In security systems this is extremely important, since we would like that a system does not reach a state where a secret becomes observable to potential attackers. This work studies the reachability problem in fragments of the π-calculus and explores some expressiveness results beyond this problem. We prove the relation between local names and sequences of actions in CCS ! processes. Using this result and the decidability of barbs from [BGZ09] we prove that the reachability problem for some fragments of π-calculus is decidable. We also provide an algorithmic approach for solving this problem using the theory of well-structured transition systems [FS01], in consequence we are able to verify this property in infinite state systems with a finite number of steps. Finally, we provide a small interpreter for CCS ! , useful as an initial practical approach for checking properties in real life systems specified by this calculus.

Chapter 1 Introduction

In today's world, technology is one of the most important cores for the development of the society. This role has made access to high-tech devices increasingly frequent. Elements like Web, wireless networks, high capacity laptops, mobile devices, among others, have allowed advance towards information globalization, but carrying with it new challenges and problems that need to be solved for assuring a reliable, correct and secure service.

Computer science offers a framework in which information technology can be formalized, allowing establishing conditions where they work correctly. There are many factors that affect the correctness of such technologies, one of the most recent and challenging is concurrency, and this consists in many processes making use of a system in a simultaneous way. It is here where an area of computer science named concurrency theory goes into action.

In this theory, process calculi are distinguished, its intention is to model and reason about concurrent systems. Such calculi are capable to express systems formally, hence it is possible to argue about them for obtaining correct results. There are many examples such as CCS 1 , π-calculus 2 , Spi-calculus (π-calculus for arguing about security), among others, they have been specialized for solving specific problems since all of them count on with a modeling approach and an associated expressiveness (a measure of how powerful the calculus is). This analysis is focused on a fragment of the π-calculus that is fundamental in concurrency theory.

This project aims at analyzing the reachability problem in fragments of the πcalculus, such analysis will allow determining if a state of a system can be reached. It also aims at providing an algorithm resulting from the previous step, and for 1 Calculus of Communicating Systems more information in: http://en.wikipedia.org/wiki/Calculus_of_communicating_systems 2 More information in: http://en.wikipedia.org/wiki/Pi-calculus 2 1.1. PROBLEM DESCRIPTION practical effects, another analysis focused on the complexity of such algorithm.

Problem Description

Concurrency theory investigates how to analyze those systems where many processes act in a simultaneous way, and arguing about them for obtaining conclusions about correctness, security, reliability and other important aspects.

Process calculi are used for this purpose, because they allow making process modeling in concurrent systems, and depending of its specialization they are able to express, until certain point, a series of actions that can be object of study for a subsequent reasoning.

The π-calculus is one of the most influential calculi in concurrency theory, its simplicity and powerful operators make it an excellent tool for modeling concurrent systems. It also allows expressing mobile behavior and it is widely used around the world for analyzing several kinds of systems. This project focuses in this calculus due to its importance and by the impact of the results which could be easily used worldwide.

Nowadays, the notion of security has become one of the most important topics in research. This is because we have very complex systems and they represent a giant pillar in every second of our daily life. Moreover, in most cases the information must be managed carefully and privacy (among other aspects) is hugely valuable. Then, making a system safe means that it cannot reach a state in which private information can be revealed to an external agent that should not know such information.

By these reasons, we can say that establishing which are the states that make the system to be in danger are very important for arguing about its security. This problem is called reachability problem, and it is a central topic in security research.

Therefore, the problem is to determine whether a specific action β can be reached in some execution of the system. Such system is specified using the summation-free zero-adic fragment of the π-calculus (CCS ! ). This project will provide a decidability analysis of this problem by proving (or refusing) the strict relationship between the actions needed to reach such state and the use of local names.

The next step will be to bring the theory into practice, by giving an algorithm that can determine (given a process P and an action β) whether such action can be reached by using the information proved previously. For practical purposes, the 1.2. OBJECTIVES complexity of that algorithm is very important, and then it will conclude the analysis proposed in this project.

Objectives 1.2.1 Main Objective

To analyze the reachability problem in the CCS ! .

Specific Objectives

• To determine the decidability of the reachability problem for the CCS ! .

• To propose an algorithm for determining the reachability of an action given a process written in the CCS ! .

• To analyze the complexity of the proposed algorithm.

Justification

For long time, sequential systems have been the center of computer science studies, but these approaches have not been enough for a growing world that demands more complex systems everyday. In that sense, concurrent systems are present in our daily activities, from our cells to social networks. In the late 20 th and 21 st century the core of our society is based on information systems that carry out all kind of tasks.

Following this idea, analyzing concurrent systems must be a central activity in computer science. Here is where the π-calculus goes into scene, because it is an excellent tool for modeling concurrent and mobile systems, for this reason it is one the most influential process calculus in concurrency theory.

Another important thing is that system's security is a growing problem that has always been present in computer science, but in the last decade has become a very important topic in research. The reason of its importance lies in the increasing complexity of systems, then it is difficult to determine the "danger" states and to predict the behavior of them. That is why it is important to have theoretical tools that allow facing this problem.

The importance of this project lies in the reinforcement of the π-calculus by giving an analysis that could be very important for modeling and evaluating systems.

The main advantage will be given in security analysis which is a essential topic for computer science research.

As an additional benefit, all the results obtained here can be linked with the work made by Aranda [START_REF] Aranda | On the Expressivity of Infinite and Local Behaviour in Fragments of the π-calculus[END_REF] in his Ph.D. thesis about the expressiveness in π-calculus. That work has inspired the fundamental aspects of this project, then our analysis will allow proving other interesting things about expressiveness due to its relation with such work.

Background

Technical Background

Process Calculi

The process calculi are a diverse family of related approaches to formally modeling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes.

There are many different process calculi in the literature mainly agreeing in their emphasis upon algebra. The main representatives are CCS [START_REF] Milner | Communication and Concurrency[END_REF], CSP [START_REF] Hoare | Communications Sequential Processes[END_REF] and the process algebra ACP [START_REF] Bergstra | Algebra of communicating processes with abstraction[END_REF][START_REF] Baeten | Process Algebra[END_REF]. The distinctions among these calculi arise from issues such as the process constructions considered (i.e., the language of processes), the methods used for giving meaning to process terms (i.e. the semantics), and the methods to reason about process behavior (e.g., process equivalences or process logics). Some other issues addressed in the theory of these calculi are their expressive power, and analysis of their behavioral equivalences. We will describe some of the issues named previously.

The π-calculus

Syntax. Names are the most primitive entities in the π-calculus. We presuppose a countable set N of (port, links or channel) names, ranged over by x, y, . . .. For each name x, we assume a co-name x thought of as complementary, so we decree that x = x. We use x to denote a finite sequence of names x 1 x 2 . . . x n . The other entity in the π-calculus is a process. Processes are built from names as follows.

Definition 1.4.1. (Syntax) The processes, the summations and the prefixes in π-calculus are given respectively by: P := M (νx)P P | P !P M := 0 π.P M + M π := x(y) xy τ First we explain the summations and the prefixes and then the processes. The process (summation) 0 does nothing. xy.P and x(y).P represent the output and input process respectively, xy.P is a process which can output a datum y on channel x and then it behaves like P , xy is called a guard or (output) prefix . x(y).P is a process which can perform an input action on channel x and then it behaves like P {z/y}, the process which has replaced every occurrence of the name y, by the datum z received, {z/y} is a substitution of z by y, x(y) is called a guard or (input) prefix . τ.P can evolve invisibly to P . τ can be thought of as expressing an internal action of a process, τ is called a guard or (unobservable) prefix . the sum (or choice) P + Q represents the process which can has the capabilities of either P or Q but not both. Once a capability of P (Q) has been performed, Q (respectively, P ) is disregarded.

In P | Q, the parallel composition of P and Q, P and Q can proceed independently or can synchronise via shared names. In (νx)P , the name x is declared private to P , i.e. initially, components of P can use x tinteract with one another but not with other processes, the scope of x could change as a result of interaction between processes as will be seen later. Finally, the replication !P can be thought of as unboundedly many P 's in parallel P | P | P | . . ., replication is the means to express infinite behaviour. Notice that the operands in a sum must themselves be summations. Hence it says that the π-calculus considers guarded-choice.

In each of x(y).P and (νy)P , the occurrence of y is binding with scope P . An occurrence of a name in a process is bound if it is under the scope of a binding occurrence of the name. An occurrence of a name is free if it is not bound. Given Q we define its bound names bn(Q) as the set of names with a bound occurrence in Q, and its free names fn(Q) as the set of names with a non-bound occurrence in

Q, hence n(Q) = fn(Q) ∪ bn(Q) is the set of names of Q.
As consequence of the interchange of names between processes an unintended capture of names by binders could arise, to avoid it, the following definition of α-convertability is useful. Definition 1.4.2. (α-convertability) [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF] 1. If the name w does not occur in the process P , then P {w/z} is the process obtained by replacing each occurence of z in P by w.

2. A change of bound names in a process P is the replacement of a subterm x(z).P of P by x(w).Q{w/z}, or the replacement of a subterm (νz)Q of P by (νw)Q{w/z}, where in each case w does not occur in Q.

3. Processes P and Q are α-convertible, P = Q, if Q can be obtained from P by a finite number of changes of bound names.

Hence we adopt two well-known conventions:

Convention 1.4.1. [START_REF] Sangiorgi | The π-calculus: A Theory of Mobile Processes[END_REF] Processes that are α-convertible are identified.

Convention 1.4.2. [SW01] When considering a collection of processes and substitutions, we assume that the bound names of the processes are chosen to be different from their free names and from the names of the substitutions.

Semantics. The semantics of the language described above made precise by a labelled transition system. A transition P α -→ Q says that P can perform an action α and evolve into Q. The set of actions used in the transition system is composed by xy, xy, x(y), τ . xy, a free output, sends the name y on the name x, xy, an input, receives the name y on the name x, x(y), a bound output, sends a fresh name on x and τ is an internal action .

Definition 1.4.3. (Actions) The actions, which are ranged over by α, are given by:

α := xy xy x(y) τ (1.1)
Act refers to the set of actions. The set of labels, ranged over by l and l , is L which is composed of all non-internal actions.

Functions f n( ), bn( ) and n( ) are extended to cope with labels as follows:

bn(xy) = ∅ bn(xy) = ∅ bn(x(y)) = {y} bn(τ ) = ∅ f n(xy) = {x, y} f n(xy) = {x, y} f n(x(y)) = {x} f n(τ ) = ∅
The subject , subj( ) , and object , obj( ) , of these actions is defined as:

( τ -→) * α 1 -→ ( τ -→) * . . . ( τ -→) * αn -→ ( τ -→) * . =⇒ is the reflexive and transitive closure of τ -→. τ =⇒ is =⇒ and β =⇒ is β =⇒.
Some comments on the rules: the side-condition in Rule Par-L rule avoids the capture of a name by the extrusion of the scope of another name. The Open rule expresses extrusion of the scope of a name, this action allows the passing of a name beyond its original scope, its side-condition avoids the execution of an action whose subject is a bound-name as it should not interact with other processes out of the scope of the name. Rule Close-L reflects the interaction between processes in which the left-process has transmitted a bound name to the right-process, thus the scope of the restricted name is extended to include the process which receives it. Table 1.1: Operational semantics for the π-calculus.

Par-L P α -→ P P | Q α -→ P | Q bn(α) ∩ f n(Q) = ∅ Com-L P xy -→ P , Q xy -→ Q P | Q τ -→ P | Q Close-L P x(y) -→ P , Q xy -→ Q P | Q τ -→ (
Remark 1.4.1. We abbreviate, for any names x, y, the guards x(y) and xy by x and x, respectively, where y, is a dummy name: in these cases the datum which can be received or sent is irrelevant Notation 1.4.1. Throughout this work, we use (νa 1 . . . a n )P as a short hand for (νa 1 ) . . . (νa n )P . We often omit the "0" in α.0.

BACKGROUND

Now we define ≡ which shall be useful in the project although it is not included in the semantics: Definition 1.4.5. Let ≡ be the smallest congruence over processes satisfying αequivalence, the commutative monoid laws for composition with 0 as identity, the replication law !P ≡ P |!P , the restriction laws (νx)0 ≡ 0, (νx)(νy)P ≡ (νy)(νx)P and the extrusion law:

(νx)(P | Q) ≡ P | (νx)Q if x / ∈ f n(P ).

The Calculus of Communicating Systems

Undoubtedly CCS [START_REF] Milner | Communication and Concurrency[END_REF], a calculus for synchronous communication, remains as a standard representative of process calculi. In fact, many foundational ideas in the theory of concurrency have sprung from this calculus. In the following we shall consider two variants of CCS according to its mechanism to model infinite behaviour.

Hence, first we show the Finite fragment of CCS and then we introduce the two "recursive" extensions.

Finite CCS. The finite CCS processes can be obtained as a restriction of the finite processes of the π-calculus, i.e those π processes without occurrence of a term of the form !P , by requiring all inputs and outputs to have empty subjects only. Intuitively, this means that in CCS there is no sending/receiving of links but synchronisation on them.

In CCS, the actions are names, co-names and τ and therefore, we shall use l, l , . . . to range over names and co-names, where L is the set of names and co-names. The set of actions Act , ranged over by α and β, extends L with the symbol τ.

The syntax of finite CCS processes is the following:

Par-L P α -→ P P | Q α -→ P | Q Com-L P x -→ P , Q x -→ Q P | Q τ -→ P | Q Table 1
.2: Operational semantics for the finite CCS.

Replication CCS ! : As said before, replication is the way of expressing infinite behaviour which has been used in the π-calculus and the Aπ-calculus. It has also studied in the context of CCS in [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF][START_REF] Giambiagi | On the expressiveness of infinite behavior and name scoping in process calculi[END_REF]. For replication the syntax of finite processes (Definition 1.4.6) is extended as follows: P, Q, . . . := . . . !P (1.2) CCS ! is the restriction of the π-calculus seen by requiring all inputs and outputs to have empty subjects only. The operational rules for CCS ! are those in Table 1

|(ν x)P | ν = 1 + |P | ν |P | Q| ν = max(|P | ν , |Q| ν ) |α.P | ν = |!P | ν = |P | ν |0| ν = 0
We also need the concept of weak barb in CCS ! :

Definition 1.4.9 (Weak Barb). A process P has a barb x denoted by P ⇓ x iff P → * α -→ and x ∈ α.

Parametric Definitions: CCS and CCS p : A typical way of specifying infinite behaviour is by using parametric definitions [START_REF] Milner | Communicating and Mobile Systems: the π-calculus[END_REF]. In this case we extend the syntax of finite processes (Definition 1.4.6) as follows: P, Q, . . . := . . . A(y 1 , . . . , y n )

(1.3)

Here A(y 1 , . . . , y n ) is an identifier (also call, or invocation) of arity n. We assume that every such an identifier has a unique, possibly recursive, definition A(x 1 , . . . , x n ) def = P A where the x i 's are pairwise distinct, and the intuition is that A(y 1 , . . . , y n ) behaves as its body P A with each y i replacing the formal parameter x i . For each

A(x 1 , . . . , x n ) def = P A , we require fn(P A ) ⊆ {x 1 , . . . , x n }.
Following [START_REF] Giambiagi | On the expressiveness of infinite behavior and name scoping in process calculi[END_REF], we use CCS p to denote the calculus with parametric definitions with the above syntactic restrictions.

Remark 1.4.2. As shown in [START_REF] Giambiagi | On the expressiveness of infinite behavior and name scoping in process calculi[END_REF], however, CCS p is equivalent w.r.t. strong bisimilarity to the standard CCS. We shall then take the liberty of using the terms CCS and CCS p to denote the calculus with parametric definitions as done in [START_REF] Milner | Communicating and Mobile Systems: the π-calculus[END_REF].

The rules for CCS p are those in Table 1.2 plus the rule:

CALL P A [y 1 , . . . , y n /x 1 , . . . , x n ] α -→ P A(y 1 , . . . , y n ) α -→ P if A(x 1 , . . . , x n ) def = P A (1.4)
As usual P [y 1 . . . y n /x 1 . . . x n ] results from replacing every free occurrence of x i with y i renaming bound names in P wherever needed to avoid capture.

Notions and equivalences

A central concept is the notion of encoding : A map from the terms of a π-calculus variant (e.g., CCS p ) into the terms of another (e.g., CCS ! ). The existence of encodings that satisfy certain properties is typically used as a measure of expressiveness (see [CCP06, Gor07, Gor06, CM03, CC01, Pal03]).

Bisimilarity

Definition 1.4.10 (Reduction Bisimilarity). A reduction simulation is a binary relation R satisfying the following: (P, Q) ∈ R implies that:

1.4. BACKGROUND • if P τ -→ P then ∃Q : Q τ -→ Q ∧ (P , Q ) ∈ R.
The relation R is a reduction bisimulation iff both R and its converse R -1 are reduction simulations. We say that P and Q are reduction bisimilar, written P ∼ r Q iff (P, Q) ∈ R for some reduction bisimulation R.

Definition 1.4.11 (Strong Bisimilarity). A strong simulation is a binary relation R satisfying the following: (P, Q) ∈ R implies that:

• if P α -→ P then ∃Q : Q α -→ Q ∧ (P , Q ) ∈ R.
The relation R is a strong bisimulation iff both R and its converse R -1 are strong simulations. We say that P and Q are strongly bisimilar, written P ∼ Q iff (P, Q) ∈ R for some strong bisimulation R.

Definition 1.4.12 (Weak Bisimilarity). A (weak) simulation is a binary relation R satisfying the following: (P, Q) ∈ R implies that:

• if P s =⇒ P where s ∈ L * then ∃Q : Q s =⇒ Q ∧ (P , Q ) ∈ R.
The relation R is a bisimulation iff both R and its converse R -1 are simulations. We say that P and Q are (weakly) bisimilar, written P ≈ Q iff (P, Q) ∈ R for some bisimulation R.

Language and failures equivalences

We shall use the notion of language and failures in order to measure the expressive power of the calculi. Language notion is particularly suitable for this work, because the comparison involves different computability models.

Following [START_REF] Jos | Decidability of bisimulation equivalence for processes generating context-free languages[END_REF], we say that a process generates a sequence of non-silent actions s if it can perform the actions of s in a finite maximal sequence of transitions. More precisely: Definition 1.4.13 (Sequence and language generation). The process P generates a sequence s ∈ L * if and only if there exists Q such that P s =⇒ Q and Q α -→ for any α ∈ Act. Define the language of (or generated by) a process P , L(P ), as the set of all sequences P generates. We say that P and Q are language equivalent , written

P ∼ L Q , iff L(P ) = L(Q).
The above definition basically states that a sequence is generated when no transition rules can be applied. It is clearly related to the notion of language generation of models of computation. Namely, formal grammars where a sequence is generated when no rewriting rules can be applied.

We recall the notion of failure following [START_REF] Milner | Communication and Concurrency[END_REF]. We first need the following notion: Definition 1.4.14. We say that P is stable iff P τ -→.

Intuitively we say that a pair e, L , with e ∈ L * and L ⊆ L, is a failure of P if P can perform e and thereby reach a state in which no further action (including τ ) is possible if the environment will only allow actions in L.

Definition 1.4.15 (Failures). A pair e, L , where e ∈ L * and L ⊆ L, is a failure of P iff there is P such that: (1) P e =⇒ P , (2) P l -→ for all l ∈ L, and (3) P is stable. Define Failures(P ) as the set of failures of a process P . We say that P and Q are failures equivalent , written

P ∼ F Q iff Failures(P ) = Failures(Q).

State of the Art

This project aims at analyzing the reachability problem in CCS ! , hence it is important to highlight other similar theories developed for the most representative process calculi, like CCS and π-calculus. Moreover, it is important to know which tools using this theories have been developed. In the following section, those aspects are going to be presented.

Scientific Background

We will present a short abstract of three works that are related with our project

• On the expressivity of infinite and local behavior in fragments of the π-calculus[Ara09]: This Ph.D. thesis is an expressiveness study for fragments of the π-calculus. The main results of this dissertation includes a characterization of CCS ! in the Chomsky Hierarchy, i.e., the author propose a way to generate formal languages using CCS ! processes. Besides, they prove the relationship between context-free grammars and the CCS ! processes by showing that not all the context-free grammars can be generated by those processes (preserving termination). As stated before, the work proposed here is based on the results from such study, since the relation between the formal languages, the language generation and the reachability problem is direct. Then, our results will help to prove other important aspects on the expressiveness of π-calculus.

• On the decidability of the control reachability problem in the asynchronous π-calculus[AM02]: This work studies an analog problem, it consists basically that given a process in asynchronous π-calculus (with some special constraints) they need to determine if such process can reach a special configuration. The main difference lies in the calculus, since they use an strictly asynchronous formalism then their results do not apply directly in our problem.

• On the expressive power of recursion, replication and iteration in process calculi [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF]: This report provides a wide analysis about three mechanisms for giving infinite behavior in process calculi, namely they study the expressiveness of recursion, iteration and replication. The authors provide an hierarchy between the three mechanisms, they give an encoding from recursion to replication, and replication to iteration. They also study four basic issues, termination (all computations of a given process are finite), convergence (the existence of a finite computation), barb (the possibility of performing an action after a sequences of synchronizations) and weak bisimulation (check whether two processes are weak bisimilar). In this work, we shall use the decidability of barb in the replication case.

Technological Background In this section, we present two practical tools related to process calculi

• The Edinburgh Concurrency Workbench (CWB):3 This workbench is an automated tool which caters for the manipulation and analysis of concurrent systems. In particular, the CWB allows for various equivalence, preorder and model checking using a variety of different process semantics. For example, with the CWB it is possible to:

-define behaviors given either in an extended version of CCS or in SCCS, and perform various analyses on these behaviors, such as analyzing the state space of a given process, or checking various semantic equivalences and preorders;

-define propositions in a powerful modal logic and check whether a given process satisfies a specification formulated in this logic;

-play Stirling-style model-checking games to understand why a process does or does not satisfy a formula;

-derive automatically logical formulae which distinguish nonequivalent processes;

-interactively simulate the behavior of an agent, thus guiding it through its state space in a controlled fashion.

• The Mobility Workbench (MWB):4 MWB is a similar to the previous tool, but its application is focused on π-calculus instead of CCS. In an analogous way this workbench is used to model concurrent systems and it allows to reason about equivalences, behaviors, among other functionalities.

Project Context

This project is part of a much bigger project named FORCES As it can be seen, the application of process calculus such as π-calculus is important in different areas. This project will help for developing and implementing new tools based in this calculus, since determining if an action can be made is central for many models in different areas. The main advantage will be given in security analysis which is a very important topic nowadays.

Then, the results will reinforce the work made in FORCES and also they will give a new result in concurrency theory. An additional advantage of this project is to consolidate relationship between AVISPA and École Polytechnique at Paris, through teacher Frank Valencia (Project Co-Supervisor), since this project feeds the interests that have been built-up jointly.

Contributions

The main contributions of our work are listed below:

1. We provide an accurate analysis for the relation between the local names and the observable actions by showing an encoding that reveals the logarithmic relation between them.

2. We give an impossiblility result concerning with the use of a fixed amount of local names in a process. In consequence, we cannot impose a delay of an action progressively growing using a constant amount of nested restrictions.

3. We show a special case of the relation between nested restrictions and observable actions, where there is no process with two nested restrictions which can delay the execution of an action by three previous actions.

4. We prove the direct relation between nested local names and sequence of observable actions.

5. We present a transformation of the reachability problem to barbs. In consequence, we prove the decidability of the reachability problem for CCS ! .

6. We provide an algorithmic approach for solving the reachability problem and its respective computational complexity.

7. We present a small interpreter for CCS ! . It receives a process written in CCS ! and returns its possible evolutions according to the operational semantics.

Chapter 2

Local Names vs. Observable Actions

In this chapter we describe the influence of the local names on the amount of observable actions that a process can perform before reaching a specific state. First, we shall introduce the notion of a special family of CCS ! processes called trios and its relationship with the dependency of actions. We then show how to use this kind of processes to analyze the relation between local names and observable actions. Then, we prove the limit of the local names when trying to perform observable actions before reaching a special state. We after relate the decidability of barbs with reachability problem and finally we use this relation and our result to determine the decidability of the reachability problem.

A Special Family of Processes: Trios

Trios-Processes [Ara09] is a special family of CCS ! processes with a simple but powerful structure which conserves the behavior of CCS ! processes. Its structure will allow us to analyze more easily the dependency between actions.

Formal Definition

Intuitively, trios processes are a subset of arbitrary CCS ! processes composed only by "trios" (sequences of three actions). Formally we have:

Definition 2.1.1 (Trios Process). We shall say that a CCS ! process T is a triosprocess iff all prefixes in T are trios; i.e., they all have the form α.β.γ and satisfy the following: If α = τ then α is a name bound in T , and similarly if γ = τ then γ is a co-name bound in T . For instance (νl)(τ.τ.l | l.a.τ ) is a trios-process. We will view a trio l.β.l as linkable node with incoming link l from another trio, outgoing link l to another trio, and contents β.

A SPECIAL FAMILY OF PROCESSES: TRIOS

Interestingly, the family of trios-processes can capture the behaviour of arbitrary CCS ! processes via the following encoding: Definition 2.1.2. Given a CCS ! process P , P is the trios-process (ν l)(τ.τ.l | P l ) where P l , with l ∈ n(P ), is inductively defined as follows:

0 l = 0 α.P l = (ν l )(l.α.l | P l ) where l ∈ n(P ) P | Q l = (ν l , l )(l.l .l | P l | Q l ) where l , l ∈ n(P ) ∪ n(Q) !P l = (ν l )(!l.l .l | ! P l ) where l ∈ n(P ) (ν x)P l = (ν x) P l
Notice that the trios-process α.P l encodes a process α.P much like a linked list. Intuitively, the trio l.α.l has an outgoing link l to its continuation P l and incoming link l from some previous trio. The other cases can be explained analogously. Clearly the encoding introduces additional actions but they are all silent-i.e., they are synchronisations on the bound names l, l and l .

Unfortunately the above encoding is not invariant w.r.t. language equivalence because the replicated trio in !P l introduces divergence. E.g, L((νx)!x) = { } but L( (νx)!x ) = ∅. It has, however, a pleasant invariant property: weak bisimilarity, ≈.

Proposition 2.1.1. For every CCS ! process P , P ≈ P where P is the triosprocess constructed from P as in Definition 2.1.2.

Action Dependency in Trios

Intuitively, the reachability problem consists in checking whether a process can perform a specific action at some point in its evolution. Then we are specially interested in the sequences that a process can perform before such action, since we shall use the relationship between these sequences and the structure of the process in order to obtain an useful measure for determining reachability. Now we shall present the influence of the dependencies in a trios process.

For analyzing the influence of dependencies, let s = a.b.c and s = a 10 b be sequences of actions. Now take a trios-process P and see it as a linked list, it is easy to check that if P s =⇒ then the there must be a "link" between a and b, and similarly between b and c, since the observable actions can only be in the center of a trio (as data in a linked list). On the other hand, take a process Q s.t. Q s =⇒, this case is different from s , since there is no order between the a's thus what you can only infer from the structure of the process is that you need a special link after performing a 10 , and the independence of the a's implies that they can be performed anytime. This intuitive description gives us a powerful insight at analyzing the sequences that a trios-process can perform. From this fact we can say that the case when you need a maximum amount of "links" is when there is a complete dependency among actions. Therefore, when the links are used in the worst way, the result is a relation 1-1 between observable actions and local names. This is not the case when there exist independent actions.

In the next section we will focus mainly on the behavior of trios-processes with independent sequences in order to find the best way of exploiting local names, and then figuring out the limits of the possible sequences that a process can perform given an amount of local names.

Exploring the Limits of Local Names

In this section we shall show the limits of the local names when we need to build a process which performs a set of actions before reaching a specific state. Using trios-processes, we will be able to show the optimal way of using the local names. Later, we shall prove that using a fixed number of local names will not allow to have an unbounded amount of actions, i.e., at some point we will obtain an undesirable behavior. Finally, we shall show a specific case of this limit.

Logarithmic Local Names for Independent Actions

As said before, we will focus in minimizing the use of local names in order to find the relation between local names and sequence of observable actions. The intuitive idea is to build a trios-process T which performs a sequence of independent actions s = a n then β = b using as least local names as possible.

We propose a logarithmic amount of local names with respect to n. Let v n ∈ N the number of local names used; t n ∈ N the number of resulting trios, f (i, n) ∈ N×N a function (used for convenience) that takes the half of t n , i times; i P denotes the parallel composition of P , i times; and form now on, we will use l i to denote local names in the process.

v n = log 2 n + 1 t n = 2 Vn f (i, n) = 2 (vn-i)
Then, we construct T in four parts. In the first part (P 1 ), every a is encoded in a trios-process of the form τ.a. l1 . The second part (P 2 ) is used when n is not a power of 2, then we need to fill the output actions that left to complete an amount of l1 that must be a power of 2 (This will be used for making one reception for two variables in a progressive way). The third part (P 3 ) consists in the reception of every output name l1 and every trio finish with an acknowledge l2 . For the first n trios (which output in l1 ) we need the same amount of receptions, then this process is made successively, thus the amount of new trios is reduced to the half until we get just one trio which outputs in the channel ( lvn ). The last part (P 4 ) consists in the last reception that represents the acknowledge of all the a's previously specified, hence the b can be executed for having a n b.

P 1 = n τ.a. l1
(2.1)

P 2 = f (1,n)-n τ.τ. l1
(2.2)

P 3 = vn i=2 f (i,n) l i-1 .l i-1 . li (2.
3)

P 4 = l vn .b.τ (2.4) T = P 1 | P 2 | P 3 | P 4
For illustrating the process proposed above, let us show the process that results for a 4 b, n = 4. (2.5)

v 4 = log 2 4 + 1 = 3 t 4 = 2 v 4 = 8 f (i, n) = 2 (vn-i) f (1, 4) = 4, f (2, 4) = 2, f (3, 4) = 1 P 1 =
P 2 = f (1,4)-4
τ.τ. l1 = 0 τ.τ. l1 = 0 (2.6)

P 3 = 3 i=2 f (i,4) l i-1 .l i-1 . li = f (2,4) l 1 .l 1 . l2 | f (3,4) l 2 .l 2 . l3 (2.7) = 2 l 1 .l 1 . l2 | 1 l 2 .l 2 . l3 (2.8) = l 1 .l 1 . l2 | l 1 .l 1 . l2 | l 2 .l 2 . l3 (2.9) P 4 = l 3 .b.τ
(2.10)

Q = P 1 | P 2 | P 3 | P 4 (2.11) = (τ.a. l1 | τ.a. l1 | τ.a. l1 | τ.a. l1 ) | (l 1 .l 1 . l2 | l 1 .l 1 . l2 | l 2 .l 2 . l3 ) | l 3 .b.τ (2.12)
This construction uses a logarithmic amount of local names with respect to the amount of observable actions. From now on, we shall show that this is the best way of using local variables in order obtain the longest sequence of independent observable actions before reaching a subprocess which is able to perform a particular action (in this case b).

Constant Local Names and Unbounded Independent Actions

In order to prove that the previous encoding uses the local names in an optimal way, first we will proceed by proving that using a fixed number of local names (less than logarithmic) we cannot build processes which delay an action unboundedly, i.e., there is no amount of local names s.t. we can unboundedly construct processes where the action (we are analyzing) can only be executed after a growing number of observable actions.

Moreover, we want to prove that a constant number of local names constrains the expressiveness of the calculus, we shall show that if we only use a fixed number of local variables then there is a limit for the processes that we can build. We will begin by providing some results about sets and its relation with infinite sequences. Then, we will introduce a lemma that proves the limits of using fixed local names.

Remark 2.2.1. We are interested in infinite sequences using natural numbers as elements, then from now on the alphabet for constructing the sequences will be the natural numbers. Besides, we will use x ∈ s to indicate that the number x is in the sequence s (as a symbol taken from the alphabet).

This kind of sequences will be very useful for analyzing the infinite behavior when we try to generate an infinite amount of processes with fixed local names. The next result is from sets, but it will be helpful when we relate it to infinite sequences.

Theorem 2.2.1. [Apo67] (The Well-Ordering Principle) Every non-empty set of positive integers contains a smallest element. Now we will state the relationship between a set and and an infinite sequence, basically such sequences can be seen as a set with the same elements but without repeated elements and order. The set might not be infinite, but it is irrelevant for our purposes. In consequence, we can make a relation between the result of the "well-ordering principle" in sets and infinite sequences of naturals as a corollary.

Corollary 1. Every non-empty infinite sequence of naturals contains a smallest element.

We have related the results from sets to infinite sequences of naturals, now we introduce a convention for the smallest value in a sequence and the definition of "delay" an specific action.

Definition 2.2.1. Let s be a non-empty infinite sequence, we use min(s) to denote a function that takes an infinite of naturals and gives the smallest value in s and it exists by 1.

Definition 2.2.2 (Delay). A process P delays β with a minimum number of k actions defined over a finite alphabet Σ iff P =⇒ with s = b 1 . . . b k , and s, s ∈ Σ * . From now on, P k,β,Σ denotes a process P which produces β with a minimum number of k actions defined over a finite alphabet Σ. Now we can present the general result about fixed local names, we will prove a lemma that states that if we only have a specific amount of local variables then we are not able to build every process P k,β,Σ with k ≥ 0. This impossibility is based in the idea that if there are finite local variables, then all processes can only be constructed using a finite amount of possible trios, as consequence every process can be seen as a tuple since we can count the ocurrences of the trios and save such values in the tuple.

The result is an infinite sequence of tuples and we can order it to find two subsequent processes (say P i,β,Σ and P j,β,Σ ) which are supposed to have a minimum delay for the β action (i and j actions respectively), but this order means that the "greater" process P j,β,Σ can do the same things as the "smaller" P i,β,Σ then we can conclude that P j,β,Σ could finish before than planned (after i actions) leaving us in a contradiction. After introducing intuition, the lemma is formally stated.

Lemma 1. Let S be defined as {P k,β,Σ ∈ T rios | k ≥ 0}, there is no n ν s.t for every P ∈ S then |bn(P )| ≤ n ν .

Proof. Suppose by means of contradiction that there exists n ν such that for every P ∈ S then |bn(P )| ≤ n ν . The number of possible trios N is finite since actions (alphabet, local names and τ ) are finite. Hence, we have the finite set L T = {t 1 , t 2 , ..., t j , ..., t N } where every t j is a trio and L T represent all possible trios.

If the trios are finite then every P k,β,Σ can be written in a normal form P k,β,Σ = (ν -→ x ) i α i .β i .γ i where every α i .β i .γ i ∈ L T . It is important to notice that P k,β,Σ represents the family of processes with a delay of k actions for β, but we are only interested in the minimum process of such family (ommiting unnecesary trios).

Every P k,β,Σ can be seen as a tuple p k = (t k 1 , t k 2 , ..., t k j , ..., t k N ) where t k j represents the amount of t j present in P k,β,Σ . Hence, S can be represented as an infinite sequence I = p 1 .p 2 . . . p k . . ., the idea is to find a subsequence of I (say I ) that is nondecreasing ordered with respect to every field (t i where 1 ≤ i ≤ N). This can be done by taking the projection of every field as an infinite sequence and filter it to obtain a nondecreasing order.

Let L = T 1 .T 2 . . . be an infinite sequence of tuples, L i = T i 1 .T i 2 . . . be the projection of the field i in every tuple of the sequence and N the number of fields (as much as possible trios). Then we have the family of functions f i : (π) ω → (π) ω and F : (π) ω → (π) ω , these functions must satisfy the following equations:

F (L) = f N • . . . • f 1 (L) f i (L) = T j .f i (L )
where T i j = min(L i ) and L = T 1 . . . T j .L Therefore, I ord = F (I) is an infinite and nondecreasing ordered subsequence of I. From I ord , we can take two subsequent elements say p i = (t i 1 , t i 2 , ..., t i N ) and p j = (t j 1 , t j 2 , ..., t j N ) where for every t i m ≤ t j m (1 ≤ m ≤ N) and i < j.

By hypothesis there exist a sequence s = α 1 . . . α i such that P i,β,Σ s .β =⇒, and for every sequence s if P i,β,Σ s =⇒ then P j,β,Σ s =⇒ since for every trio t = α.β.γ if t ∈ P i,β,Σ then t ∈ P j,β,Σ . Hence, P j,β,Σ s .β =⇒ but P j,β,Σ was supposed to delay β with j actions minimum, leaving us in a contradiction. As a result, the set S cannot be obtained with a fixed number of local variables.

In conclusion, we cannot get the set S since in some point a process will have a lesser delay than supposed. This result shows that we can give an specific behavior to a process depending in the amount of variables that we have, since in some point we will be limited to express a different behavior if we have already used all the process that are available. Therefore, if we can control the number of local variables then we can have more expressiveness since could have more processes that can be built.

Two Local Names for Three Independent Actions

The previous result proved the limit of fixed local names, now we present a particular case where we try to build a process which is able to delay b with a 3 minimum. This is a proof by cases where we show that there is no possible combination of trios in order to obtained the desired behavior. Theorem 2.2.2. There is no CCS ! trios-process P with two nested local variables l 1 and l 2 that delays the execution of an action b with a 3 independent actions at least.

Proof. We want to prove that there is no CCS ! trios-process which execute the b action after 3 independent a's. We will proceed by contradiction, then suppose that exists a trios-process T that delays b with a 3 .

Suppose that we can build a trios-process T that can only output the sequence a 3 b where b depends from the three a's and they are independent among themselves. Consider two nested local names (l 1 , l 2 ), then T has to be composed by the following trios:

1. There must be a final trio of the form l 2 .b.τ , where l 2 will be synchronized with an l2 action when the three a's have been executed. Case 1 (t 1 = l 1 .a.β) By definition the three a's are independent, then we do not need to prefix any a thus we can replace l 1 by τ .

Case 2 (t 2 = l 2 .a.β) We will prove that none initial trio can have the form l 2 .a.β. By definition there exist a trio t f = l 2 .b.τ and there must be a l2 that allows the execution of t 2 . In the moment that we can execute t 2 we can also execute t f and ommit one a. Then b can be executed before than planned, a contradiction.

Case 3 (t 3 = l 2 .α.β) We will prove that none intermediate trio can have the form l 2 .α.β. Suppose by means of contradiction that such trio exists and will be synchronized with t f = l 2 .b.τ . By definition α = l2 or β = l2 and by hypothesis t 3 is the "last" trio before t f and after the a 3 . Now t 3 contains a l 2 then there must be another trio containing a l2 for synchronizing with this action, but this action can also be synchronized with t f and it would be the "last" trio before t f , leaving us in a contradiction.

Case 4 (t 4 = α.l 2 . l2 ) We will prove that none intermediate trio can have the form α.l 2 . l2 . By definition there exist al least one trio τ.a. l1 and α ∈ {τ, l 1 , l 2 }. If α = l 2 we are in case 2, else if α = τ we can execute it then we will obtain l 2 . l2 analog to case 2 and if α = l 1 we can execute τ.a. l1 and the result is also l 2 . l2 analog to case 2.

Case 5 (t 5 = α. l1 . l2 ) We will prove that none intermediate trio can have the form α. l1 . l2 . By definition α ∈ {τ, l 1 } and there exist al least one trio τ.a. l1 . If α = τ then we can execute it and the result is l1 . l2 , else if α = l 1 we can execute τ.a. l1 and the result is also l1 . l2 . Besides, there exist another trio τ.a. l1 then there must be a trio that contains l 1 that will be synchronized with it, but this action can also be synchronized with l1 . l2 and after that we can execute l 2 .b.τ . As consequence, we can execute ab or a 2 b (depending of α), then b can be performed before than planned, a contradiction.

The Reachability Problem

Optimizing the Use of Local Names

In this section we shall show our main result that relates the amount of nested local variables and the amount of observable actions that can be performed before reaching a state. This relation will be based on the representation of a trios process as a binary tree.

First we introduce the notion of dependency and its relation with trios process by a convenient structure that we call trio dependency tree. This tree is basically a binary tree adapted to represent trios processes, they have some useful properties that will allow us to show the limits of the local variables. Finally we prove the relation between the amount of local variables and the observable actions by showing that the best tree that can be built has a logaritmic height with respect to the number of independent actions you want to perform.

Let us define the notion of dependency for actions and trios, and a notion of multi-set for trios processes. Intuitively, an action β depends on another action α (in a process P ) if P could not had performed β without performing α first.

Definition 2.3.1 (Causal Dependency). Let P be a CCS ! process, s be a sequence of actions, α and β be actions. We say that β depends on α if there exists s s.t. P s.β =⇒ and α ∈ s (and directly depends if s = α). If an action β does not depend on any action we say that is independent, this means that β can be performed by P anytime.

Remark 2.3.1 (Multi-Set of Trios). We will use S P for representing the multi-set of trios built from a trios process P . The idea is that any trios process P can be seen as a parallel composition of trios, then we can take P as a multi-set of trios. More formally, any trios-process P can be transformed into P = (ν -→ x ) α 1 .β 1 .γ 1 | . . . | α m .β m .γ m and from P we can build S P = {α 1 .β 1 .γ 1 , . . . , α m .β m .γ m } a multi-set of trios. Notice that if P contains a replicated trio !t then we can take its expansion in order to perform β (the action we want to analyze). This multi-set can be built if we only consider processes without restriction under the scope of replication !(νx), then from now on we restrict our calculus to CCS -!ν ! . We are interested in finding the possible dependencies of an specific action β, such action must be in a trio of the form α.β.γ hence we focus on analyzing the dependencies from α. For this analysis we introduce the trio dependency trees, the idea is to take a trios process and see it as a binary tree induced by the dependencies present on the process related to α. We define three general rules for building a tree given a trios process.

Every rule takes a multi-set of trios S P and a tree T then check if there exists a trio t = α 1 .α 2 .α 3 ∈ S P such that some co-action of α 1 , α 2 , or α 3 is a leaf of T . Depending on the position of α i in t it may discard some names. Intuitively, the rules simulate a possible execution of the dependencies in the process P , then it will check if a leaf l can be synchronized and check whether that l is being guarded by something else.

Notice that there are several ways for taking the dependencies due to the order in which the rules are applied, since there are many ways of executing the actions in a trios process. These rules reflect any possible execution of a process, i.e., if you take a trios process and apply these rules then you can build any possible execution of observable actions in the process.

More precisely, each rule takes a pair (T, S P ) and evolves to (T , S P ) where T has the same nodes as T but there is a leaf of T that in T has two children and a trio is removed from S P to obtain S P . This new node is built from a trio t = α 1 .α 2 .α 3 ∈ P just by checking if the co-action of α 1 , α 2 or α 3 is a leaf of T . In every case, we compare a leaf with the actions present in a trio t ∈ S P by the first, second or third action respectively. If t is used for the synchronization then we remove a copy of t from S P and we can apply the rules again. The next definition states formally the notion of trio dependency tree.

Definition 2.3.2 (Trio-Dependency Tree). Let P be a trios process, then a triodependency tree T (P,t) is a binary tree which represents the dependencies of a trio t = α.β.γ in a multi-set of trios S P . Let T (t,t) be a tree with one node labeled γ and children labeled α and β, then (T (t,t) , S P ) → * (T (P,t) , S P ) → where → * is the closure of → given by the following rules:

Rule 1 T (Q,t) = γ and α.β.γ ∈ S R (T (Q,t) , S R ) → ( γ α β , S R -{α.β.γ}) Rule 2 T (Q,t) = β and α. β.γ ∈ S R (T (Q,t) , S R ) → ( β τ α , S R -{α. β.γ}) Rule 3 T (Q,t) = α and ᾱ.β.γ ∈ S R (T (Q,t) , S R ) → ( α τ τ , S R -{ ᾱ.β.γ})
From T (P,t) then L(T (P,t) ) are the leaves of T (P,t) . If l is the root of a tree T (P,t)

then P s =⇒ l -→ where s is a permutation of L(T (P,t) ) (leaves of T (P,t) ). These rules can be applied non-deterministically then from a multi-set of trios S P and a trio t ∈ S P we can build different trees depending on the order that the rules are applied. The final tree represents the actions that must be performed for reaching t in S P . First, the leaves are the actions that must be done and the nodes represent synchronizations that must be performed. This combination will allow P to reach t, the order of execution is divided in two groups leaves and nodes (see figure 2.4). The left leaves l can be performed anytime as observable actions (unless it is τ ) and right leaves must wait for its brother to be performed. The left nodes needs to be preceeded by its children to be synchronized and right nodes must also wait for its brother. Therefore, every node and leaf must be consumed to reach the root of a given trio-dependency tree T .

Moreover, if we want to read a trio-dependency tree T as a trios process P then we just take every node γ with children α and β and put a trio α.β.γ in P (see figure 2.5). It is important to notice that if we have a leaf labeled with a local name at the end of the computation, then when this leaf is reached then the process will be blocked.

With these definitions we can introduce the result about the expresiveness of the local variables in a CCS ! process. Intuitively, there exists a direct relation between the number of local names and the amount observable actions that can be done before releasing an specific action (say β). This relation is based in the representation of the trios in a trio dependency tree and we prove that the best way for building this kind of tree with the least amount of variables is by using a logaritmic amount of nested local names with respect to the observable actions. We state the lemma formally.

Lemma 2. Let Σ be a finite alphabet, k ∈ N, β ∈ Σ and P ∈ CCS -!ν ! . The minimum |P | ν that P needs to delay β with k independent actions (definition 2.2.2) is log 2 k + 1.

Proof. Without loss of generality we will use β = b and the sequence of k independent actions a k where every a is independent. We proceed by stating the minimum trios that P must contain such that P delays b with k actions.

The final action must be b, then we need at least one trio t f = l 1 .b.τ . Here l 1 guards the execution of b before a k and the continuation can be τ since it does not affect the result.

There must be at least k trios containing a, then we have t i = α i .a.γ i with 0 ≤ i ≤ k. Every α can be τ since the actions are independent then they can be performed anytime. Every γ must be a co-name we need to make a synchronization for ensuring the execution of every a. With the above conditions, we can state that every minimal (using the least possible local names) process Q that that delays b with a k actions must contain the trios t i and t f . Since b is the last action, then the synchronizing action l1 should be available after the synchronization of γ actions. Therefore, l1 must be guarded by other actions that allows this behavior. Then P must have (at least) a structure such that the name that guards b (l 1 in this case) is the last synchronization (if there are τ actions after b we can ommit them).

We can build a trio dependency tree where we need that l 1 be the root (the other trios must be guarding it) and we need at least k leaves contianing a's. Remember that observable actions like a must be right leaves since they cannot be in the first position of a trio. Then we need k nodes, every one with left child τ and right child a, hence the minimum tree must have at least log 2 k + 1 height for containing such quantity of leaves.

Moreover, if we take any node of this tree l then none descendant of it can be l nor l, since they could reach the root of the tree ommiting some leaves and reducing the delay expected. There are three cases illustrated in the figure 2.6. All of them can ommit leaves in order to reach the root. Now suppose by means of contradiction that the minimum tree T (Q,t f ) contains repeated descendants (name or co-name) and the process Q associated to the tree Therefore if we want a tree T P such that h(T P ) = log 2 k + 1 and P delays b with a k actions then every path from the root to a leaf s = l 1 .l 2 . . . l k+1 must have a different name for every step, hence we need at least log 2 k + 1 local names to obtain a process P such that P delays b with minimum a k actions.

k ≤ 1 k ≤ 2 k ≤ 4 . . . . . . . . . . . . . . . . . . k ≤ 2 m-2 k ≤ 2 m-1 k ≤ 2 m-1 m ≥ log 2 k + 1 l 1 l 2 l 2 l 3 l 3 l 3 l 3 l m-1 l m l m l m-1 l m l m
In summary, the result obtained directly relates the number of nested local names in a process and the sequences it can perform before an action. Intuitively, there is a limit on the size of the sequences related to the execution of some action in the process, and such limit says that (in th best case) we can use n local names to delay an action by 2 n independent actions at most. Using the encoding from arbitrary process to trios, the previous result also applies since it preserves weak bisimulation.

As a result, we have that given a CCS -!ν ! process there is a bound on the delay we can apply to an action. Therefore, if we overpass this limit, it means that there exists another sequence that can execute the action before and this sequence is strictly related with the number of nested local names. In conclusion, this result gives us an insight on the expressiveness given by the local names and its relation with observable actions.

From barbs to reachability

In this section we will use the decidability result for barbs from [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] and the relation between local names and sequences, in order to give the proof of the decidability of reachability for CCS -!ν ! .

We need to establish the relation between barbs and reachability. Basically, the reachability problem consists in checking whether an action can be performed by a process after a sequence of observable actions, then we can put a process in parallel that has a sequence of co-actions for every element in the sequence of observables and an "acknowledge" channel at the end.

In the resulting process, every observable action in the original can be transformed into a synchronization with the co-actions in the new one. Hence, we can check that the sequence was succesfully executed if all the co-actions were consumed and the "acknowledge" was released, and actually it is a barb for the whole process. After this evolution, the action we are analyzing must be performed after a (possible empty) synchronizations, then becoming also in a barb.

Following this idea, we can now state formally the relation between barbs and reachability.

Lemma 3. Let P and Q be a CCS ! processes, s be a sequence of actions and n ∈ N. P

-→ Q 1 ᾱ2 -→ . . . ᾱn -→ Q n x -→ therefore Q ⇓ ᾱ1 , . . ., Q n ⇓ x.Finally if we take the process (P | Q) then (P | Q) → * (P 1 | Q 1 ) . . . → * (P n | Q n ) ⇓ x⇓ β , we can conclude that (P | Q) ⇓ x⇓ β . (⇐) If (P | Q) ⇓ x⇓ β then P s.β =⇒. By hypothesis (P | Q) → * (P n | Q n ) x -→⇓ β .
From the initial assumptions we can say that since

β ∈ n(Q n ) then P n β =⇒ and x ∈ fn(P n ) then Q n x =⇒. Now using the definition of Q we have that Q ᾱ1 -→ Q 1 ᾱ2 -→ . . . ᾱn -→ Q n x -→.

=⇒.

The previous lemma tranforms the reachability problem into a barbs problem, now we will combine our previous result with this reduction in order to obtain the decidability of the reachability problem. Intuitively, the reachability was reduced to a problem of checking whether given a sequence and an action then the process has two special barbs, with our previous results we know that this sequences are bounded on the number of nested local names. Therefore, we only need to check all the possible sequences until the size limit (finite amount of sequences) and check if the process has a barb with any of them. Formally we have: Theorem 2.3.1 (Decidability of Reachability Problem). Let P be a CCS -!ν ! process, Σ be a finite alphabet. The problem of deciding whether P

=⇒ is decidable.

As the main result, we have that checking whether an action can be reached by a process (with possible infinite behavior) is decidable.

Chapter 3 Computing Reachability

In this chapter we shall present an algorithmic approach for solving the reachablity problem. As seen previously, this problem is reduced to checking some special barbs in a given process then we need to introduce the basic concepts behind the decidability of barb. First, we shall present the concept of well-structured transition system (WSTS) which is central in the barb problem. Later, we shall use the relation between CCS ! and WSTS from [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] in order to present the solution proposed for the reachability problem. Finally, we will provide the solution for the reachability problem and its respective complexity analysis.

Background

In this section we will give an algorithm for determining the reachablity of an action in a given CCS ! process. First, we will introduce the notion of well-structured transition systems, an useful tool for analyzing infinite state systems. Then, we shall show the result from [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] for barb decidability based on well-structured transition systems. With this notions, we will propose an algorithm for solving reachability problem. Finally, we will give a brief analysis of the complexity of the algorithm. (The background presented here was taken from [BGZ09])

Well-Structured Transition Systems (WSTS)

The following results and definitions are from [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. Recall that a quasi-order (or, equivalently, preorder) is a reflexive and transitive relation. Definition 3.1.1. A well-quasi-order (wqo) is a quasi-order ≤ over a set X such that, for any infinite sequence x 0 , x 1 , x 2 , . . . in X, there exist indexes i < j such that x i ≤ x j .

Note that if ≤ is a wqo then any infinite sequence x 0 , x 1 , x 2 , . . . contains an infinite increasing subsequence x i 0 , x i 1 , x i 2 , . . . (with i 0 < i 1 < i 2 < . . .). Thus well-Theorem 3.1.2. Let P, Q, P ∈ CCS ! . If P α -→ P and P Q then there exists Q such that Q α -→ Q and P Q .

With the previous definitions, they define a WSTS with the reduction relation and the well-quasi-order above defined.

Theorem 3.1.3. Let P ∈ CCS ! . Then the transition system (Deriv(P ), →, ) is a finitely branching well-structured transition system with strong compatibility, decidable and computable Succ.

Decidability of barb

In [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] they prove the decidability of the barb in CCS ! . Given a process, determine if it can perform, possibly after some internal moves, an observable action on a given channel. This result is based on WSTS, hence we need other definitions from this theory [START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

Recall that given a quasi-order ≤ over X, an upward-closed set is a subset I ⊆ X such that the following holds: ∀x, y ∈ X : (x ∈ I ∧x ≤ y) ⇒ y ∈ I. Given x ∈ X, we define its upward closure as ↑ x = {y ∈ X | x ≤ y}. This notion can be extended to sets in the obvious way: given a set Y ⊆ X we define its upward closure as ↑ Y = y∈Y ↑ y. Definition 3.1.8 (Finite basis). A finite basis of an upward-closed set I is a finite set B such that I = x∈B ↑ x.

In this case the notion of basis is particularly important when considering the basis of the predecessor of a state in a transition system. The main interest is on effective pred-basis as defined below.

Definition 3.1.9 (Effective Pred-basis). A well-structured transition system has effective pred-basis if there exists an algorithm such that, for any any state s ∈ S, it returns the set pb(s) which is a finite basis of ↑ P red(↑ s).

The following proposition is a special case of Proposition 3.5 in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

Proposition 3.1.2. Let T S = (S, →, ≤) be a finitely branching, well-structured transition system with strong compatibility, decidable ≤ and effective pred-basis. It is possible to compute a finite basis of P red * (I) for any upward-closed set I given via a finite basis.

In [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] they use this proposition for proving the decidability of barbs in CCS ! . They are based on the idea the next idea: Clearly a process can perform an action α (in any number of steps) if such process is a predecessor of a process which can perform α immediately (i.e. in one step). If one can show that the set S consisting of those processes which can immediately perform α is upward closed, previous result allows us to compute effectively a finite pred-basis of P red * (S) and therefore to decide whether a process Q belongs to P red * (S): To this aim, in fact, it is suficient to decide whether in the (finite) basis there exist a process which is smaller than Q (this is possible because the quasi-order ≤ is decidable). [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] From now on, we will use the WSTS for CCS ! defined previously (but using P P,|P |ν instead of Deriv(P ), since Deriv(P ) ⊆ P P,|P |ν ). Now we shall present the definition of the effective pred-basis for (P P,|P |ν , →, ) from [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF].

They start by defining the set of processes Now α (P ) that can immediately perform the labeled action α and which are constructed by using sequential and bang subprocesses of P (in the sense made precise by Definition 3.1.7). Definition 3.1.10. Let P ∈ CCS ! . The set of processes Now α (P ) is defined as

{Q ∈ P P,|P |ν | Q α -→}.
Next they show that this set is upward-closed.

Proposition 3.1.3. Let P ∈ CCS ! . Then Now α (P ) =↑ Now α (P ) holds.

They provide a finite basis for the previously defined set. It is based on the fact that the set of sequential and bang subprocesses of a process is finite. Definition 3.1.11. Let P ∈ CCS ! . The set f bNow α (P ) is defined as follows:

f bNow α (P ) = {(νx 1 . . . x m )Q | Q ∈ Sub(P ), m ≤ |P | ν , x 1 . . . x m ⊆ bn(P ), Q α -→, n(α) ∈ {x 1 , . . . , x m }} Proposition 3.1.4. Let P ∈ CCS ! and α = τ . Then the set f bNow α (P ) is a finite basis of Now α (P )
Using the above definitions, they define the pred-basis as follows: Definition 3.1.12. Let P ∈ CCS ! . Given a process Q ∈ P P,|P |ν , we define

basic α ={Q|R | R ∈ f bNow α (P )}∪ {R ∈ Sub(P ) | ∃R : R α -→ R ∧ Q R }∪ synchbasic α (Q)
where:

synchbasic τ (Q) = {Q 1 |Q 2 | Q 1 ∈ Sub(P ) ∧ Q 2 ∈ f bNow α (P )∧ ∃Q 1 : Q 1 ᾱ -→ Q 1 ∧ Q Q 1 } synchbasic α (Q) = ∅ if α = τ
The pred-basis pb α (Q) of a process Q w.r.t α is defined by induction on the structure of the process as follows:

pb α (0) =basic α (0) pb α (α .Q) =basic α (α .Q) pb α (Q 1 + Q 2 ) =basic α (Q 1 + Q 2 ) pb α ((νx)Q) =basic α ((νx)Q )∪ {(νx)Q | Q ∈ pb α (Q) ∧ x = n(α)} pb α (Q 1 |Q 2 ) =basic α (Q 1 |Q 2 )∪ {Q 1 |Q 2 | Q 1 ∈ pb α (Q 1 )}∪ {Q 1 |Q 2 | Q 2 ∈ pb α (Q 2 )}∪ sync α (Q 1 , Q 2 ) pb α (!Q) =basic α (!Q) sync τ (Q 1 , Q 2 ) ={Q 1 |Q 2 | ∃α ∈ n(P ) : Q 1 ∈ pb α (Q 1 ) ∧ Q 2 ∈ pb ᾱ(Q 2 )} sync α (Q 1 , Q 2 ) =∅ if α = τ
With this definition, they provide the following result:

Lemma 4. Let P ∈ CCS ! and Q ∈ P P,|P |ν . Then pb τ (Q) is a computable finite basis of ↑ P red(↑ Q).
From this lemma it is strictly forward the following theorem Theorem 3.1.4. Let P ∈ CCS ! . Then the transition system (P P,|P |ν , →, ) is a well-structured transition system with strong compatibility, decidable and effective pred-basis.

Finally they present the decidability of barb. This result will be very useful for solving the reachability problem.

Proposition 3.1.5. Let P ∈ CCS ! . P ⇓ x iff P ∈ P red * (Now x (P )) or P ∈ P red * (Now x(P )).

Corollary 2. Let P ∈ CCS ! . Then P ⇓ x is decidable.

The last result is based on the idea that the barb can be expressed as the set of processes which can perform α immediately (say Now α (P )) and the set of predecessors (say P red * ) of them (using reduction relation). From previous results, the set Now α is upward closed and has a finite basis, hence it is possible to compute an finite pred-basis (a basis for the possible predecessors). Therefore, we only need to compare the original process with the elements in the basis, and check whether it is "bigger" (w.r.t ) than one of them in order to answer if it has the barb.

Solving Reachability

We can now present the algorithm for solving the reachability problem. As stated previously, asking if an action can be reached by a process is transformed in asking if the process has two special barbs, the first one is the acknowledge of a sequence of observable actions and the other is the action itself. In the same way, if we plan to describe a procedure which solve this problem, we need to consider the solution for the barb problem. Therefore, we will base our algorithm in the previous relation between barbs and WSTS in order to solve the reachability problem.

A procedure for reachability problem

From previous results, the reachability problem can be transformed in a barb problem for a set of sequences (built based on the structure of the process). Then, for solving this problem it is sufficient with checking these two special barbs with every sequence in the set. The first barb consists in asking whether the initial process is a predecessor (up to reduction) of a process which can perform the acknowledge action immediately.

Applying the procedure for decidability of barb, we will get a basis for this process and instead of stopping here, we can take this set to ask for the second barb in the same way. Finally we will obtain a (finite) pred-basis (a bit more complex than just one barb) and then we can check whether our process is related (w.r.t well-quasi-order) to any of the elements of the basis. If it is related, then the action is reachable, otherwise it is not.

After introducing the idea, we define a function that checks whether a process has a barb x and then checks if the resulting process (after performing this barb) has another barb y. Definition 3.2.1. Let P be a CCS ! process, x and y actions. We define the function apply the same principle (over the finite basis) in order to compute the next barb x. Finally, we only need to compare if the process R is bigger (w.r.t ) than one of the elements of the basis. Then we answer whether R has these two barbs and such procedure is repeated for every sequence in the set giving us the final result.

Following the same idea used in [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] for deciding a barb in a CCS ! process, we gave a function for checking whether an action can be performed by a process after a sequence of observable actions.

Analyzing the complexity

The complexity of this procedure depends basically on the amount of nested local names in a given process P , since it determines the size and the amount of sequences that we need to test in order to give a solution. It depends also on the structure of the process, since we need to compute some special sets defined by WSTS.

Therefore, the complexity of this function is divided in two parts. The first part consists on the amount of sequences, this value basically depends on the size of the alphabet c = |Σ| (possible actions for the sequences) and the limit l given by the nested restrictions |P | ν which is exponential w.r.t to |P | ν , then l = 2 |P |ν in the worst case (sequences of independent actions). In the case of sequences with size 2 |P |ν we have |Σ| 2 |P |ν possibilities, since we have |Σ| for every position in the sequence. This analysis is applied with size going from 1 to 2 |P |ν and the result is the sum of them. Hence, the amount of sequences |S| is given by the following expression:

2 |P |ν i=1 |Σ| i
The second part is based on the theory of well-structured transition systems. There are no complexity analysis (so far) for this methods, we cannot say much about them. It is important to notice, that infinite-state systems can be specified by this calculus and even that, we give a finite (huge) number of steps for solving the problem.

If we put the two parts together then we have to apply a method from WSTS for every possible sequence. We know how many possibilities we have, but we do not know exactly the complexity of the methods form WSTS. Nevertheless, this algorithm becomes too complex in real life only taking into account the amount of sequences that need to be checked. Using this grammar we build a small interpreter that takes a CCS ! process and returns its possible evolution, and it also point out which is needed to be performed in order to reach some process. For this purpose, we use another rule called step composed by an action and a process, then represents the evolution of a process by such action.

step ::= step(act: act newProc: ccsProc )

The interpreter will take a process and return a set of steps representing the process in which the input can be transformed using the operational semantics for CCS ! . Since we are specially interested in trios-proceses, we also provide a function (ProcessToTrio) that takes a CCS ! and performs the encoding from 2.1.1. This transformation can be exploited for attacking the reachability problem, but due to the complexity it becomes useless to implement the naive algorithm. Nevertheless, this can be an initial practical approach that could be optimized for real life as future work.

Tests and Examples

For performing the tests we use the function TestEval that takes a process written with grammar of figure 4.1. The answer is a record called Test, it has three fields p, realResult, and nicePrint where p is the input process, realResult is a set of steps that the process can perform and nicePrint contains the same that realResult but with a legible text format.

Chapter 5

Concluding Remarks

Summary

In chapter 2 we provide an accurate analysis for the relation between the local names and the observable actions by showing an encoding that reveals the logarithmic relation between them. Using this fact, we give an impossiblility result concerning with the use of a fixed amount of local names in a process. Therefore, we cannot impose a delay of an action progressively growing using a constant amount of nested restrictions.

In order to give an insight for the general proof, we show an special case of the relation between nested restrictions and observable actions, where there is no process with two nested restrictions which can delay the execution of an action by three previous actions. Using this results, we prove the direct relation between nested local names and sequence of observable actions.

As one of the main results, given n nested restrictions then the maximum delay for an action that can be imposed is 2 n . Finally, we present a transformation of the reachability problem to barb problem from [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF]. In conclusion, we can relate the amount of sequences with the decidability of barbs in order to prove the decidability of the reachability problem for CCS ! .

In chapter 3 we provide an algorithmic approach for solving the reachability problem and its respective computational complexity. The resulting algorithm is much more complex than exponential order, but if we consider that we are dealing with infinite state systems then we are giving a finite number of steps for checking a property in an infinite state space.

In chapter 4 we present a small interpreter for CCS ! . It receives a process written

FUTURE WORK

in CCS ! and returns its possible evolutions. This interpreter can be the beggining of a complex system for checking properties in infinite state systems.

Future Work

The results presented in this work may have three main extensions. First, we need to explore the relation between local names and observable actions when having the full calculus, i.e, there is name generation. We think that this should not affect the result since !(νx) does not raise the nesting value (depth) but the local names could grow in width, thus this variant could be explored. Second, we need to look for an algorithmic approach closer to real life since the complexity of the first approach is too expensive, hence it is not practical for real systems. Finally, the CCS ! stepper could be extended in order to obtain a CCS ! workbench for specification and verification of concurrent systems.

  subj(xy) = subj(xy) = subj(x(y)) = x, obj(xy) = obj(xy) = obj(x(y)) = y, subj(τ ) = obj(τ ) = ∅. Definition 1.4.4. (Semantics) The labelled transition relation α -→ is given by the rules in

  Input x(y).P xz -→ P {z/y} where x, y ∈ N Output xy.P xy

  Definition 1.4.6. (Syntax) Processes in finite CCS are given respectively by: P := M (νx)P P | P !P M := 0 π.P M + M π := x x τ Definition 1.4.7. (Semantics) The labelled transition relation α -→ is given by the rules

  4 τ.a. l1 = τ.a. l1 | τ.a. l1 | τ.a. l1 | τ.a. l1

  =⇒ where s = a 1 . . . a k and there is no k where k < k and P s .β

αFigure 2 . 1 :

 21 Figure 2.1: Three trios of the form α.a.β α Case τ Generates b l 1 Generates ab l 2 3 Figure 2.2: One trio containing l2 (Case A, α. l2 .β)

2.Figure 2

 2 Figure 2.3: One trio containing l2 (Case B, α.β. l2 )

Figure 2 . 5 :

 25 Figure 2.4: Order of execution or a trio dependency tree

  Figure 2.6: Tree representation for the properties

Figure 2 . 7 :

 27 Figure 2.7: General minimum tree for a k b

  s.β =⇒ iff (P | Q) ⇓ x⇓ β where s = α 1 . . . α n , Q = ᾱ1 . . . ᾱn .x and x ∈ fn(P ). Proof. (⇒) If P s.β =⇒ then (P | Q) ⇓ x⇓ β . By hypothesis P s.β =⇒ then ∃P 1 . . . P n s.t. P α 1 =⇒ P 1 . . . αn =⇒ P n β =⇒ there-fore P ⇓ α 1 , . . ., P n-1 ⇓ αn and P n ⇓ β . On the other hand, let us consider Q = ᾱ1 . . . ᾱn .x then by definition Q ᾱ1

  s.β =⇒ where s is a sequence over Σ * and β ∈ Σ is decidable. Proof. From lemma 3 P s.β =⇒ iff (P | Q) ⇓ x⇓ β where s = α 1 . . . α n , Q = ᾱ1 . . . ᾱn .x and x ∈ fn(P ). Besides, from [BGZ09] we know that checking (P | Q) ⇓ x⇓ β for any sequence s is decidable. From lemma 2 if P s.β =⇒ then |s| is bounded on |P | ν then the possible s are limited to those with |s| ≤ 2 |P |ν giving us a finite possible sequences S. Then the reachability depends on checking for every s ∈ S if (P | Q) ⇓ x⇓ β , with finite S and decidable barb then P s.β

  Figure 4.1: Grammar for CCS ! stepper

  Justification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Exploring the Limits of Local Names . . . . . . . . . . . . . . . . . . 2.2.1 Logarithmic Local Names for Independent Actions . . . . . . 2.2.2 Constant Local Names and Unbounded Independent Actions . 2.2.3 Two Local Names for Three Independent Actions . . . . . . . 2.3 The Reachability Problem . . . . . . . . . . . . . . . . . . . . . . . . 2.3.1 Optimizing the Use of Local Names . . . . . . . . . . . . . . . 2.3.2 From barbs to reachability . . . . . . . . . . . . . . . . . . . . Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1.1 Well-Structured Transition Systems (WSTS) . . . . . . . . . . 3.1.2 WSTS and CCS ! . . . . . . . . . . . . . . . . . . . . . . . . . 3.1.3 Decidability of barb . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Solving Reachability . . . . . . . . . . . . . . . . . . . . . . . . . . .

	3 Computing Reachability
	3.1

1 Introduction 1.1 Problem Description . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.1 Main Objective . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.2 Specific Objectives . . . . . . . . . . . . . . . . . . . . . . . . 1.3 1.4.1 Technical Background . . . . . . . . . . . . . . . . . . . . . . 1.4.2 Project Context . . . . . . . . . . . . . . . . . . . . . . . . . . 1.5 2 Local Names vs. Observable Actions 2.1 A Special Family of Processes: Trios . . . . . . . . . . . . . . . . . . 2.1.1 Formal Definition . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.2 Action Dependency in Trios . . . . . . . . . . . . . . . . . . . 2.2 3.2.1 A procedure for reachability problem . . . . . . . . . . . . . . 3.2.2 Analyzing the complexity . . . . . . . . . . . . . . . . . . . .

  Table 1.1. Omited from Table 1.1 are the symmetric forms of Sum-L, Par-L, Com-L and Close-L. Let us define the relation

α =⇒ , with s = α 1 . . . . α n ∈ Act * , as

  in Table 1.2. Omitted from Table 1.2 are the symmetric forms of Par-L, Com-L and Close-L.

	1.4. BACKGROUND
		Input x.P	x -→ P
		Output x.P x -→ P			Tau τ.P	τ -→ P
	Sum-L	P P + Q α -→ P α -→ P	Res	P (νy)P	α -→ P -→ (νy)P α	y ∈ n(α)
	There are two variants of CCS which extend the above syntax to express infinite
	behaviour in a different way. We describe them next.

  5 . It is a Colombian-French project funded by the program of "Equipes Associees" of INRIA 6 . The teams involved in this research collaboration are COM ÈTE 7 (INRIA), the Music Representation Research Group (IRCAM) 8 and AVISPA Research Group 9 (Universidad del Valle in agreement with Universidad Javeriana at Cali, Colombia -which the researcher is member-) (Colciencias). The main goal is to provide more robust formalisms for analyzing the emergent systems that our teams have been modeling during recent years: I.e., Security Protocols, Biological Systems and Multimedia Semantic Interaction.

5

  FORmalisms from Concurrency for Emergent Systems.

	More info at:
	http://www.lix.polytechnique.fr/comete/Forces/Welcome.html

6

Institut national de recherche en informatique et automatique. More info at: http://www.inria.fr/ 7 http://www.lix.polytechnique.fr/comete/ 8 Institut de Recherche et Coordination Acoustique/Musique. More info at: http://www.ircam.fr/ 9 http://cic.puj.edu.co/wiki/doku.php?id=grupos:avispa:avispa

  In order to reach x as a barb then Q must perform ᾱ1 . . . ᾱn with internal actions, then ∃P 1 . . . P n s.t. P

	α 1 =⇒ P 1 . . .	αn =⇒ P n	β =⇒. Finally we can conclude that P	s.β

http://homepages.inf.ed.ac.uk/perdita/cwb/summary.html

http://www.it.uu.se/research/group/mobility/mwb

More info at: http://www.mozart-oz.org/

http://homepages.inf.ed.ac.uk/perdita/cwb/summary.html

http://www.it.uu.se/research/group/mobility/mwb

quasi-orders exclude the possibility of having infinite strictly decreasing sequences.

We also need a formal definition for (infinitely branching) transition systems. This can be given as follows. Here and in the following → + (resp. → * ) denotes the transitive (resp. the reflexive and transitive) closure of the relation →.

Definition 3.1.2 (Transition System). A transition system is a structure T S = (S, →), where S is a set of states and →⊆ S × S is a set of transitions. We define Succ(s) as the set {s ∈ S | s → s } of immediate successors of S. We say that TS is finitely branching if, for each s ∈ S, Succ(s) is finite. We also define P red(s) as the set {s ∈ S | s → s} of immediate predecessors of s, while P red * (s) denotes the set {s ∈ S | s → * s} (of predecessors of s).

The functions Succ, P red and P red * will be used also on sets by assuming that in this case they are defined by the point-wise extension of the above definitions. The key tool to decide several properties of computations is the notion of well-structured transition system. This is a transition systems equipped with a well-quasi-order on states which is (upward) compatible with the transition relation. Here we will use a strong version of compatibility, hence the following definition. Definition 3.1.3 (Well-structured transition system with strong compatibility). A well-structured transition system (WSTS) with strong compatibility is a transition system T S = (S, →), equipped with a quasi-order ≤ on S, such that the two following conditions hold:

1. ≤ is a well-quasi order; 2. ≤ is strongly (upward) compatible with →, that is, for all s 1 ≤ t 1 and all transitions s 1 → s 2 , there exists a state t 2 such that t 1 → t 2 and s 2 ≤ t 2 .

WSTS and CCS !

In [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] they prove that CCS ! is a well-structured transition system. We will use their notions for solving the reachability problem, thus we shall introduce most of the concepts behind. First, they define a well-quasi-order over CCS ! processes and this definition uses the following congruence: Definition 3.1.4. We define ≡ w as the least congruence relation satisfying the following axioms:

Then, they define a well-quasi-order over CCS ! processes. Intuitively P Q holds if Q can be obtained, up to ≡ w , from P by adding some parallel processes while preserving the nesting structure given by restrictions.

Definition 3.1.5. Let P, Q ∈ CCS ! . We write P Q iff there exist n, x 1 , . . . , x n , P , R, P 1 , . . . ,

Now we will present some definitions from [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF] relating well-structured transition systems and CCS ! . First, they need a notation for indicating all the sequential and bang subprocesses of a given process. They also define a special set of subprocesses using this notation. Definition 3.1.6. Let P ∈ CCS ! . The set Sub(P ) containing all the sequential and bang subprocesses of P is defined inductively as follows:

Sub(!P ) ={!P } ∪ Sub(P )

With P P,n they denote the set of all those CCS ! processes whose nesting level of restrictions is not greater than n and such that their sequential subprocesses, bang subprocesses and bound names are contained in the corresponding elements of P . More precisely they propose the following definition. Definition 3.1.7 (P P,n ). Let n be a natural number and P a process. We define P P,n as follows:

The above definition will be used in the solution of the reachability problem. The following proposition is important for relating the definition of WSTS and the barb decidability. Using these definitions, they prove that is a well-quasi-order.

Theorem 3.1.1. Let P ∈ CCS ! and n ≥ 0. The relation is a well-quasi-order over P P,n .

In order to prove that CCS ! is a WSTS, they also prove that is compatible with →.

Barb(P, x, y) as follows:

Barb(P, x, y) = true if P ∈ P red * (Now x (P red * (Now y (P )))); false otherwise .

From 3 we know that, given a process P ∈ CCS ! , then P

x and x ∈ fn(P ). Then we give a function for this purpose, given a process, an action, and a set of sequences, checks whether any of this resulting processes have the barbs x and β. Definition 3.2.2. Let P ∈ CCS ! , Σ a finite alphabet, α ∈ Σ, and S a set of sequences over Σ. We define the function Reach(P, β, S) as follows:

The above function allow us to provide a decision procedure for determining the reachability of an action in a process. We apply this function to the set of possible sequences that is related with the nesting restrictions. This set contains all the possible sequences (over the finite alphabet) with size less than the limit provided by 2. The following theorem relates our previous definition with the reachability problem.

Theorem 3.2.1. Let P ∈ CCS -!ν ! , Σ a finite alphabet, β ∈ Σ, and S a set of sequences over Σ. Then Reach(P, β, S) returns true iff there exists s ∈ S such that

x and x ∈ fn(P ). Now, from 2 we know that (in the best case) we can use n nested local names to get a delay of 2 n independent actions, then it is sufficient to check if (P | Q) ⇓ x⇓ β with sequences of size 2 |P |ν at most. By construction, all of these sequences are considered in S.

Next, we need to check for every sequence s ∈ S if (P | Q) ⇓ x⇓ β . Following the same process for checking barbs, the function Reach(P, β, S) check (for all s ∈ S) whether R def = P | Q has the barbs x and β. This is done by the function Barb(R, x, β), by checking if R belongs to the set P red * (Now x(P red * (Now β (P )))). We are able to compute this set since Now β (R) is upward-closed 3.1.3 and then it is possible to compute a (finite) pred-basis 3.1.2 for it and then checking if the original process is a predecessor of a process which can perform β. Using this result, we can Chapter 4

CCS ! Stepper

In this chapter we will present a small interpreter for CCS ! . It takes a process written in CCS ! as input and returns the possible evolution according to the operational semantics from 1.2 and 1.3. It has been implemented using the mozart programming system 1 employing the advantages of the records in Oz. We shall describe some implementation details about the interpreter and finally we shall show some examples. This work can be the start point for a CCS ! workbench like the Edinburgh Concurrency Workbench (CWB) 2 or the Mobility Workbench (MWB) 3 , where it is possible to specify systems in the calculus and verify certain properties, and then explore, from the practical point of view, the application of this formalism to real life.

Grammar and General Description

In this section we shall describe some implementation details about the CCS ! stepper. First we shall describe the grammar used, we have id , act and ccsProc . The id is an string with an initial letter and a (possible empty) of alphanumeric values, examples id : "a", "a45bjbj", "P1". The act is the action that we will use inside a process, from CCS ! we have that it could be an action, co-action or internal synchronization τ . We represent the co-action with the ∼ symbol in Oz, and with "$tau" the internal action.

Finally we have the ccsProc which represents a CCS ! process, zero is the null process 0; pre("a" zero) represents the process a.0; new("x" zero) is the process (νx)0; the ccsProc par(0 0) is the process 0 | 0 and finally rep(0) represents the process !0. Formally we have the grammar of figure 4.1.