Depuis l'antiquité jusqu'à aujourd'hui, le domaine de la logique a gagné une importance remarquable et contribue désormais à de nombreuses autres branches, telles que la philosophie, les mathématiques, la fabrication de matériel informatique, la linguistique, l'informatique, l'intelligence artificielle, etc. À chacun de ces scénarios correspondent des besoins spécifiques, qui vont d'exigences très concrètes, telles qu'une méthode d'inférence efficace, à des propriétés théoriques plus abstraites, telles qu'un système d'axiomes élégant. Étant donnée cette grande diversité d'utilisations, une palette hétéroclite de langages formels a été développée. Pendant de nombreuses années, les langages classiques (notamment la logique du premier ordre) étaient la seule alternative concevable, mais cet assortiment d'applications a rendu d'autres types de logiques également désirables dans de nombreuses situations. Imaginez que l'heure de choisir une logique pour une tâche spécifique arrive. Comment choisir la plus appropriée? Quelles propriétés devrions-nous rechercher? Comment "mesurer'' une logique par rapport aux autres? Ce sont des questions difficiles, et il n'existe pas de recette générale à suivre. Dans cette thèse, nous allons simplement restreindre ces questions à une famille particulière de logiques, et dans ce contexte, nous explorerons les aspects théoriques qui aideront à répondre à ces préoccupations. Beaucoup peut être découvert par une analyse attentive des cas les plus intéressants, et notre contribution sera développée selon cette philosophie. Les logiques modales propositionnelles offrent une alternative aux langages traditionnels. Elles peuvent être considérées comme un ensemble d'outils permettant de concevoir des logiques adaptées à des tâches précises, possédant un contrôle fin sur leur expressivité. De plus, il s'est avéré que les logiques modales possèdent un bon comportement computationnel, qui se trouve être robuste y compris malgré l'ajout d'extensions. Ces caractéristiques, parmi d'autres, ont élevé les logiques modales au rang d'alternatives désirables aux langages classiques. Dans ce thèse, nous allons présenter une nouvelle famille de logiques modales appelée logiques mémorielles. Les logiques modales traditionnelles permettent de décrire les structures relationnelles d'un point de vue local. Mais pourquoi ne pas changer cette structure? Nous voulons étudier l'ajout d'une structure de stockage explicite aux logiques modales, une mémoire, qui permet de modéliser un comportement dynamique à travers des opérateurs mémoriels explicites. Ces opérateurs sauvent ou restaurent de l'information vers et à partir de la mémoire. Naturellement, selon le type de structure de sauvegarde désiré et les opérateurs mémoriels disponibles, la logique résultante possèdera différentes propriétés qui valent la peine d'être étudiées. Cette thèse est organisée de la façon suivante. Dans le Chapitre 1, nous commençons par rappeler brièvement comment la logique modale est née, en montrant les différents points de vue historiques la concernant. Puis, nous présentons formellement la logique modale de base et un ensemble d'opérateurs étendus qui aident à capturer le ``goût'' modal de langages plus riches. Nous finissons ce chapitre en donnant un premier aperçu des logiques mémorielles, et montrons comment elles peuvent aider à modéliser l'état quand nous choisissons d'utiliser un ensemble comme une structure de sauvegarde. Le Chapitre 2 est dédié à la présentation détaillée des logiques mémorielles. Nous montrons quelques exemples qui peuvent être décrits en ajoutant un ensemble à des structures relationnelles usuelles, ainsi que les opérateurs ensemblistes usuels permettant l'ajout d'élément et le test d'appartenance. Puis, nous montrons que d'autres opérateurs mémoriels peuvent être envisagés, et nous discutons de la possibilité d'ajouter des contraintes à l'interaction entre la mémoire et les opérateurs modaux. Ces contraintes peuvent être vues comme une manière d'avoir un contrôle fin sur l'expressivité de la logique. Comme nous avons fait des changements aux logiques modales classiques, nous nous intéressons à l'analyse de l'impact de ces changements sur les logiques résultantes. Ainsi, le reste de ce chapitre présente une boite à outils logique basique avec laquelle nous pouvons analyser cette nouvelle famille de logiques. Cette boite à outils peut être vue comme un plan qui organise le reste de cette thèse et qui permet d'analyser les logiques mémorielles en termes d'expressivité, de complexité, d'interpolation et de théorie de la preuve. Le reste des chapitres consiste à étudier en détail chacun de ces aspects. Dans les Chapitres 3 et 4, nous explorons l'expressivité de plusieurs logiques mémorielles et nous étudions la décidabilité de leur problème de satisfiabilité. Dans les cas décidables, nous déterminons leur complexité. Nous analysons l'impact des différents opérateurs mémoriels considérés, et leur interaction. Nous étudions également d'autres conteneurs mémoriels, tels que la pile. Puis, dans le Chapitre 4, nous analysons l'interpolation de Craig et la définabilité de Beth pour certains fragments des logiques mémorielles. Nous étudions également les logiques mémorielles du point de vue de la théorie de la preuve. Dans les Chapitres 6 et 7, nous passons aux axiomatisations à la Hilbert et aux systèmes de tableaux, et nous caractérisons plusieurs fragments de la famille des logiques mémorielles, en utilisant principalement des techniques empruntées aux logiques hybrides. Nous concluons dans le Chapitre 8 avec quelques remarques, des problèmes ouverts et des directions pour de futures recherches. / From ancient times to the present day, the field of logic has gained significant strength and now it actively contributes to many different areas, such as philos- ophy, mathematics, linguistic, computer science, artificial intelligence, hardware manufacture, etc. Each of these scenarios has specific needs, that range from very concrete requirements, like an efficient inference method, to more abstract theoretical properties, like a neat axiomatic system. Given this wide diversity of uses, a motley collection of formal languages has been developed. For many years, classical languages (mainly classical first order logic) were the alternative, but this assortment of applications made other types of logics also attractive in many situations. Imagine that the time for choosing a logic for some specific task arrives. How can we decide which is the one that fits best? Which properties should we look for? How can we “measure” a logic with respect to others? These are not easy questions, and there is not a general recipe one can follow. In this thesis we are just going to restrict these questions to a particular family of logics, and in that context we will investigate theoretical aspects that help to answer some of these concerns. Much can be discovered by carefully analyzing appealing cases, and our contribution will be developed having that philosophy in mind. Propositional modal logics offer an alternative to traditional languages. They can be regarded as a set of tools that allow to design logics specially tailored for specific tasks, having a fine-grained control on their expressivity. Additionally, modal logics turned out to have a good computational behavior, which proved to be quite robust under extensions. These characteristics, among others, placed modal logics as an attractive alternative to classical languages. In this dissertation we are going to present a new family of modal logics called memory logics. Traditional modal logics enables to describe relational structures from a local perspective. But what about changing the structure? We want to explore the addition of an explicit storage structure to modal logics, a mem- ory, that allows to model dynamic behavior through explicit memory operators. These operators store or retrieve information to and from the memory. Natu- rally, depending on which type of storage structure we want, and which memory operators are available, the resulting logic will enjoy different properties that are worth investigating. The thesis is organized as follows. In Chapter 1 we start by giving a brief recap of how modal logic was born, showing the different historical perspectives used to look at modal logic. Then we formally present the basic modal logic and a set of extended operators that helps grasp the modal “flavor” of some richer languages. We finish this chapter by giving a first glance of memory logics, and showing how they can help to model state when we choose to use a set as storage structure. Chapter 2 is devoted to present memory logics in detail. We show some examples that can be described by adding a set to standard relational structures, and the usual set operators to add elements and test membership. We then show some other memory operators that can be considered, and we discuss the possibility of adding constraints to the interplay between memory and modal operators. These constraints can be regarded as a way to have a finer-grained control on the logic expressivity. Since we have made changes to classical modal logics, we are interested in analyzing the impact those changes cause in the resulting logics. Therefore, the rest of this chapter presents a basic logic toolkit through which we can analyze this new family of logics. This toolkit can be seen as an outline that organizes the rest of the thesis and that allows to analyze memory logics in terms of expressivity, complexity, interpolation and proof theory. The rest of the chapters investigate each of these aspects in detail. In Chap- ters 3 and 4 we explore the expressive power of several memory logics and we study the decidability of their satisfiability problem. In the decidable cases, we determine their computational complexity. We analyze the impact of the differ- ent memory operators we consider, and how they interact. We also study other memory containers, such as a stack. Then, in Chapter 5, we analyze Craig inter- polation and Beth definability for some memory logic fragments. We also study memory logics from a proof theoretical perspective. In Chapter 6 and 7 we turn to Hilbert style axiomatizations and tableau systems, and we characterize several fragments of the memory logic family mostly using techniques borrowed from hy- brid logics. We close in Chapter 8 with some concluding remarks, open problems and directions for further research.

No description available.

Les problèmes traités et les résultats obtenus dans ce travail s'inscrivent essentiellement dans le domaine de la théorie des automates, la logique mathématique et leurs applications. Dans un premier temps on utilise les automates finis pour démontrer l'automaticité de plusieurs structures logiques sur des mots finis écrits dans un alphabet infini dénombrable. Ceci nous permet de déduire la décidabilité des théories logiques associées à ces structures. On a considéré par exemple la structure $X=(Sigma^*;prec,clone)$ où $Sigma^*$ désigne l'ensemble des mots finis sur l'alphabet infini dénombrable $Sigma$, $prec$ désigne la relation de préfixe et $clone$ désigne le prédicat qui est vrai pour un mot se terminant par deux lettres identiques. On a démontré l'automaticité de la structure $X$ et la décidabilité de sa théorie du premier ordre et de sa théorie monadique du second ordre. On a aussi considéré des extensions de la structure $X$ obtenues en ajoutant des prédicats comme $sim$ qui est vrai pour deux mots de même longueur. Nous avons en particulier démontré la $M$-automaticité de la structure $(Sigma^*;prec,clone,sim)$, d'où la décidabilité de sa théorie du premier ordre. On a par ailleurs étudié des structures qui comportent le prédicat $diff$ qui est vrai pour un mot dont les lettres sont toutes distinctes. En particulier on a démontré l'automaticité de la structure $D=(Sigma^*;prec,clone,diff)$ et la décidabilité de sa théorie du premier ordre et de sa théorie monadique du second ordre. On a également obtenu, par interprétation logique, des résultats de décidabilité et des résultats d'indécidabilité pour plusieurs variantes des structures $X$ et $D$, ainsi que pour des familles de structures appelées emph{structure d'applications exclusives} et emph{structure de décomposition}.Dans un deuxième temps on s'est intéressé au problème de la réduction du nombre de transitions dans les automates finis. On a commencé par étendre le concept de emph{Common Follow Sets} d'une expression régulière aux automates finis homogènes. On a montré comment établir une liaison assez directe entre des systèmes de CFS spécifiques et les arbres binaires complets. Ce lien est prouvé en utilisant un objet combinatoire appelé emph{triangle d'Ératosthène - Pascal}. Cette correspondance permet de transformer la valeur qui nous intéresse (le nombre de transitions) en une valeur assez naturelle associée aux arbres (le poids d'un arbre). En effet, construire un automate ayant un minimum de transitions revient à trouver un arbre de poids minimal. On a montré, d'une part, que ce nombre de transitions est asymptotiquement équivalent à $n(log_2 n)^2$ (la borne inférieure). D'autre part, les tests expérimentaux montrent que pour les petites valeurs de $n$, les automates minimaux en nombre de transitions coïncident (en nombre et en taille) avec ceux obtenus par notre construction. Cela nous mène à suggérer que notre réduction est finalement une minimisation pour les automates triangulaires. Dans un dernier temps on a présenté une étude expérimentale concernant l'application des automates à trous dans le domaine de la recherche approchée de motif dans les dictionnaires de mots. Contrairement aux complexités théoriques, temps de recherche et espace de stockage exponentiels, nos expérimentations montrent la linéarité de l'automate à trous / This work deals mainly with automata theory, mathematical logic and their applications. In the first part, we use finite automata to prove the automaticity of several logical structures over finite words written in a countable infinite alphabet. These structures involve predicates like $pred$, $clone$ and $diff$, where $x pred y$ holds if $x$ is a strict prefix of $y$, $clone(x)$ holds when the two last letters of $x$ are equal, and $diff(x)$ holds when all letters of $x$ are pairwise distinct. The automaticity results allow to deduce the decidability of logical theories associated with these structures. Other related decidability/undecidability results are obtained by logical interpretation. In the second part, we generalize the concept of Common Follow Sets of a regular expression to homogeneous finite automata. Based on this concept and a particular class of binary trees, we devise an efficient algorithm to reduce/minimize the number of transitions of triangular automata. On the one hand, we prove that the produced reduced automaton is asymptotically minimal, in the sense that for an automaton with $n$ states, the number of transitions in the reduced automaton is equivalent to $n(log_2 n)^2$ , which corresponds at the same time to the upper and the lower known bounds. On the other hand, experiments reveal that for small values of $n$, all minimal automata are exactly those obtained by our reduction, which lead us to conjecture that our construction is not only a reduction but a minimization. In the last part, we present an experimental study on the use of special automata on partial words for the approximate pattern matching problem in dictionaries. Despite exponential theoretical time and space upper bounds, our experiments show that, in many practical cases, these automata have a linear size and allow a linear search time

Les systèmes digitaux jouent un rôle croissant dans le bon fonctionnement de notre société.Au delà de la grande diversité de leur domaines d'utilisations, on confie aujourd'hui destâches importantes à des algorithmes. Déjà largement utilisés dans des domaines aussi délicatque le transport, la chirurgie ou l'économie, il est aujourd'hui de plus en plus question defaire de la place aux systèmes digitaux dans les domaines sociaux et politiques :vote électronique, algorithmes de sélection, profilage électoraldotsPour les tâches confiées à des algorithmes, la responsabilité est déplacées de l'exécutantvers les concepteurs, développeurs et testeurs de ces algorithmes. Il incombe aussi auxchercheurs qui étudient ces algorithmes de proposer des techniques de vérifications fiablequi pourront être utilisées à tous les niveaux : conception, développement et test.Les méthodes de vérifications formelles donnent des outils mathématiques pourprévenir des erreurs à chaque niveaux. Parmi elle, le diagnostic d'erreur consiste en lacréation d'un diagnostiqueur basé sur un modèle formel du système à vérifier.Le diagnostiqueur est exécuté en parallèle du système qu'il doit surveiller et prévientun contrôleur si il détecte un comportement dangereux du système.Pour les systèmes modélisés par des automates temporisés, il n'est pas toujours possiblede construire un diagnostiqueur sous la forme d'un autre automate temporisé. En effetles automates temporisés, introduits par cite{AD94} dans les années 90 et largementétudiés et utilisés depuis pour modéliser des systèmes avec contraintes temporelles,ne sont pas déterminisable. Une machine plus puissante qu'un automate temporisé peutcependant être utilisée pour construire le diagnostiqueur d'un automate temporisé commele montre cite{Tripakis02}. L'aboutissement de ce travail de thèse est la constructionautomatique d'un diagnostiqueur pour les automates temporisés à une horloge.Ce diagnostiqueur, dans le même esprit que celui de cite{Tripakis02}, est une machineplus puissante qu'un automate temporisé. La partie~I du manuscrit introduit un cadreformel pour ce type de machine et plus généralement pour la modélisation et ladéterminisation de systèmes quantitatifs. Y est introduit le modèle des automates surstructures temporisés, qui apporte un nouveau point de vue sur la manière de modéliserles systèmes avec variables quantitatives. La partie~II étudie le problème de ladéterminisation des automates sur structures temporises, et plus spécifiquement celuides automates temporisés qui peuvent se traduire dans ce cadre nouveau cadre formel.La partie~III montre comment utiliser les automates sur structure temporisés pourconstruire de manière générique un diagnostiqueur pour les automate temporisés à unehorloge. Cette technique est implémentée dans un outils, DOTA , et comparée à lamachine construite par cite{Tripakis02}. / Digital system are now part of our society. They are used in a wide range of domainsand in particular they have to handle delicate tasks. Already used in domainssuch as transportation, surgery or economy, we speak now of using digital systemsfor social or political matters : electronic vote, selection algorithms, electoralprofilingdots For task handled by algorithm, the responsibility is moved from theexecutioner to the designer, developer and tester of those algorithms. It is alsothe responsibility of computer scientists who study those algorithms to proposereliable techniques of verification which will be applicable in the design, thedevelopment or the testing phase. Formal verification methods provide mathematicaltools to prevent executions error in all phases. Among them, fault-diagnosis consiston the construction of a diagnoser based on a formal model of the system we aim tocheck. The diagnoser runs in parallel with the real system and emit a warning anytime it detect a dangerous behavior. For systems modeled by timed automata, it isnot always possible to construct a timed automaton to diagnose it. Indeed timed automata,introduce in the nineties by cite{AD94} and widely studied and used since to modeltimed systems, are not determinizable. A machine, more powerful than a timed automaton,can still be used to construct the diagnoser of a timed automaton as it is done incite{Tripakis02}. This thesis work aim at constructing a diagnoser for any one-clocktimed automata. This diagnoser is constructed with the help of a machine more powerfulthan timed automata, following the idea of cite{Tripakis02}. Part~I of this thesisintroduce a formal framework for the modeling of quantitative systems and the study oftheir determinization. In this framework we introduce automata on timed structures,the model used to construct the diagnoser. Part~II study the determinization problemof automata on timed structures, and particularly the one of timed automatadeterminization in this framework. Part~III illustrate how automata on timed structurescan be used to construct in a generic way a diagnoser for one clock timed automata.This technique is implemented in a tool, DOTA , and is compared to the technique usedin cite{Tripakis02}.

À mesure que le nombre d’objets capables de communiquer croît, le besoin de sécuriser leurs interactions également. La conception des protocoles cryptographiques nécessaires pour cela est une tâche notoirement complexe et fréquemment sujette aux erreurs humaines. La vérification formelle de protocoles entend offrir des méthodes automatiques et exactes pour s’assurer de leur sécurité. Nous nous intéressons en particulier aux méthodes de vérification automatique des propriétés d’équivalence pour de tels protocoles dans le modèle symbolique et pour un nombre non borné de sessions. Les propriétés d’équivalences ont naturellement employées pour s’assurer, par exemple, de l’anonymat du vote électronique ou de la non-traçabilité des passeports électroniques. Parce que la vérification de propriétés d’équivalence est un problème complexe, nous proposons dans un premier temps deux méthodes pour en simplifier la vérification : tout d’abord une méthode pour supprimer l’utilisation des nonces dans un protocole tout en préservant la correction de la vérification automatique; puis nous démontrons un résultat de typage qui permet de restreindre l’espace de recherche d’attaques sans pour autant affecter le pouvoir de l’attaquant. Dans un second temps nous exposons trois classes de protocoles pour lesquelles la vérification de l’équivalence dans le modèle symbolique est décidable. Ces classes bénéficient des méthodes de simplification présentées plus tôt et permettent d’étudier automatiquement des protocoles taggués, avec ou sans nonces, ou encore des protocoles ping-pong. / As the number of devices able to communicate grows, so does the need to secure their interactions. The design of cryptographic protocols is a difficult task and prone to human errors. Formal verification of such protocols offers a way to automatically and exactly prove their security. In particular, we focus on automated verification methods to prove the equivalence of cryptographic protocols for a un-bounded number of sessions. This kind of property naturally arises when dealing with the anonymity of electronic votingor the untracability of electronic passports. Because the verification of equivalence properties is a complex issue, we first propose two methods to simplify it: first we design a transformation on protocols to delete any nonce while maintaining the soundness of equivalence checking; then we prove a typing result which decreases the search space for attacks without affecting the power of the attacker. Finally, we describe three classes of protocols for which equivalence is decidable in the symbolic model. These classes benefit from the simplification results stated earlier and enable us to automatically analyze tagged protocols with or without nonces, as well as ping-pong protocols.

En informatique, les logiques formelles ont une place centrale dans la représentation et le traitement des connaissances. Elles sont utilisées pour la modélisation et la vérification de systèmes informatiques et de leurs propriétés ainsi que pour la formalisation de différents types de raisonnement. Dans ce contexte il existe un large spectre de logiques non-classiques parmi lesquelles les logiques modales jouent un rôle important. Alors que les logiques modales classiques ont été largement étudiées, nous nous focalisons dans cette thèse sur les logiques modales intuitionnistes et aussi hybrides floues en abordant un certain nombre de questions principalement du point de vue de la théorie de la démonstration. Nous proposons pour ces logiques de nouveaux systèmes de preuve, notamment suivant les formalismes de déduction naturelle et de calcul des séquents, qui sont fondés sur de nouvelles structures multi-contextuelles généralisant la structure standard de séquent / In computer science, formal logics are central for studying the representation and the treatment of knowledge. Indeed, they are widely used for modeling and verifying computer systems and their properties and also for formalizing different kinds of reasoning. In this context there exist many non-classical logics and among them modal logics play a key role. As classical modal logics have been deeply studied, we focus in this thesis on the intuitionistic modal logics and also on fuzzy hybrid logics by studying some important questions mainly from the viewpoint of proof theory . We define for these logics new proof systems, following natural deduction and sequent calculus formalisms, that are based on new multi-contextual structures generalizing the standard sequent structure

Les systèmes hybrides sont des systèmes qui combinent des composantes discrètes et des composantes continues. Les composantes continues peuvent représenter un environnement physique obéissant à des règles de changement continu, par contre les composantes discrètes peuvent représenter des contrôleurs discrets qui sondent et manipulent les composantes continues en temps réel. Deux approches peuvent être adoptées pour spécifier ces systèmes, la première étant basée sur des automates (hybrides) et utilise des méthodes d'analyse algorithmiques. La seconde est basée sur les logiques et utilise des preuves formelles comme méthodes d'analyse. Dans une première partie de cette thèse nous considérons l'approche basée sur les automates. Nous étudions la décidabilité du problème de la vérification pour certaines classes de systèmes hybrides linéaires. Nous prenons comme modèles des automates hybrides linéaires avec des structures de données discrètes non bornées. Nous exhibons différents cas de tels systèmes dont le problème de la vérification est décidable. Dans une seconde partie nous considérons l'approche basée sur les logiques et plus particulièrement celle basée sur le «Calcul de Durées». Nous étudions les relations existantes entre cette approche et la précédente ; nous montrons comment cette liaison permet de mettre en évidence un fragment important du «Calcul de Durées» pour lequel le problème de la vérification est décidable

Les protocoles cryptographiques jouent un rôle majeur dans les applications ou l'intégrité des données, la confidentialité, l'authenticité et autres propriétés sont essentielles. Ils sont utilisés par exemple dans le commerce électronique, la téléphonie mobile, le vote électronique. Dans la première partie de la thèse nous montrons que le problème d'atteignabilité pour des protocoles cryptographiques temporisés bornés est décidable est NP-complet. Notre procédure se base sur une logique de Hoare complète pour des protocoles cryptographiques bornés et un langage de propriétés très expressif. Dans la deuxième partie, en utilisant des techniques d'interprétation abstraite, nous appliquons cette méthode pour vérifier des propriétés de secret pour les protocoles cryptographiques dans un modèle général. Nous traitons un nombre non borné de sessions, de participants et de nonces ainsi que des messages de taille arbitraire. Nous proposons un algorithme qui calcule un invariant inductif en utilisant des patterns comme représentation symbolique. Cette méthode a été implanté dans l'outil Hermes et validée sur plusieurs études de cas.

Le problème de la combinaison des services, autrement appelé problème de la composition, constitue le foyer d'une intense activité de recherche. Composer les services entre eux, c'est entrelacer leurs séquences d'actions, de manière à obtenir des séquences qui satisfassent les exigences des clients. Le problème de la composition de services est difficile à résoudre en général. Dans cette thèse nous considérons des services qui peuvent à la fois exécuter des actions de communications ainsi que des actions internes. De plus, des conditions peuvent être exigées et des effets peuvent être appliqués sur les transitions. Formellement, les services sont représentés par des automates communicants conditionnels. Nous définissons, pour ce modèle, le problème de la composition et nous étudions sa décidabilité pour différentes relations d'équivalence et de préordre à savoir : l'inclusion de traces, l'équivalence de traces, la simulation et la bisimulation. Suite aux résultats de décidabilité obtenus, nous proposons trois variantes pour le modèle initial. Pour chacune d'elles, nous définissions le problème de la composition et nous étudions sa complexité pour les relations citées ci-dessus.

Les systèmes polygonaux à inclusions différentielles (SPDIs) sont des systèmes planaires non déterministes qui peuvent être représentés par des inclusions différentielles constantes par morceaux. Cette thèse porte sur les aspects théoriques et pratiques des SPDIs tels que le problème de l'atteignabilité et de la construction du portrait de phase. Nous montrons que le problème de l'atteignabilité est décidable pour les SPDIs. Notre procédure est basée sur le calcul des limites des trajectoires individuelles : l'idée sous-jacente est l'utilisation de fonctions de Poincaré unidimensionelles, pour lequelles on peut facilement calculer les points fixes et qui permettent dans la plupart des cas d'accélérer les cycles. Nous avons implanté cet algorithme d'atteignabilité dans l'outil SPeeDI. Ensuite, nous construisons le portrait de phase des SPDIs. Nous savons identifier les noyaux de viabilité des boucles simples. Il s'agit des ensembles de points initiaux de trajectoires restant dans la boucle. Nous introduisons la notion de noyau de controlabilité de boucles simples comme l'ensemble des points atteignables les uns à partir des autres par des trajectoires qui restent dans le noyau. Nous proposons un algorithme non itératif pour calculer ces deux noyaux, qui nous permet ensuite de construire le portrait de phase des SPDIs. Enfin, nous étudions la décidabilité du problème de l'atteignabilité pour d'autres classes de systèmes hybrides à deux dimensions : les systèmes hiérarchiques constants par morceaux (HPCDs) et les systèmes constants par morceaux, définis sur les surfaces. Nous montrons que le problème de l'atteignabilité pour ces deux classes de systèmes est équivalent à l'atteignabilité pour des systèmes affines par morceaux, dont la décidabilité est un problème ouvert. Nous montrons enfin que le problème de l'atteignabilité pour quelques extensions de HPCDs est indécidable.