Dans cette thèse, nous avons tout d'abord fait une étude de l'état de l'art dans les différents domaines des procédés (métier, logiciel, militaire, médical, etc) afin d'identifier et de catégoriser les principales propriétés à garantir. À partir de cette étude, nous avons défini une bibliothèque de propriétés générique et paramétrable pour tout modèle de procédé. Ensuite, nous avons défini un framework pour la vérification de procédés appelé Alloy4PV. Il utilise un sous-ensemble des diagrammes d'activités UML 2 comme langage de modélisation. Afin d'effectuer la vérification de procédés, nous avons (1) défini un modèle formel des diagrammes d'activités basé sur la sémantique fUML (le standard de l'OMG donnant une sémantique à un sous-ensemble de UML) en utilisant la logique de premier ordre, (2) implémenté cette formalisation en utilisant le langage Alloy afin d'effectuer du model-checking borné, et (3) automatisé, dans un outil graphique intégré à Eclipse, la possibilité d'exprimer et de vérifier des propriétés sur toutes les perspectives du procédé. / In this thesis, we realized a study of the start-of-the-art on different process domains (business, software, military, medical, etc.). The aim was to identify and categorize critical properties that can be verified on any process model. This study resulted in a library of generic and configurable properties. As a second step, we have defined a framework for process verification called Alloy4PV. This framework uses a subset of UML 2 Activity Diagram as a process modeling language. For process verification, (1) we defined a formal model of UML 2 Activity Diagram based on the fUML semantics, the OMG standard that gives a semantic to a subset of UML 2. This was achieved using first-order logic, (2) we implemented this formalization using the Alloy language in order to perform bounded model-checking, and (3) we automatized in a graphical tool integrated to Eclipse, the possibility to express and verify properties on all the perspectives of a process model. This contribution resulted in a tool which is under evaluation by our MerGE project’s partners and to five publications in conferences proceedings.

Expressiveness, and more recently, succinctness, are two central concerns of finite model theory and descriptive complexity theory. Succinctness is particularly interesting because it is closely related to the complexity-theoretic trade-off between parallel time and the amount of hardware. We develop new bounds on the expressiveness and succinctness of first-order logic with two variables on finite words, present a related result about the complexity of the satisfiability problem for this logic, and explore a new approach to the generalized star-height problem from the perspective of logical expressiveness. We give a complete characterization of the expressive power of first-order logic with two variables on finite words. Our main tool for this investigation is the classical Ehrenfeucht-Fra¨ıss´e game. Using our new characterization, we prove that the quantifier alternation hierarchy for this logic is strict, settling the main remaining open question about the expressiveness of this logic. A second important question about first-order logic with two variables on finite words is about the complexity of the satisfiability problem for this logic. Previously it was only known that this problem is NP-hard and in NEXP. We prove a polynomialsize small-model property for this logic, leading to an NP algorithm and thus proving that the satisfiability problem for this logic is NP-complete. Finally, we investigate one of the most baffling open problems in formal language theory: the generalized star-height problem. As of today, we do not even know whether there exists a regular language that has generalized star-height larger than 1. This problem can be phrased as an expressiveness question for first-order logic with a restricted transitive closure operator, and thus allows us to use established tools from finite model theory to attack the generalized star-height problem. Besides our contribution to formalize this problem in a purely logical form, we have developed several example languages as candidates for languages of generalized star-height at least 2. While some of them still stand as promising candidates, for others we present new results that prove that they only have generalized star-height 1.

Cette thèse se concentre autour du problème de l'évaluation des requêtes. Étant donné une requête q et une base de données D, l'objectif est de calculer l'ensemble q(D) des nuplets résultant de l'évaluation de q sur D. Toutefois, l'ensemble q(D) peut être plus grand que la base de données elle-même car elle peut avoir une taille de la forme n^l où n est la taille de la base de données et l est l'arité de la requête. Calculer entièrement q(D) peut donc nécessiter plus que les ressources disponibles. L'objectif principal de cette thèse est une solution particulière à ce problème: une énumération de q(D) avec un délai constant. Intuitivement, cela signifie qu'il existe un algorithme avec deux phases: une phase de pré-traitement qui fonctionne en temps linéaire dans la taille de la base de données, suivie d'une phase d'énumération produisant un à un tous les éléments de q(D) avec un délai constant (indépendant de la taille de la base de données) entre deux éléments consécutifs. En outre, quatre autres problèmes sont considérés: le model-checking (où la requête q est un booléen), le comptage (où on veut calculer la taille |q(D)|), les tests (où on s'intéresse à un test efficace pour savoir si un uplet donné appartient au résultat de la requête) et la j-ième solution (où on veut accéder directement au j-ième élément de q(D)). Les résultats présentés dans cette thèse portent sur les problèmes ci-dessus concernant: - les requêtes du premier ordre sur les classes de structures de degré borné, - les requêtes du second ordre monadique sur les classes de structures de largeur d'arborescente bornée, - les requêtes du premier ordre sur les classes de structures avec expansion bornée.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

Deux groupes sont dits élémentairement équivalents s'ils satisfont les mêmes énoncés du premier ordre dans le langage des groupes. Aux environs de l'année 1945, Tarski posa la question suivante, connue désormais comme le problème de Tarski : les groupes libres non abéliens sont-ils élémentairement équivalents ? Une réponse positive à cette fameuse question fut apportée plus d'un demi-siècle plus tard par Sela, et en parallèle par Kharlampovich et Myasnikov, comme le point d'orgue de deux volumineuses séries de travaux. Dans la foulée, Sela généralisa aux groupes hyperboliques sans torsion, dont les groupes libres sont des représentants emblématiques, les méthodes de nature géométrique qu'il avait précédemment introduites à l'occasion de son travail sur le problème de Tarski. Les résultats rassemblés ici s'inscrivent dans cette lignée, en s'en démarquant toutefois dans la mesure où ils traitent des théories du premier ordre des groupes hyperboliques en présence de torsion. Dans un premier chapitre, on démontre, entre autres, que tout groupe de type fini qui est élémentairement équivalent à un groupe hyperbolique est lui-même hyperbolique. On démontre ensuite que les groupes virtuellement libres sont presque homogènes, ce qui signifie que deux éléments qui sont indiscernables du point de vue de la logique du premier ordre sont dans la même orbite sous l'action du groupes des automorphismes du groupe ambiant, à une indétermination finie près. Enfin, on donne une classification complète des groupes virtuellement libres de type fini du point de l'équivalence élémentaire à deux quantificateurs. / Two groups are said to be elementarily equivalent if they satisfy the same first-order sentences in the language of groups, that is the same mathematical statements whose variables are only interpreted as elements of a group. Around 1945, Tarski asked the following question : are non-abelian free groups elementarily equivalent? An affirmative answer to this famous Tarski's problem was given in 2006 by Sela and independently by Kharlampovich and Myasnikov, as the culmination of two voluminous series of papers. Then, Sela gave a classification of all finitely generated groups that are elementarily equivalent to a given torsion-free hyperbolic group. The results contained in the present thesis fall into this context and deal with first-order theories of hyperbolic groups with torsion. In the first chapter, we prove that any finitely generated group that is elementarily equivalent to a hyperbolic group is itself a hyperbolic group. Then, we prove that virtually free groups are almost homogeneous, meaning that elements are almost determined up to automorphism by their type, i.e. the first-order formulas they satisfy. In the last chapter, we give a complete classification of finitely generated virtually free groups up to elementary equivalence with two quantifiers.

This paper analyzes relationships between the roles of descriptions and actions in large scale, open ended, geographically distributed, concurrent systems. Rather than attempt to deal with the complexities and ambiguities of currently implemented descriptive languages, we concentrate our analysis on what can be expressed in the underlying frameworks such as the lambda calculus and first order logic. By this means we conclude that descriptions and actions complement one another: neither being sufficient unto itself. This paper provides a basis to begin the analysis of the very subtle relationships that hold between descriptions and actions in Open Systems.

Specification for process oriented applications tends to use languages that suffer from infinite, intractable or unpredictably irregular state spaces that thwart exhaustive searches by verification heuristics. However, conceptual schemas based on FOL, offer techniques for both integrating and verifying specifications in finite spaces. It is therefore of interest to transform process based specifications into conceptual schemata. Process oriented languages have an additional drawback in that reliable inputs to the integration of diverse specifications can result in unreliable outputs. This problem can more easily be addressed in a logic representation in which static and dynamic properties can be examined separately. The first part of the text describes a translation method from the process based language SDL, to first order logic. The usefulness of the method for industrial application has been demonstrated in an implementation. The method devised is sufficiently general for application to other languages with similar characteristics. Main contributions consist of: formalising the mapping of state transitions to event driven rules in dynamic entity-relationship schemas; analysing the complexity of various approaches to decomposing transitions; a conceptual representation of the source language that distinguishes meta- and object models of the source language and domain respectively. The second part of the text formally describes a framework for the integration of schemata that allows the exploration of their properties in relation to each other and to a set of integration assertions. The main contributions are the formal framework; an extension to conflicts between agents in a temporal action logic; complexity estimates for various integration properties. / QC 20101004

Με σκοπό την ενίσχυση του μαθήματος Τεχνητή Νοημοσύνη στο τμήμα Μηχανικών Η/Υ και Πληροφορικής της Πολυτεχνικής σχολής του Πανεπιστημίου Πατρών έχει δημιουργηθεί από την Ομάδα Τεχνητής Νοημοσύνης το πρωτότυπο για ένα Ευφυές Σύστημα Διδασκαλίας Τεχνητής Νοημοσύνης (ΣΔΤΝ). Το σύστημα αυτό, ανάμεσα στα άλλα, διδάσκει την Κατηγορηματική Λογική ως γλώσσα Αναπαράστασης Γνώσης και Αυτόματου Συλλογισμού. Πρόκειται για ένα σύστημα που προσαρμόζεται, επιτρέποντας στους φοιτητές να επιλέγουν οι ίδιοι τον ρυθμό και το επίπεδο μάθησης. Ένα από τα θέματα που διαπραγματεύεται το σύστημα είναι και η μετατροπή από προτάσεις φυσικής γλώσσας (ΦΓ) σε εκφράσεις Κατηγορηματικού Λογισμού Πρώτης Τάξεως (ΚΛΠΤ). Επειδή η διαδικασία αυτή δεν είναι αυτοματοποιήσιμη, ο φοιτητής δεν μπορεί να πάρει κάποια βοήθεια ή υπόδειξη από το σύστημα, κατά τη διάρκεια μιας τέτοιας άσκησης, πριν δώσει την τελική του απάντηση. Γι’ αυτό, στα πλαίσια του ΣΔΤΝ αποφασίστηκε να ενσωματωθεί μια επιπλέον δυνατότητα: να μετατρέπει εκφράσεις ΚΛΠΤ τις οποίες δημιουργεί ο φοιτητής, στην προσπάθειά του να λύσει μια τέτοια άσκηση, σε προτάσεις ΦΓ. Σκοπός της λειτουργίας αυτής είναι να χρησιμοποιηθεί σαν ανατροφοδότηση από το σύστημα στον φοιτητή, προκειμένου ο τελευταίος να αξιολογήσει την απάντησή του, πριν την καταθέσει σαν τελική απάντησή στην άσκηση. Για την υλοποίηση της παραπάνω δυνατότητας ξεκίνησε η ανάπτυξη ενός συστήματος βασισμένου σε κανόνες, του FOLtoNL (First Order Logic to Natural Language). Στόχος του συστήματος ήταν η επιτυχής μετατροπή εκφράσεων ΚΛΠΤ σε ΦΓ. Το FOLtoNL υλοποιήθηκε σε Jess, μια γλώσσα προγραμματισμού με κανόνες (γραμμένη εξ’ ολοκλήρου σε Java) και αξιολογήθηκε με βάση τα αποτελέσματά του σε ειδικά σχεδιασμένο σύνολο εκφράσεων ΚΛΠΤ. / To help teaching the course of Artificial Intelligence in Computer Engineering and Informatics Department of Patras University, a web-based intelligent tutoring system, called Artificial Intelligence Teaching System (AITS), was created. Among other things, AITS teaches Predicate Logic as a Knowledge Representation and Automated Reasoning language and is an adapting system, allowing students to choose themselves the teaching rate and level. One of the issues that AITS deals with is the conversion of natural language (NL) sentences into First-Order Logic (FOL) formulas. Given that this is a non-automated process, it is difficult to give some hints to the students-users during their effort to convert an “unknown” (to the system) NL sentence into a FOL formula. However, some kind of help could be provided, if the system could translate (after checking its syntax) the proposed by the student FOL formula into a NL sentence. The student then will be able to compare the initial NL sentence with the one that its FOL formula corresponds to. In this way, it is easier to see whether his/her proposed FOL formula is compatible with the given NL sentence and perhaps make some amendments, before submitting the final answer. FOLtoNL (First Order Logic to Natural Language) is a rule-based system that converts FOL formulas into NL in order to provide the functionality described above. It uses the expert systems approach alongside natural language processing aspects. FOLtoNL is implemented in Jess (an expert system shell written in Java) and has been evaluated via an appropriately created set of FOL expressions.

Les réseaux biologiques, notamment les réseaux de signalisation déclenchés par les hormones, sont extrêmement complexes. Les méthodes expérimentales à haut débit permettent d’aborder cette complexité, mais la prise en compte de l’ensemble des données générées requiert la mise au point de méthodes automatiques pour la construction des réseaux. Nous avons développé une nouvelle méthode d’inférence reposant sur la formalisation, sous forme de règles logiques, du raisonnement de l’expert sur les données expérimentales. Cela nécessite la constitution d’une base de connaissances, ensuite exploitée par un moteur d’inférence afin de déduire les conclusions permettant de construire les réseaux. Notre méthode a été élaborée grâce au réseau de signalisation induit par l’hormone folliculo-stimulante dont le récepteur fait partie de la grande famille des récepteurs couplés aux protéines G. Ce réseau a également été construit manuellement pour évaluer notre méthode. Un contrôle a ensuite été réalisé sur réseau induit par le facteur de croissance épidermique, se liant à un récepteur tyrosine kinase, de façon à montrer que notre méthode est capable de déduire différents types de réseaux de signalisation. / Biological networks, including signalling networks induced by hormones, are very complex. High-throughput experimental methods permit to approach this complexity, but to be able to use all generated data, it is necessary to create automatical inference methods to build networks. We have developped a new inference method based on the formalization of the expert’s reasoning on experimental data. This reasoning is converted into logical rules. This work requires the creation of a knowledge base which is used by an inference engine to deduce conclusions to build networks. Our method has been elaborated by the construction of the signalling network induced by the follicle stimulating hormone whose receptor belongs to the G protein-coupled receptors family. This network has also been built manually to assess our method. Then, a test has been done on the network induced by the epidermal growth factor, which binds to a tyrosine kinase receptor, to demonstrate the ability of our method to deduce differents types of signaling networks.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.