Cette thèse présente des contributions dans le domaine de la planification en intelligence artificielle, et ce, plus particulièrement pour une classe de problèmes qui combinent des actions concurrentes (simultanées) et de l'incertitude. Deux formes d'incertitude sont prises en charge, soit sur la durée des actions et sur leurs effets.Cette classe de problèmes est motivée par plusieurs applications réelles dont la robotique mobile, les jeux et les systèmes d'aide à la décision.Cette classe a notamment été identifiée par la NASA pour la planification des activités des rovers déployés sur Mars. Les algorithmes de planification présentés dans cette thèse exploitent une nouvelle représentation compacte d'états afin de réduire significativement l'espace de recherche. Des variables aléatoires continues sont utilisées pour modéliser l'incertitude sur le temps. Un réseau bayésien, qui est généré dynamiquement, modélise les dépendances entre les variables aléatoires et estime la qualité et la probabilité de succès des plans. Un premier planificateur, ACTUP LAN nc basé sur un algorithme de recherche à chaînage avant, prend en charge des actions ayant des durées probabilistes. Ce dernier génère des plans non conditionnels qui satisfont à une contrainte sur la probabilité de succès souhaitée. Un deuxième planificateur, ACTUP LAN, fusionne des plans non conditionnels afin de construire des plans conditionnels plus efficaces. Un troisième planificateur, nommé QUANPLAN, prend également en charge l'incertitude sur les effets des actions. Afin de modéliser l'exécution simultanée d'actions aux effets indéterminés, QUANP LAN s'inspire de la mécanique quantique où des états quantiques sont des superpositions d'états classiques. Un processus décisionnel de Markov (MDP) est utilisé pour générer des plans dans un espace d'états quantiques. L'optimalité, la complétude, ainsi que les limites de ces planificateurs sont discutées. Des comparaisons avec d'autres planificateurs ciblant des classes de problèmes similaires démontrent l'efficacité des méthodes présentées. Enfin, des contributions complémentaires aux domaines des jeux et de la planification de trajectoires sont également présentées.

El lambda-cálculo es una teoría sin tipos que interpreta las funciones como reglas, es decir, el proceso de ir de un argumento a un valor, un proceso codificado por una definición. La idea de utilizar el lambda-cálculo como un marco matemático para la descripción y el Razonamiento acerca de los sistemas computacionales es antigua. De hecho, gracias al análisis realizado por Turing, se puede afirmar que, a pesar de que su sintaxis Es muy simple, el lambda-cálculo es lo suficientemente potente para describir todas las funciones computables mecánicamente. Pero, como mostró G. Berry, la computación que captura el lambda-cálculo es esencialmente secuencial. Un desafío importante que, sobre Todo desde _males de los años ochenta, está implicando a muchos investigadores es la construcción de un marco similar al _-cálculo para la concurrencia y la comunicación entre procesos. El objetivo fundamental que guiara el trabajo que a continuación presentamos es la Formalización de un cálculo que extiende el lambda-cálculo para modelizar la concurrencia y la comunicación entre procesos. El lenguaje desarrollado se denomina lambda-cálculo Etiquetado Paralelo (LCEP). Su origen está en una propuesta inicial de H. A _t-Kaci (el _-calculo Etiquetado) que describe un lenguaje, extensión del lambda-cálculo, en el que los argumentos de las funciones se seleccionan mediante etiquetas, incluyendo tanto posiciones numéricas como simbólicas. Esta extensión es conservativa en el sentido de que, cuando el conjunto de etiquetas es el conjunto unario f1g, el lambda-cálculo Etiquetado coincide exactamente con el lambda-cálculo, condición que no se cumple en las otras propuestas que vamos a estudiar comparativamente como punto de partida. Para describir el nuevo cálculo vamos a utilizar una semántica operacional dada por un sistema de transición, a partir de la cual propondremos diferentes relaciones de equivalencia para modelar los distintos aspectos relacionados con el comportamiento operacional de los procesos. Por último, ya que la escritura directa de programas en LCEP resulta demasiado compleja en la mayoría de los casos como para pensar en _el como recurso expresivo adecuado para la programación, vamos a definir un lenguaje de más alto nivel, ALEPH, que posee los recursos expresivos deseables en programación y permite aprovechar la potencia computacional del sistema. Mostraremos como ALEPH se traduce a LCEP como código máquina y es a través de este como se realizan las ejecuciones de los programas. A lo largo del texto es importante descubrir que a través de una sintaxis razonablemente simple es posible expresar todas las características que conlleva la concurrencia dentro de un paradigma funcional / Oliver Villarroya, FJ. (1996). Extension del lambda-cálculo para la modelizacion de procesos concurrentes [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/58867

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

La biologie systémique cherche à comprendre la dynamique cellulaire qui émerge des interactions des constituantes cellulaires au cours du temps. La modélisation et la simulation sont des méthodes fondamentales de ce domaine. Nous nous inspirons de la proposition de Regev et Shapiro (2002) consistant à appliquer le pi-calcul stochastique comme langage formel de représentation de connaissances biomoléculaires. Nos études portent sur la modélisation à l´échelle moléculaire de l'expression génétique bactérienne et s'avèrent pertinentes pour des organismes supérieurs. Nos points de départs sont des études de cas concrets de la régulation de la bascule génétique du phage lambda, de la transcription et de la traduction. Ces études révèlent l'utilité de concepts de programmation tels que les objets concurrents et motivent une extension du pi-calcul stochastique avec des motifs de réception. Nous présentons une sémantique pour ce langage qui attribue des chaînes Markoviennes en temps continu aux programmes. Nous validons nos modèles par des simulations stochastiques.

La croissance des capacités de calcul des processeurs se poursuit, non plus par l'augmentation des fréquences d'horloge, mais par la multiplication d'unités de traitement (coeur) au sein des chips. Cette augmentation du nombre de coeurs par processeur induit un partage des autres omposants de la machine entre les différentes requêtes. En outre, les applications parallèles provenant du calcul scientifique s'efforcent d'exploiter au maximum les ressources d'une architecture parallèle. La compréhension du partage de ressource devient un des défis majeurs pour utiliser efficacement ces architectures.<br />Ces nouveaux comportements de partage de ressources, ainsi produits, sont difficiles à interpréter et à prédire. Dans cette thèse, nous avons étudié le problème du partage du réseau. Les grappes de calcul utilisent des réseaux dédiés tels que Gigabit Ethernet, Myrinet ou Quadrics. L'exécution simultanée des tâches d'une application entraîne des accès concurrents sur la ressource réseau. Leurs effets conduisent à une perte de performance qui découle du partage de la bande passante réseau entre communications.<br />Suivant ce contexte, nous présentons une analyse fine des comportements concurrents sur les architectures : Quadrics, Myrinet et Gigabit Ethernet. Cette analyse conduit à la définition de modèles prédictifs basés sur la notion de partage de la bande passante. En outre, nous montons que l'intégration de ces modèles dans une simulation permet de prédire les impacts dûs à la concurrence entre communications MPI résultantes de l'exécution d'applications scientifiques. La prédiction des comportements concurrents donne lieu, au niveau scientifique et technique, à une meilleure connaissance des besoins des applications et, au niveau industriel, à la proposition de solutions de grappes adaptées aux besoins de leurs clientèles.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Afin de pouvoir répondre au mieux aux différents appels d'offres, les constructeurs de grappe de calcul ont besoin d'outils et de méthodes permettant d'aider au mieux la prise de décisions en terme de design architectural. Nos travaux se sont donc intéressés à l'estimation des temps de calcul et à l'étude de la congestion sur le réseau InfiniBand. Ces deux problèmes sont souvent abordés de manière globale. Néanmoins, une approche globale ne permet pas de comprendre les raisons des pertes de performance liées aux choix architecturaux. Notre approche s'est donc orientée vers une étude plus fine. Pour évaluer les temps de calcul, la démarche proposée s'appuie sur une analyse statique ou semistatique du code source afin de le découper en blocs, avant d'effectuer un micro-benchmarking de ces blocs sur l'architecture cible. Pour l'estimation des temps de communication, un modèle de répartition de bande passante pour le réseau InfiniBand a été développé, permettant ainsi de prédire l'impact lié aux communications concurrentes. Ce modèle a ensuite été intégré dans un simulateur pour être validé sur un ensemble de graphes de communication synthétiques et sur l'application Socorro.

Els mètodes de verificació formal s'estan usant cada vegada més en la indústria per establir la correctessa i trobar els errors en models de sistemes; per exemple la descripció de hardware, protocols, programes distribuïts, etc. En particular, els verificadors de models ho fan automàticament per sistemes d'estats finits, per-o estan limitats degut al problema de l'explosió d'estats; i la verificació formal interactiva, l'àrea d'aquesta tesi, es necessita.L'enfocament de la verificació automàtica treballa sobre el sistema de transicions del model, el qual defineix la seva semàntica. Aquest sistema de transicions té sovint molts estats, i sempre una mida gran comparada amb la mida del model del sistema, el qual és sempre infinit. Aquestes consideracions suggereixen un enfocament de verificació estàtica com els d'aquesta tesi, evitant els sistemes de transicions, treballant directament sobre el model del sistema, en principi, la complexitat computacional hauria de ser menor. L'enfocament estàtic d'aquest treball es fa sobre models de sistemes expressats en notació imperativa amb paral·lelisme explícit, sentències de comunicacions síncrones i variables d'emmagatzematge locals.Els raonaments d'equivalència són molt empleats per números, matrius i altres camps. Tanmateix, per programes imperatius amb paral·lelisme, comunicacions i variables, encara que potencialment sigui un mètode de verificació molt intuïtiu, no han estat massa explorats. La seqüencialització formal via l'eliminació de comunicacions internes, l'àrea d'aquesta tesi, és una demostració basada en el raonament estàtic d'equivalències que, donat que disminueix la magnitud del vector d'estats, pot complementar altres mètodes de demostració. Es basa en l'aplicació d'un conjunt de lleis , apropiades per tal propòsit, com reduccions de reescriptura del model del sistema. Aquestes depenen de la noció d'equivalència i de les suposicions de justícia.Aquesta tesi contribueix a la quasi inexplorada àrea de l'eliminació de comunicacions formal i seqüencialització de models de sistema. Les lleis estan definides sobre una equivalència feble: equivalència d'interfície. L'eliminació de comunicacions est-a limitada a models sense seleccions, per exemple models en els quals les comunicacions internes no estan dins de l'àmbit de sentències de selecció. Aplicacions interessants existeixen dins d'aquest marc. Les lleis són vàlides només per justícia feble o sense justícia. Aquesta ha estat desenvolupada seguint la semàntica proposada per Manna i Pnueli per a sistemes reactius [MP91, MP95]. S'han formulat les condicions d'aplicabilitat per les lleis de la pròpia eliminació de comunicacions. A més a més, es proposa un procediment de construcció de demostracions per l'eliminació de comunicacions, el qual intenta aplicar automàticament les lleis de la eliminació. També s'ha dissenyat un conjunt de procediments de transformació, els quals garanteixen que la transformació equivalent sempre correspon a l'aplicació d'una seqüència de lleis. Degut a que la construcció de les demostracions és impracticable, normalment impossible, sense l'ajuda d'una eina, s'ha desenvolupat un demostrador interactiu per la construcció semiautomàtica de la seqüencialització de models de sistemes i demostracions d'eliminació. Tant els procediments de transformació com els de l'eliminació de comunicacions estan integrats en l'eina. Amb l'ajuda del demostrador s'ha construït la demostració de seqüencialització d'un model, no trivial, de processador pipeline. Per aquest exemple s'ha assolit una reducció, respecte del model original, de la cota superior del nombre d'estats de 2&#8722;672.Malgrat l'enorme quantitat d'esforç dedicat a l'àrea, abans i durant la tesi, encara queda molt treball per a que l'eliminació de comunicacions i la seqüencialització sigui realment un mètode pràctic. No obstant els resultats d'aquesta tesi han establert els fonaments i han donat l'estímul necessari per continuar l'esforç. / Los métodos de verificación formal se están usando cada vez más en la industria para establecer la corrección y encontrar los errores en modelos de sistemas; por ejemplo, la descripción de hardware, protocolos, programas distribuidos, etc. En particular, los verificadores de modelos lo hacen automáticamente para sistemas de estados finitos, pero están limitados debido al problema de la explosión de estados; y la verificación formal interactiva, el área de esta tesis, es necesaria.El enfoque de la verificación automática trabaja sobre el sistema de transiciones del modelo, el cual define su semántica. Este sistema de transiciones tiene a menudo muchos estados, y siempre un tamaño grande comparado con el tamaño del modelo del sistema, el cual es siempre infinito. Estas consideraciones sugieren un enfoque de verificación estática como los de esta tesis, evitando los sistemas de transiciones, trabajando directamente sobre el modelo del sistema, en principio, la complejidad computacional tendría que ser menor. El enfoque estático de este trabajo se lleva a cabo sobre modelos de sistemas expresados en notación imperativa con paralelismo explícito, sentencias de comunicaciones síncronas y variables de almacenamiento locales.Los razonamientos de equivalencia son muy empleados para números, matrices y otros campos. Sin embargo, para programas imperativos con paralelismo, comunicaciones y variables, aún teniendo la potencialidad de ser un método de verificación muy intuitivo, no han sido muy explorados. La secuencialización formal vía la eliminación de comunicaciones internas, el área de esta tesis, es una demostración basada en el razonamiento estático de equivalencias que, ya que disminuye la magnitud del vector de estados, puede complementar otros métodos de demostración. Se basa en la aplicación de un conjunto de leyes, apropiadas para tal propósito, como reducciones de reescritura del modelo del sistema. Éstas dependen de la noción de equivalencia y de las suposiciones de justicia.Esta tesis contribuye a la casi inexplorada área de la eliminación de comunicaciones formal y secuencialización de modelos de sistema. Las leyes están definidas sobre una equivalencia débil: equivalencia de interfaz. La eliminación de comunicaciones está limitada a modelos sin selecciones, por ejemplo modelos en los cuales las comunicaciones internas no están dentro del ámbito de sentencias de selección. Aplicaciones interesantes existen dentro de este marco. Las leyes son válidas sólo para justicia débil o sin justicia. Ésta ha sido desarrollada siguiendo la semántica propuesta por Manna y Pnueli para sistemas reactivos [MP91, MP95]. Se han formulado las condiciones de aplicabilidad para las leyes de la propia eliminación de comunicaciones. Además, se propone un procedimiento de construcción de demostraciones para la eliminación de comunicaciones, el cual intenta aplicar automáticamente las leyes de la eliminación. También se ha diseñado un conjunto de procedimientos de transformación, los cuales garantizan que la transformación equivalente siempre corresponde a la aplicación de una secuencia de leyes. Debido a que la construcción de las demostraciones es impracticable, normalmente imposible, sin la ayuda de una herramienta, se ha desarrollado un demostrador interactivo para la construcción semiautomática de la secuencialización de modelos de sistemas y demostraciones de eliminación. Tanto los procedimientos de transformación como los de la eliminación de comunicaciones están integrados en la herramienta. Con la ayuda del demostrador se ha construido la demostración de secuencialización de un modelo, no trivial, de procesador pipeline. Para este ejemplo se ha logrado una reducción, respecto del modelo original, de la cota superior del número de estados de 2&#8722;672.A pesar de la enorme cantidad de esfuerzo dedicado al área, antes y durante esta tesis, todavía queda mucho trabajo para que la eliminación de comunicaciones y la secuencialización sea realmente un método práctico. Sin embargo los resultados de esta tesis han establecido los cimientos y han dado el estímulo necesario para continuar el esfuerzo. / Formal verification methods are increasingly being used in industry to establish the correctness of, and to find the flaws in, system models; for instance, descriptions of hardware, protocols, distributed programs, etc. In particular, model checking does that automatically for finite-state systems, but it is limited in scope due to the state explosion problem; and interactive formal verification, the broad area of this thesis, is needed.Automatic verification approaches work on the transition system of the model, which defines its semantics. This transition system has often infinitely many states, and always a large size compared to the size of the system model, which is always finite. These considerations suggest that static verification approaches such as those of this thesis, avoiding the transition system, working directly on the system model would have less computational complexity, in principle. The static approach of this work is carried out on system models expressed in imperative notations with explicit parallelism and synchronous communication statements, and with local storage variables.Equivalence reasoning is heavily used for numbers, matrices, and other fields. However, for imperative programs with parallelism, communications, and variables, although having the potentiality of being a very intuitive verification method, it has not been much explored. Formal sequentialization via internal communication elimination, the area of this thesis, is a static equivalence reasoning proof that, since it decreases the size of the state vector, could complement other proof methods. It is based on the application of a set of laws, suitable for that purpose, as rewriting reductions to a system model. These proofs need both proper communication elimination laws and auxiliary basic laws. These depend on the notion of equivalence and on the fairness assumptions.This thesis contributes to the almost unexplored area of formal communication elimination and system model sequentialization. The laws are defined over a weak equivalence: interface equivalence. Communication elimination is confined to selection-free models, i.e. models none of whose inner communications are within the scope of selection statements. Interesting applications already exist within this framework. The laws are valid only with weak fairness or no fairness. It has been developed following the same semantics as Manna and Pnueli for reactive systems [MP91, MP95]. Applicability conditions for the proper communication elimination laws are derived. In addition, a communication elimination proof construction procedure, which attempts to apply the elimination laws automatically is proposed. A set of transformation procedures, guaranteeing that the equivalence transformation always corresponds to the application of a sequence of laws have been designed as well. Since the construction of elimination proofs is impractical, even impossible, without a tool, an interactive prover for semi-automatic construction of system model sequentialization and elimination proofs has been developed. Both transformation and communication elimination procedures are integrated within the tool. As a non-trivial example, a sequentialization proof of a pipelined processor model, has been constructed with the help of the prover. Areduction, with respect to the original model, of 2&#8722;672 on the upper bound on the number of states has been achieved in this example.In spite of the huge amount of effort already devoted to the area, before and during this thesis, much work still needs to be done until communication elimination and sequentialization become a practical method. Nevertheless the results of this thesis have established its foundations and given the necessary encouragement for continuing the effort.

Ces travaux portent sur la conception multidisciplinaire de systèmes intégrés. Ces systèmes sont soumis à un nombre d’exigences toujours croissant, entraînant des besoins en termes d’intégration fonctionnelle et spatiale. Ces différents types d’intégration relative au produit sont également la source d’une complexité organisationnelle, provenant à la fois de la multitude d’acteurs réalisant différentes activités d’ingénierie, mais également de la diversité des domaines impliqués, désignée dans ce manuscrit par « intégration multidisciplinaire ». Pour favoriser cette intégration multidisciplinaire, les phases de « conception préliminaire » et de « conception détaillée » ont été identifiées comme déterminantes, notamment car elles se caractérisent par la collaboration de nombreux experts, manipulant un grand nombre de données techniques de définition. Les systèmes conçus lors de conceptions multidisciplinaires restent faiblement intégrés. Cela est en partie dû au cloisonnement entre les disciplines et à un mode d’organisation projet basé sur une planification prédominante, caractérisé notamment par une diffusion de l’information principalement descendante (top-down). Afin d’assurer une meilleure collaboration entre ces différentes disciplines, de permettre des prises de décision éclairées par des indicateurs opérationnels et de pouvoir analyser et mieux comprendre les phénomènes d’intégration des expertises, l’introduction d’une méthode inspirée des principes fondateurs des méthodes agiles est proposée pour la conception collaborative de systèmes intégrés.La contribution de ces travaux s’appuie sur trois concepts complémentaires. Le premier, intitulé Collaborative Actions Framework correspond à un cadre de collaboration opérationnelle autour d’actions. Un des objectifs de ce framework est de faciliter la collaboration des acteurs des projets de conception, quelle que soit leur origine disciplinaire, mais également d’assurer une traçabilité entre les prises de décision et les corrections/modifications apportées sur les données techniques. Cette traçabilité est rendue possible grâce aux liens existants avec le second concept intitulé Workspace. Apportant un nouvel éclairage sur les possibilités offertes par la collaboration autour de ces espaces de collaboration, ce concept offre un certain nombre de possibilités,notamment la mise en commun continue des travaux, l’intégration multidisciplinaire et la validation des modifications. Les échanges de données techniques entre les workspaces, ou le travail simultané sur les mêmes données techniques, s’appuient quant à eux sur la possibilité de pouvoir gérer de façon parallèle différentes versions d’une même donnée technique. Ces possibilités sont proposées par le troisième concept, intitulé branch & merge, qui permet également à différents acteurs de travailler simultanément sur les mêmes données. Enfin, ces trois concepts sont ensuite illustrés par l’intermédiaire d’un démonstrateur composé d’un scénario et d’un prototype informatique. Un produit mécatronique, combinaison synergique et systémique de la mécanique, de l'électronique et de l'informatique temps réel, est utilisé afin d’illustrer les possibilités offertes par nos travaux en termes d'intégration multidisciplinaire lors de la conception collaborative. / This work focuses on the multidisciplinary and collaborative design of integrated systems. These systems are subject to an ever increasing number of requirements, leading to the need for more comprehensive functional and spatial integration. These different types of product integration are also at the origin of organizational complexity. This complexity arises not only from the great number of actors performing various engineering activities but also from the diversity of disciplines involved (designated in this manuscript as “multidisciplinary integration”). To encourage this multidisciplinary integration, “preliminary design” and “detailed design” have been identified as the most significant steps, especially since they are characterized by the collaboration of multiple experts handling a large number of product definition’ technical data. Systems that have been designed thanks to multidisciplinary approaches are generally poorly integrated. This is partially due to the compartmentalization of disciplines, as well as to the “project-planned” method, where project planning is predominant and information is mainly spread out “top-down”. To ensure better cooperation between the various disciplines, to enable decision making based on operational indicators and to analyze and understand the multidisciplinary integration processes, a method inspired by the founding principles of agile methods (the agile manifesto) is proposed for the collaborative design of integrated systems. This work is based on three complementary concepts. The first is, the Collaborative Actions Framework, an operational framework for collaboration around actions. One objective of this framework is to improve the collaboration among designers, whatever their disciplinary origin. It also ensures traceability between decision making and corrections/changes made to technical data. This traceability is made possible by the useof the second concept, called Workspace. Even if this term is already well known, we propose a new definition/usage to transform it into collaboration spaces. This concept offers great possibilities, including the continuous delivering/sharing of experts’ contributions, multidisciplinary integration and change validation. The exchange of technical data between workspaces, or simultaneous work on the same data, relies on the ability to manage several parallel versions of the same item into a single datamanagement system. These opportunities are offered by the third concept, called Branch & Merge. Finally, these three concepts are illustrated through a scenario and a computer prototype. A mechatronic product, “the synergistic combination of mechanical and electrical engineering, computer science, and information technology” (Harashima et al., 1996), is used to illustrate the opportunities offered by our work in terms of multidisciplinary integration during collaborative design.

Le coauteur est traditionnellement défini en droit pénal comme l’individu qui, agissant avec un autre, réunit sur sa tête l’ensemble des éléments constitutifs de l’infraction. Pourtant, il est permis de douter de la pertinence de cette affirmation tant la jurisprudence comme la doctrine en dévoient le sens.En réalité, loin d’être cantonnée à une simple juxtaposition d’actions, la coaction doit être appréhendée comme un mode à part entière de participation à l’infraction. En effet, elle apparaît comme un titre d’imputation à mi-chemin entre l’action et la complicité, auxquelles elle emprunte certains caractères. Autrement dit, elle se révèle être un mode de participation à sa propre infraction. Surtout, son particularisme est assuré par l’interdépendance unissant les coauteurs : parce que chacun s’associe à son alter ego, tous sont placés sur un pied d’égalité. Ces différents éléments, qui se retrouvent dans sa notion et dans son régime, permettent ainsi d’affirmer la spécificité de la coaction tout en renforçant la cohérence entre les différents modes de participation criminelle. / In criminal law, the co-perpetrator is classically presented as an individual who, acting jointly with another, gathers all the constitutive elements of the offence. However, one may harbor doubts concerning the relevance of this assertion since both case law and legal scholars denature its meaning.Actually, far from being limited to a mere juxtaposition of perpetrations, co-perpetration must be understood as a full mode of participation in the offence. Indeed, it appears as a form of imputation halfway between perpetration and complicity, from which it borrows some characteristics. In other words, it proves to be a mode of participation in one’s own offence. Above all, its particularism is provided by the interdependence between the co-perpetrators : because each of them joins forces with his alter ego, all are placed on an equal footing. These elements, which are found both in it’s concept and in it’s regime, demonstrate thereby the specificity of co-perpetration while strengthening the coherence of the different modes of criminal participation.