Andrés Véjar -Frédéric

Chaxel -Jean-Yves Bron

Patrick Charpentier

Génération automatique de modèle de simulation par les données de localisation des produits

Keywords: Flux, Localisation, Produit, Géolocalisation, Simulation, Modélisation Flux, Location, Product, Geolocation, Simulation, Modeling

Le travail présenté dans ce papier vise, à partir d'un flux de données de localisation de produits dans un processus de production, à construire un modèle de simulation à événements discrets. La construction de ce modèle, via un «générateur» en ligne, s'appuie sur les trajectoires et l'identification des produits. Le modèle ainsi construit est capable de s'autoadapter aux évolutions du système réel.

ABSTRACT. This paper aims to build a discrete-event simulation model for production processes using a location data flux of products. The model building is carried out by an on-line generator and it is based on the identification of trajectoires and products. The resulting model presents a self-adaptive behavior to changes in the environment.

Introduction

La simulation est devenue un outil incontournable lors de l'évaluation des performances des systèmes de production manufacturier. Les étapes du processus conduisant à l'élaboration d'un modèle et à l'identification de ses paramètres (récolte des données, analyse comportementale, . . . ) sont encore très souvent réalisées par l'homme. Ces étapes constituent la plus grosse partie du temps dévolu à une simulation [START_REF] Willemain | Model Formulation : What Experts Think About and When[END_REF]. Pour tenter de raccourcir ces durées, quelques travaux ont proposé une automatisation de certaines des étapes, comme par exemple [START_REF] Guru | A Template-Based Conceptual Modeling Infrastructure for Simulation of Physical Security Systems[END_REF][START_REF] Zhou | What Can Be Done to Automate Conceptual Simulation Modeling[END_REF][START_REF] Jun Son | Automatic Generation of Simulation Models From Neutral Libraries : An Example[END_REF]. Nous proposons pour notre part une approche utilisant les données de localisation des produits en cours de transformation, pour construire automatiquement, et en temps réel, un modèle de simulation de flux. Les produits sont donc ici considérés comme des objets immergés dans un système de production, aptes à fournir en tout lieu, en cas de besoin, des informations diverses, dans notre cas, des informations de localisation et d'identité. On parlera de systèmes ambiants pour le produit.

Système Décisionnel

Système

Réel Générateur Modèle de Simulation

Figure 1. Le «générateur» dans son environnement

Ce modèle, de type réseau de file d'attente, est capable de s'auto-adapter aux modifications du système réel. En effet, un flux permanent de données issues du système réel, permet une mise à jour du modèle en cas d'évolution. Le modèle ainsi obtenu peut, de part sa nature, être utilisé pour améliorer le fonctionnement du système (réengineering) ou pour contrôler le système (exploitation). Un générateur de code de simulation, visant à prouver la faisabilité de la démarche a été développé en Python [START_REF] Rossum | Python reference manual[END_REF][START_REF] Downey | How to Think Like a Computer Scientist : Learning with Python[END_REF][START_REF] Cai | On the performance of the Python programming language for serial and parallel scientific computations[END_REF] avec l'aide du package SimPy [START_REF] Muller | SimPy : Simulating Systems in Python[END_REF][START_REF] Muller | Advanced systems simulation capabilities in SimPy[END_REF]Bahouth et al., 2007). Quelques tests ont été réalisés, et il s'avère que les comportements des systèmes réels et des modèles de simulation obtenus par le biais de ce générateur sont très proches.

Contexte

Depuis quelques années maintenant, de nouvelles visions du produit manufacturé tendent à lui conférer des capacités de communication et des capacités sensitives dans le cadre du paradigme de produit intelligent [START_REF] Karkkainen | Intelligent products -a step towards a more effective project delivery chain[END_REF]. La part informationnelle liée à chaque produit est donc alimentée soit par l'environnement matériel direct du produit physique ou soit par le biais de sa propre instrumentation (MEMS, GPS, . . . ). Les échanges informationnels entre le produit et son environnement peuvent s'effectuer :

1) À certains points de synchronisation (emplacements des lecteurs R/W, technologies RFID, code-barre, . . . ).

2) De façon quasi-continue (réseaux sans fil de type Wifi, Zigbee, Bluetooth, . . . ).

Ces technologies de communication peuvent elles même contribuer à la localisation du produit dans son environnement en complément à l'instrumentation embarquée. Elles font l'objet de nombreux travaux de recherches visant a définir et/ou améliorer les architectures, les services, les communications, . . . , des systèmes de géolocalisation [START_REF] Wan | An OLAP system for networkconstrained moving objects[END_REF]ALRahmawy and Wellings, 2007;[START_REF] Xu | Adaptive location constraint processing[END_REF][START_REF] Satoh | A location model for smart environments[END_REF][START_REF] Coronato | A Semantic Location Service for Pervasive Grids[END_REF][START_REF] Goßmann | Location Models for Augmented Environments[END_REF]. De nombreux et divers domaines applicatifs et/ou scientifiques utilisent des informations de localisation. Sans être exhaustif, on peut entre autre citer les applications géographiques cherchent à mettre en relation les variables spatiales et temporelles d'un territoire donné, [START_REF] Church | Geographical information systems and location science[END_REF][START_REF] Quiroga | Performance measures and data requirements for congestion management systems[END_REF][START_REF] De Oliveira | Production and analysis of coordination plans using a geographic information system[END_REF]Bonnifait et al., 2007). On peut également citer les applications en architecture, qui visent à la numérisation de bâtiments existants [START_REF] Chen | Object Finding System Based on RFID Technology[END_REF][START_REF] Caron | Locating sensor nodes on construction projects[END_REF][START_REF] Song | A proximity-based method for locating RFID tagged objects[END_REF]. Enfin, un des domaines les plus en avance dans l'utilisation des données de localisation est sans doute celui de la robotique mobile visant à la localisation des robots et à la cartographie de leur environnement (Begum et al., 2008;[START_REF] Gechter | A reactive agent-based problem-solving model : Application to localization and tracking[END_REF][START_REF] Paulo Moreira | Vision Based Real-Time Localization of Multiple Mobile Robots[END_REF]Borges and Aidon, 2001;[START_REF] Herianto | Artificial Pheromone System Using RFID for Navigation of Autonomous Robots[END_REF].

Les applications dans le domaine de la production et logistique de ces technologies sont également nombreuses [START_REF] Qiu | RFID-enabled automation in support of factory integration[END_REF][START_REF] Kim | Forwardbackward analysis of RFID-enabled supply chain using fuzzy cognitive map and genetic algorithm[END_REF][START_REF] Harry | A dynamic logistics process knowledge-based system -An RFID multi-agent approach[END_REF][START_REF] Kim | Value analysis of location-enabled radio-frequency identification information on delivery chain performance[END_REF]. La traçabilité des produits, l'inventaire des stocks produits, la géolocalisation d'une flotte de transport n'en sont que quelques exemples. Il semble qu'à l'heure actuelle le positionnement spatial d'objets physiques se limite à des objets « volumineux » (camions, bateaux,...) ou à des personnes.

Notre travail de recherche consiste à montrer les apports, sur le contrôle et les performances d'un système manufacturier, d'un flux d'information de localisation de produits durant leur élaboration. Ce papier présente ici un cas d'application possible : la génération automatique de code de simulation de flux sur la base des données de localisation des produits, durant leur passage sur le système de production. Ces données constituent un flux d'information pouvant être assimilé à la trace des produits. Depuis quelques années, la simulation de flux est devenue incontournable pour l'évaluation de la dynamique des systèmes manufacturiers, [START_REF] Cassandras | Introduction to Discrete Events Systems[END_REF][START_REF] Park | A On-line Simulation Approach to Search Efficient Values of Decision Variables in Stochastic Systems[END_REF]. En effet, les modèles de simulation de flux sont utilisés pour dimensionner un système en phase de conception, pour améliorer son fonctionnement en phase de ré-engineering, et anticiper un comportement en phase d'exploitation [START_REF] Mirdamadi | Discrete Event Simulation-Based Real-Time Shop Floor Control[END_REF]. Malgré tout, il n'en demeure pas moins que les phases de modélisation, puis de maintenance, de ces modèles restent des opérations délicates et chronophages, [START_REF] De Vin | Simulation-Based Decision Support for Maunufacturing System Life Cycle Management[END_REF][START_REF] Mittal | DEVS-Based Dynamic Model Reconfiguration and Simulation Control in the Enhanced DoDAF Design Process[END_REF][START_REF] De Vin | Information Fusion for Simulation Based Decision Support in Manufacturing[END_REF], et ce quel qu'en soit le type d'application visée. Ces raisons expliquent, à elles seules, le choix de nous intéresser à cette problématique. Le type de modèle auquel nous aboutissons par le générateur proposé doit permettre son utilisation ou en phase de ré-engineering ou en phase d'exploitation. L'intérêt de notre proposition est d'autant plus important que la complexité et la dynamique du système réel à modéliser est grande. L'idée est de remplacer la plus grosse partie des interventions des experts humains lors de la construction du modèle, mais également lors des phases de maintenance ou de reconfiguration, par un générateur automatique. La figure 1 en montre très schématiquement le principe. Le générateur est alimenté par un flux de données en provenance du système réel.

Hypothèses & Problématique

Hypothèses de départ

L'hypothèse principale de ce travail est de considérer que tous les objets élémentaires d'un système de production manufacturier peuvent être localisés. On suppose ainsi qu'il existe une technologie capable de fournir un flux de localisation de tous les objets en mouvement dans le système considéré. Nous parlerons dans notre cas de localisation plutôt que de géolocalisation de part la nature et l'échelle du système étudié, l'échelle considérée se limitant à la taille d'un atelier de production. D'autres hypothèses viennent naturellement compléter cette hypothèse principale. En effet, les données observées seront considérées dans ce travail comme fiables et non entachées d'erreur, notre idée étant ici de poser les principes de la méthode proposée le plus simplement possible (la prise en compte des erreurs fera l'objet d'autres travaux et présentations). De plus, l'obtention des données de localisation se fait naturellement par l'intermédiaire de capteurs, embarqués ou non sur les produits, qui via un système de communication alimentent un système de gestion de l'information (figure 2). Les données de localisation sont, comme d'autres grandeurs physiques, issues de l'environnement des produits en circulation : le système manufacturier. L'accès aux données de localisation doit pouvoir être considéré comme possible en tous les endroits du système et à chaque moment, c'est pourquoi le système doit être un système pervasif. Dans notre cas on peut imaginer que les données sont collectées de manière événementielle, ou de manière discrète (cela dépend de la technologie employée). Dans ce dernier cas, si la fréquence d'acquisition est très élevée, le flux d'information de localisation peut être considéré comme quasi-continu. Enfin, on considérera qu'un identifiant unique est assigné a priori à chacun des produits-objets élémentaires manipulés à un moment ou à un autre par le système de production.

Formalisation du problème

L'information de localisation accessible est définie par le 3-tuple (I, R, T ) où I est l'ensemble des identifiants des objets. Un identifiant est assigné à chacun des objets 1 de façon unique.

Soit I l'ensemble discret des identifiants de chaque objet composant un produit, R l'ensemble des positions ( par exemple r = (x, y), r ∈ R ⊂ R 2 ) , et T l'ensemble des dates. Le passage d'un objet dans l'atelier (ou processus productif) est associé à un parcours défini par un ensemble de paires position-temps pour cet objet. Si l'objet est possesseur d'un identifiant i ∈ I, chaque donnée de localisation est définie comme (i, r, t), r ∈ R, t ∈ T . Le flux de données de localisation D ⊂ I × R × T est l'information de parcours de tous les objets :

D = {d k } ∞ k=1 = {(i k , r k , t k ) : t k+1 ≥ t k , k ∈ N} (1)
Chaque (i, r, t), est un élément dans le flux D. Cette information est la seule qui sera utilisée pour la génération du code de simulation. Notre problème consiste à concevoir un générateur de modèle de simulation en ligne Φ, capable d'élaborer un modèle m à partir d'un flux de données réelles D.

m 0 = ∅ m k = Φ(d k , m k-1 )
(2)

Trajectoires et flux de données : modélisation

Durant leur passage dans le système manufacturier, les objets suivent des trajectoires dans le plan (x, y). L'observation de ces trajectoires dans le temps nous permet de déterminer la vitesse v de l'objet. A chaque point où v = 0 est possible associer un comportement de type file d'attente. En chacun de ces points deux types d'événements peuvent se produire : l'arrivée ou le départ d'objet(s). Comme la composition d'un produit ne peut être connue qu'à la sortie de cette file d'attente, les objets constituants le produit suivent alors forcément la même trajectoire.

A chaque point où v = 0, nous allons associer un comportement de type file d'attente. Nous définissons alors (figure 4) :

e 1 l'instant d'arrivée du premier objet constituant le produit.

e 2 l'instant d'arrivée du dernier objet constituant le produit.

s est l'instant commun de sortie de tout les objets constituants le produit. -O, la durée entre l'arrivée du premier objet et l'arrivée du dernier objet nécessaire à la constitution du produit.

-A, le temps d'attente du service : durée définie entre le moment où toutes les pièces nécessaires à la constitution du produit sont arrivées et le moment réel de passage.

-T , le temps de service au point v = 0.

-T T ot , le temps total d'arrêt au point v = 0.

On peut lier ces différentes variables par l'équation :

T T ot = O + A + T (3)
Pour calculer A il est nécessaire de connaître le temps de sortie du produit précédent s k-1 où k -1 représente l'ordre de sortie du produit. La règle de calcul de A est : si e k 2 < s k-1 alors le temps d'attente est s k-1e k 2 , sinon le temps d'attente est 0. De manière plus formelle et en utilisant la fonction d'Heaviside :

θ(y) = 1 si y ≥ 0 0 si y < 0, (4)
nous pouvons maintenant définir à chaque k ième sortie d'un produit les variables introduites jusqu'à présent :

y k = e k 2 -s k-1 α k = θ(y k ) β k = 1 -α k T k = α k (s k -e k 2 ) + β k (s k -s k-1 ) A k = β k (s k-1 -e k 2 ) O k = e k 2 -e k 1 (5)
à la condition où s 0 = 0. Le 3-tuple (T, A, O) possède toute l'information nécessaire à la caractérisation du point v = 0 comme point de service. Il nous faut noter que l'analyse présentée ici n'est valide qu'à la condition théorique où la file d'attente se réduit à un seul point (tout les objets attendent au même point). De plus, il nous est impossible en l'état, sur la base des informations récoltées, de déterminer un comportement détaillé au niveau des files d'attentes (type de règles de gestion, préemption, ...), ou de discriminer la panne d'un «serveur» d'un autre état d'attente. Le modèle n'est que le reflet des informations qui ont servies à le construire, avec le point de vue du produit : celui-ci ne sait si la machine est en panne ou dans un autre état.

Algorithme

L'algorithme proposé ici correspond naturellement au générateur de code de simulation. Il est composé de trois parties principales. La première partie génère les positions des machines et les chemins suivis par les produits, sur la base des flux de données temps réel qui l'alimentent. La seconde partie traite la problématique de sortie des produits du système. La sortie des produits est en effet le moment où il est possible de savoir si oui ou non ce produit existait ou pas. S'il existait on met à jour ses données, sinon on le créer. La troisième partie sert à modéliser les lois de comportement pour le modèle ainsi généré. Des lois statistiques sont proposées pour représenter les temps d'inter-arrivées et de services pour chaque type de produit et chaque machine. L'algorithme lié à cette première partie est déclenché à chaque modification du flux. ⊲ Les distributions end procedure L'algorithme lié à cette deuxième partie est déclenché à chaque sortie de produit du système. Savoir si un produit sort du système peut être en soi un problème difficile à résoudre. Nous avons fait le choix de considérer un produit comme sorti du système si les données avec l'identifiant i n'apparaissent plus dans le flux pendant une durée considérée (choisie arbitrairement mais suffisamment importante). Il faut être capable de retrouver la composition du produit final à la sortie (ses composés). A ce niveau nous utilisons les matrices d'adjacence liées à chaque produit élémentaire La troisième partie consiste à caractériser le comportement stochastique des différents points d'arrêt. Cette troisième et dernière phase est une phase de post-traitement de l'ensemble des informations collectées en phase 1 et 2. Une estimation de la fonction de densité de probabilité pour les temps d'inter-arrivées et les temps de services est menée. Elle est ensuite validée par un test de Wilcoxon [START_REF] Wilcoxon | Individual Comparisons by Ranking Methods[END_REF]. Nous présentons (cf. algorithme 3) un fragment de l'algorithme développé dans sa version simplifiée. Ce fragment permet de collecter les positions des points d'arrêts pour chaque produit, leurs temps d'inter-arrivées et leurs temps de service à chaque point d'arrêt. Dans l'algorithme présenté une donnée (i, r, t) est définie par la structure d, où d.i est l'identifiant, d.r la position (x, y) et d.t l'instant. Les autres structures de données utilisées sont m et p. La structure m, est définie dans (cf. tableau 1), et la fonction pour la créer est m(r, t). La structure p est définie dans (cf. tableau 1). Elle est créée par la fonction p(i, m). En plus des structures d, m, p, il existe deux ensembles globaux, M , et P , vides par défaut.

Application

Cette partie à vocation à valider le principe de faisabilité de la génération automatique d'un code de simulation sur la base d'informations de localisation. Nous avons donc dans un premier temps généré un module de simulation avec SimPy (Simulation in Python) [START_REF] Muller | Advanced systems simulation capabilities in SimPy[END_REF]; [START_REF] Muller | SimPy : Simulating Systems in Python[END_REF]; Bahouth et al. (2007). Celui-ci nous génère le flux de localisation des produits. Il fait office d'artefact du système réel. Nous nous limitons ici volontairement à un cas simple pour limiter le volume imparti à sa présentation et à l'analyse des résultats dans le cadre de ce papier. Le flux de localisation est ensuite récupéré par le module générateur de modèle de simulation qui met en oeuvre les phases 1 et 2 vues précédemment. Enfin, un module d'analyse des données (phase 3) permet de vérifier les résultats obtenus. Tout les modules sont programmés avec le langage Python [START_REF] Rossum | Python reference manual[END_REF]; [START_REF] Downey | How to Think Like a Computer Scientist : Learning with Python[END_REF]; [START_REF] Cai | On the performance of the Python programming language for serial and parallel scientific computations[END_REF].

Présentation du cas d'application choisi

L'atelier modélise ici est composé de différentes machines entre lesquelles les produits évoluent, transportés par des AGV's. Les différents types de produits sont générés pour la formule :

mach(s, l) = (s -l) mod M (6)
l : le type de produit, l = 0, . . . , L -1, -s : l'opérations dans la gamme, s = 0, . . . , S -1, -M : nombre de machines ou poste de travail, basée sur la formulation initiale proposée par [START_REF] Thiesse | On the value of location information to lot scheduling in complex manufacturing processes[END_REF]. La formule ainsi proposée permet de générer des séquences de transformation (les gammes) pour chacun des produits.

-Les temps d'inter-arrivées des produits dans l'atelier sont fournis par une fonction de distribution exponentielle. Une proportion identique de chaque type de produit est générée.

-Les temps de service de chaque machine sont également fournis par une fonction de distribution exponentielle.

-La disposition des machines dans le système est réalisée de manière aléatoire en début de simulation, dans un cadre également figé (dimensions du système).

-Le système de localisation permet d'obtenir l'information de localisation du produit (i, r, t) avec une fréquence fixe.

Les paramètres utilisées dans la simulation sont présentés dans (cf. tableau 2).

Tableau 2. Conditions expérimentales

Paramètres Valeurs nombre de types de produits 3 nombre de machines 3 nombre d'opérations ou phases 3 quantité de produits 100 temps d'inter-arrivées exponentiel, µ = 1/3 temps de service sur machines exponentiel, µ = 13 nombre d'AGV's 10 vitesse des AGV's 0.44 dimensions de l'atelier (-10, -10), (10, 10) période d'échantillonnage 0.5 pour la localisation

Résultats

Les résultats fournis par le modèle issu du générateur de code sont tout a fait cohérents avec ceux issus de l'artefact du système réel. En effet le test de Wilcoxon, montre que les données, concernant les temps d'inter-arrivées et les temps de service générées par les deux modèles sont distribuées selon la même loi statistique (cf. tableau 3). Les produits et leurs gammes sont intégralement identifiés par le générateur de code. Celui-ci positionne également de manière précise les différentes ressources mises en oeuvre pour l'élaboration des produits. Ces premiers résultats montrent la faisabilité de la méthode proposée. Ils ont été confirmés par des tests effectués sur des systèmes de taille plus importante (jusqu'à 15 machines, 15 opérations ou phases, 15 types de produits).

Conclusions

Les résultats obtenus valident la démarche mise en oeuvre ainsi que l'outil que nous avons développé. Le «générateur» tel qu'il a été conçu possède des avantages liés à la réalisation du modèle de manière automatique et en ligne :

-réduction globale du temps de modélisation par la réduction du temps de collecte de données, de génération du modéle et de sa maintenance.

-fiabilisation du modèle obtenu par la réduction de l'intervention humaine dans le processus.

Nous développons actuellement une autre version du «générateur» qui tienne compte des imprécisions de mesure de localisation, ainsi que des variations de la période d'échantillonnage. Une fois développé, cette version du «générateur» pourra alors être confrontée à une validation en aveugle sur un système réel. De manière encore plus large, nous réflechissons actuellement à l'ouverture à d'autres types d'application (hors manufacturing), du même concept.

Figure 2 .

 2 Figure 2. Obtention du flux de localisation

Figure 3 .

 3 Figure 3. Système de construction du modèle de simulation

Figure 4 .

 4 Figure 4. Temps dans un point v = 0 avec congestion

Tableau 1 .

 1 Structures de données m et p var description défaut m.r position (x, y) none mstructure de type m none p.M ensemble ordonné de structures m ∅

  A chaque nouvelle donnée (i, r, t) un nouveau produit est créé si son identifiant est nouveau. A chaque arrêt de ce produit est créé un «point d'arrêt» (point de localisation d'une file d'attente et/ou point de service), et un lien entre produit et «point d'arrêt». Ce «point d'arrêt» est validé si la position du produit i est la même entre deux instant d'observations t et t s , le point correspond à une réelle attente du produit. Dans ce cas les temps d'entrée et de sortie du produit i sur le point d'arrêt localisé en r sont conservés. Ils servent ensuite à la modélisation du comportement dynamique du type de produit en ce point.

	Algorithme 1 Génération du Layout
	procedure LAYOUT(D)
	S ← SERVEURS(D)	⊲ Points de vitesse nulle avec récurrence
	A ← PARCOURS(D)	⊲ Les arcs entre points
	P ← PRODUITS(A, S)	⊲ C'est un graphe p j = (arcs, points)
	L ← CREERLAYOUT(A, S, P )	⊲ C'est l'union de tous les
		⊲ graphes de produits L = ∪ j p j
	return L	⊲ Le layout
	end procedure
	Algorithme 2 Génération des Distributions
	procedure DISTRIBUTIONS(D, L)
	T ← DISTRTYPES(D, L)	⊲ Identifier la distribution d'entrée de
	⊲ chaque type de produit pour chaque serveur
	(t i , t s ) ← DISTRTEMPS(D, L)	⊲ Identifier la distribution de temps
		⊲ d'inter-arrivées, et de temps de service
	⊲ pour chaque serveur et pour chaque produit
	return (T, t i , t s )

  Tableau 3. Test de Wilcoxon temps inter-arrivées et de service

	Produit		T inter-arrivées			T de service
		opération	0	1	2	0	1	2
	0	t-statistic 168.5	138.0 131.0 220.0	187.0	185.5
		two-tailed	0.7	0.0	0.0	0.8	0.35	0.3
		p-value
		opération	0	1	2	0	1	2
	1	t-statistic	96.0	5.0 124.0 154.0	175.0	166.0
		two-tailed	0.49	0.0	0.0	0.07	0.15	0.17
		p-value
		opération	0	1	2	0	1	2
	2	t-statistic 240.5	195.5 192.5 261.0	270.0	309.0
		two-tailed	0.73	0.0	0.0	0.07	0.09	0.37
		p-value

  T srv real T srv generated kde-g T srv real kde-g T srv gen Figure 5. Distributions des temps inter-arrivées (première file) et des temps de service (deuxième file) Références Mohammed ALRahmawy and Andy Wellings. A model for real time mobility based on the RTSJ. In JTRES '07 : Proceedings of the 5th international workshop on Java technologies for real-time and embedded systems, pages 155-164, New York, NY, USA, 2007. ACM Press. ISBN 978-59593-813-8. Alex Bahouth, Steven Crites, Norman Matloff, and Todd Williamson. Revisiting the Issue of Performance Enhancement of Discrete Event Simulation Software. In 40th Annual Simulation Symposium (ANSS'07), volume 0, pages 114-122, Los Alamitos, CA, USA, 2007. IEEE Computer Society. Momotaz Begum, George K.I. Mann, and Raymond G. Gosin. Integrated fuzzy logic and genetic algorithmic approach for simultaneous localization and mapping of mobile robots. Applied Soft Computing, 2008. Philippe Bonnifait, Maged Jabbour, and Gérald Dherbomez. Real-Time Implementation of a GIS-Based Localization System for Intelligent Vehicles. EURASIP Journal on Embedded Systems, 2007, 2007.

représenté par son identifiant. La somme des matrices d'adjacence de chacun des produits élémentaires sortant au même lieu et eu même moment, permet l'obtention de la composition du produit. L'algorithme compare cette somme des matrices avec celles obtenues précédemment. Si cette matrice n'existe pas encore, cela signifie qu'un nouveau produit est sorti du système. On lui relie alors les informations sur ses points de service (ou d'arrêt) obtenus pendant le parcours de ses différents composants dans l'atelier.


Emmanuel Beffara

Functions as proofs as processes

This paper presents a logical approach to the translation of functional calculi into concurrent process calculi. The starting point is a type system for the π-calculus closely related to linear logic. Decompositions of intuitionistic and classical logics into this system provide type-preserving translations of the λ-and λµ-calculus, both for call-by-name and call-by-value evaluation strategies. Previously known encodings of the λ-calculus are shown to correspond to particular cases of this logical embedding. The realisability interpretation of types in the π-calculus provides systematic soundness arguments for these translations and allows for the definition of type-safe extensions of functional calculi.

Introduction

The π-calculus was introduced in the late 1980's as a core model of concurrent computation, in the same way as the λ-calculus is a core model of functional computation. Soon afterwards, Milner showed in the seminal paper Functions as processes [START_REF] Milner | Functions as processes[END_REF] that the λ-calculus could be precisely encoded into the π-calculus. Around the same time, Girard introduced linear logic as a logic to study fine properties of denotational models of intuitionistic logic. Indeed the ideas behind it led to significant insights on the structure and semantics of the λ-calculus and functional computation, along the lines of the functions as proofs slogan. It might not be a coincidence that these two contributions appeared at the same time, and intuitions from one have been seen in the other from the beginning. Formal connections appeared some years later, giving formal ground to the proofs as processes idea, in particular in work by Abramsky [START_REF] Abramsky | Computational interpretations of linear logic[END_REF][START_REF] Abramsky | Proofs as processes[END_REF] and in a notable contribution by Bellin and Scott as an encoding of proof nets in the π-calculus [START_REF] Bellin | On the π-calculus and linear logic[END_REF].

The purpose of this paper is to present a formal way to make these pieces fit together. We use a recent version of the proofs-as-processes approach [START_REF] Beffara | A concurrent model for linear logic[END_REF][START_REF] Beffara | réalisabilité et concurrence[END_REF] as a way to make a link between a form of π-calculus (with more symmetry and expressiveness) and a form of linear logic (with the significant difference that formulas have arities). In this framework, we adapt previous work by Danos, Joinet and Schellinx on the translation of classical logic into linear logic [START_REF] Vincent Danos | Lkq and lkt: Sequent calculi for second order logic based upon linear decomposition of classical implication[END_REF][START_REF] Vincent Danos | A new deconstructive logic: linear logic[END_REF]. We show that, when considering each logic as a type system, we can extract a family of typed translations of the λ-and λµ-calculi into the π-calculus. The now familiar duality [START_REF] Curien | The duality of computation[END_REF] between call-by-name and call-by-value appears clearly in our system, moreover several previously known translations are shown to fit in as particular instances of the general technique.

Our type system for the π-calculus was developed by realisability as a logic of behaviours of concurrent processes. We show that this realisability construction can be used to prove properties of the considered execution models of the λ-calculus. We also argue that realisability provides a way to introduce new constructs in functional calculi while keeping the type system semantically correct.

Parallel composition and scoping: 2 Framework

p | q ≡ q | p (p | q) | r ≡ p | (q | r) p | 1 ≡ p (νx)(

The calculus

The concurrent calculus we use, hereafter named π = -calculus, is a formulation of π-calculus with explicit fusions (à la Gardner and Wischik [START_REF] Gardner | Explicit fusions[END_REF]) with binding input and output. We assume an infinite set N of names, ranged over by the letters u, v, x, y, z. The calculus is generated by the following grammar: actions:

α ::= u(x 1 . . . x n ) input ū(x 1 . . . x n )
binding output processes: p, q ::= α.p, !α.p linear action, guarded replication 1, p | q, (νx)p inaction, parallel composition, hiding

x=y name unification
The operational semantics of the calculus is defined as a reduction relation up to structural congruence, with the rules in table 1. The reduction relation is the smallest relation → that is closed under structural congruence, parallel composition and hiding and that contains u( x).p | ū( x).q → (ν x)(p | q). We consider a strong bisimilarity relation ∼ = whose precise definition (that can be found in the appendix) uses a labelled transition system. The point is that ∼ = is a congruent equivalence such that p ∼ = q implies that for each reduction p → p ′ there is a reduction q → q ′ with p ′ ∼ = q ′ . We use this calculus instead of a more standard form of π-calculus because it provides a clear distinction between synchronisation and name substitution. It also allows a cleaner type system. By combining binding actions and equators, we get usual non-binding actions with their usual semantics, by defining

ū x 1 . . . x n := ū(y 1 . . . y n ).(x 1 =y 1 | . . . | x n =y n )

The type system: linear logic with arities

We assume a set V of type variables, ranged over by X or Y . The language of formulas is generated by the following grammar: The dual (or linear negation) is the involution (•) ⊥ defined as X ⊥⊥ := X and

A, B ::= X | X ⊥ | A ⊗ B | A `B | ´A | ˆA | !A | ?A | ∃X.A | ∀X.A
(A ⊗ B) ⊥ := A ⊥ `B⊥ (´A) ⊥ := ˆ(A ⊥ ) (∀X.A) ⊥ := ∃X.(A ⊥ ) (!A) ⊥ := ?(A ⊥ )
A type Γ is a sequence x 1 : A 1 , . . . , x n : A n where each A i is a formula and each x i is a sequence of names of length ar(A i ). All the names occurring in all the x i must be distinct.

ˆΓ denotes a sequent where all formulas have the form ˆA or ?A, and ?Γ denotes a sequent where all formulas have the form ?A. A typing judgement is written p ⊢ Γ, where p is a process and Γ is a type. A process p has type Γ if p ⊢ Γ is derivable by the rules of table 2.

We call LLa (for linear logic with arities) this logical system. The inference rules are those of multiplicative-exponential linear logic (MELL), extended with the linear modalities ˆand ´. The main difference is in the rule for the existential quantifier: ∃X.A can be deduced from A[B/X] only when X and B have the same arity. As a consequence, although the language of MELL is a subset of our language of types, provability of a sequent Γ in MELL is not equivalent to provability of Γ in LLa.

Second-order λµ-calculus

Our model of functional computation is the λµ-calculus [START_REF] Parigot | λµ-calculus: an algorithmic interpretation of classical natural deduction[END_REF]. We assume an infinite set of λvariables ranged over by x, y and an infinite set of µ-variables ranged over by α, β. Terms are generated by the following grammar:

M, N ::= x | λx.M | (M )N | µα[β]M
Thus we consider the version of the calculus where µα and [β] cannot appear separately. The language of types is minimal second-order logic, i.e.

A, B ::= X | A → B | ∀X.A

A typing judgement has the form Γ ⊢ M : A | ∆ where Γ is a sequence of type assignments x : A for distinct λ-variables and ∆ is a sequence of type assignments α : A for distinct µ-variables. The typing rules are given in table 3. The intuitionistic fragment, i.e. system F, is the fragment of this calculus where µα[β] is never used and where the ∆ part is always empty.

Simply typed λ-calculus and head linear reduction

The basis of linear logic is the decomposition of intuitionistic implication A → B into an linear implication and an exponential modality, as !A ⊸ B. The idea is that linear implication A ⊸ B = A ⊥ `B is the actual implication, while the modalities !A and ?A control weakening and contraction. In this section, we describe the operational meaning of this embedding.

Axiom and cut:

u 1 =v 1 | . . . | u k =v k ⊢ u : X ⊥ , v : X p ⊢ Γ, x : A q ⊢ x : A ⊥ , ∆ (ν x)(p | q) ⊢ Γ, ∆ Multiplicatives: p ⊢ Γ, x : A q ⊢ ∆, y : B p | q ⊢ Γ, ∆, x y : A ⊗ B p ⊢ Γ, x : A, y : B p ⊢ Γ, x y : A `B
Actions:

p ⊢ Γ, x : A ū( x).p ⊢ Γ, u : ˆA p ⊢ Γ, x : A ū( x).p ⊢ Γ, u : ?A p ⊢ ˆΓ, x : A u( x).p ⊢ ˆΓ, u : ´A p ⊢ ?Γ, x : A !u( x).p ⊢ ?Γ, u : !A
Exchange, contraction and weakening:

p ⊢ Γ, x : A, y : B, ∆ p ⊢ Γ, y : B, x : A, ∆ p ⊢ Γ, u : ?A, v : ?A p[w/u, v] ⊢ Γ, w : ?A p ⊢ Γ p ⊢ Γ, u : ?A Quantifiers: p ⊢ Γ, x : A X / ∈ fv(Γ) p ⊢ Γ, x : ∀X.A
Definition. Let LJ 0 be the language of formulas generated by variables and → as the only connective. The translation A 0 of a formula A is defined as

X 0 := X (A → B) 0 := !A 0 ⊸ B 0
where each variable of LJ 0 is mapped to a variable of arity 1 in LLa.

Here propositional variables are considered as base types of arity 1. A functional type A 1 → • • • → A n → X is thus translated into a formula of arity n + 1. The translation of formulas naturally induces a translation of type derivations.

Definition. The translation of a simply typed λ-term M at type A on channels y (with | y| = ar(A 0 )) is the process M A y defined as

x A y := x y λx.M A→B x y := M B y (M )N B y := (νx)( M A→B x y | !x( z). N A z)
The soundness and faithfulness of this translation are easily checked:

Proposition. A judgement x 1 : A 1 , . . . , x n : A n ⊢ M : B is derivable in LJ 0 if and only if M B y ⊢ x 1 : ?(A 0 1 ) ⊥ , . . . , x n : ?(A 0 n ) ⊥ , y : B 0 is derivable in LLa.
Let us now study the operational meaning of the translation. Remark that, up to structural congruence, redexes can be permuted without affecting the translation, i.e. the translation captures σ-equivalence [START_REF] Regnier | Une équivalence sur les λ-termes[END_REF]. Subsequently, we get that τ -transitions in the translations correspond to what is known as head linear reduction [START_REF] Danos | How abstract machines implement head linear reduction[END_REF]. We briefly recall the definition of these two notions:

Definition. σ-
M i . Thus we have A = A 1 . . . A k → B and x has type C 1 . . . C p → B.
Then we have

M A x z = (ν y u) x u z p i=1 u i = M i Ci n j=1 y j = N j Bj with x = T A := !x( y). T A y.
The only possible reduction in this process is x u z interacting with one of the u i = M i Ci or y j = N j Bj . By construction x cannot be one of the u i , so M A x z has a τ -transition if and only if x = y j for some j. In this case, we can remark that the following reduction holds:

ȳj u z | y j = N j Bj → N j Bj u z | y j = N j Bj
Putting this reduction in context, we get that the reduct of M A x z, up to structural congruence, is λ x.(λ y.(N j ) M ) N A x z. Therefore, τ -transitions in translations of λ-terms strictly correspond to head linear reductions in the terms.

Interestingly, this translation was first described by Hyland and Ong as a syntax for strategies in a game semantics of PCF [START_REF] Hyland | Pi-calculus, dialogue games and pcf[END_REF], thus with different (but clearly related) arguments.

System F and modal translations

The translation presented above is remarkably light. However, the arity of the translation of a term depends on its type, and as a consequence polymorphism in the style of system F does not hold. Modal translations [START_REF] Vincent Danos | Lkq and lkt: Sequent calculi for second order logic based upon linear decomposition of classical implication[END_REF] are a generalisation of the standard embedding of intuitionistic logic into linear logic, which allow full polymorphism by providing a type-independent (and type-safe) translation.

6 Definition. A generalised modality is a word γ over {ˆ, ´, ?, !}. The dual of γ is the modality γ such that (γX) ⊥ = γX ⊥ . A modal translation of LK into LLa is defined by a pair (γ, δ) of generalised modalities. The translation A * of a formula A is defined as

X * := X (A → B) * := γ(A * ) ⊸ δ(B * ) (∀X.A) * := ∀X.(A * )
where each variable of LK is mapped to a variable of arity 2 in LLa. For Γ = {x i :

A i } 1 i n , define Γ * := {x i : A * i } i and Γ * ⊥ := {x i : (A * i ) ⊥ } i . For a generalised modality γ, define γΓ := {x i : γA i } i . A type Γ ⊢ A | ∆ is translated at a channel u into the type γΓ * ⊥ , u : δA * , δ∆ * . A modal translation (γ, δ) is valid if Γ ⊢ A | ∆ holds if and only if ⊢ LLa γΓ * ⊥ , δA * , δ∆ * holds.
An important fact needs to be stressed: in the source language LK, any variable can be substituted by any formula. On the other hand, in the target language LLa, a variable can only be substituted by a formula of the same arity. Note that a translation commutes with substitution, i.e. (A[B/X]) * = A * [B * /X], if and only if variables are preserved, therefore any translation must assign sensible arities to variables. For this substitution to be correct in any case, we must ensure that the arity of A * is independent from A. This condition is satisfied if and only if neither γ nor δ is empty, and then ar(A * ) = 2 for any A.

General translation

7 Definition. Given a non-empty generalised modality γ and names u and x, define the protocol γu( x).p as ´u( x).p := u( x).p, ˆu( x).p := ?u( x).p := ū( x).p, and inductively γ †u( x).p := γu(v). †v( x).p for a fresh name v. In the case of the empty modality ε, let εu(x).p := p[u/x], and εu( x).p is undefined for | x| = 1. Note that protocols are typed in the expected way: p ⊢ Γ, x : A implies γu( x).p ⊢ Γ, u : γA. If γ contains ! then the context must be ?Γ, else if γ contains ´then the context must be ˆΓ. For a modal translation (γ, δ) to be valid for classical logic, essentially two conditions are required:

• It must be possible to apply weakening and contraction to formulas γA and δA, i.e. γ must start with ! and δ must start with ?.

• For the application rule, it must be possible to deduce a common modality ζ from γ and δ, in a context of γ and δ modalities, which essentially implies that one of γ, δ must be a suffix of the other.

For a pair (γ, δ) to be valid for intuitionistic logic, contraction and weakening of δ formulas is not required, and contexts only contain γ formulas. Let (γ, δ) be a modal translation for which these conditions are satisfied. Let Γ and ∆ be types where all formulas start with the modalities γ or δ. We can deduce the translation of the rules for λ and µ independently of the modalities:

p ⊢ Γ, x : γA ⊥ , v : δB p ⊢ Γ, xv : γA ⊸ δB δu(xv).p ⊢ Γ, u : δ(γA ⊸ δB) p ⊢ Γ, u : δB, α : δA, β : δB p[β/u] ⊢ Γ, α : δA, β : δB Hence we get λx.M u := δu(xv). M v µα[β]M α := M β
The formulation of the translation of µα[β]M is valid since α-conversion can be applied to the variable bound by µ. The fact that µα [β] does not modify the process in any other way stresses the fact that the µ binder is nothing more than a way to name conclusions of a proof in the sequentialised syntax of λ-calculus.

It is clear that the introduction rule for ∀ is not affected by the translation. There is a slight difference for the elimination rule: the λ-calculus is a syntax for natural deduction with intro/elim, while our type system for the π-calculus is a sequent calculus with only introduction rules and an actual cut rule. We can translate the elimination rule for ∀ by using an extra cut and axiom:

p ⊢ Γ, u : ∀X.A u=v ⊢ u : A[B/X] ⊥ , v : A[B/X] u=v ⊢ u : ∃X.A ⊥ , v : A[B/X] (νu)(p | u=v) ⊢ Γ, v : A[B/X]
By structural congruence we have (νu)(p|u=v) ≡ p[v/u], hence we can also accept the elimination rule itself in our type system. For the application rule, assume there is a generalised modality ζ of which γ and δ are suffixes, and set γ ′ and δ ′ such that ζ = γ ′ γ = δ ′ δ. Then the translation of application is:

p ⊢ Γ, v : δ(γA ⊸ δB) δv xu ⊢ v : δ(γA ⊗ (δB) ⊥ ), x : (γA) ⊥ , u : δB (νv)(p | δv xu ) ⊢ Γ, x : (γA) ⊥ , u : δB γ′ z(x).(νv)(p | δv xu ) ⊢ Γ, z : (ζA) ⊥ , u : δB q ⊢ ∆, w : δA δ ′ z(w).q ⊢ ∆, z : ζA (νz)(γ ′ z(x).(νv)(p | δv xu ) | δ ′ z(w).q) ⊢ Γ, ∆, u : δB
As explained above, one of γ, δ must be a suffix of the other, so one of γ ′ , δ ′ must be empty. We thus have two cases for the axiom, depending on which one it is:

u ′ =u ⊢ u ′ : (δA) ⊥ , u : δA δ′ x u ⊢ x : (γA) ⊥ , u : δA x=x ′ ⊢ x : (γA) ⊥ , x ′ : γA γ ′ u x ⊢ x : (γA) ⊥ , u : δA
When both γ ′ and δ ′ are empty, these cases collapse into u=x ⊢ x : (γA) ⊥ , u : δA.

γ and δ are given, γ ′ , δ ′ are such that γ ′ γ = δ ′ δ.

x γδ u :=      u=x if γ = δ δ′ x u if γ = δ ′ δ γ ′ u x if δ = γ ′ γ λx.M γδ u := δu(xv). M γδ v (M )N γδ u := (νz) γ′ z(x).(νv) M γδ v | δv xu | δ ′ z(w). N γδ w µα[β]M γδ α := M γδ β Table 4: General case translation of λµ into π.
Definition. Let (γ, δ) be pair of non-empty generalised modalities. The translation M γδ u of a λ-term M is defined inductively by the rules of table 4.

Theorem. Let (γ, δ) be a valid modal translation. For any λµ-term M , Γ ⊢

M : A | ∆ is derivable if and only if M γδ u ⊢ γΓ * ⊥ , u : δA * , δ∆ * is derivable.
Actions in the π-calculus, in particular replications, are blocking. As a consequence, in the standard semantics, there is no reduction inside replications, so the execution of M does not represent the full β-reduction. In the following sections, we give a detailed description of this execution. As explained above, there are two cases, depending on which of γ, δ is a suffix of the other:

Definition. A pair of generalised modalities (γ, δ) is called left-handed if δ is a suffix of γ. It is called right-handed if γ is a suffix of δ.

Call-by-name

Here we consider the left-handed case, i.e. with γ = δ ′ δ for some non-empty δ ′ . As a simplification we consider the case where δ and δ ′ are simple modalities, one easily checks that the other cases are not significantly different. The validity constraints impose δ ′ = !, and δ has to be ? for the classical case.

To describe precisely the operation of translated terms, we introduce a new form of term ♯M and define a continuation K as M 1 . . . M k α where α is a µ-variable and the M i are terms. An executable is a pair M * K, equivalence ≡ and execution → of executables are defined as

(M )N * K ≡ M * N K ♯M * K → M * K µα[β]M * K ≡ M [K/α] * β λx.M * N K → M [♯N/x] * K The substitution M [M 1 . . . M n α/β] is the substitution of every subterm of the form [β]N of M by [α](N )M 1 . . . M n .
The translation of terms is extended to executables as

α u := α=u x = M := δ ′ x(u). M u M K u := (νvz)( δu zv | z = M | K v) α = K := K α ♯M u := (νx)( x u | x = M ) M * K := (νu)( M u | K u)
Proposition. For any call-by-name executables e 1 and e 2 , e 1 ≡ e 2 implies e 1 ∼ = e 2 and e 1 → e 2 if and only if e 1 → e 2 .

Classical call-by-name (γ = !?, δ = ?):

x u = x u λx.M u = ū(xv). M v (M )N u = (νv) M v | !v(xy).(!x(w). N w | y=u)
Intuitionistic call-by-name (γ = !´, δ = ´):

x u = x u λx.M u = u(xv). M v (M )N u = (νvx) M v | !x(w). N w | v xu
Classical call-by-value (γ = !, δ = ?!):

x u = ū x λx.M u = ū(y).!y(xv). M v (M )N u = (νw) !w(x).(νv) M v | !v(w). w xu N w
Intuitionistic call-by-value (γ = !, δ = !): Proof. Remark that the translation M u of a variable or an abstraction has exactly one transition, labelled by an action on u or on a variable. Similarly, the translation K u of a continuation either is an equator u=α or has a unique transition labelled by an action on u. ♯M u has a single transition to a process bisimilar to M u. Then the key of the proof is the remark that bindings correctly implement substitution up to bisimilarity, i.e. (να)( e | α = K ) ∼ = e[K/α] for any fresh name α, and (νx)( e | x = M ) ∼ = e[♯M/x for any fresh name x. The rule for µα [β] applies only in the classical case, then δ starts with ! and continuations are replicable. Details can be found in the appendix.

x u = u=x λx.M u = !u(xv). M v (M )N u = (νvw) M v | N w | v wu
Executing a λµ-term simply means executing it on a continuation α for a fresh variable α, since M α ≡ M * α . Hence we can summarise this result as:

12 Theorem. Left-handed translations implement call-by-name execution.

The case for γ = !´and δ = ´is an adaptation of the standard !A ⊸ B decomposition that allows polymorphism. Operationally, it exactly corresponds to Milner's translation [START_REF] Milner | Functions as processes[END_REF]. The case for γ = !? and δ = ? corresponds to the system known as LKT in Danos-Joinet-Schellinx. As far as we know, its operational counterpart in the π-calculus is new. These particular translations are shown in table 5. In the classical case, the application uses an equator y=u which is not standard π-calculus, however it can be argued that replacing it by a forwarder !y(ab).ū ab does not affect the validity of the translation, although the step-by-step operational description is a bit heavier to formulate.

Call-by-value

We now consider the right-handed case, i.e. with δ = γ ′ γ. As in the previous section, we assume without loss of generality that γ is a single modality, necessarily ! because of the validity constraints. We now have two main choices for γ ′ , namely ? for the classical case and ˆfor the intuitionistic case. We now have to distinguish values, terms and continuations:

values V, W := x | λx.V terms M, N := V | (M )N | µα[K]M | V • W continuations K, L := α | KM f | KV a
An executable is a pair K * M . Equivalence and execution are defined as

KM f * V → KV a * M K * (M )N ≡ KM f * N KW a * V → K * V • W K * µα[L]M ≡ L * M [K/α] K * λx.M • V → K * M [V /x]
A continuation contains functions as unevaluated terms M f and arguments as values V a , so arguments are evaluated first. The terms V • W and µα[K]M are introduced to get a precise bisimulation. Translations are extended as Proof. The proof follows the same principle as in call-by-name. The substitution lemma now states (νx

V u := γ ′ u(x). x = V (M )N u := (νv)( v = uM f | N v) V • W u := (νxy)( x = V | y = W | γx yu ) x = y := x=y x = λy.M := γx(yu). M u α = β := α=β α = KM f := (νv)( γ′ α(x).(νu)( M u | δu xv ) | v = K ) α = KV a := (νvx)( x = V | δα xv | v = K ) µα[K]M α := (νβ)( β = K | M β) K * M := (νu)( u = K | M u)
)( e | x = V ) ∼ = e[V /x]
) where e is an executable, V is a value and x is a λ-variable; the same lemma for µ-variables and continuations also holds. We then remark that translations of terms and continuations always have at most one transition, and the correspondence with the operational semantics above is easily checked. Details can be found in the appendix.

Given a fresh µ-variable α, once again we get M α = α * M , hence the semantics above precisely describes the execution of translations of λµ-terms in right-handed translations, which can be summarised as follows:

14 Theorem. Right-handed translations implement call-by-value execution.

The case for γ = ! and δ = ?! corresponds to the system called LKQ in Danos-Joinet-Schellinx. Operationally, we get exactly Honda, Yoshida and Berger's translation [START_REF] Berger | Genericity and the π-calculus[END_REF][START_REF] Honda | Control in the π-calculus[END_REF]. The case for γ = ! and δ = ˆ! is a version of this translation linearised with respect to conclusions. It is actually very close to Milner's encoding of call-by-value λ-calculus [START_REF] Milner | Functions as processes[END_REF], which corresponds to the slightly more expensive decomposition

(A → B) * = ´(!A * ⊸ ˆ!B * ).
The simplest intuitionistic version is obtained by taking γ = δ = !, which is both left-and right-handed. It is easy to check that the operational meaning of this translation is an extension of the call-by-value strategy where functions and arguments can be executed in parallel. These translations are shown in table 5.

Realisability interpretations

The previous sections define a family of type-preserving translations of the λµ-calculus into the π = -calculus, and provide a detailed description of the operational semantics induced by the translations. Since the operational translations are deduced from simple embeddings of intuitionistic and classical logics into linear logic, we can expect more semantic interpretations.

The soundness of the type system we use for processes is formulated using realisability, as described in the following section.

Soundness of LLa

For a finite set of names I, a process p has interface I if fv(P ) ⊆ I.

Definition. An observation is a set ⊥ of processes of empty interface. Given an observation ⊥, two processes p and q of interface I are orthogonal, written p ⊥ q, if (νI

)(p | q) ∈ ⊥. An observation ⊥ is valid if • ⊥ is closed under bisimilarity,
• if p has a unique labelled transition p τ -→ p ′ and p ′ ⊥ q then p ⊥ q.

If A is a set of processes of interface I, its orthogonal is the set

A ⊥ := {p : I | ∀q ∈ A, p ⊥ q}. A behaviour is a set A such that A = A ⊥⊥ . The complete lattice of behaviours of interface I is noted B I .
Let (u i ) i∈N be an infinite sequence of pairwise distinct names. Let B k := B u1...u k . A valuation of propositional variables is a function ρ that associates, to each variable X of arity k, a behaviour ρ(X) ∈ B k . Given a valuation ρ, the interpretation of a type A localised at x, with | x| = ar(A), is the behaviour x : A ρ of interface x defined inductively by

x 1 . . . x n : X ρ := v(X)[x 1 /u 1 , . . . , x n /u n ] x y : A ⊗ B ρ := {(p | q) | p ∈ x : A ρ, q ∈ y : B ρ} ⊥⊥ u : ´A ρ := {u( x).p | p ∈ x : A ρ} ⊥⊥ x : ∃X k .A ρ := X ∈B k x : A (ρ[X := X ])
⊥⊥ and x : A ⊥ ρ := ( x : A ρ) ⊥ . Exponential modalities require a more subtle definition: for each name u, define the contraction δ u over behaviours of interface {u} as

δ u (A) := {p[u/v, w] | p ∈ A[v/u] `A[w/u]} ⊥⊥
where v and w are fresh names. Then, for a behaviour B of interface {x 1 . . . x n }, define F u (B, X ) := u : ˆB ∪ {1 : u} ⊥ ∪ δ u (X ) ⊥⊥ . This operator is obviously monotonic in X , and the interpretation of exponential modalities is defined as a fixed point of it:

u : ?A ρ := lfp(X → F u ( x : A ρ, X )) u : !A ρ := ( u : ?(A ⊥ ) ρ) ⊥
Finally, a type Γ = x 1 : A 1 , . . . , x n : A n is interpreted as

Γ ρ := (p 1 | . . . | p n ) p 1 ∈ x 1 : A 1 ρ ⊥ , . . . , p n ∈ x n : A n ρ ⊥ ⊥
Definition. Given an observation, a process p realises a type Γ if p ∈ Γ ρ for any valuation ρ. This fact is written p Γ.

From the definition of observations and the interpretation of formulas, we easily deduce the adequacy theorem (we do not expose the proof here, a detailed study on this technique can be found in other works by the author [START_REF] Beffara | réalisabilité et concurrence[END_REF][START_REF] Beffara | A concurrent model for linear logic[END_REF]):

Theorem. If p ⊢ Γ is derivable, then p Γ for any observation ⊥.
The usual notions of testing fit in our notion of observation, for instance: Proposition. Let ω be a channel, assume ω is not taken into account in interfaces. Define the must-testing observation as {p | ∀p → * q, ∃q → * ω | r}. Must-testing is a valid observation.

Properties of typed processes, such as termination or deadlock-freeness, can be obtained by choosing appropriate observations. For instance:

19 Proposition. Let p ⊢ Γ be a typed process such that any propositional variable occurring in Γ is under a modality. For any reduction p → * p ′ there is a reduction p ′ → * p ′′ such that p ′′ has a visible action.

Proof. We use the must-testing observation with a channel ω that does not occur in p. Note that ω ∈ x : A for any formula A, hence u( x).ω ∈ u : ´A . By similar arguments we get u( x).ω ∈ u : !A , ū( x).ω ∈ u : ˆA and ū( x).ω ∈ u : ?A . Moreover it is clear that, for q ∈ A and r ∈ B , (q | r) ∈ A ⊗ B and (q | r) ∈ A `B . Each name u i occurring in Γ occurs with a polarity ε i (depending on the modality that introduces it) and a particular arity.

Let t := i ūεi i ( x).ω, by the above remarks we know that t ∈ ( Γ ρ) ⊥ for any valuation ρ. This implies that, for any reduction p | t → * p ′ | t there is a reduction p ′ | t → * ω | q. Since ω only occurs in t, this implies that an action in t must be triggered during this reduction. By induction on the typing rules, on proves that if all type variables occur under modalities, no equator in p can relate free names, hence triggering an action in t must be done by an action in a reduct of p ′ . 20 Corollary. The execution of a typed λµ-term in call-by-name or call-by-value always ends with a λor µ-variable in active position.

Proof. Let Γ ⊢ M : A | ∆ be a typed λµ-term. Using non-divergence as the observation we can prove that M α has no infinite reduction. Consider a reduction M α → * p with p irreducible. By proposition 19 we deduce that p must have a visible action, and this action can only be on α or a name that occurs in Γ or ∆. Conclude by reasoning on the shape of translations of terms: in call-by-name, executables with visible actions are x * K or λx.M * α; in call-by-value they are

K * x • V or α * λx.M .

Extending the λµ-calculus

Realisability presents the type system LLa as an axiomatisation of the algebra of process behaviours. This allows for the introduction of new logical connectives and new rules: by semantic means (i.e. by reasoning on the reductions of processes) we can define the interpretation of a connective as an operation on sets of processes. If we prove the adequacy of a new logical rule, we can then use it as a typing rule for processes with the guarantee that any property that is proved by realisability is preserved; this includes termination and deadlock-freeness. This technique can be used to extend the typed λµ-calculus. As soon as a connective can be translated into LLa (possibly extended as explained above), a translation of the underlying syntax is deduced the same way as for the core calculus, which induces an evaluation strategy. This provides a framework for extending our type-preserving translations, without loosing any of the properties of the translations. We now provide some examples of these ideas.

Product types Products can be added to the λµ-calculus by means of a pair of constructs for introduction and elimination:

Γ ⊢ M : A | ∆ Γ ⊢ N : B | ∆ Γ ⊢ (M, N ) : A × B | ∆ Γ ⊢ M : A × B | ∆ Γ, x : A, y : B ⊢ N : C | ∆ Γ ⊢ let x, y = M in N : C | ∆
Given a pair (γ, δ), we extend the translation of types by (A × B) * = γA * ⊗ γB * . Note that, when γ and δ are not empty, the arity of (A ⊗ B) * is 2, hence polymorphism is preserved. The translation of terms is extended as follows:

(M, N ) γδ u := δu(xy).(δ ′ x(v). M γδ v | δ ′ y(w). N γδ w)

let x, y = M in N γδ u := (νv)( M γδ v | δv(xy). N γδ u)
In both strategies, let x, y = M in N must reduce M into a pair before evaluating N . The evaluation of the parts of a pair in call-by-value is done in parallel since δ ′ is empty. We leave to the reader the formulation of precise evaluation rules.

Sum types Sum types in λµ can be defined as follows (with i ∈ {1, 2}):

Γ ⊢ M : A i | ∆ Γ ⊢ inj i M : A 1 + A 2 | ∆ Γ ⊢ M : A 1 + A 2 | ∆ Γ, x i : A i ⊢ N i : C | ∆ Γ ⊢ case M of {inj i x i → N i } : C | ∆
Decomposing this in linear logic requires the additives ⊕ and &. The general rules in LLa are complicated, but here we only need simplified versions:

p ⊢ Γ, u : ˆA p ⊢ Γ, uv : ˆA ⊕ ˆB p ⊢ Γ, x : A q ⊢ Γ, y : B u( x).p + v( y).q ⊢ Γ
inj i M u := δu(a 1 a 2 ).ˆδ ′ a i (v). M v case M of {inj i x i → N i } u := (νv) M v δv(ab). i a i (x i ). N i u
Obviously, in any strategy, the evaluation of case M of {inj i x i → N i } must always reduce M into an inj i before proceeding.

Subtyping Behaviours of a given interface form a complete lattice, with intersection as the lower bound and bi-orthogonal of the union as the upper bound. Write ∧ and ∨ these dual connectives with ar(A ∧ B) = ar(A) = ar(B). This induces subtyping over types, defined as A B if A ⊆ B , and the rules:

p ⊢ Γ, x : A p ⊢ Γ, x : B p ⊢ Γ, x : A ∧ B p ⊢ Γ, x : A p ⊢ Γ, x : A ∨ B p ⊢ Γ, x : A A B p ⊢ Γ, x : B
It is clear that all connectives except negation are increasing for this relation, and that A B if and only if B ⊥ A ⊥ . By the interpretation of modalities we also get !A ´A and ˆA ?A. Subtyping rules in λµ can be written as

Γ ⊢ M : A | ∆ Γ ⊢ M : B | ∆ Γ ⊢ M : A ∩ B | ∆ Γ ⊢ M : A | ∆ A B Γ ⊢ M : B | ∆

Fix points

The fact that behaviours form complete lattices also guarantees that any increasing function over behaviours of a fixed interface have (least and greatest) fix points. We can thus extend LLa with dual constructs µX.A and νX.A, with the constraints that ar(X) = ar(A) and that X does not occur as X ⊥ in A. The typing rules for fix points are rather technical to formulate, mainly because the proper rule for νX.A requires the introduction of a recursion operator in the π-calculus. Fix points in the types for λµ-calculus would be simply translated as (µX.A) * = µX.(A * ). The constraint that permits polymorphism à la system F also allows this fix point to be used for any A where X only occurs positively.

These various extensions to the type system can be freely combined. Other extensions, notably with concurrent primitives, could be studied in a similar way. However, for this purpose, it seems necessary to enforce serious linearity in the calculus. This fits naturally in our type system for the π-calculus but it is incompatible with full control in the style we get from translations of full classical logic. Precise studies of this idea are deferred to further work. Renaming of transition labels:

p u = v u, v / ∈ {x 1 . . . x n } p u ε (x 1 . . . x n ) = v ε (x 1 . . . x n ) p u = u ′ p v = v ′ p [u=v] = [u ′ =v ′ ]
Table 6: Rules for name unification.

A Technical details A.1 Bisimulation in π =

A polarity ε is an element of {´, ˆ}. ´is called positive and ˆis called negative. The notation u ε ( x) stands for u( x) if ε = ´and for ū( x) if ε = ˆ. Two names x and y are unified by a process p if p x = y is derivable using the rules of table 6. Note that an action like u(x).y=z does not unify y and z, i.e. the equator y=z is inactive as long as the action u(x) has not been consumed. A transition can have one of three kinds of labels:

e ::= u ε (x 1 . . . x n )
visible action (with the x i fresh and distinct) [u=v] conditional internal reduction τ internal reduction

The notation p a = b is extended to transition labels as detailed in table 6. For a label e, n(e) is the set of names that occur in e, i.e. n(u(x 1 . . . x n )) = {u, x 1 . . . x n }, n([u=v]) = {u, v} and n(τ ) = ∅. The labelled transition system of the calculus is defined in table 7.

A simulation is a relation S over processes such that pSq implies that

• for any x, y ∈ N , p x = y implies q x = y,

• for each transition p e -→ p ′ there is a transition q e -→ q ′ such that p ′ Sq ′ .

A bisimulation is a relation S such that both S and S -1 are simulations. Two processes p and q are bisimilar if there is a bisimulation S such that pSq.

Actions (with α = u ε (x 1 . . . x n )) and composition:

α.p α -→ p !α.p α -→ p | !α.p p ū(x1...xn) ------→ p ′ q v(x1...xn) ------→ q ′ p | q [u=v] ---→ (νx 1 . . . x n )(p ′ | q ′ ) Renaming: p e -→ p ′ p e = e ′ p e ′ -→ p ′ p [u=v] ---→ p ′ p u = v p τ -→ p ′ Context: p e -→ p ′ p | q e -→ p ′ | q p e -→ p ′ q | p e -→ q | p ′ p e -→ p ′ x / ∈ n(e) (νx)p e -→ (νx)p ′

A.2 Simulation in call-by-name

For the "push" rule, we have: In the intuitionistic case the rule is not applicable, but it would hold too under the condition that each µ-variable is used linearly. For the ♯M rule, we have:

(M )N * K = (νu) (νz) (νv)( M v | δv zu ) z = N K u ≡ (νuvz) M v δv zu z = N K u ≡ (νv) M v (νu) (νz)( δv zu | z = N ) K u ≡ (νv) M v (νuz)( v = N u | K u) = M * N K
♯M * K = (νux) δ′ x u δ ′ x(v). M v K u → (νux) M u K u δ ′ x(v). M v ∼ = (νu) M u K u = M * K
where → contains one transition for each modality in the word δ ′ . Since K u and E are blocked on actions that cannot be on channel x, this reduction is clearly the only one possible. The term δ ′ x(v). M v is not consumed since δ ′ must contain !, however there is no other occurrence of x so we can discard it by bisimilarity.

For the substitution rule for terms, the argument is the same as for continuations. In this case, the only outputs on the channel of a λ-variable x are of the form x u = δ′ x u , hence after distribution of x = M we get (νx ′ )( x ′ u | x ′ = M ) = ♯M u for a fresh x ′ . For the "pop" rule, we thus have where → contains one transition for each modality in the word δ. In the classical case, δu xw is not consumed since δ contains !, however we know that u does not occur elsewhere since all duplications of continuations are performed by the rule for µα [β], so this action becomes inactive and it is bisimilar to the empty process. As above, this reduction is the only one possible.

A.3 Simulation in call-by-value

The substitution rule for continuations and the equivalence rule for µα [β] hold by the same arguments as in the case of call-by-name.

For the first equivalence, we have

K * (M )N = (νu) u = K (νv)( v = uM f | N v) ≡ (νv) (νu)( u = K | v = uM f ) N v = KM f * N
For the first reduction rule, we have

KM f * V = (
M w (νvx)( x = V | δw xv | v = K ) ∼ = KV a * M
where → contains one transition for each modality in the word γ ′ . In the classical case γ′ contains ! so the continuation at u is not consumed, however we know that u has no other occurrence since continuations are duplicated by the rule for µ, so we can erase the residual term on u by bisimilarity. This is the only possible reduction as soon as γ ′ is not empty. The second reduction

  Each variable is supposed to have a fixed arity. Given an arity function ar : V → N, the arity of a formula is defined as ar( †A) := 1 with † ∈ {ˆ, ´, ?, !} ar(∃X.A) := ar(∀X.A) := ar(A) ar(A ⊗ B) := ar(A `B) := ar(A) + ar(B)

  , uv : ´A & ´B assuming the underlying π-calculus has guarded choice. We get adequacy by defining uv : A ⊕ B ρ := ( u : A ρ ∪ v : B ρ) ⊥⊥ and interpreting A & B by duality. The sum type of λµ is translated as (A + B) * = ˆγA * ⊕ ˆγB * (which preserves polymorphism). The translation of terms follows:

  Translations are extended as (A ∩ B)* = A * ∧ B * . The usual subtyping rules, like (A → B) (A ′ → B ′ ) if A ′ A and B B ′ , hold through translation.

  Axioms and context rules for unification:x=y x = y p x = y p | q x = y p x = y q | p x = y p x = y z / ∈ {x, y} (νz)p x = yReflexivity, symmetry and transitivity of equators:

For the substitution rule

  for continuations, consider a process (να)( M u | K α), with K = M 1 . . . M k β. When δ starts with ?, each K α is a guarded replication on channel α. By construction there is no other input on α so each output on α can only interact with K α. Hence, up to bisimilarity, we can distribute K α in M u by substituting each action ᾱ( x).p by (να ′ )(ᾱ ′ ( x).p | K α ′ ) for a fresh α ′ . All output occurrences of α occur in processes of the form µθ[α]N θ = N α, but (να ′ )( N α ′ | K α ′ ) = N * Kand by the previous rule we have N * K ≡ (N )M 1 . . . M k * β = µθ[β](N )M 1 . . . M k θ. By this rule we can deduce the validity of the rule for µα[β]: µα[β]M * K = (να) M β K α ∼ = M [K/α] β ≡ M [K/α] * β

  λx.M * N K = (νu) δu(xv). M v (νw) (νz)( δu zw | z = N ) K w ≡ (νuwx) δu(xv). M v δu xw x = N K w → (νuwx) M w δu xw x = N K w ≡ (νwx) M w (νu) δu xw x = N K w ∼ = (νwx) M w x = N K w ∼ = (νw) M [♯N/x] w K w = M [♯N/x] * K

  νu) (νv) γ′ u(x).(νw)( M w | δw xv ) v = K γ ′ u(x). x = V ≡ (νuv) γ′ u(x).(νw)( M w | δw xv ) v = K γ ′ u(x). x = V → (νuvx) γ′ u(x).(νw)( M w | δw xv ) (νw)( M w | δw xv ) v = K x = V ≡ (νw) (νu)γ ′ u(x).(νw)( M w | δw xv )

Table 1 :

 1 Structural congruence and reduction.

	νy)p ≡ (νy)(νx)p	(νx)(p | q) ≡ p | (νx)q if x / ∈ fv(p)	(νx)1 ≡ 1
	Equators:
	1 ≡ x=x	x=y ≡ y=x	x=y | p[x/z] ≡ x=y | p[y/z]
	Replication and reduction:
	!α.p ≡ α.(p | !α.p)	u( x).p | ū( x).q → (ν x)(p | q)

  equivalence is the congruence over λ-terms generated by Head linear reduction is the relation over σ-equivalence classes generated byλx 1 . . . x k .(λy 1 . . . y n .(y i )M 1 . . . M p )N 1 . . . N n → λx 1 . . . x k .(λy 1 . . . y n .(N i )M 1 . . . M p )N 1 . . . N n First note that for M and N of type A, if M = σ N then M A y ≡ N A y,so we can consider terms up to σ-equivalence. Consider a typed term Γ ⊢ M : A. By σ-equivalence we assume that M is written λ x.(λ y.(x) M ) N with | y| = | N |. Call A i the type of each x

	(λx.M )N P = σ (λx.(M )P )N	(λxy.M )N = σ λy.(λx.M )N
	with x / ∈ fv(P ) and y / ∈ fv(N ). Any λ-term M can be normalised as
	M = σ λx 1 . . . x k (λy 1 . . . y n .(x)M 1 . . . M p )N 1 . . . N n
	Proposition. For any simply typed λ-term Γ ⊢ M : A, M A y is bisimilar to M for head linear
	reduction.
	Proof.

i , B i the type of each y i and N i (these are the same since M is well typed), and call C i the type of each

Table 5 :

 5 Particular cases of translations.

Table 7 :

 7 Labelled transition system.

p ⊢ Γ, x : A[B/X] ar(B) = ar(X) p ⊢ Γ, x : ∃X.A Table 2: Typing rules for the π = -calculus. Intuitionistic rules: Γ, x : A ⊢ x : A | ∆ Γ, x : A ⊢ M : B | ∆ Γ ⊢ λx.M : A → B | ∆ Γ ⊢ M : A → B | ∆ Γ ⊢ N : A | ∆ Γ ⊢ (M )N : B | ∆ Quantifiers: Γ ⊢ M : A | ∆ X / ∈ fv(Γ, ∆) Γ ⊢ M : ∀X.A | ∆ Γ ⊢ M : ∀X.A | ∆ Γ ⊢ M : A[B/X] | ∆ Control: Γ ⊢ M : B | α : A, β : B, ∆ Γ ⊢ µα[β]M : A | β : B, ∆Table 3: Typing rules for the λµ-calculus.

rule is deduced as

where → contains one transition for each modality in the word γ ′ , since δ = γ ′ γ. As above, this is the only reduction. For the substitution rule, we have

where there is one transition for each modality in γ. The step after the reduction is an instance of the substitution lemma (νx

. This lemma holds by the same argument as in the case of call-by-name: the binding x = V can be distributed to all occurrences of x, but any occurrence of x occurs in a binding y = x so we have


L Daniault
email: louis.daniault@institutoptique.fr

M Hanna

L Lombard

D Goular

P Bourdon

F Druon

P Georges

Coherent combining of two femtosecond fiber chirped pulse amplifiers

We demonstrate coherent combining of two fiber chirped pulse amplifiers seeded by a common oscillator. A phase stability of λ/20 is obtained using a fiber electro-optic phase modulator, and the recombined pulsewidth is 485 fs. Time (a. u.

Introduction

Ytterbium-doped fiber amplifiers present great advantages in femtosecond regime, including high optical-to-optical efficiency, good thermal handling and high spatial beam quality. However, the tight confinement of the beam inside the fiber and the long interaction length can lead to strong nonlinear effects at high energies. This constitutes a limit to femtosecond fiber chirped-pulse amplifier (CPA) setups.

Different techniques can be used to bypass this drawback and provide higher peak powers. The first one consists in enlarging the mode field area of the fiber amplifier, so that the nonlinear effects can be handled at higher energies. This has been made in the last few years using large mode area fibers [START_REF] Zaouter | Transform-limited 100 μJ, 340 MW pulses from a nonlinear-fiber chirped-pulse amplifier using a mismatched grating stretcher-compressor[END_REF]. However, the core scaling capability is limited by the transverse multimode character that inevitably appears for large core fibers.

Another way to scale the energy is to use several amplifiers, and to combine them at the output to get the sum of the energies, thereby avoiding detrimental effects at high peak powers in the fiber. This technique is already used in continuous-wave and nanosecond regimes [START_REF] Cheung | Phase Locking of a Pulsed Fiber Amplifier[END_REF], and is scalable in terms of achievable energy. Several combination techniques exist, but only active coherent combining can easily be transposed to the femtosecond regime.

In CW regime, the relative phase between the beams has to be carefully measured and controlled through a feedback loop to be able to coherently add the electric fields. In femtosecond regime, the group delay and the phase have a priori different roles and should be taken independently. In our case, for pulses of duration above 100 fs, we show that a static adjustment of the delay, along with an active correction of the phase, is sufficient to efficiently combine the pulses, because the pulsewidth is long compared to an optical cycle. A major difference for fs regime is also the group velocity dispersion, which has an impact on temporal pulse shapes as opposed to ns regime, and has to be matched in both arms to ensure a good time overlap of the pulses and retrieve the initial duration.

We report on the coherent combining of two standard femtosecond Yb-doped fiber CPA, using active control of the relative phase between the amplifiers. To the best of our knowledge, only one similar experiment has been done independently by another research team and reported very recently, but with another method for the phase control [START_REF] Seise | Coherent combining of fiber-amplified ultrashort laser pulses[END_REF]. These combining experiments open a novel way for energy / average power scaling of femtosecond amplifiers.

Experimental setup and results

Our experimental setup, depicted in Fig. 1, begins with a femtosecond oscillator that delivers 200 fs pulses at 35 MHz repetition rate. It is followed by a stretcher that broadens the pulses to 150 ps. A half wave plate with a polarizing beam splitter allows us to separate the seed into two arms with adjustable power in each. The first one is made of a fiber-coupled LiNbO 3 integrated phase modulator followed by a 2 m Yb-doped double clad LMA fiber amplifier. The second one contains a 2.40 m single-mode fiber that precedes a 1 m Yb-doped double clad LMA fiber amplifier. This discrepancy in amplifier length is only due to the availability of fibers in the lab, and should be corrected in further reports. The aim of the single-mode fiber is to balance the group velocity dispersion of both arms, and it also acts as a coarse delay matching element. Both amplifiers are operated in linear regime. Their respective outputs are collimated and overlap on a 50/50 beam splitter. Provided that the pulses are synchronous and have the same temporal shape, they interfere on the beam splitter and can be recombined coherently. When the delay between the arms is matched adequately, the overall power is distributed in the two outputs of the recombining 50/50 cube, depending on the relative phase between the two pulses. One of the outputs of the cube goes directly to the compressor, whereas the other one is followed by a photodiode that detects a signal to be minimized. If the delay between the two pulses is not well adjusted, the cube behaves like a simple 50/50 beam splitter for each of them. This setting is tuned by a fine delay on the second arm.

OSA / ASSP 2011

AMC2.pdf

The relative phase between the pulses is controlled using the technique described in reference [START_REF] Shay | First experimental demonstration of self-synchronous phase locking of an optical array[END_REF]. A small modulation at 250 kHz is added to the error signal to drive the phase modulator. At the output of the photodiode a lock-in amplifier allows the detection of the small resulting amplitude modulation. This signal is then sent to a digital card that acts as a PID circuit and manages 2π phase jumps to stay in the phase modulator input voltage range. The integration time of the lock-in amplifier is set to 40 µs, meaning that the maximum phase noise frequency that can be corrected is 12.5 kHz. On Fig. 2 are represented the relative phase between the amplifiers as a function of time and the phase noise spectral density, for free running and phase-locked operation. Most of the phase noise content is below 1 kHz, and our setup is therefore adapted to correct these phase fluctuations. The small phase errors observed around 3s on fig. 2 (left) are due to the electronic circuit that generates a 2π phase jump. We also measured the energy fluctuations at the output of the compressor with a fast photodiode (rise time 1 ns). The temporal traces of the pulses obtained in persistence mode over 10 s are displayed in Fig. 3 in both unlocked (left) and locked regime (right). The measured standard deviation of the pulse intensity corresponds to a phase standard deviation of λ/20. We estimate the contrast between the two outputs to be 70%. This contrast, that determines the combining efficiency, is only limited in our case by a non perfect spatial overlap of the two recombined beam, a well-identified issue that should be solved shortly. The total recombined power at the output of the compressor is 250 mW at 35 MHz repetition rate, limited by the very short length of fiber that is used in the first arm for availability reasons. Finally, we focus on the temporal and spectral properties of the pulses for each channel independently, and for the recombined output. The autocorrelations and spectra are plotted in Fig. 4. Assuming a Gaussian temporal shape, the pulse duration for isolated arms is 460 fs, while the recombined pulse exhibits 485 fs duration, indicating that the recombination does not affect the pulsewidth significantly. The recombined spectrum is also very similar to isolated ones, and the absence of large modulation shows that the group-velocity delay is adjusted adequately.

OSA / ASSP 2011

Conclusion

We demonstrated coherent combining of two fiber chirped pulse amplifiers using a single stretcher and compressor. The RMS residual phase error is λ/20, and we did not observe any combining-related degradation of the pulse shape or spectrum at this power level. Theoretical and experimental [START_REF] Jiang | Impact of self-phase-modulation on coherently combined fiber chirped-pulse amplifiers[END_REF] considerations to evaluate the tolerance of the system to residual discrepancies between the arms in terms of phase, group-delay, dispersion, and B-integral indicate that these systems are realistically scalable. This experiment therefore represents a promising result for further investigations in the field of coherent combining of several discrete femtosecond amplifiers. The authors acknowledge the financial support of the RTRA Triangle de la Physique (Femtocombo project).

Fig. 1 :

 1 Fig.1: Experimental setup of femtosecond coherent combining, mixing a CPA architecture with a Mach-Zehnder interferometer.

Fig. 2 :

 2 Fig.2: Retrieved relative phase as a function of time (left) and phase noise spectral density (right), in free running (black) and locked phase regime (red).

Fig. 3 :

 3 Fig.3: Oscilloscope temporal trace at the output of the compressor for unlocked phase (left) and stabilized phase (right). The persistence time is 10 seconds.

Fig. 4 :

 4 Fig.4: Autocorrelation traces (left) and optical spectra (right) of the output for channels 1 (green) and 2 (blue) independently, and for the recombined beam (red).


Carolina Albea
email: calbea@cartuja.us.es

Francisco Gordillo
email: gordillo@esi.us.es

Javier Aracil
email: aracil@esi.us.es

Control of the Boost DC-AC Converter by Energy Shaping

In this paper a control strategy for generation of alternating current without using any reference signal is applied to a nonlinear boost dc-ac converter. A Phase-Locked Loop is added to the control law in order to achieve synchronization between the two parts of the circuit. It is also shown that this idea is also valid for synchronization with the network. The resultant control laws are tested by means of simulations.

I. Introduction

In electronics converters with ac output the control objective can be seen as the generation of a stable limit cycle with given amplitude and frequency for which voltages and currents present a sinusoidal behavior with pre-specified phase shift. If a control law is able to produce such a limit cycle, the generation of alternating current will be accomplished without the necessity of introducing any time dependent reference signal. The generation of limit cycles for producing self-oscillations has been successfully applied to electro-mechanical systems [START_REF] Aracil | Stabilization of oscillations in the inverted pendulum[END_REF], [START_REF] Gómez-Estern | The Hopf bifurcation and controlled oscillations in electromechanical systems[END_REF], [START_REF] Gordillo | Stabilization of autonomous oscillations and the Hopf bifurcation in the ball and beam[END_REF]. Some applications to electronics converters are [START_REF] Aracil | On the control of oscillations in DC-AC converters[END_REF], [START_REF] Gordillo | Autonomous oscillation generation in electronic converters[END_REF], where a three-phase UPS and a boost converter are controlled using this idea. Concretely, in the boost converter application, a simple boost converter was used to produce oscillating voltage, which is not centered around zero due to the impossibility of achieve negative voltages with this circuit. Therefore, alternating current was not achieved. In this paper, we deal with this problem using a double boost converter [START_REF] Cáceres | A boost DC-AC converter: analysis, design, and experimentation[END_REF] and extending the control law proposed in [START_REF] Gordillo | Autonomous oscillation generation in electronic converters[END_REF] to this case. It is shown that the direct application of this extension does not fulfil the objective due to the lack of synchronization between both parts of the circuit. In order to achieve the synchronization a phase-locked loop (PLL) is added to the previous control law. This idea can be used for synchronization with the electrical network in order to achieve satisfactory power factor. The resultant controllers are checked by means of simulations.

The rest of the paper is organized as follows.c

II. Generation of Oscillations by Energy Shaping

In power electronic converters with ac output the control objective can be seen as the generation of a stable limit cycle with given amplitude and frequency for which voltages and currents present a sinusoidal behavior with pre-specified phase shift. If a control law is able to produce such limit cycle, the generation of alternating current will be accomplished without the necessity of introducing any reference signal. For this, a target system may be defined and by matching its equations and the system equations a control law can be obtained. In order to define the target system consider the following energy-like function

V 0 (x 1 , x 2 ) = ω 4 Γ 2 (x 1 , x 2 ), (1) with
Γ(x 1 , x 2 ) = ω 2 (x 1 -x 10 ) 2 +(x 2 -x 20 ) 2 -µ.
Parameters ω, x 10 , x 20 and µ > 0 should be chosen so that the closed curve Γ = 0 defines the desired behavior. This curve is an ellipse centered at the point (x 10 , x 20 ). We can define a dynamical system such that this closed curve is its limit set. This can be reached adopting V 0 as a Hamiltonian function, and defining the dynamical system (3)-( 4)

ẋ1 ẋ2 = -k a1 1 Γ -1 Γ -k a2 D x1 V 0 D x2 V 0 , (2)
resulting ẋ1 = (x 2 -x 20 ) -k a1 ω 2 (x 1 -x 10 )Γ (3) ẋ2 = -ω 2 (x 1 -x 10 ) -k a2 (x 2 -x 20 )Γ (4)
Noticing that

V0 = -Γ 2 k a1 ω 4 (x 1 -x 10 ) 2 + k a2 (x 2 -x 20 ) 2 ≤ 0 (5)
and using LaSalle invariance principle it can be seen that for all initial conditions except the origin the trajectories of the system tend to the curve Γ = 0. The behavior of this target system corresponds to the sinusoidal behavior that it is desired of a dc-ac converter. Constants ω, x 10 , x 20 and µ are design parameters for the frequency bias and amplitude of the desired behavior while k a1 and k a2 define the speed of the transient response.

III. Boost DC-AC Converter: Analysis, Control and Results

The boost inverter is specially interesting because it generates an ac output voltage larger than the dc input one. It is made up of two dc-dc converters and a load connected differentially across them Fig. 1. Each converter produces a dc-biased sine wave output, V a and V b , so that each source generates an unipolar voltage. The circuit implementation is shown in Fig. 2.

Voltages V a and V b should present a phase shift equal to 180 • , which maximizes the voltage excursion across the load [6] Fig. 3. The boost dc-ac converter can be simplified as shown in Fig. 4. This simplification lets see clearer the bidirectional current of each boost dc-dc converter.

V a V b + + load - - converter converter A B
In order to make easier the studies, we will use this simplification for obtaining the control law, and then we will extrapolate these results to the full converter.

A. System Description

It is necessary to assume that all the components are ideal and that the currents of the converter are continuous. The two performance modes for a time period are shown in Fig. 5. Defining the control variable q as q = 0 , when Q 1 = OF F and Q 2 = ON , and q = 1, when Q 1 = ON and Q 2 = OF F , the converter dynamic equations are

L di L dt = -v C1 + qv C1 + V in (6)
C dv C1 dt = i L -qi L - v C1 R + V 2 R (7)
If u = 1q is taken as the control action on equations ( 6)-( 7), we have

L di L dt = -uv C1 + V in (8)
C dv C1 dt = ui L - v C1 R + V 2 R (9)
The control law, u can only take two values u ∈ {0, 1}. Nevertheless, as usual, we consider its average value and, thus, u is a continuous variable u ∈ [0, 1].

B. Normalized Model

In order to simplify the study, system (8)-( 9) is normalized by using the following change of variables

x 1 = 1 V in L C i L (10) x 2 = v C1 V in (11)
z 2 = V 2 V in (12)
and defining t = ωt (13)

as a new time variable with

ω 0 = 1 √ LC (14) yielding ẋ1 = -ux 2 + 1 (15) ẋ2 = ux 1 -ax 2 + az 2 (16)
where a = 1 R L C . Notice that eliminating u in (15)-( 16) we obtain

x 1 (1 -ẋ1 ) = x 2 ( ẋ2 + ax 2 -az 2 ). ( 17
)
This relationship will be used later.

C. Controller Design

System (15)-( 16) is not directly matchable with system (3)-( 4). The main problem is that two pairs of equations have to be matched while only one degree of freedom u is available. Another change of variables is needed in order to get a model structure similar to (3)-( 4). For this, define

y 1 = x 2 1 + x 2 2 2 (18)
y 2 = x 1 -ax 2 2 + ax 2 z 2 + y 20 (19)
where y 20 is an offset term that will be a tuning parameter. From ( 18)-( 19), it is easy to see that

ẏ1 = y 2 -y 20 (20) ẏ2 = 1 + 2a 2 x 2 2 -3a 2 z 2 x 2 + a 2 z 2 2 + ax 2 ż2 -u(x 2 + 2ax 1 x 2 -az 2 x 1 ) (21)
It is not easy to obtain a simple relationship x 1 = f (y 1 , y 2 ) and x 2 = f (y 1 , y 2 ) due to complexity of definitions (18)-( 19).

Looking at the target system structure (3)-( 4) and comparing it with (20)-(21) the choice k a1 = 0 is obvious resulting, as target system

ẏ1 = y 2 -y 20 (22) ẏ2 = -ω 2 (y 1 -y 10 ) -kΓ(y 2 -y 20 ) (23)
where, for simplicity, k a2 has been renamed to k.

The control law u that matches (20)-( 21) and ( 22)-( 23) is

u = 1 + 2a 2 x 2 2 -3a 2 z 2 x 2 + a 2 z 2 2 + ax 2 ż2 x 2 + 2ax 1 x 2 -az 2 x 1 + kΓ(y 2 -y 20 ) + ω 2 (y 1 -y 10 ) x 2 + 2ax 1 x 2 -az 2 x 1 (24)
The ellipse parameters have to be defined as a function of the desired behavior. For this, it is necessary to obtain an analytical expression of the desired objective curve in the plane x 1 , x 2 . Assume that the desired time evolution for x 2 is

x * 2 = A sin ωt + B ( 25
)
where A, B and ω take pre-specified values to obtain the desired evolution for v C and i L using (10)-( 12), ( 13) and ( 14). Time shift need not to be taken into account. Assume that the desired steady state for x 1 can be approximated by

x * 1 = aα 0 + α 1 cos ωt + β 1 sin ω (26)
Substituting ( 25) and ( 26) in (17), neglecting the second order harmonics and equating the bias, sin ωt and cos ωt the parameters α 0 , α 1 and β 1 can be obtained. The expressions appear in [START_REF] Gordillo | Autonomous oscillation generation in electronic converters[END_REF] and are omitted here for brevity.

The only question that remains now is to show that the desired behavior for y 1 and y 2 is an ellipse and to define the ellipse parameters (ω, y 10 , y 20 and µ) in terms of the desired behavior for x 2 . For this, we have to obtain the desired evolution for y 1 and y 2 applying the change of variables ( 18)-( 19) to ( 25) and (26).

y 1 = 1 2 [(aα 0 + α 1 sin ωt + β 1 cos ωt) 2 +(A 1 sin ωt + B 1 ) 2 ] ( 27
)
y 2 = aα 0 + α 1 sin ωt + β 1 cos ωt -a(A 1 sin ωt + B 1 ) 2 +a(A 1 sin ωt + B 1 )z 2 + y 20 (28)
Expanding these expressions in Fourier terms yield

y 1 = y (0) 1 + y (11) 1 cos ωt + y (12) 1
sin ωt + y Equating the terms an expression for the Fourier coefficients can be obtained. The expressions appear in [START_REF] Gordillo | Autonomous oscillation generation in electronic converters[END_REF]. Assuming that the double frequency terms, y can be neglected, these expressions can be approximated by an ellipse in the plane y 1 , y 2 since, using the expressions previously obtained for α 0 , α 1 and β 1 ,

ωy (11) 1 = -y (12) 2 (31) ωy (12) 1 = y (11) 2 (32)
The parameters of this ellipse are given by

y 10 = y (0) 1 (33) y 20 = y (0) 2 (34) µ = ω 2 ((y (11) 1 ) 2 + (y (12) 1 ) 2 ) (35)

D. Control Law for the Full Converter

In this section the previous control law is extrapolated to consider that the boost inverter is composed of two dcdc converters and, thus, it has two control signals. The model of the system is

L 1 di L1 dt = -u 1 v C1 + V in (36) C 1 dv c1 dt = u 1 i L1 - v C1 R + v C2 R (37) L 2 di L2 dt = -u 2 v C2 + V in (38) C 2 dv c2 dt = u 2 i L2 - v C1 R + v C2 R (39)
By comparison of systems (36)-( 39) and ( 8)-( 9) we can notice a similar structure for the pairs of current and voltage of both boost dc-dc converters. Therefore, the two control laws are easy to be obtained. The first control law u 1 is almost the same expression as (24), the only difference is that z 2 must be replaced by x 4 . Control law u 2 is obtained by symmetry. The control laws are

u 1 = 1 + 2a 2 1 x 2 2 -3a 2 1 x 2 x 4 + a 2 1 x 2 4 + a 2 1 x 2 ẋ4 x 2 + 2a 1 x 1 x 2 -a 1 x 4 x 1 + k 1 Γ 1 (y 2 -y 20 ) + ω 2 (y 1 -y 10 ) x 2 + 2a 1 x 1 x 2 -a 1 x 4 x 1 (40)
u 2 = 1 + 2a 2 2 x 2 4 -3a 2 2 x 2 x 4 + a 2 2 x 2 2 -a 2 2 x 4 ẋ2 x 4 -2a 2 x 3 x 4 + a 2 x 2 x 3 + -k 2 Γ 2 (y 4 -y 40 ) + ω 2 (y 3 -y 30 ) x 4 -2a 2 x 3 x 4 + a 2 x 2 x 3 (41)
The expressions for derivatives ẋ2 and ẋ4 are taken directly from the normalized equations of the boost inverter.

E. Simulation Results

The following simulations are made considering

V in = 10V , R = 100Ω, L 1 = 100µH, L 2 = 100µH, C 1 = 100µF , C 2 = 100µF .
The desired frequency and voltage amplitude are 50 Hz and 40 V respectively.

In this case, as the dc-dc converter voltages must have a phase shift of 180 • the normalized desired voltages are

x * 2 = A sin ωt + B (42) x * 4 = -A sin ωt + B ( 43
)
Parameter A has to be the half of the desired output voltage amplitude and B is chosen, so that, x 2 and x 4 are always positive. In order to obtain this voltage, the parameters are A = 2 and B = 10 with ω = 0.0314 in the normalized variables x 1 , x 2 . The ellipse parameters, using the previous development, result y 10 = 51.14, y 30 = 51.14, µ 1 = µ 2 = 0.395 . On the other hand, the tuning parameters are chosen as k 1 = k 2 = 0.8 and y 20 = 0, y 40 = 0.

Figure 6 shows the results of a simulation using a sample time of 0.001s. Both dc-dc converters achieve the desired limit cycle.

Figure 7 shows the boost inverter input and output voltages. In this figure only the steady state behavior is shown. It can be seen that the desired amplitude is not achived. Indeed, the previous design does not impose that the phase shift between signals v c1 and v c2 is 180 • . Figure 8 shows that this requirement is not achieved. Next Section will deal with this problem.

IV. Voltage Synchronization

In the previous design, we found that the voltage signal did not present a phase shift of 180 • . In order to get the desired output voltage, we need to synchronize these signals. In this section, a PLL is added to achieve the desired phase shift.

A PLL is a device which causes one signal to track another one. This tracking is in frequency as well as in phase. Fig. 6. a) State spaces (x 1 , x 2 ) (solid) and (x 3 , x 4 ) (dashed); b) state spaces (y 1 , y 2 ) (solid) and (y 3 , y 4 ) (dashed). A PLL consists basically of three parts [START_REF] Hsieh | Phase-Locked Loop techniques-a survey[END_REF]- [START_REF] Abramovich | Phase-Locked Loop: a control centric tutorial[END_REF]: a phase detector (PD), a loop filter (LF) and a voltage-controlled oscillator (VCO). A functional scheme of the device is shown in Fig. 9. Signal x i is the reference signal and x 0 is the synchronized signal. The PD is a signal multiplier and it has a gain k d . The resultant product is filtered in the LF, so that, the higher frequency component is eliminated. The VCO is a frequency-modulated oscillator, and it generates a signal which is in phase quadrature with respecto to the input signal.

A. PLL Applied to the Boost DC-AC Converter

The objective is to synchronize the voltage curves with a phase shift equal to 180 • . The scheme of Fig. 10 is used. The voltage of the second dc-dc converter, x 4 , is taken as reference signal and the voltage of the first dcdc converter, x 2 , is the signal to be synchronized. The first dc-dc converter with its controller can be regarded as a VCO: the controller receives as input a frequency increment that it is ordered by the PLL. This frequency increment is added to the nominal frequency, and the resultant frequency is entered in (40). The output of the converter is a sinusoidal signal of that frequency. The PLL block diagram appears in Fig. 11. The multiplier obtains the product x * 2 × x * 4 in such a way that, see [START_REF] Hsieh | Phase-Locked Loop techniques-a survey[END_REF], its output, once filtered by a low pass filter (LPF), is a measure of the deviation of the phase shift with respect to 90 • . For this reason, one of the inputs of the multiplier, e.g. x * 2 , is obtained passing the voltage x 2 through a high pass filter (HPF) in order to eliminate its continuous component. On the other hand, x * 4 is obtained after passing x 4 through another HPF and, then, changing its sign and integrating. In this way if x 4 = B 2 +A 2 sin(ωt), then, x * 4 = -A2 ω sin ωt -π 2 +C. Constant C is eliminated by the LPF.

1) Simulation Results: The high pass filter applied are:

1.4s

s+ω for the reference signal and 1.4s s+ω+∆ω for the signal to be synchronized. The LPF is a second order Butterworth filter [START_REF] Ifeachor | Digital signal processing: a practical aproach[END_REF]:

64 • 10 -6( √ 2 2 - √ 2 2 j)( √ 2 2 + √ 2 2 j) (s + 0.008( √ 2 2 - √ 2 2 j))(s + 0.008( √ 2 2 + √ 2 2 j)) (44)
The value of the PLL gain is

K dv = 5 • 10 4 .
The results of the PLL application are shown in Fig. 12. The voltages v c1 and v c2 present a phase shift of 180 • . In Fig. 13 the boost inverter output voltage is represented. This voltage signal is compared with the ideal boost inverter output, getting a excellent result.

B. Synchronizing with the Electrical Network

In order to synchronize the boost inverter output signal with the electrical network, the voltage signals of both dcdc converters (v c1 , v c2 ) are treated with a PLL to get the aim (Fig. 14). Voltage v c1 is synchronized with the network voltage without phase shift, while voltage v c2 is synchronized with the network voltage with a phase shift of 180 • . (45)

The filter parameters and gain used in the PLLs are the same which were used previously. The performance of the synchronization of the boost dc-ac converter with the electrical supply voltage is represented in Fig. 15.

V. Conclusions

This paper presents a control strategy for the boost dc-ac converter. The method is based on energy shaping and generation of a limit cycle and does not need the introduction of time-dependent reference signals. It has been shown that the resultant controller achieves the objective provided that a phase locked loop is added. The same idea has been used in order to solve the problem of network synchronization.

Open problems are the consideration of unknown and non-resistive loads.

Fig. 1 .Fig. 2 .Fig. 3 .

 123 Fig. 1. Basic representation of the boost inverter.

Fig. 4 .Fig. 5 .

 45 Fig. 4. Symplified Boost dc-ac Converter.

Fig. 7 .Fig. 8 .

 78 Fig. 7. Output (solid) and input (dashed) voltages of the boost inverter.

Fig. 9 .

 9 Fig. 9. Basic PLL block diagram.

Fig. 10 .

 10 Fig. 10. Block diagram of boost dc-ac converter with output voltages synchronized by PLL.

Fig. 11 .

 11 Fig. 11. Conceptual block diagram of PLL applied to boost dc-ac converter.

Fig. 12 .

 12 Fig. 12. Output voltage of the first (solid) and second (dashed) boost dc-dc converters.

Fig. 13 .

 13 Fig.13. Ideal (solid) and simulated (dashed) output voltages with PLL.

Fig. 14 .

 14 Fig. 14. Conceptual block diagram of PLL applied to the boost dc-ac converter for network synchronization.

1 )

 1 Simulation Results: The network voltage isV net = 325 sin(100πt).

Fig. 15 .

 15 Fig. 15.Electrical supply voltage (solid) and simulated output voltage synchronized with PLLs (dashed).

Acknowledgments

This research has been supported by the MCyT-FEDER grant DPI2003-00429.