Keywords: results

Hybrid systems are complex systems that combine both discrete and continuous behaviors. Verifying behavioral or safety properties of such systems, either at design stage or on-line is a challenging task. Actually, computing the reachable set of states of a hybrid system is undecidable. One way to verify those properties over such systems is by computing discrete abstractions and inferring them from the abstract system back to the original system. We are concerned with abstractions oriented towards hybrid systems diagnosability checking. (Bounded)diagnosability can be see as the ability of the system (or an extended system) to localize a problem in bounded time such as the occurrence of a fault. Our goal is to create discrete abstractions in order to verify if a fault that would occur at runtime could be unambiguously detected in finite time by the diagnoser. This verification can be done on the abstraction by classical methods developed for discrete event systems, which provide a counterexample in case of nondiagnosability. The absence of such a counterexample proves the diagnosability of the original hybrid system. In the presence of a counterexample, the first step is to check if it is not a spurious effect of the abstraction and actually exists for the hybrid system, witnessing thus non-diagnosability. Otherwise, we show how to refine the abstraction and continue the process of looking for another counterexample.

I am forever in debt to my professor Philippe Dague for guiding me throughout the thesis. He provided me with constant feedback, was always available for any inquiry and showed me new horizons to extend the research. Without his help the current quality of the thesis work and the present manuscript would have never been achieved. I thank my supervisor Jean-Pierre Gallois for the daily discussions about the thesis topic and his constant supervision over the works.

My sincerest thanks goes also to Lina Ye for bringing her expertise in the diagnosability verification domain, her work in co-authoring the publications and her numerous advice.

The help I received at CEA from my colleagues Arnault and Stéphane during my implementation work was of major importance, for that I thank them indefinitely. I address my profound thanks and gratitude to professor Walid Taha and professor Goran Frehse for taking the time to evaluate my manuscript, their valuable comments and for taking part of the jury for my thesis defence. I also thank professor Erika Ábrahám and professor Sylvain Conchon for accepting to take part in the jury and assisting to the oral defense.

I thank my family, my mother Hala, father Samir and sister Saly living in my home country Lebanon for their eternal support and their visits to France for checking up on me constantly.

My thanks goes also to my friends Ben, Jad, Houssam, Nadine, Ghida, Dory, Slim, Lamia, Minh-Thang and Imene for being there for me in time of need.

Chapter 1 Introduction

The thesis is concerned with the formal verification of complex systems at modeling stage. Precisely, the complex systems dealt with are hybrid systems that exhibit a twofold behavior: continuous and discrete. Hybrid Automata are a common framework to model hybrid systems using finitely many discrete modes and continuous real-valued variables. They provide an intuitive, powerful and general way to model a large number of practical systems, applicable in many domains: aeronautics, railway, biology and more generally cyber-physical systems (CPS) where control loops act upon digital electronic circuits (discrete behavior) and are orchestrated by the physical environment (continuous processes).

The problem of hybrid systems verification is addressed, i.e., given a hybrid automaton model and a property, does the model verify this property? The literature shows that the verification of hybrid systems is challenging. In fact, the study of hybrid systems requires cross-disciplinary competences. Consequently, verification methods must couple and extend results originating from different domains such as control theory, applied mathematics and both theoretical and practical computer science. Moreover, due to the expressiveness of the hybrid automata modeling language, verifying the most simple properties (such as reachability) is undecidable for hybrid systems. Progress in hybrid systems is also held back by the lack of a strong standardized specification and modeling language. Many tools for hybrid systems verification exist today, each of them having its own input language and addressing a specific problem with particular methods.

The work addressed by this thesis is the application of principles from the qualitative reasoning domain to hybrid systems verification. Intuitively, qualitative reasoning aggregates similar behaviors of the system into representative sets and reasons over these sets. The relations describing the representative sets allow a global overview of the system behavior, performing as such, what is called in the literature, a qualitative simulation. For hybrid systems, it is difficult to aggregate any exact set of behaviors. For this reason, representative sets that are over-approximations of the real system behaviors are used. The overview mapping is thus an abstraction relating the real (or concrete) system and the related representative (or abstract) sets. The abstract system being an over-approximation, a class of properties can be verified using the abstraction and inferring the result to the concrete system.

The topic of hybrid systems verification being too general, a particular property is addressed: diagnosability. This property of the system supposes that a given hybrid automaton models, not only the correct behavior of the system, but faulty ones as well. Practically speaking, if the system is inevitably unable to avoid the occurrence of a fault(s) and if the faulty behavior can be characterized in advance, one can model this faulty behavior. The system is considered diagnosable if it is able to detect the faulty behavior and identify the fault that occurred among the set of possible faults after the fault occurrence. Moreover, the system is supposed partially observable, thus, diagnosability analysis should only use the partial observations to establish its verdict. Our goal is to create discrete abstractions in order to verify, at design stage, if a fault that would occur at run time could be unambiguously detected in finite time (or within a given finite time bound for bounded diagnosability) by the diagnoser using only the allowed observations. This verification can be done on the abstraction by classical methods developed for discrete event systems, which provides a counterexample in case of non-diagnosability. The absence of such a counterexample proves the diagnosability of the original hybrid system. In presence of a counterexample, the first step is to check if it is not a spurious effect of the abstraction and actually exists for the hybrid system, witnessing thus non-diagnosability. Otherwise, the abstraction is to be refined, guided by the elimination of the counterexample, and the process of looking for another counterexample continues until some precision is reached.

Contributions

The contributions of the thesis are:

• The elaboration of a method that performs a qualitative simulation of a given hybrid system. The method incorporates reasoning from the qualitative domain and extend previous results from the literature.

• The implementation of a tool that performs the qualitative simulation of the hybrid system given a polynomial hybrid automaton as input.

• An extension to the qualitative simulation framework for producing timed abstractions of a given hybrid system using existing flow-pipe computation techniques. The flow-pipe computation is guided by the resulting qualitative simulation. Timed automata are used to represent the qualitative timed abstraction.

• The elaboration of a method that applies the results issued from the qualitative simulation and timed abstractions to diagnosability verification of hybrid systems in the framework of counter-example guided abstraction refinement (CEGAR) loop. Methods that were specific to diagnosability analysis of discrete and timed automata are used.

Thesis outline

The upcoming chapters are organized as follows:

• Chapter 2 presents the scientific context. The literature concerned with model driven engineering, qualitative reasoning and simulation, hybrid system verification techniques for reachability and diagnosability verification and the existing tools and challenges are reviewed.

• Chapter 3 introduces a formal framework for hybrid system verification, fault modeling and diagnosability. The adopted notations are introduced and practical examples from known benchmarks are used to illustrate the definitions.

• Chapter 4 presents qualitative reasoning based abstraction methods for hybrid systems and their applicability to diagnosability verification. The method combines predicate abstraction with qualitative based reasoning and is instantiated to the class of polynomial hybrid automata.

• Chapter 5 presents the tool for performing a qualitative simulation of a given hybrid system illustrated and tested on different examples.

• Chapter 6 concludes the thesis. The chapter reviews the contributions while comparing with closely related work from other authors and finally draws some perspectives.

Résumé français 1.3 Summary in french

Cette partie résume en français le contenu de la thèse. On présentera d'abord la structure du manuscrit et le contenu des chapitres puis le résumé des publications.

Mot-clés

Systèmes et automates hybrides, raisonnement qualitatif, diagnosticabilité, systèmes à évènements discrets, automate temporisé, techniques d'abstraction.

Structure de la thèse

Le manuscrit de thèse est constitué de six chapitres et deux annexes.

• Chapitre 1 : Le premier chapitre est introductif. Il décrit la problématique traitée par la thèse et présente le contexte scientifique général ainsi qu'une liste des contributions de la thèse.

• Chapitre 2 : Le deuxième chapitre fournit un aperçu global des différentes problématiques évoquées par la thèse et les éléments de l'état de l'art sur lesquels se fondent les travaux de la thèse : la modélisation et l'analyse des systèmes hybrides, la modélisation et la simulation qualitatives et la diagnosticabilité. Cette partie résume les concepts de base pour permettre au lecteur de se familiariser avec la thématique. Les concepts sont illustrés par des exemples.

• Chapitre 3 : Le troisième chapitre présente le formalisme de base utilisé pour la description des systèmes hybrides : les automates hybrides. Le problème de diagnosticabilité sous observation partielle, formalisé en termes d'automates hybrides, est également présenté, suivi des classes particulières de systèmes hybrides notamment les automates temporisés et les automates hybrides polynomiaux qui nous intéressent pour les travaux de la thèse.

• Chapitre 4 : Le quatrième chapitre présente une approche pour construire des abstractions temporisées d'un automate hybride et son application à la diagnosticabilité. Cette abstraction peut être raffinée, à la précision souhaitée, en partitionnant davantage l'espace d'états. Ensuite cette approche est utilisée pour résoudre le problème de diagnosticabilité : deux copies de l'automate hybride sont utilisées pour former un nouveau système de jumeaux (twin plant). Ainsi on peut caractériser un problème de diagnosticabilité comme une exécution du système dans laquelle une copie atteint un état fautif et l'autre non, les deux produisant les mêmes observations sur l'horizon de temps donné. L'abstraction est utilisée pour permettre l'analyse des automates hybrides avec une dynamique polynomiale.

• Chapitre 5 : Ce chapitre présente les expériences sur des études de cas. Un outil prototype qui permet d'effectuer la simulation qualitative d'une manière automatique est présentée. L'architecture de l'outil est présentée puis une étude des performances avec les temps de calculs évalués sur plusieurs modèles de systèmes hybrides et continus est établie.

• Chapitre 6 : Le chapitre final présente les conclusions. Une comparaison des travaux avec d'autres travaux proches de la thématique considérée est présentée. Finalement, des perspectives envisageables sont illustrées.

Résumé des publications

• [START_REF] Zaatiti | Automating Abstraction Computations of Hybrid Systems[END_REF] Les systèmes hybrides exhibent une interaction entre des décisions de contrôle discret et des processus physiques continus, ces systèmes sont au coeur des systèmes dits cyber-physiques. Suite à ces interactions, la vérification de ces systèmes est difficile. Dans cet article, on s'intéresse aux techniques d'abstraction des systèmes hybrides. Les abstractions sont utiles pour automatiser le processus de vérification du système hybride, comme la vérification de la sûreté ou même des propriétés plus compliquées lorsque la vérification est combinée avec des algorithmes de "model checking" classiques. L'article présente un outil qui calcule de façon automatique l'abstraction d'un système hybride donné en entrée, celui-ci ayant une expressivité polynomiale. L'abstraction peut être manuellement raffinée afin d'atteindre une meilleure précision, cette opération est guidée par le concepteur du système. L'outil est testé sur plusieurs exemples.

• [START_REF] Zaatiti | Counterexample-guided abstraction-refinement for hybrid systems diagnosability analysis[END_REF] La vérification des propriétés des systèmes hybrides depuis leur conception, comme la sûreté ou la diagnosticabilité, ou pendant leur exécution, telle que la détection et l'isolation de fautes, est une tâche difficile. Dans ce papier on est concerné par les techniques d'abstraction orientées pour la vérification de la diagnosticabilité d'un système hybride donné. La vérification est effectuée sur l'abstraction utilisant des méthodes classiques développées pour les systèmes à évènements discrets étendues avec des contraintes temporelles, qui fournissent un contre-exemple dans le cas où le système n'est pas diagnosticable. L'absence d'un tel contre-exemple prouve la diagnosticabilité du système original. En présence d'un contre-exemple, la première étape est de vérifier si celui-ci n'est pas un faux contre-exemple résultant de l'abstraction et qu'il figure bien au niveau concret, témoignant ainsi de la non-diagnosticabilité. Dans le cas contraire, on montre comment raffiner l'abstraction guidé par l'élimination du contre-exemple puis le processus de recherche d'un nouveau contre-exemple continue jusqu'à atteindre un résultat ou un verdict non concluant. On se sert des principes de modélisation et raisonnement qualitatifs pour le calcul de l'abstraction discrète. Les abstractions en tant qu'automate temporisé sont particulièrement étudiées, en effet elles permettent de gérer les contraintes temporelles qui sont capturées à un niveau qualitatif du système hybride.

• [START_REF] Zaatiti | Abstractions Refinement for Hybrid Systems Diagnosability Analysis[END_REF] La croissance en complexité des systèmes rend plus difficile la détection et l'isolation de fautes. Ce fait s'applique aux systèmes hybrides qui combinent un double aspect discret et continu. La vérification de propriétés durant la phase de conception du système, telles que la sûreté, la diagnosticabilité et la prédictabilité, ou durant leur exécution, telles que la détection et l'isolation de fautes, est une tâche difficile.

En effet, calculer l'ensemble des états atteignables d'un système hybride donné n'est pas décidable, ceci est principalement dû à la grande expressivité du langage de modélisation des systèmes hybrides notamment en ce qui concerne la partie continue. Une méthode employée pour vérifier les propriétés de tels systèmes consiste à calculer une abstraction discrète du système considéré, à appliquer le processus de vérification à l'abstraction et à inférer le résultat obtenu au système hybride original. La diagnosticabilité est une propriété qui décrit la capacité d'un système à déterminer l'occurrence d'une faute à partir des observations. Ce problème a reçu une attention considérable dans la littérature. Néanmoins, la plupart des travaux existants sont appliqués aux systèmes à évènements discrets ou, dans une moindre mesure, aux systèmes continus mais très peu aux systèmes hybrides. Dans ce chapitre d'ouvrage, on est concerné par les méthodes d'abstraction orientées pour la vérification de la diagnosticabilité d'un système hybride donné. Notre objectif est de créer des abstractions discrètes pour vérifier, dès la modélisation de ce système, si une faute qui peut avoir lieu durant l'exécution du système peut-être détectée sans ambiguïté en temps fini (temps borné donné) par le diagnostiqueur en utilisant seulement les observations disponibles. La vérification peut être effectuée sur l'abstraction en utilisant des méthodes classiques développées pour les systèmes à évènements discrets, qui fournissent un contre-exemple si le système n'est pas diagnosticable. En présence d'un contre-exemple, la première étape est de vérifier s'il ne résulte pas de l'abstraction et existe au niveau du système hybride témoignant ainsi de la nondiagnosticabilité du système. Dans le cas contraire, on montre comment raffiner l'abstraction, guidé par l'élimination du contre-exemple et on poursuit le processus de recherche d'un autre contre-exemple jusqu'à l'obtention d'un résultat final ou d'un verdict non concluant.

On se sert des principes du raisonnement et modélisation qualitatifs pour calculer l'abstraction discrète et on définit plusieurs stratégies de raffinement. Les abstractions en tant qu'automate temporisé sont particulièrement étudiées, vu qu'elles permettent de représenter qualitativement les contraintes temporelles.

Chapter 2

Scientific Context

In this chapter the scientific context related to the thesis work is introduced. Sec-

Modeling and verification

Models today are present in every scientific discipline to reason, exchange information and withdraw conclusions from any process. The act of modeling involves three stakeholders: what is being modeled or the system to be modeled S, the model M and the modeling language (or paradigm). Given S and the chosen modeling language(s), the act of modeling produces M . Practically speaking, M holds information about S which often is not all the information contained within S. In other words, a model is never complete unless it is the actual system [START_REF] Lee | The past, present and future of cyber-physical systems: A focus on models[END_REF].

This lack of information between the model and the system translates naturally to a distance indicating how faithful the model is towards S for a given purpose. A portrait photo can be seen as a model of a person, illustrating the facial form, skin tone, eye color and so on, it is a faithful model if the purpose is to illustrate the physical characteristics of the person. However it is not the case for representing personality traits of the person such as likes or dislikes and interests.

Usage In scientific disciplines, models serve various purposes such as communication and collaboration between teams, testing and prototyping, simulation and verification. The use of models today is central for any scientific and research activity. Engineers use models as specifications to build systems in the future that do not exist today, chemists use models to describe observations from real experiments, physicists use models to predict future behaviors or trace back the unknown history of a physical process of the environment [START_REF] Lee | The past, present and future of cyber-physical systems: A focus on models[END_REF]. Today, modeling languages are numerous and can range from application specific languages to domain specific ones.

Deterministic models If a model can react to specific actions, then a deterministic model is one that reacts the same way for the same action. For example, a function that always gives the same output for a given input is a deterministic function. A function that could provide one of two possible outputs for a given input is a non-deterministic function. Determinism is useful for modeling systems that necessarily exhibit some behavior. Non determinism is also useful in representing systems with uncertainties, where the real system may exhibit many "correct" behaviors.

Abstracting and modeling A model can be seen as an abstract representation of S. The model can carry a wide variety of information, one can further abstract the model to see a specific aspect of the system such as abstracting the model of a building to see the places of wires. Such abstraction of the model is useful for the electrical engineer. In the computer science field and the early design phase of a large software, it comes as a first step to build a conceptual model of the software. Such a model does not represent the underlying code or programming language and libraries used, but only the broad idea and intent for which the software serves and clarifying all idea-related ambiguities. It thus specifies what is the software supposed to do and not how and is certainly an abstraction of it.

Different modeling languages such as the Unified Modeling Language (UML) are used for conceptual modeling.

Model checking

In engineering fields, modeling is often conceptual at the early design stage. The real system is then built while being faithful to the model. One would like to test or verify that the conceptual model behaves according to a given specification [START_REF] Clarke | Model checking[END_REF].

Verification and Validation Given a model M and a verification purpose V (a specification) then model checking refers to deciding whether or not V is verified by M denoted M |= V . This process is called model checking. It refers to methods and algorithms for exploring M and determining if it obeys the specification of its intended behavior. Research in model checking aims to automate the verification process of M . Note that model checking does not take into account mistakes that can occur at the modeling phase in which case the model is not credible with respect to the actual system S. The process of checking if the system designer built the right model is referred to as system validation. Model checking attracted interest in industry, providing, at design stage, error-prone software and products.

However model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem via abstraction techniques and compositional reasoning [START_REF] Falkenhainer | Cmpositional modeling: finding the right model for the job[END_REF].

Symbolic Model Checking Around 1990, techniques that used symbolic state space exploration arose. If the system is modeled as a simple automaton with states and transitions, then the verification procedure is carried out by reasoning over a set of states [START_REF] Mcmillan | Symbolic model checking[END_REF]. BDDs (binary decision diagrams) encode these sets of states using functions and allow one to compute transitions based on them rather than on individual states [START_REF] Akers | Binary decision diagrams[END_REF]. These techniques allowed one to handle larger designs and target a greater class of complexity through the use of abstraction and compositional reasoning. Nonetheless, they lack applicability due to each model application requiring a reasoning on its own, as to how to group the states and finding equivalence classes. Today many arising projects observe collaborations between large industrial groups working in the same field. The aim is to obtain application specific verification tools in avionics, autonomous vehicles, railway and other system manufacturing domains where the human knowledge and expertise are directly taken into account in the elaborated tools.

Bounded Model Checking (BMC) [START_REF] Clarke | Bounded model checking using satisfiability solving[END_REF] Bounded model checking refers to verifying a property up to a tolerated bound. In a simple automaton, the bound can be expressed by the maximum number of transition that can be taken starting from some initial state. BMC was applied to reachability and liveness properties where in the first, all generated sequences of states are within a given set of states and the second is verified by detecting whether or not we can find a loop in the sequences. Many results have been obtained in safety verification, where invariants (detailed in the next paragraph) play a major role. An invariant is expressed as a property that holds in each and every state of the automaton. Compared to BDD, BMC is efficient when searching for a counterexample of the property to verify, which is expected since we are adding a bound when exploring the state space.

Some of the disadvantages of bounded model checking is that the method lacks completeness and the types of properties that can currently be checked are very limited. In bounded model checking only finite length sequences are explored, so only those safety properties for which it is enough to look at only bounded length sequences may be entirely verified. For the thesis work, a particular case of the diagnosability property can be seen as a bounded model checking problem. It is the case when verifying bounded diagnosability, i.e. the system's capacity of detecting a fault in a bounded time after its occurrence.

Invariants

Invariants play a key role in verification methods. We show here the different facets and characteristics of invariants.

Invariant Let us apply repeatedly to a real input x, a function f (x) = 3x -1. If the initial value is x = 1 then an invariant is an assertion which holds indefinitely in a certain context, e.g., φ = x > 0 is considered as an invariant for the system.

It is called invariant because it is not changing with respect to time. In this example, time is implicit and can be measured discretely by the number of times we applied f to the input x. The link with verification methods is the possibility of directly using found invariants of the model against the given specification. In general models, finding invariants is an extremely challenging task. Today there is no general tools that synthesize model invariants, even for loop invariants in programs. Most of the existing program verification tools require human intervention for manually inserting invariants to deduce the needed verification proof.

The difficulty arises in the fact that modeling languages with large expresiveness are needed. Consequently designing verification methods that can handle all the possible situations induced by the expressive language becomes complex.

Inductive Invariant Let us apply f for k times where k ∈ N + . Does knowing that φ is verified on the k -1th iteration enough to decide if φ is true on the kth iteration? For φ = x > 0 this cannot be true, take x = 0.2 as initial value. An inductive invariant, is an invariant that requires no further assumptions or other conditions to be met for it to be indefinitely true. Given this definition, we can consider φ ind = x > 1 as inductive invariant.

Fixed Points Given a function f : X → X, an element x ∈ X is a fixed point of f if f (x) = x.
Hence x is invariant by f . Many problems in mathematics and computer science can be formulated in terms of the existence of a fixed point.

Application to computer science Due to the increasing complexity of computer programs, rigorous methods for error detection are needed. Invariants and fixed points are important in error detection in computer programs. Theorem proving over computer programs requires finding complex invariants, which is a very difficult task that, most of the time, cannot be automated by a program itself. In computer science, semantics is the mathematical study of the meaning of programming languages. They describe the processes a computer follows when executing a program in a specific language. Verification tasks over computer programs often involves abstracting the semantics of the program. This field is known as the Abstract Interpretation, the theory for approximating semantics of programming languages. This theory allows us to rigorously describe the idea that a certain semantic can be more or less precise depending on the level of observation. Many reasoning present in program verification have been applied to hybrid systems verification.

Satisfiability Solvers

A solver is a mathematical software that takes as input a mathematical representation of a problem and tells whether or not the problem admits a solution.

In any verification problem, a solver is usually used to find solutions given a set of constraints. Some of these problems is solving equations, applying sorting or shortest path algorithms, finding the maximum and minimum values of a table or a continuous multi-variable function and so on. SAT or Satisfiability Problem can be summarized as: Given a formula φ with specified variables, the goal is to determine whether exists or not an interpretation for all variables for which φ is satisfied. Example of a sat problem: Find x ∈ R such that φ = {x 2 + 2x + 1 = 0}.

A verification problem can be coded as a formula that can be checked for a solution using a satisfiability solver, this is the case for diagnosability of discrete event systems.

Boolean SAT

It is the particular case where φ is a formula over Boolean variables. So one asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE.

If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is identically FALSE for all possible variable assignments and the formula is unsatisfiable. Example: The formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make the formula TRUE. In contrast, "a AND NOT a" is unsatisfiable.

Definition 2. K-SAT problem is : given a CNF formula f , in which each clause has exactly K literals, decide whether or not f is satisfiable. That is, whether there is an assignment to the atoms such that f evaluates to TRUE.

Satisfiability modulo Theories (SMT) [54]

Satisfiability modulo Theories (SMT) solvers couple a SAT solver with a solver of a given theory T to check the satisfiability of logical formulas whose atoms are interpreted in T. An SMT formula is generally quantified, i.e., can be expressed using ∀-universal quantifiers and ∃-existential quantifiers. For example, diagnosability verification of a timed automaton can be coded as a SMT problem. In particular, Satisfiability modulo ODEs solvers are suitable to reason about continuous and more generally hybrid systems. Many mathematical problems involving ODEs can be expressed as quantified SMT formulas, such as the following.

General Initial Value Problem Given a system of ODEs ẋ = f (t, x(t)) and a point (t 0 , x 0 ) in the domain of f , find a function x that is a solution to the ODE system and satisfies x(t 0 ) = x 0 . Some widely used SMT solvers are Z3 [START_REF] Moura | Z3: An efficient smt solver[END_REF], CVC [START_REF] Barrett | CVC4[END_REF], OpenMath.

Qualitative Modeling and Simulation

In this chapter, a summary of the principles of qualitative reasoning, modeling and simulation is presented as they will form a basis for the abstraction process considered in this thesis work. First, the basic concepts of qualitative reasoning are presented then the most important works accomplished in qualitative modeling and simulation are reviewed and discussed [START_REF] Louise Travé-Massuyès | Modèles et raisonnements qualitatifs[END_REF][START_REF] Eggers | Improving sat modulo ode for hybrid systems analysis by combining different enclosure methods[END_REF][START_REF] Nishida | Grammatical description of behaviors of ordinary differential equations in two-dimensional phase space[END_REF].

Qualitative Reasoning and Simulation

Intuitive concept Given an object or a concept, qualitative reasoning (or QR) refers to the usage of "quality" descriptors to illustrate it. For example, to characterize the mass of an object, one can reason numerically by attributing a real value for it under a certain precision metric. On the other hand, one can reason qualitatively: instead of giving a precise numerical value for the mass of an object, we point out that it is heavy. Consequently, the values that can be taken by the mass of the object which, when represented by real numbers, are infinite, are assigned a label from a finite qualitative set, e.g., Qal = {"light , "heavy }.

Quantitative mapped to Qualitative The qualitative labels are abstractions of numerical valuations, which implies naturally that a relation between both can be defined. Intuitively, a modeling approach that uses numerical procedures always considers (up to a certain sufficient precision) that the attributed numerical valuations to the model variables are a faithful and sufficient representation of reality. A qualitative modeling approach describes the valuations using ranges. Back to our simple object mass example, one can map numerical values to their qualitative sets. We define a mapping function α : R + → Qal by, e.g., α(x) = "light if x ∈ [0, 100] and α(x) = "heavy if x ∈ (100, +∞).

Safe modeling of partially known systems

If one is told this object is "heavy , one cannot point back the numerical value of the mass of the object. This implies the use of the partially provided information to reason about the object, with nevertheless frequently important decisions to make. Consider a robotic lifter arm whose maximum weight lifting capacity is of 100. The arm, provided the correct qualitative label assigned by α, can decide whether or not to lift the object without any further information. We remind next some of the main applications of QR (which are not limited to).

Application Domain Qualitative reasoning has been applied to numerous domains, such as robotics, computer science, formal methods and verification, modeling of cyber physical-systems, testing and prototyping, biology and so on. The usage of QR tackles the fundamental issue of states explosion when simulating systems with large number of dependent entities and when numerical simulations are not rigorous enough to validate the system. Qualitative reasoning is mainly present in, but not limited to:

• Artificial intelligence: this is one of the main domains where qualitative reasoning is used, as real time decision making processes require a fast recognition of the context in which to operate and do not necessarily require a high level of precision.

• Embedded Control and Signal Processing: computer programs are limited in computational resources and qualitative reasoning can provide information at the sufficient abstract level to make correct processing and controlling.

• Economics: specific data are unknown most of the time, but the changing behavior, such as prices fluctuation of stock markets, is known. Thus, qualitative reasoning can be used to model the partially known system and perform a simulation with the given information and "predict" the possible future fluctuations.

Qualitative models of continuous systems

In this section, we introduce the mathematical foundations of qualitative reasoning and some of the main works done in this field. As a start, we consider continuous systems modeled as a set of functions and we study qualitative models assigned to these systems. both limits lim t→a + f (t) and lim t→b -f (t) exist in R and are equal respectively to f d (a) and f g (b) when defined.

Continuity and Differentiability Reminders

[f is continuously differentiable] is equivalent to [f is differentiable (hence continuous) and f (x) is continuous] equivalent to the notation [f ∈ C 1 ]. A critical point of a differentiable function f is a point where the derivative of f is null. Let R = R ∪ {+∞} ∪ {-∞}. Definition 2.2 (Reasonable Function). A function f : [a, b] ⊆ R → R is reason- able if
Assumption 2.1. All functions modeling the constraints in the qualitative models we will consider in this section are assumed reasonable. , is a couple (q val , q dir ).

Landmarks of continuous functions

For a given real t 0 ∈ [a, b] then QS(f, t 0 ) is given by:

• q val (qualitative state value) is the landmark value f (t 0 ) if t 0 is a TDP, or the couple of the previous and next landmarks (l j , l j+1 ) encompassing f (t 0 ) if t 0 is not a TDP.

• q dir (qualitative state direction) is

+ if f (t 0 ) > 0, 0 if f (t 0 ) = 0 and -if f (t 0 ) < 0. Example 2.1 (Continuous Square Function). Consider f (x) = x 2 .
One of its landmark is 0 for the TDP x = 0. So, at the coarsest level, there are three qualitative states S 1 = ((-∞, 0), -), S 2 = (0, 0), S 3 = ((0, +∞), +). The number of qualitative states grows linearly with the number of landmarks. of f and open intervals between two such consecutive points: QS(f, t 0 ), QS(f, (t 0 , t 1 )), QS(f, t 1 ), ..., QS(f, t n ) such that, for all i, QS(f, (t i , t i+1 )) = ( t i <t<t i+1 q t val, q dir ) with (q t val , q dir ) = QS(f, t).

Qualitative Differential Equations (QDEs)

Ordinary differential equations An ordinary differential equation (ODE) describes the relation between real variables and their change w.r.t time. In other words, in dimension two for example, for a given time value t 0 for which the values of x and y are x 0 and y 0 , an ODE represents how the future (or past) values of the variables (i.e., after or before some infinitesimal time δt) are obtained according to the current values x 0 and y 0 and perhaps the time moment t 0 as well. This can be described as :

x(t 0 + δt) = f 1 (x 0 , y 0 , t 0 )δt (2.1)
y(t 0 + δt) = f 2 (x 0 , y 0 , t 0 )δt (2.2)
To model the variables change continuously, δt is supposed infinitesimally small, hence the usual representation of an ODE ẋ = f (x, t). ODEs are widely used to model systems with tightly dependent variables changing continuously with time.

Qualitative differential equations A qualitative differential equation (QDE) also constrains the future evolution of the variables according to their past values.

However, a QDE relaxes the constraints of the ODE, it is thus an abstraction of the ODE. The main difference between a QDE and an ODE is that the valuations of the variables belong to a finite domain instead of the usual R n . This finite domain is defined by given landmarks associated to time-distinguished points of a function. For example consider the differential equation ẋ = x + 1 assigning to each real value of x ∈ R + a value of the derivative ẋ with respect to time.

Suppose x is a traveling distance and ẋ is the traveling speed. And that, according to a specification, different actions are to be performed for each different speed interval from Qal = {"slow", "normal", "f ast"}, where "slow", "normal" and "f ast" label respectively the sets ẋ ∈ [START_REF] Akers | Binary decision diagrams[END_REF][START_REF] Falkenhainer | Cmpositional modeling: finding the right model for the job[END_REF], [START_REF] Falkenhainer | Cmpositional modeling: finding the right model for the job[END_REF][START_REF] Taha | Acumen: An Open-Source Testbed for Cyber-Physical Systems Research[END_REF], and (100, +∞). Given the partitioning Qal of ẋ we can define a qualitative differential equation as a mapping relating regions of x to regions of ẋ as:

∆X : Q → Qal (2.3)
where Q = {q slow , q normal , q f ast } such that: q slow = [0, 49], q normal = (49, 99] and q f ast = (99, +∞), and ∆X(q slow ) = slow, ∆X(q normal ) = normal, ∆X(q f ast ) = f ast.

Using automata to model qualitative differential equations

Definition 2.6 (Automaton). An automaton A is a tuple

A = (Q, Σ, T, Q 0 , Q F )
where:

• Q is a set of states

• Σ (or alphabet) is a finite set of labels (or symbols)

• T ⊆ Q × Σ × Q is a set of labeled transitions • Q 0 ⊆ Q and Q F ⊆ Q are sets

of respectively initial and final (also called accepting) states

An execution (or run) r of A is a sequence l 0 l 1 ...l n where l i ∈ Q, l 0 ∈ Q 0 and for each consecutive states l i l i+1 there is a label σ ∈ Σ such that (l i , σ, l i+1 ) ∈ T . If additionally l n ∈ Q F , then r is an accepting execution.

We can model a qualitative differential equation using an automaton. For this purpose, let A = (Q, T ) be a simple automaton where Q is a set of states and T is a set of transitions T ⊆ Q × Q. For our previous example, we consider each region of x as a state: q slow , q normal and q f ast . A transition t = (q 1 , q 2 ) ∈ T represents that there could be (but not necessarily) at least one trajectory initially in q 1 that reaches, after a certain time, q 2 (without reaching any other intermediate state between). For the state q slow this means two outgoing transitions t 1 = (q slow , q normal ), t 2 = (q slow , q slow ). Given only the two pieces of information x ∈ [0, 49] and ẋ ∈ [START_REF] Akers | Binary decision diagrams[END_REF][START_REF] Falkenhainer | Cmpositional modeling: finding the right model for the job[END_REF], we can conclude that an outgoing transition is guaranteed to an adjacent region, i.e., t 2 . Given an automaton A, then if ∃q ∈ Q, t = (q, q) / ∈ T then the region of q is a singleton and 0 / ∈ ∆X(q). In other words, we can relate any differentiable trajectory to a path of the automaton derived from the qualitative differential equation, however the inverse is not true. The constructed automaton provides a computational model over which model checking methods are applied to obtain verification results on the system. In our case, the automaton can provide non reachability results, i.e., deciding if some regions of the state space are never reached. Starting from a set of initial regions, a region is never reached if there is no path rooted in the set of initial states and leading to it in the corresponding automaton. The presented example is a simplified version taken from QSIM encyclopedia consisting of a U-shaped tube that shows a practical case to model a system using qualitative principles [START_REF] Kuipers | Qualitative simulation[END_REF]. Water is filled with two different levels A and B and a thin tube linking both of them (Figure 2.2). Water is added to tank A, which causes a pressure difference between the two tanks, water passes through the thin tube until both tanks have the same water level. The problem is studied using the variables: H A , H B water quantities (proportional to water levels) respectively in tanks A and B; P A and P B pressures at the bottom of tanks A and B respectively. The variables are continuous in time. The pressure in the tank increases with the amount of water, this constraint can be modeled qualitatively by P = g + (H) with g + some monotonically increasing continuous function. Let us associate landmarks to the model variables: to H A we associate L H A = {0, H A M AX , +∞} where H A M AX is the maximum water quantity in tank A and to P A we associate L P A = {0, +∞}.

Similar qualitative constraints are assigned to variables H B and P B . Additionally we know about the function g + that, if the tank is empty, then the pressure is null and analogically, infinite water quantity causes infinite pressure: thus we express these two statements with regards to the landmarks as g + (0) = 0 and g + (+∞) = +∞. The flow f lowAB in the thin tube (i.e., the quantity of water going through a section of the tube during a time unit) results from a pressure difference in the two tanks p AB = p A -p B , what we model by another monotonically increasing function f + such that f lowAB = f + (p AB ) with f + (0) = 0 and f + (+∞) = +∞. If the water quantity in A decreases then the quantity in B increases accordingly and vice versa, thus we have dH B dt = -dH A dt . The flow is equal to this water quantity variation:

f lowAB = dH B dt = -dH A
dt . The equations are qualitative differential equations where each variable V is not in R but in the finite domain L(V ) defined by the associated landmarks. The qualitative model is the set of all the constraints given previously (see Figure 2.3). In the next section, we recall the principles of simulating a given qualitative model.

g + A g + B H A H B P A P B f lowAB

Qualitative Simulation

After the modeling phase, one can perform a qualitative simulation that derives a set of possible behaviors from the model. Given an (or several) initial qualitative state, the simulation computes successors of it. Once a fixed point has been reached, i.e., the successors are not new qualitative states, the simulation stops.

Since the qualitative space is finite when the considered functions are reasonable, termination of the qualitative simulation algorithm is guaranteed. The successor is computed by applying a set of rules relying on the continuity and differentiability assumptions. The simulation results can be used to verify if specifications or desired properties are met, i.e., for model checking purposes [START_REF] Kuipers | Qualitative reasoning: modeling and simulation with incomplete knowledge[END_REF]. Adaptive reasoning can be incorporated to the simulation, whereas some significant points can be identified and used in the simulation, increasing the size of the landmarks set and thus the accuracy of the simulation (the number of dynamically created landmarks has to be finitely bounded to guarantee termination of the simulation).

Compared to numerical approaches, qualitative simulation allows the usage of only partial information provided about the system (derivative sign, curvature points, other important points) and termination of the simulation is guaranteed since the state space is abstracted to a finite space. On the other hand, one looses the accuracy that is provided by a numerical approach. The fundamental steps are:

• Find the landmarks of all continuous functions representing the system.

• Find all qualitative states whose landmarks cover the given initial set. Mark these states.

• Compute successor qualitative states of each marked state by applying the qualitative rules and unmark it.

• Stop the computation when all states are unmarked.

The result is a graph where each path is a sequence of qualitative states (QS 0 , ..., QS n ) where QS i+1 is a successor of QS i . Every change from one qualitative state to another is associated to a time-distinguished point. The graph illustrates possible behaviors of the system and can be analyzed to verify given specifications.

Example 2.3 (U-shaped tube). Qualitative Simulation The simulation provides a set of the different possible behaviors of the system. Back to the U-tube example, we know that from any initial state, the levels in the two tanks will converge to become equal and the flow f lowAB to become null. Consider an initial state where tank A is full and B is empty, i.e., H A = H Amax and H B = 0. Let us find the initial qualitative states for the rest of the variables together with their derivative signs. By inference rules, P B = 0 and P A = (0, +∞), consequently

Qualitative Variable p AB = (0, +∞). Similarly f lowAB = (0, +∞) which determines that the flow is from A to B, i.e., qdir(H A ) = -and qdir(H B ) = +. g + A , g + B and f + are monotonically increasing functions, which implies that qdir(P A ) = -and qdir(P B ) = + and then qdir(P AB ) = -and finally qdir(f low AB ) = -. This completes all valuations of the initial qualitative state QS(t = 0) (Table 2.1). Let us compute the successor states of QS(t = 0), i.e., the the new possible valuations of the qualitative variables at a time t > t 0 . H B is initially zero and increasing, since the increase process is continuous thus in the next state H B will be positive and still increasing. Similar reasoning is applied to the rest of the variables to obtain the successor qualitative state (Table 2

q val q dir H A H Amax - H B 0 + P A (0, +∞) - P B 0 + P AB (0, +∞) - f lowAB (0, +∞) -
q dir q val q dir q val q dir H A (0, H Amax ) 0 (0, H Amax ) 0 (0, H Amax ) - H B H Bmax 0 (0, H Bmax ) 0 H Bmax + P A (0, +∞) 0 (0, +∞) 0 (0, +∞) - P B (0, +∞) 0 (0, +∞) 0 (0, +∞) + P AB 0 0 0 0 (0, +∞) - f lowAB 0 0 0 0 (0, +∞) - Table 2.
3: Branching of successor qualitative states

Hybrid Systems Verification

This section reviews the literature concerned with verification methods for hybrid systems and more specifically reachability analysis. In the existing literature, we distinguish several modeling frameworks for hybrid systems: hybrid automata, Petri nets, hybrid bond graphs and hybrid programs. In this thesis, we adopt hybrid automata as models of hybrid systems because of their common use in the scientific community and their intuitive way of coupling finite state machines with differential equations. A formal definition of a hybrid automaton and its semantics are proposed in chapter 3 and will be used for the following sections (Def. the set of all executions of H (i.e., the semantics of H).

Hybrid Automata Reachability Analysis

Reachability analysis for hybrid systems received a considerable attention in the literature due to the emerging need for formal verification of complex critical systems, in particular of cyber-physical systems.

Reachability Problem Statement Let B be a set of states. We wish to verify if any execution of H starting from its initial set reaches B at some time. Determining the reachable set of states with certainty decides whether or not the system is safe. However, for hybrid systems, reachability analysis is generally undecidable. We summarize and review three large categories of hybrid automata verification techniques: numerical simulations, over(under)-approximation flow-pipes and invariant synthesis, and symbolic abstraction techniques.

Numerical Simulation

Let C = (X, S 0 , F, Inv) be a continuous system, where the dynamics F is given by Lipschitz continuous functions w.r.t. all variables in X. Given an element x 0 from the set S 0 then numerical simulation consists in computing a trajectory φ : T → R at some time points T ⊆ R + starting from the initial element φ(t 0 ) = x 0 . This trajectory is unique for a given x 0 as stated by the Picard-Lindelof theorem. Numerical simulation explores the reachable set of states depth first. This method examines trajectories one by one. The exact trajectory is abstracted to a set of points computed at specific time moments via the integration step ∆t. To validate a model via numerical simulations, a number of them are performed and when each of them does not violate the safety property then the system is supposed safe up to the considered precision (estimated from the integration step and the tolerated approximation error). Numerical simulations are aimed at local verification given some bounded local error and are not suitable for studying a modeled perturbation. Today, numerical simulation is widely used to validate and test models in the industry. Many schemes have been elaborated for numerical simulations such as Runge-Kutta and Euler's method. Matlab & Simulink offers a wide library of models applied in diverse fields and is of common use for academics and industry. The simulation part in the software is limited to numerical simulation. The simulation algorithm such as ode45 is sophisticated and is able to use shortcuts in some situations in an ad hoc manner for increased computation efficiency or precision.

In critical industry applications notably Avionics, the certification process remains today time consuming and often based on documentation. Consequently, there is an emerging urgent need for tools with better formal basis, where the reached precision is accurately quantified. Set-based simulation consists in computing the reachable states from the whole initial set S 0 , this is a breadth first search and will be reviewed in the next paragraph. The Acumen simulator applies numerical simulation while having solid underlying semantics [START_REF] Taha | Acumen: An Open-Source Testbed for Cyber-Physical Systems Research[END_REF], it offers a good understanding of the underlying computations in such a way that the user is directly confronted to problems that could arise such as the zero-crossing problem. The latter problem occurs when the chosen precision is not enough to test whether or not the computed trajectory satisfies a given condition.

Flow-pipe methods

The term flow-pipe has been coined as an over-approximation set of reachable states of a continuous dynamical or hybrid system given an initial set of states [START_REF] Chen | Taylor model flowpipe construction for non-linear hybrid systems[END_REF][START_REF] Maler | Algorithmic verification of continuous and hybrid systems[END_REF][START_REF] Lal | Bounded error flowpipe computation of parameterized linear systems[END_REF][START_REF] Bak | Reducing the wrapping effect in flowpipe construction using pseudoinvariants[END_REF]. In the next chapter we will review some tools that compute the flow-pipe of the executions of a hybrid system from the initial set of states. These tools showed success in verifying safety and robustness in reaction to perturbations or uncertainty. The mathematical foundation of the tools relies on set based integration and safe approximations of functions. Intuitively, the idea is the following: given the initial set and the differential equations attributing locally the first order derivative of each variable, a safe upper bound of the first order derivative is computed. Then, given a time step, the computed bounds derive a constraint over the variables valuations, representing parts of the state space that cannot be reached at this time step. For example, a car is at distance d = 0 and running at 2km/min initially at t = 0. A safe lower and upper bounds of 2 are 1 and 3, the car is supposed never to over-or-underpass these bounds. At t = 5min, we can safely say that the car is at a distance of at least 5km and not exceeding 15km. In general, the exact first derivative is not constant but it is continuously changing according to the variables of the state space and possibly time. Consequently, the bounds over the dynamics are changing with time and must be computed accordingly..

Computing a flow-pipe Algorithm 1 presents a rough scheme for computing a flow-pipe with some notation abuse.

input : H := Hybrid Automaton; ∆t := Time Step (float precision real); T := Time Horizon (float precision real) output: Flow-pipe := F low(H) F low ← {(q 0 , Init(q 0 )}; T ime ← 0; List ← F low; while List = ∅ ∧ T ime < T do (q, S) ← List.pop(); C ← ContinuousTimeElapsed (S, ∆t);

T ime ← T ime + ∆t; F low ← F low ∪ {(q, C)}; for G guard in q do D ← ComputeDiscreteJump (C, G); if D = ∅ then List ← List ∪ {D}; end end return F low;
Algorithm 1: Hybrid automaton flow-pipe computation rough scheme Algorithm operations The algorithm does not present all the required details, for example one needs to remove from F low the parts that do not satisfy the invari-ant of each mode but this operation has been omitted. It is written here for only one initial mode. The reachability algorithm requires operations over the states S, represented each one by a subset of R n . The main procedures that are required are:

• ContinuousTimeElapsed (S, ∆t): given a state S reached at some time t and the time step ∆t, the procedure computes a continuous successor of S denoted S reached at t + ∆t. All the concrete trajectories of H initially in S are in S after ∆t time units have elapsed. The procedure is the challenging part in reachability computation because it requires using the dynamics of H to extract S .

• ContinuousDiscreteJump (S 1 , S 2 ): given two states S 1 and S 2 in a mode, where S 2 corresponds to the change of mode condition associated to a transition from this mode (also called guard/jump condition), this operation computes the reachable set via the discrete jump. In other words, an intersection between the guard and the current reached set is computed then its image via the reset (if present) is computed.

Additionally, the regular set based operations are used by the reachability algorithm such as: Minkowsky sum ⊕, Union ∪ and intersection ∩.

Forward and backward reachability Flow-pipe computation tackles straightforwardly safety verification, the time step for integration is always taken forward starting from the initial set. To incorporate the specification (i.e., the unsafe set), many tools compute two flow-pipes: the first one, F low(S 0 , T ) is initialized the initial set with a forward time integration step and the second F low(B, T ) is initialized from the unsafe set with a backward integration time step (Figure 2.4).

If the two flow-pipes do not intersect, the system is safe, if not, back and forth operations are applied to further refine the flow-pipes until a specified precision is achieved (i.e., computing more accurate bounds) [START_REF] Mitchell | A time-dependent hamiltonjacobi formulation of reachable sets for continuous dynamic games[END_REF]. Computing two flow-pipes instead of one reduces the computation time for the verification process by making use of parallelism. resentation. An important concern in these methods is to balance the trade off between accuracy and computation complexity [START_REF] Maler | Algorithmic verification of continuous and hybrid systems[END_REF]. The need for accuracy is seen when computing the continuous time elapsed, where the error between the overapproximate representation and the actual concrete state should be bounded. The computation complexity arises when performing operations such as set addition (Minkowsky sum), intersection and union. We review important state representations.

S 0 B F low(S 0 ; T ) F low(B; T 0 ) _ t f orward = 1 _ t backward = -1
Convex sets have been extensively studied as state representations.

Definition 2.7 (Convex Set). A set S = {x | x ∈ R n } is convex if
and only if for all x and y in S and any real λ ∈ (0, 1), (1 -λ)x + λy ∈ S.

A convex polyhedron is obtained by intersecting any number of half-spaces (Figure 2.5). A polytope is a bounded convex polyhedron.

Definition 2.8 (Hyper-rectangle). A hyper-rectangle HR of dimension n is a subset of R n such that HR is a product of boxes: HR = n i=1 I i where each I i is an interval over the reals.

ã1 T :x + b1 = 0 ã2 T :x + b2 = 0 ã3 T :x + b3 = 0 ã4 T :x + b4 = 0 ã5 T :x + b5 = 0 ã6 T :x + b6 = 0 Figure 2.5: Convex polytope, intersection of half-spaces Zonotopes Definition 2.9 (Zonotope). A zonotope Z = (G, c) where G ∈ R n×m is the gen- erator vectors set matrix with m, n ≥ 0, c ∈ R n is called the center of Z is the set Z ⊂ R n such that: Z = {x ∈ R n | ∃a ∈ [-1, 1] m , x = G.a + c} (2.4)
A zonotope is symmetrical w.r.t to its center c, a more generalized representation that is not necessarily symmetrical is given by star sets. A star set is the intersection of a zonotope with a set defined by some predicate constraints.

Example 2.4 (Flow-pipe computation using zonotopes). Consider the following linear system where the initial set is given by a hyper-rectangle set x(0) and the state x(t) is subject to bounded perturbation given by a zonotope u(t). We use CORA, a tools suite for reachability computation of continuous and hybrid systems, to compute the flow-pipe of the system using zonotopes (Figure 2.6).

The flow-pipe (in grey) is computed till the time horizon T = 5 time units. Matlab

Simulink is used to run numerical simulations randomly generated from the same initial set observed in black.

ẋ =       -1 -4 0 0 0 4 -1 0 0 0 0 0 -3 1 0 0 0 -1 -3 0 0 0 0 0 -2       x+u(t), x(0) ∈      
(0.9, 1.1) (0.9, 1.1) (0.9, 1.1) (0.9, 1.1) (0.9, 1.1)

      , u(t) ∈       0.9, 1.1 (-0.25, 0.25) (-0.1, 0.1) (0.25, 0.75) (-0.75, -0.25)       (a) (b)
f (x) = P n (x) + R n (x) (2.5)
where for some c ∈ (a, b)

P n (x) = f (c) + f (c) 1! (x -c) + f (c) 2! (x -c) 2 + ... + f (n) (c) n! (x -c) n (2.6)
And if f (n+1) exists and is continuous on an open interval containing c and x is in this interval, then there is some d ∈ (x, c) between such that:

R n (x) = f (n+1) (d) (n + 1)! (x -c) n+1 (2.7) Definition 2.10 (Over-approximative Taylor model). Given a polynomial p ∈ R[X]
, where X is a set of n variables, an interval I, and a function f defined over a domain U ⊆ R m , then (p, I) is an over-approximative Taylor model of f if:

∀x ∈ U, f (x) ∈ p(x) + I (2.8)
To construct an over-approximative Taylor model of a function f one can: compute till a certain order the Taylor polynomial of f , find the interval I = (q, r) using the remainder.

q ≤ R n (x) ≤ r ⇒ P n (x) + q ≤ P n (x) + R n (x) ≤ P n (x) + r ⇒ p 2 (x) ≤ f (x) ≤ p 1 (x) (2.9)
Example 2.5 (Taylor model of e x ). Consider f (x) = e x and x ∈ (-1, 1). We use a method proposed in previous works to find a suitable Taylor model of f (x) [START_REF] Chen | Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models[END_REF]. Compute the Taylor polynomial at the midpoint of (-1, 1) till a certain order then evaluate a upper and lower bound of the remainder. Observing Table 2.4,

Polynomial Order k P I 0 1 [-0.75, 1.75] 1 1 + x [0,0.75] 2 1 + x + x 2 2 [-0.25,0.25] 3 1 + x + x 2 2 + x 3 6 [0.0345,0.0517] 4 1 + x + x 2 2 + x 3 3! + x 4 4!
[-0.02266, 0.02266] Table 2.4: Taylor polynomial of the exponential function with a safe remainder interval we notice that the higher the computed Taylor polynomial order is, the lower the remainder error (given by I) is. If the computation of the remainder satisfies:

f (x) -P k (x) converges to zero if k → +∞,

Abstraction Techniques

Flow-pipe computation provides methods for accurately computing the reachable set, however termination of the algorithm cannot be generally guaranteed without specifying the time horizon T . In some situation, self-containment is achieved (i.e., there is some time instant t < T for which the flow-pipe part obtained at time t + ∆t is totally contained within one or more of the flow-pipe parts computed at times before t). Consequently, flow-pipes remain a bounded model checking algorithm suitable for continuous dynamical and hybrid systems. In many applications, verifying time-unbounded properties is necessary, most notably in controller certification. Some techniques emerged for synthesizing invariants, i.e., sets that hold for any time t. The main idea is to find functions in the state space over which all change directions point inwards. We review in this part existing abstraction methods and invariant synthesis techniques.

Abstraction Methods Abstraction methods extract information from a given model to show a desired behavior or property. Figure 2.7 illustrates the high level scheme for abstracting a hybrid automaton H into an abstract system A via the abstraction function α. These methods retain important information from the hybrid system that are possibly "sufficient" to prove the property. These properties can range from reachability or liveness of a set of states to more complex ones. In the existing literature, authors studied and elaborated different abstraction methods of a given hybrid system model. Methods for constructing quality abstractions cannot be automated for the broad class of hybrid automata. This is explained by the fact that many differential equations have no closed form solutions and it is thus difficult to define a general abstraction method that would apply for any continuous change. Two fundamental issues have to find a solution by any abstraction method:

• Describe formally the abstraction method M that produces the abstract system given the concrete one (and automate the construction operations as much as possible) and give the algorithmic steps to compute it.

• Give the necessary proofs that once the abstract system, constructed with the method M , verifies property F (P ) then the original hybrid system verifies P where F relates a concrete property to its abstract counterpart. Or more generally, deduce a class of properties that is preserved in the abstraction constructed using method M .

Other questions follow naturally the previous ones such as the time and space complexity of the abstraction algorithm, termination and worse execution time, application of the method in a distributed framework and so on. An example is the state reachability property which is undecidable for hybrid systems. Nonetheless, if the abstract system falls within the decidable class, then the abstract counterpart of the property can be verified using classical model checking algorithms. If the property is verified at the abstract level, the abstraction relation allows one to infer this result back to the original hybrid system.

Predicate Abstraction Hybrid systems are generally infinite state machines.

Early work in [START_REF] Alur | Reachability analysis of hybrid systems via predicate abstraction[END_REF][START_REF] Alur | Progress on reachability analysis of hybrid systems using predicate abstraction[END_REF] shed the light on the completeness of abstracting infinite state machines into finite ones for linear dynamical hybrid systems. The infinite space of the hybrid system is abstracted into the finite possible valuations of a given set of linear predicates. A valuation represents concretely a convex polyhedron. From each obtained abstract state, transitions towards other abstract states are computed according to the continuous and discrete changes. To compute transitions outgoing from an abstract state A a flow-pipe is computed with the concrete set In [START_REF] Gulwani | Constraint-based approach for analysis of hybrid systems[END_REF][START_REF] Tiwari | Abstractions for hybrid systems[END_REF][START_REF] Tiwari | Series of abstractions for hybrid automata[END_REF][START_REF] Sankaranarayanan | Relational abstractions for continuous and hybrid systems[END_REF], Tiwari proposed to combine predicate abstraction with qualitative reasoning to have a more representative abstraction; his work is of an important basis for this thesis. A study for timing the abstraction is given in a complementary article [START_REF] Mover | Time-aware relational abstractions for hybrid systems[END_REF]. In [START_REF] Sloth | Complete abstractions of dynamical systems by timed automata[END_REF], Sloth addresses abstractions of non-linear systems with polynomial dynamics. The idea is to generate a partitioning of the state space, whose abstraction is always complete and in some cases sound. For soundness, the task is formulated as an optimization problem that could yield results similar to those obtained by invariant synthesis techniques. Nonetheless, the termination of the optimization procedure is generally not guaranteed. [START_REF] Chen | Compositional relational abstraction for nonlinear hybrid systems[END_REF] combines in a recent work relational abstractions and flow-pipe constructions allowing one to cover a larger class of properties, and shows that using each method separately fails to do so.

A 1 A 2 A 3 F low(A 2 ; T ) F low(A 3 ; T 0 )
Invariant Synthesis Seen from a computational perspective, invariant computation consists in computing a set of mathematical constraints satisfied by all states of the system. The property we wish to prove is expressed as a set of constraints as well. One can then check if the property constraints violate any of the computed invariant constraints, if none is violated then the system verifies this property. Invariant computation is difficult and not automatic as the form of the invariant varies differently with the form of the dynamics and other components of the hybrid system. Some techniques assume the invariant takes a template form. For example, for a linear invariant with two real variables x, y, the form can be αx + βy = 0 with α and β two unknown constants. Then one encodes the hybrid system, the property to verify and a specific parametric form of the invariant into an SMT (Satisfiability Modulo Theories) based solver and evaluates the unknown parameters α and β of the invariant automatically [START_REF] Gulwani | Constraint-based approach for analysis of hybrid systems[END_REF]. Other techniques attempt to generate barrier certificate functions that enclose the reachable set of states.

A barrier certificate is an inductive invariant that helps in safety verification of dynamical and hybrid systems. For a given system, if a barrier certificate function is found and does not intersect the unwanted set of states, the system is considered safe and that is valid for any execution within the barrier certificate and for unbounded time (Figure 2.9). The main challenge is to find barrier certificates that can be efficiently encoded (i.e., expressed in a usable form), as their structure can become complex [START_REF] Kong | Exponential-conditionbased barrier certificate generation for safety verification of hybrid systems[END_REF][START_REF] Djaballah | Construction of parametric barrier functions for dynamical systems using interval analysis[END_REF]. Recently, generating barrier certificates was applied to safety verification in a compositional framework [START_REF] Sloth | Compositional safety analysis using barrier certificates[END_REF].

B X 0
Figure 2.9: A barrier certificate enclosing the reachable set of states from X 0 without intersecting the unwanted set of states B

Counter-Example Guided Abstraction Refinement (CEGAR)

The CEGAR loop consists in combining the abstraction model checker together with a refinement method of the abstraction. Since model-checking can be inconclusive (i.e., when the abstraction is not sufficient to establish the proof), one can refine the abstraction for further precision. We now recall counter-example guided abstraction refinement (CEGAR) that was originally proposed to verify safety properties [START_REF] Edmund | Verification of hybrid systems based on counterexample-guided abstraction refinement[END_REF][START_REF] Alur | Counterexample-guided predicate abstraction of hybrid systems[END_REF]. Very generally, CEGAR is an incremental way to decide if a problem admits a solution. The method starts with very coarse abstraction of the original problem, checks the abstraction for a solution, then depending on whether or not a solution is found concludes that the original problem is solvable or that the abstraction does not retain enough information to make a decision. In the latter case a refinement is applied (i.e., information is added to the abstraction from the original problem) and the verification procedure is repeated on the refined abstraction.

As example, consider in our case the following situation, which will be made precise in the next chapters. Given a hybrid automaton H, a set B ⊂ S of so-called "bad" states, where S = Q × X is the state space of H, we say that H is safe with respect to B if and only if there is no execution in H from an initial state to a bad state in B. Otherwise, we say that H is not safe. This safety property is thus expressed as H |= AG¬B in Computation Tree Logic (CTL), which means that all hybrid automaton executions never reach a bad state from B. An execution h = (q 0 , x 0 )

l 0 -→ (q 1 , x 1 )...(q m , x m ) with (q m , x m ) ∈ B is called a counterexample of H with respect to this safety property.
Let DA a discrete automaton obtained by applying an abstraction function α on H. We say that ĥ = ŝ0 l0 -→ ŝ1 ... ŝm is the abstract counterexample of DA corresponding to h, if ŝi = α(q i , x i ) holds ∀i ∈ {0, ..., m}. Reciprocally, given a counterexample ĥ of DA, h is called a corresponding concrete counterexample if ŝi = α(q i , x i ) and (q i , x i )

l i -→ (q i+1 , x i+1 ) ∈→,
where → is a transition relation of the labeled transition system representing the semantics of H. If a counterexample ĥ of DA has no corresponding concrete counterexample of H, then ĥ is called a spurious counterexample. The following theorem expresses that if the safety property is satisfied at the abstract level then it is satisfied at the concrete level. Now we introduce a scheme for CEGAR to verify safety properties for a given hybrid automaton, whose idea is to repeat the following steps until the considered property is verified or refuted (it is assumed that α(q i , x i+1 ) ∈ B implies (q i , x i+1 ) ∈ B):

1. analyze DA |= AG¬ B with model checking:

• if the property holds, return the conclusion that H is safe from Theorem 2.1;

• if it does not hold, a counterexample is obtained before turning to 2;

2. validate whether this counterexample has a corresponding concrete counterexample in H:

• if there does exist a corresponding concrete counterexample, then return that H is not safe;

• otherwise, the counterexample is spurious and thus is used to refine DA before returning to 1 by replacing DA with the newly obtained refined abstraction.

System Diagnosability

In this section we review works concerned with diagnosability verification of hybrid systems and the particular classes of discrete event systems and timed automata.

Diagnosability Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on the system property called diagnosability. This is a property describing the ability to determine without ambiguity whether a fault of a given type has effectively occurred based on the observations provided by the system. Diagnosability analysis has already received considerable attention in the literature over latest decades. However, most of the existing works refer to discrete event systems [START_REF] Sampath | Diagnosability of Discrete Event System[END_REF][START_REF] Cimatti | Formal Verification of Diagnosability via Symbolic Model Checking[END_REF][START_REF] Pencolé | Diagnosability Analysis of Distributed Discrete Event Systems[END_REF][START_REF] Schumann | A Scalable Jointree Algorithm for Diagnosability[END_REF][START_REF] Grastien | Symbolic testing of diagnosability[END_REF][START_REF] Ye | Diagnosability Analysis of Discrete Event Systems with Autonomous Components[END_REF][START_REF] Germanos | Diagnosability under weak fairness[END_REF] with stochastic and fuzzy variants [START_REF] Thorsley | Diagnosability of stochastic discrete-event systems[END_REF][START_REF] Liu | Safe diagnosability of stochastic discrete-event systems[END_REF][START_REF] Kilic | Diagnosability of fuzzy discrete event systems[END_REF] or continuous systems [START_REF] Chen | A re-examination of the relationship between. parity space and observer-based approaches in fault diagnosis[END_REF][START_REF] Basseville | On fault detectability and isolability[END_REF][START_REF] Nyberg | Criterions for detectability and strong detectability of faults in linear systems[END_REF][START_REF] Travé-Massuyès | Diagnosability analysis based on component-supported analytical redundancy relations[END_REF]. Diagnosability was also studied in the framework of decentralized and distributed architectures [START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF][START_REF] Ribot | Design requirements for the diagnosability of distributed discrete event systems[END_REF][START_REF] Yan | Diagnosability for Patterns in Distributed Discrete Event Systems[END_REF][START_REF] Melliti | Generalizing diagnosability definition and checking for open systems: a Game structure approach[END_REF]. But many modern technological processes exhibit both continuous evolution and discrete transitions, whose combination is at the origin of complex behavior and important phenomena of such systems. To the best of our knowledge, very few works handle diagnosability of hybrid systems with satisfactory results. Given a model that describes both correct and faulty behavior and what is presumed observable (i.e., generated externally by the model), then the model is said to be diagnosable if the observations are enough to determine that a fault has occurred and, in the case of multiple faults, to identify which one of them happened. The diagnoser is a function which, given an observable trace of the system, is able to decide whether or not a fault has occurred. Thus, the model is diagnosable if and only if such a function exists. For example, if a and b are the only two observable events and u and f are two unobservable events where f corresponds to the fault event, then given a generated observable trace ab, one cannot determine, with certainty, whether the model behavior (i.e., combined with the unobservable events) corresponds for example to ab or aub or af b (if the three may exist) and thus whether the faulty event f occurred or not.

Diagnosability of discrete event systems

As a first step, [START_REF] Travé-Massuyès | Comparing diagnosability criterions in continuous systems and descrete events systems[END_REF] proved that the existing definitions of diagnosability for discrete event systems and for con-tinuous systems can be stated as a property of the system fault signatures (w.r.t.

normal behavior signatures), and a unified definition of diagnosability was established. However hybrid systems diagnosability was not considered. Among the contributions concerned with hybrid diagnosability, we can mention [START_REF] Biswas | Diagnosability analysis of real time hybrid systems[END_REF] that slightly modified the classical necessary and sufficient condition for diagnosability of a discrete event system of [START_REF] Sampath | Diagnosability of Discrete Event System[END_REF] and expressed it in terms of reachability. [START_REF] Fourlas | Diagnosability of hybrid systems[END_REF] generalized this condition requiring more restrictive hypotheses. Despite the claim that the two above methods deal with hybrid systems, these works do not really account for the hybrid nature of the system as they use only a very high level discrete abstraction and ignore the continuous dynamics. On the other hand, in [START_REF] Cocquempot | Fault detection and isolation for hybrid systems using structured parity residuals[END_REF], diagnosability is expressed in terms of mode discernability (also called distinguishability by other authors) and is only based on the continuous dynamics.

Diagnosability of time-dependent systems (timed automata) Diagnosability for systems with time constraints classically modeled using finite state machines with clocks (i.e., real valued variables with constant dynamics) has been studied [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF]. This type of models describes a more general class of systems than discrete event systems (DES), the clocks can measure the sojourn time in a state and constraints to enable a transition can be based on the clock valuations. Timed automata, a class of hybrid automata, are extensively used to model finite state machines with clock variables. Diagnosability of timed automata reveals a more challenging task than DES: in fact, the executions generated by discrete event systems are regular and many efficient algorithms exist for solving emptiness and reachability problems. This is possible since such models can be determinized. However, timed automata and more generally hybrid automata, cannot be usually turned to deterministic models, hence property verification becomes more complex at the expense of expressiveness. When a feasible diagnoser exists, the model is diagnosable. Some works aimed further at finding a deterministic diagnoser which itself is a timed automaton. It has been shown that for deterministic timed automata (DTA), it is decidable to check whether a diagnosis function is realizable and that its complexity class is 2EXP T IM E [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF]. This class supposes that any two outgoing transitions from a given state cannot be labeled by the same event as long as their guards are enabled for the same valuations (i.e., the events are time-deterministic). A method describing the conditions to obtain a diagnoser as a deterministic timed automaton is also described.

Diagnosability of Hybrid Systems [START_REF] Bayoudh | Coupling continuous and discrete event system techniques for hybrid systems diagnosability analysis[END_REF] was among the early works that coped with actual hybrid systems, introducing the idea to consider a hybrid model as a twofold mathematical object. A hybrid system is modeled as a hybrid automaton whose discrete states represent its operation modes for which the continuous dynamics are specified. The discrete event part (automaton) constrains the possible transitions among modes and is referred to as the underlying DES. The restriction of the hybrid system to the continuously-valued part of the model is defined as the multimode system. Considering the analytical redundancy approach to define a set of residuals [START_REF] Gertler | Fault Detection and Diagnosis in Engineering Systems[END_REF] for every mode, [START_REF] Bayoudh | Coupling continuous and discrete event system techniques for hybrid systems diagnosability analysis[END_REF] introduced the concept of mode signature which refines the classical concept of fault signature. Mode signatures determine mode distinguishability. The key idea of [START_REF] Bayoudh | Coupling continuous and discrete event system techniques for hybrid systems diagnosability analysis[END_REF] is to abstract the continuous dynamics by defining a set of "diagnosis-aware" events, called signature-events, associated to mode signature changes across modes. Signature-events are used to enrich appropriately the underlying DES. The behavior of the abstract system is then modeled by a prefix-closed language over the alphabet enriched by these additional events.

The finite state machine generating this language is called the behavior automaton.

Based on the abstract language, the diagnosability analysis of the hybrid system is cast into a discrete event framework and standard methods of this field can be used.

The approach of [START_REF] Bayoudh | Coupling continuous and discrete event system techniques for hybrid systems diagnosability analysis[END_REF] later consolidated in [START_REF] Bayoudh | Diagnosability analysis of hybrid systems cast in a discrete-event framework[END_REF] can be compared to the approach proposed in [START_REF] Daigle | An event-based approach to integrated parametric and discrete fault diagnosis in hybrid systems[END_REF][START_REF] Daigle | A comprehensive diagnosis methodology for complex hybrid systems: A case study on spacecraft power distribution systems[END_REF] which uses fault signatures to capture the continuous dynamics. The fault signatures of [START_REF] Daigle | An event-based approach to integrated parametric and discrete fault diagnosis in hybrid systems[END_REF][START_REF] Daigle | A comprehensive diagnosis methodology for complex hybrid systems: A case study on spacecraft power distribution systems[END_REF] are based on fault transients and they directly express the expected dynamic behavior of measured variables after the fault abstracted in qualitative terms. The approach of [START_REF] Bayoudh | Coupling continuous and discrete event system techniques for hybrid systems diagnosability analysis[END_REF][START_REF] Bayoudh | Diagnosability analysis of hybrid systems cast in a discrete-event framework[END_REF] differs in that it uses mode signatures that are specifically built for diagnosis, based on standard analytical redundancy residual methods of the FDI control field [START_REF] Ding | Model-based fault diagnosis techniques: design schemes, algorithms, and tools[END_REF]. Its originality relies in that it proposes a way to integrate these methods with equally standard methods of the DES diagnosis field [START_REF] Zaytoon | Overview of fault diagnosis methods for discrete event systems[END_REF]. [START_REF] Bayoudh | Coupling continuous and discrete event system techniques for hybrid systems diagnosability analysis[END_REF][START_REF] Bayoudh | Diagnosability analysis of hybrid systems cast in a discrete-event framework[END_REF] adopt the diagnoser approach [START_REF] Sampath | Diagnosability of Discrete Event System[END_REF] because it has the advantage to also support straightforwardly online diagnosis. [START_REF] Diene | Analysis and verification of the diagnosability of hybrid systems[END_REF] repeats these ideas differing by the fact that the diagnoser is directly built from the underlying DES and mode distinguishability is used to cluster its state labels. This method leads to a so-called clustered diagnoser. Let us note that this method only applies to a restricted class of hybrid systems for which transitions triggered by continuous dynamics are not allowed.

Checking DES diagnosability with methods based on the construction of diagnosers has exponential complexity with the size of the underlying DES automaton.

Hence, approaches based on verifiers, also known as twin plant approaches, are generally preferred. This is because, although a twin plant cannot be used for online diagnosis, it can be constructed in polynomial time. Methods integrating a twin plant approach with mode distinguishability checking for assessing hybrid system diagnosability are recent. The reader can refer to [START_REF] Diene | Computational methods for diagnosability verification of hybrid systems[END_REF] as a first piece of work in this direction. Later, [START_REF] Grastien | Solving diagnosability of hybrid systems via abstraction and discrete event techniques[END_REF] indicated that mode distinguishability could be complemented by another property of the continuous dynamics named ephemerality. Ephemerality states when the system cannot stay forever in a given set of modes. The continuous dynamics are hence abstracted remembering only these two pieces of information. In addition to this, [START_REF] Grastien | Solving diagnosability of hybrid systems via abstraction and discrete event techniques[END_REF] checks diagnosability in an incremental way. It starts by generating the most abstract DES model of the hybrid system and checking diagnosability of this DES model. A "counterexample" that negates diagnosability is possibly provided based on the twin plant. The model is then refined to try to invalidate the counterexample and the procedure repeats as far as diagnosability is not proved. This approach hence uses just the necessary information about continuous dynamics, in an "on request" manner, hence making the best out of computation. In the most recent literature concerned with hybrid system diagnosability like [START_REF] Grastien | Solving diagnosability of hybrid systems via abstraction and discrete event techniques[END_REF] and also [START_REF] Deng | Verification of hybrid automata diagnosability with measurement uncertainty[END_REF], which characterizes the maximum delay for diagnosing faults given measurement uncertainty, abstraction is key. Abstraction is also at the core of other methods to check other properties of hybrid systems.

Diagnosability via abstraction [START_REF] Di Benedetto | Verification of hybrid automata diagnosability by abstraction[END_REF] applied the use of abstractions as timed automata to diagnosability verification and showed that for a certain class of abstractions, the verification problem belongs to the complexity class P . [START_REF] Deng | Verification of hybrid automata diagnosability with measurement uncertainty[END_REF] presents a procedure to determine the (δ d , δ m )-diagnosability of a hybrid system where δ d is the maximum time to diagnose a fault after its occurrence and δ m is a precision metric representing the uncertainty in measuring the observable events. The method, given a hybrid automaton H with initial set of hybrid states S 0 , a precision metric , a time horizon T end , operates as follows. Find a set of so-called robust neighborhoods around elements from S 0 where the executions initially in one of these neighborhoods are alike, having the same observable events and are consistent in time until the specified horizon T end . This similarity relation is defined formally using Hausdorff distance metrics guaranteeing the time consistency up till a certain imposed precision . Continue finding neighborhoods until S 0 is fully covered by them. The abstraction is formed by the many sets of executions from each of the computed neighborhoods. Proofs of the inclusion of the timed language of the hybrid automaton into the constructed abstraction are given.

Tools and Challenges in Hybrid Systems Verification 2.5.1 Numerical simulation

Acumen testbed for cyber-physical systems [START_REF] Taha | Acumen: An Open-Source Testbed for Cyber-Physical Systems Research[END_REF] Acumen is an experimental modeling and simulation environment for hybrid systems. It is built around a small, textual modeling language. Different plotting libraries and visualization are embedded into graphical user interfaces, providing an environment for researchers in the simulation field to run experiments.

Flow-pipe tools

Ariadne [START_REF]Ariadne: An open tool for hybrid system analysis[END_REF] Ariadne is an open source library developed for hybrid automata modeling and verification. It provides structures and types for the analysis and description of hybrid automata. In addition it holds state reachability computation algorithms [START_REF] Benvenuti | Reachability computation for hybrid systems with ariadne[END_REF].

SpaceEx [START_REF] Frehse | Spaceex: Scalable verification of hybrid systems[END_REF] is a platform for the verification of hybrid systems. SpaceEx allows the use of different types of state representation and refinement strategies and combination of flow-pipes with symbolic techniques.

Flow* [START_REF] Chen | Flow*: An analyzer for non-linear hybrid systems[END_REF] Flow Star (Flow*) is a reachability analysis tool for hybrid systems with non linear dynamics. It computes a flow-pipe, represented by a Taylor model, which is an over-approximation of the set of reachable states.

Cora [START_REF] Althoff | Implementation of taylor models in cora 2018[END_REF] Cora is a Matlab based library for formal verification and analysis of hybrid systems. Cora embeds different state representations such as polytopes, zonotopes and Taylor models.

SMT solvers

DReach [START_REF] Kong | dreach: δ-reachability analysis for hybrid systems[END_REF] DReach encodes a given hybrid automaton and a safety specification as SMT formulas, then uses DReal for solving the obtained set of constraints.

Automated proof tools

KeyMaera [START_REF] Platzer | [END_REF] is a theorem prover dedicated to hybrid systems verification.

KeyMaera uses differential dynamic logic (dL) to write hybrid programs [START_REF] Platzer | Differential dynamic logic for verifying parametric hybrid systems[END_REF]. These programs have precise semantics and can model non-deterministic choices.

The dynamics can be expressed as non linear differential equations, inequalities and non deterministic inputs. The tool combines the use of different results from algebraic calculus. A hybrid program is defined using the following grammar:

hp 1 , hp 2 ::= x := γ |?θ | x = γ&θ | hp 1 ∪ hp 2 | hp 1 ; hp 2 | hp * 1
Less formally, respectively:

• assignment of an expression γ to a variable x

• test θ over the variables which acts as a guard: if ?θ = true then it is possible to transit, else no transition is made

• formula for the derivative x of x with respect to time

• non deterministic choice to go through hp 1 or hp 2

• sequence ordering of the execution, hp 1 first then hp 2

• iteration of hp 1 an arbitrary finite number of times Forms of the expressions An expression can be: [a := -v; x = x + y + a]φ, the brackets "[ ]" refer to the LTL operator always, in other terms, in all reachable states, φ is satisfied. • ctrl evaluates the condition on the MA, if it is verified then the train acceleration can be a positive constant (acceleration mode), else it is negative (brake mode). Thus, ctrl decides whether a discrete jump is applied or not.

• drive represents the continuous evolution in the hybrid system specified by the differential equation z = a KeyMaera takes as input the hybrid program and a formula to verify such as

φ := z M A.
Temporal logic is used to state that φ should be verified in all states of the controller. The tool then applies proof strategy over the hybrid program to deduce the truth value of φ w.r.t the ET CS program.

Challenges in Hybrid Systems Verification

Cross Disciplinary The study of hybrid systems involves different disciplines such as applied mathematics, control theory, theoretical and practical computer science. Consequently, the classical education curriculum taking one of the fields as a specialty is not fit for the study of hybrid systems and cyber-physical systems in general.

Large scale systems The verification of large scale hybrid systems (i.e., with the number of coupled variables exceeding around 40) remains a challenge. The future aim of the scientific community will be to develop formalism adapted to larger systems such as in distributed framework. Many applications arise in distributed hybrid systems such as managing a fleet of unmanned vehicles or aircrafts.

Distributed Hybrid Systems Very few works tackle the verification of hybrid systems in a distributed framework. The large scale complexity can be relaxed through distribution and local computations.

Standardization There is a lack of standardized specification language for cyberphysical and hybrid systems.

Chapter Summary

The chapter introduced model based verification and reviewed the existing literature concerned with qualitative modeling, reasoning and simulation, then the existing hybrid systems verification techniques, tools and challenges and the literature concerned with the diagnosability property. In fact, qualitative reasoning allows modeling systems with partially known knowledge while still getting conclusions via simulation. We have seen that it is crucial to precisely denote the assumptions such as continuity of functions, differentiability and smoothness, as these hypotheses are a basis for computing correct successors of an initial given qualitative state.

We reviewed different verification techniques for verifying hybrid systems. In particular Flow-pipe computation aims at finding over and under-approximations of the reachable set of states of a hybrid system that are semantically correct but still not computationally expensive.

Chapter 3

Framework for Hybrid Automata Verification

Hybrid Automata

In this part we introduce the formal framework describing hybrid automata that will be adopted throughout the thesis and the different notations that will be used. Later on, we provide an example of a practical system modeled as a hybrid automaton. Lastly, we formally introduce the different classes of hybrid automata, in which timed and polynomial hybrid automata are of our primary interest.

Hybrid Automata overview

Hybrid systems are dynamical systems that include discrete and continuous behaviors [START_REF] Henzinger | The theory of hybrid automata[END_REF]. Hybrid automata (HA) are a mean to model such systems. A hybrid automaton is an infinite state machine. Each state of the hybrid automaton is twofold with a discrete and a continuous part. The discrete part ranges over a finite domain while the continuous part ranges over the Euclidean space R n .

Intuitively a hybrid automaton permits modeling continuous change and discrete behavior such as digital electronics controlling a physical environment. The main components of a hybrid automaton are:

• Graph: A graph of nodes and edges, where nodes are Modes (or Locations, or Discrete State) of the system and edges representing control switches, each edge relates unidirectionally two modes with each other and expresses a mode change.

• Continuous Dynamics (or Flow Condition): Each mode of the graph, is assigned a set of constraints, describing the continuous change. More precisely, continuous dynamics can be expressed as differential equations (or inclusions) or, in a much simpler form, a set of the possible valuations of the derivative such as an interval over the reals.

• Variables: A finite set of containers, whose valuations are over the set of real numbers.

• Jump Conditions: A set of constraints assigned to each mode. When a jump constraint is satisfied, a switching between two related modes is allowed to occur.

Hybrid Automata Definition

We now propose a general formal definition of hybrid automata and introduce the different notations that will be used throughout this thesis.

Definition 3.1 (Hybrid Automata (HA)). An n-dimensional hybrid automaton (HA) is a tuple H = (Q, X, S 0 , Σ, F, Inv, T ) where:

• Q is a finite set of modes (or locations), that can be possibly defined as the valuations set of a finite number of finite valued variables, and represents the discrete part of H. X is a set of n real-valued variables (which are locally continuously differentiable functions of time), whose valuations set X ⊆ R n represents the continuous part of H. S = Q × X is the state space of H, whose elements, called states, are noted (q, x) with q and x the respective discrete and continuous parts of the state.

• S 0 ⊆ S is the set of initial states. If unique, it is noted (q 0 , x 0 ).

• Σ is a finite set of events.

• F : S → 2 R n is a mapping assigning to each state (q, x) ∈ S a set F (q, x) ⊆ R n constraining the time derivative ẋ of the continuous part of the mode q by ẋ ∈ F (q, x). If there is no uncertainty on the derivative, then F is a function S → R n specifying the flow condition ẋ = F (q, x) in each mode q (the dynamics in each mode is thus given by a set of n first-order ordinary differential equations (ODEs)).

• Inv : Q → 2 X assigns to each mode q an invariant set Inv(q) ⊆ X, which constrains the values of the continuous part of the state while the discrete part is q. We require, for all q ∈ Q, that {x | (q, x) ∈ S 0 } ⊆ Inv(q).

• T ⊆ S × Σ × S is a relation capturing discontinuous state changes, i.e., instantaneous discrete transitions from one mode to another one. Precisely, t = (q, x, σ, q , x ) ∈ T represents a transition whose source and destination states are (q, x) with x ∈ Inv(q) and (q , x ) with x ∈ Inv(q ), respectively, and labeled by the event σ. It represents a jump from x in mode q to x in mode q .

We will call (concrete) behavior of H any sequence of continuous solution flows and discrete jumps, rooted in an initial state, satisfying all the constraints above defining H.

Set Based Notations Hybrid systems are typically represented as finite automata with (discrete, i.e., modes) states Q, initial states

Q 0 = {q ∈ Q | ∃x ∈ Inv(q) (q, x) ∈ S 0 } and transitions δ defined by δ = {(q, σ, q ) ∈ Q × Σ × Q | ∃x, x (q, x, σ, q , x ) ∈ T }.
To each state q ∈ Q 0 is associated an initial (continuous) nonempty set Init(q) = {x ∈ Inv(q) | (q, x) ∈ S 0 }. To each transition τ = (q, σ, q ) ∈ δ are associated a nonempty guard set

G(τ ) = {x | ∃x (q, x, σ, q , x ) ∈ T } ⊆ Inv(q) and a set-valued reset map R(τ ) : G(τ ) → 2 Inv(q ) given by R(τ )(x) = {x | (q, x, σ, q , x ) ∈ T }. It is actually equivalent
in the definition to provide either T or δ, G and R. In the last case, H is denoted by (Q, X, S 0 , Σ, F, δ, Inv, G, R) and we have: ∀(q, x), (q , x ) ∈ S, ∀σ ∈ Σ,

((q, x, σ, q , x ) ∈ T ⇔ τ = (q, σ, q ) ∈ δ ∧ x ∈ G(τ ) ∧ x ∈ R(τ )(x)).
Relational Based Notations It can be in some cases more convenient to adopt a relational-based representation than a set-based representation and to use predicates instead of subsets. By a slight abuse of notation, for each mode q, Init(q) (for q ∈ Q 0 ), F (q) and Inv(q) indicate then predicates whose free variables are respectively from X, X × Ẋ and X and Init(q)(x), F (q)(x, ẋ) and Inv(q)(x) being true means respectively x ∈ Init(q), ẋ ∈ F (q, x) and x ∈ Inv(q). In the same way, for each mode transition τ , G(τ ) and R(τ ) indicate predicates whose free variables are respectively from X and X × X and G(τ )(x) and R(τ )(x, x ) being true means respectively x ∈ G(τ ) and x ∈ R(τ )(x). We will make use equally of both representations.

Assumption 3.1. Guards in any mode q will be assumed non-intersecting: ∀q ∈

Q, ∀τ 1 = (q, σ 1 , q 1 ) ∈ δ, ∀τ 2 = (q, σ 2 , q 2 ) ∈ δ, (τ 1 = τ 2 ⇒ G(τ 1 ) ∩ G(τ 2 ) = ∅).
Non-deterministic state machine Thus, at any moment of its continuous evolution in a mode q, the system may jump to at most one other mode and by a unique event. Nevertheless, a HA is generally non-deterministic: the continuous dynamics in each mode may be non-deterministic, the moment where a jump occurs is non-deterministic (as long as Inv(q)(x) and G(τ )(x) are true, where q is the source mode of the mode transition τ , the system may continue to continuously evolve in q or make the transition τ ) and the reset after a jump may be nondeterministic.

Graphical representation

A hybrid automaton is visually represented by a set of nodes and arcs:

• Nodes: each node represents a mode of the system and is labeled by the flow constraints such as differential equations followed by the mode invariant sets.

• Arcs: each arc represents a jump (discrete transition) from one mode to another. The arc is labeled by its event and its associated guard (and possibly its reset map).

off ẋ = -x x ≥ 68 on ẋ = -x + 100
x ≤ 82

x ∈ [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF] x ≤ 70/B on 80 ≤ x/B off A temperature regulator or thermostat system maintains the temperature of an object quasi-constant by turning on and off a heater device. Practically speaking, such system contains at least, a temperature sensor, a heater device and logic control electronic circuits. An algorithm computes, given the actual measured temperature of the object, the corresponding order for the circuitry to activate or not the heater. A hybrid automaton H = (Q, X, S 0 , Σ, F, δ, Inv, G, R) models the behavior of such system (Figure 3.1) such that: [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF])

• Q = {on, off }, X = {x}, S 0 = (off ,
• Σ = {B on , B off }, F (on) = { ẋ = -x + 100}, F (off ) = { ẋ = -x} • δ = {τ 1 = (of f, B on , on), τ 2 = (on, B off , off )}, Inv(off ) = x ≥ 68, Inv(on) = x ≤ 82 • G(τ 1 ) = x ≤ 70, G(τ 2 ) = x ≥ 80, R(τ 1 ) = R(τ 2 ) = (x = x )
The assigned hybrid automaton H is one dimensional, where x represents the sensed temperature.

Hybrid Automata semantics

The semantics of a hybrid automaton (i.e., the set of executions of a HA) is a set of sequences, every sequence aggregates continuous time lapses with mode jumps while satisfying all the flow, invariant and jump constraints. We denote by q 0 , q 1 , ... the modes of Q, and by x 1 , x 2 , ..., x n the variables of X. is the set of all executions (or runs), which are labeled sequences of states from S with labels in L = Σ∪R + : (q 0 , x 0 )

l 0 -→ (q 1 , x 1 )...(q i , x i ) l i
-→ ... such that (q 0 , x 0 ) ∈ S 0 and, for any two successive states (q i , x i )

l i -→ (q i+1 , x i+1 )
in the sequence, one of the following is true:

• l i = σ i ∈ Σ and (q i , x i , σ i , q i+1 , x i+1 ) ∈ T ; • l i = d i ∈ R + , q i = q i+1 , x i , x i+1 ∈ Inv(q i ) and ∃x : [0, d i ] → X continuously differentiable function, with x(0) = x i , x(d i ) = x i+1
and ∀t ∈ (0, d i ) ẋ(t) ∈ F (q i , x(t)) and x(t) ∈ Inv(q i ).

In the first case, the system executes a discrete transition (also called discrete jump) τ i = (q i , σ i , q i+1 ) from the source mode q i to the destination mode q i+1 . Such a transition is possible (enabled) as soon and as long as x i ∈ G(τ i ). After the jump, the system may follow the new dynamics given by F (q i+1 ), starting from the continuous state x i+1 ∈ R(τ i )(x i ). Notice that no time elapses during a discrete jump, which is instantaneous. In the second case, the system performs a continuous transition (also called continuous flow) of duration d i inside the mode q i , constrained by the dynamics F (q i ) and the invariant set Inv(q i ). The sequence h = (off , 80) the sequence of its labels, is a word from L (or L ω for infinite h), denoted as trace(h). We denote the total time duration of h by time(h) ∈ R + ∪ {+∞}, which is calculated as the sum of all time periods in the trace of h: time(h) = d i . Figure (3.2) illustrates the behavior of the thermostat system: the reachable set of states starting from the initial set S 0 , the guard and invariant states sets.

Zeno behavior An execution h ∈ [[H]

] is zeno if it is infinite with finite time, i.e., the sum given by +∞ i=0 d i converges (i.e., tends to a real finite value). Consequently, in a zeno execution h, an unbounded number of discrete jumps occur while the execution time time(h) is finite. Real systems in general do not show zeno behavior. Such behavior arises at the modeling stage and is due to the abstraction and incompleteness of the model.

Many works addressed the conditions for zeno behaviors to exist [START_REF] Zhang | Zeno hybrid systems[END_REF]. Assumption 3.2. We limit our work to cases that do not account for any zeno behavior.

Example 3.2 (Bouncing Ball). The classical bouncing ball example illustrates zeno behavior. A ball is initially released from some height H 0 without initial speed. Once it hits the ground, the ball bounces back. The example at some abstraction level, can be modeled by a hybrid automaton with a single mode and one jump. The variables of the system are: the vertical position of the ball x 0 and its velocity x 1 = dx 0 dt . The forces applied to the ball are limited to the gravitational force, thus dx 1 dt = -g is constant with g the gravitational acceleration of the Earth. The ball is assumed semi-elastic and hollow, so when the collision with the ground occurs some of the air inside the ball is compressed for a short period of time due to the deformation of the ball. The ball is well sealed, so while the ball takes back its normal form, the compressed air allows the ball to bounce again. Due to friction with the ground, some of the ball's kinetic energy is lost and some is restituted.

The energy loss and restitution happen in a short duration of time when compared with the time elapsed between two successive bounces of the ball. Consequently, the energy loss can be assumed instantaneous, the change of speed is modeled as a discrete jump back to the same mode while having a different value of the speed (because of the energy loss, modeled as a reset) and an opposite direction of the velocity after the jump (because the ball does not penetrate through the ground). The guard holds the condition x 1 < 0∧x 0 = 0 and the associated reset, x 1 := -r.x 1 with r ∈ (0, 1) the restitution factor. Using the reachability computation tool CORA initialized from the set [0.9, 1.1] we compute the flow-pipe till a time horizon of 2.1 time units using zonotopes as state representation (Figure 3.3). We can clearly see that the bouncing ball simulated trajectory exhibits zeno behavior: in a bounded area of x 0 such as [0, 0.2] the number of bounces increases infinitely often.

Figure 3.3: Flow-pipe of the bouncing ball simulated using zonotopes

Hybrid Automata Classes and Particular Cases

The components of the hybrid automaton previously defined can be further constrained to find particular classes. On the two opposite sides of the continuity spectrum we find discrete automata and continuous systems. When constraining primarily the dynamics F we find practical classes of hybrid automata such as the rectangular or linear class or timed automata. For the rectangular class the dynamics valuations are a cartesian product of intervals and it lies on the boundary of the decidability over reachability problem with some restrictions [START_REF] Henzinger | What's decidable about hybrid automata[END_REF]. The timed and polynomial hybrid automata classes are of particular interest for this thesis work. Definition 3.3 (Discrete Automata (DA)). It is the case where there is no continuous space. Thus, a (finite) discrete automaton (DA) is a tuple

D = (Q, Q 0 , Σ, δ)
where:

• Q is a finite set of discrete states (modes).

• Q 0 ⊆ Q is the set of initial states.
• Σ is a finite set of events. Timed Automata It is a class of hybrid automata where the continuous variables x i , 1 ≤ i ≤ n, with values in R + , called clocks, have all first order derivatives equal to one. So time elapses identically for all clocks. The set C(X) of constraints over a set of clocks X is defined as follows: a constraint is either a primitive constraint of the form x i op c i where c i ∈ R + (at the theoretical level because, in practice, Q is used instead of R for computer implementation reasons) and op is one of <, ≤, =, ≥, > or a finite conjunction of primitive constraints. The satisfiability set of a constraint is thus a rectangle in R n + , i.e., the product of n intervals of the half real line R + , and we will identify C(X) to the set of rectangles. Definition 3.5 (Timed automata (TA)). A timed automaton (TA) is a hybrid automaton T = (Q, X, S 0 , Σ, F, δ, Inv, G, R) such that:

• δ ⊆ Q × Σ × Q is a set of transitions of the form τ = (q, σ, q ).
• X = R n + . • S 0 = Q 0 × {0}.
• ∀q ∈ Q F (q, .) = 1, which means that the dynamics of clocks evolution in each mode q is given by ẋi = 1.

• Inv : Q → C(X) associates to each mode q a rectangle invariant in X. We require 0 ∈ Inv(q 0 ).

• G : δ → C(X) associates to each discrete transition (q, σ, q ) a rectangle guard in Inv(q).

• ∀τ ∈ δ ∃Y (τ ) ⊆ X ∀x ∈ G(τ ) R(τ )(x) = {x } with x i = 0 if x i ∈ Y (τ ) and x i = x i otherwise, i.e.
, clocks in Y (τ ) are reset to zero with transition τ , the others keeping their values.

The notation of a timed automaton T is generally simplified as T = (Q, X, Q 0 , Σ, Inv, (δ, G, Y )). The semantics of T as a hybrid automaton, given by Definition 3.2, can be simplified by merging together in an execution successive timed transitions between two discrete transitions and summing up their time period labels. An execution in [[T ]] is thus a sequence h of alternating time steps (possibly with 0 time period) and discrete steps of the form (q 0 , x 0 )

d 1 -→ (q 0 , x 0 + d 1 ) σ 1 -→ (q 1 , x 1 ) d 2 -→ ... whose trace trace(h) is the timed word d 1 σ 1 d 2 ... ∈ R + (ΣR + ) * and duration is time(h) = d i .

Decidability results

The class of timed automata is particularly interesting as the reachability and language emptiness problems are decidable for that class and are PSPACE-complete [START_REF] Alur | A theory of timed automata[END_REF]. This result still holds for singular automata where the flow F (., .) is a constant singleton, allowing thus different constant slopes to the clocks. However, if a clock can switch from active (turned on) to inactive (turned off), or vice versa, when transiting between two modes then it is called a stopwatch, i.e., ∀q ∈ Q ∃c ∈ {0, 1} n F (q, .) = c, which means that the dynamics of clocks evolution in each mode q is given by ẋi = 1 for those clocks active in q and ẋi = 0 for those clocks inactive in q. During inactivity, it holds its last valuation when it was active (or 0 in case of reset). It has been shown that decidability for timed automata with one stopwatch holds if some strong conditions are met [START_REF] Bouajjani | On model checking for real-time properties with durations[END_REF], however it is no longer true for timed automata with three stopwatches (and thus also for the more general class of multisingular automata, where the flow singletons depend on the mode).

Rectangular Automata For this class, the unique flow condition F (., .) is the same for all modes and is given by a bounded rectangle in R n (instead of the singleton 1), Init(q 0 ) is a bounded rectangle, Inv(q) is a rectangle for any mode q and, for any discrete transition τ , the guard G(τ ) is a rectangle and the reset R(τ ) is a bounded rectangle for those reset variables, which depend only on τ [START_REF] Henzinger | The theory of hybrid automata[END_REF].

The idea behind a rectangular automaton is that changes of the discrete state has no effect over the variations of the continuous variables. The variables values can change between the discrete states but not their flow. Rectangular automata naturally express that the continuous variables are decoupled. A rectangle is bounded if each of its intervals I i is bounded.

Definition 3.7 (Rectangular Automata (RA)). A rectangular automaton (RA) is a hybrid automaton R = (Q, X, S 0 , Σ, F, δ, Inv, G, R) such that:

• X = R n + .
• ∃I, S 0 = Q 0 × I where I is an n-dimensional bounded rectangle.

• ∃I F ∀q ∈ Q, F (q, .) = I F and I F is an n-dimensional bounded rectangle.

• Inv : Q → C(X) associates to each mode q a rectangle invariant in X.

• G : δ → C(X) associates to each discrete transition (q, σ, q ) a rectangle guard in Inv(q).

• ∀τ ∈ δ ∃Y (τ ) ⊆ X ∃I i (τ ), for x i ∈ Y (τ ), bounded intervals ∀x ∈ G(τ ) R(τ )(x) = {x } with x i ∈ I i (τ ) if x i ∈ Y (τ ) and x i = x i otherwise, i.e.,
clocks in Y (τ ) are reset to intervals I i (τ ) with transition τ , the others keeping their values.

Unknown constant An unknown constant can be modeled by a variable x j with I F j = [0, 0]. x j should not be reinitialized by any control switch and other variables may depend on the value of x j .

Decidability results Decidability for the reachability problem and for language emptiness problem holds for the class of rectangular automata. And thus holds for the subclass of singular automata, whose timed automata are a particular case. But this is no longer true for the larger class of multirectangular automata where the flow rectangle conditions F (q, .) = I F q depend on the mode q (as written above it is already not true for the subclass of multisingular automata with singleton flows). Notice nevertheless that, allowing changes of flow conditions with changes of modes may remain manageable if, e.g., we require a reset of the variables concerned when it occurs. That is how initialized multirectangular automata, i.e., where for each discrete jump, each variable whose flow interval is changed in this jump has to be reset (reinitialized), can be translated to rectangular automata. Decidability does not hold any more also for the class of triangular automata which generalize rectangular automata by replacing rectangles by so-called triangles obtained by intersecting rectangles with any number of half-spaces defined by inequalities of the form x i ≤ x j , i.e., if variables are not pairwise independent (extending for timed automata the set C(X) by constraints of the form x i -x j op c ij leads already to undecidability). Linear automata generalize both multirectangular and triangular automata by allowing sets F (q, .), Init(q), Inv(q), G(τ ), R(τ )(.) to be any convex polyhedra in R n (instead of just rectangles or triangles) and different flows conditions for different modes. And polynomial automata generalize linear automata by allowing those sets to be defined no longer by just linear constraints but by polynomial constraints.

Time elapsed in a state In a multirectangular automaton and for a given state q, we can define a variable x 1 with flow condition in q given by I F q 1 = [1, 1] and in any state q different from q given by I F q 1 = [0, 0]. It models a stopwatch and can be used to measure the duration the system stays in state q, the stopwatch being off in any other state.

Linear Hybrid Automata

A linear term over a set Y = {y i , 1 ≤ i ≤ n} of real-valued variables is a linear combination over Y with real (in practice, rational) coefficients, i.e., an expression of the form k 0 + k 1 y 1 + . . . + k n y n with k i ∈ Q. A linear predicate over Y is an inequality between linear terms over Y , i.e., can be written as k 0 +k 1 y 1 +. . .+k n y n ≤ 0. A convex linear predicate over Y is a finite conjunction of linear predicates over Y , thus its satisfiability set is a convex polyhedron in R n . Definition 3.8 (Linear Hybrid Automata (LA)). A linear hybrid automaton (LA) is a hybrid automaton L = (Q, X, S 0 , Σ, F, δ, Inv, G, R) such that :

• ∀q ∈ Q, F (q) is a convex linear predicate with free variables from Ẋ only, which means that, in each mode, ẋ is constrained to belong to a given convex polyhedron, depending only on the mode.

• ∀q ∈ Q, Init(q) and Inv(q) are convex linear predicates over X.

• ∀τ ∈ δ, G(τ ) and R(τ )(.) are convex linear predicates over X.

Remark 3.1. A linear differential equation cannot necessarily be converted into a linear flow condition: the notions of linear for differential equations and hybrid automata are different.

Multi-Affine Hybrid Automata

We recall the definition of a multi-affine function [START_REF] Kloetzer | Reachability analysis of multi-affine systems[END_REF].

Definition 3.9 (Multi-affine Function). A multi-affine function f : R n → R p is a polynomial in the indeterminates x 1 , , ..., x n with the property that the degree of f in any of the variables is less than or equal to 1. Stated differently, f has the form:

f (x 1 , ..., x n ) = i 1 ,...,in∈{0,1} c i 1 ,...,in x i 1 1 ...x in n , (3.2)
with c i 1 ,...,in ∈ R p for all i 1 , ..., i n ∈ {0, 1} and using the convention that if i k = 0, then

x i k k = 1.
E.g., a two-dimensional multi-affine continuous system can be written as: which ∀q ∈ Q the flow condition F (q, .) : X → R n is a multi-affine function and ∀q ∈ Q, ∀τ ∈ δ, Init(q), Inv(q), G(τ ), R(τ )(.) are rectangle predicates.

ẋ = ax + by + cxy + d (3.3)
Polynomial Hybrid Automata Definition 3.11 (Polynomial Hybrid Automata (PA)). A polynomial hybrid automaton (PA) is a hybrid automaton P = (Q, X, S 0 , Σ, F, δ, Inv, G, R) for which ∀q ∈ Q the flow condition F (q, .) : X → R n is a polynomial function and ∀q ∈ Q, ∀τ ∈ δ, Init(q), Inv(q), G(τ ), R(τ )(.) are defined by polynomial constraints.

Modeling with hybrid automata

Hybrid automata represent an intuitive modeling framework. They are used in various domains to model complex hybrid systems. Here is a practical case where an hybrid automaton is used for modeling a system.

Example 3.3 (The switched server [START_REF] Matveev | Qualitative Theory of Hybrid Dynamical Systems[END_REF]). We consider an example of 4 buffers B 1 , ..., B 4 and a server S . To each buffer B i we assign a workflow w i representing the rate at which work is entering the buffer. The server processes work, one buffer at a time, at a rate w s . The switching between buffers is controlled by a user input. For the work processing to eventually terminate it is necessary that

w s > w 1 + w 2 + w 3 + w 4 .
Such system is modeled by a hybrid automaton H = (Q, X, S 0 , Σ, F, Inv, T ). We first identify the discrete modes and the continuous variables. With some observation, we notice that each time the server switches buffers, the continuous change of the work waiting to be processed follows a new evolution. Therefore, a simple choice for modeling the set of discrete modes Q is that each q i represents the server processing work at buffer B i . Hence, we have four modes and Q = {q 1 , q 2 , q 3 , q 4 }. The server is able to switch from and to any mode, as a result, all distinct modes q i and q j are related by a discrete jump with a given label, say switch i j. Let x i (t) be the amount of work in the buffer B i at time t. The set X of continuous variables is thus made up of those four variables x i and X ⊆ R 4 . Any state (q i , x) with x i > 0 can be chosen as initial state: Init(q i )(x) = (x i > 0). If the system is in the discrete mode q i , then we have ẋi (t) = w i -w s and, for all j such that i = j, ẋj (t) = w j , hence F is specified. Invariant sets are given by: Inv(q i )(x) = (x i ≥ 0) and reset predicates R(τ ) are the equality predicate. What is left to be specified are the values of the guards G ij which in practice represent the switching protocol of the server. Finally

T = {(q i , x, switch i j, q j , x) | i = j, x ≥ 0, G ij (x), x j > 0}. q 1 ẋ1 = w 1 -w s ẋi =1 = w i q 2 ẋ2 = w 2 -w s ẋi =2 = w i q 4 ẋ4 = w 4 -w s ẋi =4 = w i q 3 ẋ3 = w 3 -w s ẋi =3 = w i s 1 2 s 2 1 s 2 3 s 3 2

Diagnosability: Observations and Faults

In this part we introduce a formal framework for analyzing the diagnosability of a hybrid system. We specify observations and partially observable hybrid automata, we introduce fault modeling and definitions for (bounded-)diagnosability and review the important notion of critical pair.

Observations and faults

Remind that diagnosability is a system property allowing one to determine with certainty, at the design stage, that a fault occurred in the system, using available observations. Precisely, in a given system model, the existence of two infinite behaviors, with the same observations but exactly one containing the considered fault, violates diagnosability. Hence, to be able to analyze such property, it is necessary to define what can be observed for given systems as well as what are considered as faults. In practice, the observations are partial, only parts of the system are known and are usually obtained from sensors. In whole generality we will consider that both some discrete jumps between modes and some continuous variables inside a mode may be observable. The sets of observable events and variables are assumed to be time invariant, the second one being also assumed to be independent of the mode for the sake of simplicity. Events are observed together with their instantaneous occurrence time and variables values are assumed to be observed at any moment. E.g, for the thermostat system (Figure 3.1, page 56), transitions B on , B off and temperature x are assumed to be observable. For what concerns faults, we will suppose that they are modeled by some unobservable discrete jump, between precisely a normal mode and a faulty mode, translating often in a change of dynamics. This is well adapted for abrupt faults but progressive faults or degraded modes (as a shift of parameter) can be also represented in this way, the designer abstracting a slow evolution in a sudden change when he estimates that the behavior variation induced (that he will model by means of the invariant and the guard) cannot any more let consider the given mode as normal.

To sum up, we obtain the following definition. where:

• Σ = Σ o Σ u Σ f , i.e.
, the set of events is the disjoint union of the set Σ o of observable (normal) events, the set Σ u of unobservable normal events and the set Σ f of unobservable fault events.

• X = X o X u , i.e., the set of continuous real-valued variables is the disjoint union of the set X o of observable variables and the set X u of unobservable variables.

Definition 3.13 (Execution (timed) observation). Given an execution h ∈ [[H]]

of a POHA H, h = (q 0 , x 0 )

l 0 -→ (q 1 , x 1 )...(q i , x i ) l i -→ ..., with l i ∈ Σ ∪ R + , the (timed) observation of h is defined as Obs(h) = x o 0 , l o 0 , x o 1 ...x o i , l o i , .
.., where:

• x o i is obtained by projecting x i on variables in X o . • l o i = l i if l i ∈ Σ o ∪R + . Otherwise, l o i = ε, which is then removed from Obs(h).
Note that all durations labels l i = d i in h are present in Obs(h). Thus, any observable event l i = σ i in h is present in Obs(h) together with its occurrence time, obtained by adding up all durations d j in Obs(h) from the origin up to the event σ i . In the same way, any observable variable x has its value known in Obs(h) at all those instants t obtained as the sums of consecutive durations in Obs(h) from the origin. If t is the occurrence time of an (observable or unobservable) event σ and if

x is reset by the discrete transition σ, then the value of x changes instantaneously after this transition and the new value will be noted x + (t) to distinguish it from the value x(t) before the transition (a reset observable variable may thus identify the presence of an unobservable event). Similarly, one can define observation for timed automata. The difference is that we do not assume any information about continuous clocks, so there is no x o i . Then, the observation is obtained from the trace (a timed word) by erasing all unobservable events and by adding up the periods between any two successive observable events in the resulting sequence.

We have thus defined what is the observation of a POHA H at the level of its timed transition system (see subsection 4.1.3). Defining its observation at the level of its timeless transition system (see subsection 4.1.3) is similar, with l i ∈ Σ ∪ { } and l o i = l i if l i ∈ Σ o and removed otherwise. This means that the timeless observation is obtained from the timed observation Obs(h) above by removing all durations d i , keeping thus only observable events in Σ o and values x o i of observable variables at each transition step as an ordered sequence without any occurrence time attached.

System Diagnosability Definition

As we just explained, a fault is modeled as a fault event that alters the system from a normal mode to an abnormal mode. There may exist different fault events in a given system. Assumption 3.3. For the sake of reducing complexity (from exponential to linear in the number of different fault events) and of simplicity, in the following only one fault type, i.e., fault event, at a time is considered but multiple occurrences of this event are allowed, and the other types of fault events are thus processed as unobservable normal events.

By processing like this successively each fault type individually, one obtains the same result about system's diagnosability as if all fault types were considered simultaneously with a lower complexity (the system is diagnosable if and only if it is diagnosable for each fault type). Now we adapt to hybrid systems the diagnosability definition [START_REF] Sampath | Diagnosability of Discrete Event System[END_REF] introduced for discrete event systems (the bounded one and the unbounded one in terms of executions lengths). h F denotes a finite execution whose last label is a first occurrence of the fault event F considered.

Given a finite execution h ∈ [[H]] such that

h = (q 0 , x 0 ) l 0 -→ (q 1 , x 1 )...(q i , x i ), the set of post-executions of h in [[H]] is defined as [[H]]/h = {h = (q i , x i ) l i -→ ... | h.h ∈ [[H]]},
where h.h is obtained by merging the final state of h and the first state of h (both are identical). Consequently, a faulty execution is defined as follows, where we abbreviate F ∈ trace(h) by F ∈ h.

Definition 3.14 ((∆-)faulty executions). Given a hybrid automaton H and F a fault event, a faulty execution is an execution h ∈ [[H]

] such that F ∈ h. Thus h = h F h where h F is the prefix of h whose last label is the first occurrence of F .

We denote the period from (the first occurrence of ) f ault F in h by time(h, F ) = time(h ). Given a positive real number ∆ ∈ R * + , we say that at least ∆ time units pass after the first occurrence of F in h, or, in short, that h is ∆-f aulty, if time(h, F ) ≥ ∆. Definition 3.15 (Hybrid automaton (time bounded and unbounded) diagnosability).

Given ∆ ∈ R * + , a fault F is said ∆-diagnosable in a POHA H iff (if and only if ) ∀h ∈ [[H]] (h ∆-faulty ⇒ ∀h ∈ [[H]] (Obs(h ) = Obs(h) ⇒ F ∈ h )). i.e., ∀h F ∈ [[H]] ∀h ∈ [[H]]/h F (time(h) ≥ ∆ ⇒ ∀h ∈ [[H]] (Obs(h ) = Obs(h F .h) ⇒ F ∈ h )). A fault F is said diagnosable in H iff ∃∆ ∈ R * + (F ∆-diagnosable in H).
This definition states that F is ∆-diagnosable (resp., diagnosable) iff, for each execution h F in [[H]], for each post-execution h of h F with time at least ∆ (resp., with enough long time, depending only on F ), then every execution in [[H]] that is observably equivalent to h F .h should contain F . Precisely, the existence of two indistinguishable behaviors, i.e., executions holding the same observations, with exactly one containing F and time long enough after F , i.e., whose time after F is at least ∆ (resp., is arbitrarily long), violates the ∆-diagnosability (resp., diagnosability) property for hybrid automata. Inspired from the framework of discrete event systems, we define critical pairs for partially observable hybrid automata taking into account both continuous and discrete dynamics.

Definition 3.16 (∆-critical pair). A pair of executions h, h ∈ [[H]

] is called a ∆-critical pair with respect to F iff: F ∈ h and F / ∈ h and Obs(h) = Obs(h ) and time(h, F ) ≥ ∆.

We are now ready to state the sufficient and necessary condition for diagnosability verification.

Proposition 3.1. A fault F is ∆-diagnosable in a POHA H iff there is no ∆- critical pair in [[H]] with respect to F . F is diagnosable in H iff, for some ∆,
there is no ∆-critical pair in [[H]] with respect to F (i.e., there is no arbitrarily long time after F critical pair).

Proof. The equivalence between the absence of ∆-critical pairs in a POHA and its ∆-diagnosability is directly seen by negating the diagnosability definition (Def.3.15):

¬(∀h ∈ [[H]] (h ∆-faulty ⇒ ∀h ∈ [[H]] (Obs(h ) = Obs(h) ⇒ F ∈ h ))). ⇐⇒ ∃h ∈ [[H]] (h ∆-faulty ∧ (∃h ∈ [[H]] (Obs(h ) = Obs(h) ∧ F / ∈ h ))).
From the definition of a ∆-faulty execution, the previous is equivalent to

∃h ∈ [[H]] (F ∈ h ∧ time(h, F ) ≥ ∆) ∧ (∃h ∈ [[H]] (Obs(h ) = Obs(h) ∧ F / ∈ h ))). ⇐⇒ ∃h, h ∈ [[H]] (F ∈ h ∧ F / ∈ h ∧ time(h, F ) ≥ ∆ ∧ Obs(h ) = Obs(h)).
Note that all above definitions (e.g., observable projection, post-executions, diagnosability, critical pairs, etc.) are applicable in a similar way to timed automata, which can be considered as a special type of hybrid automata. The only difference is that the set of continuous variables is the set of clock variables whose derivative is always 1 [START_REF] Daigle | An event-based approach to hybrid systems diagnosability[END_REF][START_REF] Bayoudh | Active diagnosis of hybrid systems guided by diagnosability properties[END_REF][START_REF] Bayoudh | Hybrid systems diagnosability by abstracting faulty continuous dynamics[END_REF][START_REF] Daigle | A qualitative event-based approach to fault diagnosis of hybrid systems[END_REF][START_REF] Grastien | Solving diagnosability of hybrid systems via abstraction and discrete event techniques[END_REF]. And, as for automata the existence of arbitrarily long (in terms of transitions number) after F faulty executions implies the existence of an infinite faulty execution, in the same way it has been proved [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF] that for timed automata the existence of arbitrarily long time after F faulty executions implies the existence of a +∞-faulty execution (extending Definition 3.14 to = +∞) and thus that non-diagnosability is witnessed by the existence of a +∞-critical pair (extending Definition 3.16 to = +∞) and its checking is PSPACE-complete. Proof. The result and proof are elaborated in [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF].

We will rest on this result as diagnosability checking of a POHA H will be performed on a timed automaton T abstracting H. We will use also the following obvious result.

Proposition 3.3. If a P OHA H is ∆-diagnosable then it is ∆ + -diagnosable for any ∆ + > ∆. Alternatively, if H is not ∆-diagnosable then it is not ∆ --
diagnosable for any positive ∆ -such that ∆ -< ∆.

Chapter Summary

This chapter introduced a framework for hybrid automata model and semantics.

We reminded classes of interest of hybrid automata. Two practical examples of modeling using the hybrid automata formalism were presented: a thermostat and a switched buffer system. The diagnosability definitions for a hybrid automaton have been presented together with critical pairs that witness non-diagnosability of the system and we reminded complexity results for verifying diagnosability of timed automata.

Chapter 4

Qualitative Abstractions for Hybrid Automata

In this chapter we elaborate abstractions of hybrid automata using principles from the qualitative reasoning domain. Abstractions as timed automata are presented. Algorithms for computing the abstractions are shown. Section 4.1 presents statespace decomposition abstractions of a hybrid automaton where timeless and timed abstractions are defined. Section 4.2 presents algorithms for automating the computation of the defined abstractions. Finally, section 4.3 applies the elaborated abstraction method to diagnosability verification by using a counter-example guided abstraction refinement loop.

Qualitative Abstractions

The language of hybrid automata as previously defined (Section 3.1) is not directly manageable (for the purpose of model checking for example). This is mainly due to the large expressiveness of the language. This fact translates mathematically by the differential equations having no closed form solutions in general. The challenging part about hybrid systems is to encode the continuous evolution into usable representations while taking into account the guard and reset regions. Consequently, the use of abstractions allows obtaining a simplified model, but nonetheless possibly sufficient and correct for formal properties verification. The decision at the abstract level can to some extent be inferred back to the concrete hybrid system. We first remind some abstraction principles and provide some intuitive and motivating examples. We then define different abstraction schemes using and extending ideas from the qualitative reasoning domain. This is done by first introducing the finest abstractions of hybrid automata followed by decomposition of the hybrid state space into regions. We then define hybrid automata abstractions using a defined decomposition. We elaborate abstractions as discrete event systems, modeling reachability between the regions of the decomposition of the state space, and as timed automata, adding time constraints to the reachability relations. For the rest of the chapter, we consider a hybrid automaton H (Def.3.1, page 53).

Abstracting continuous change

Generally speaking, verifying basic properties such as reachability is undecidable for continuous systems. This is due in particular to the large expressiveness of continuous dynamics over the infinite domain of the reals [START_REF] Hainry | Decidability and undecidability in dynamical systems[END_REF]. A fortiori, for a hybrid system, a computation of the reachable set of states starting from an initial state is undecidable except for few classes [START_REF] Henzinger | What's decidable about hybrid automata[END_REF]. An efficient practice is to partition infinite domains into a finite number of subsets, abstracting the system behavior in each of those subsets. In this section, we thus focus on abstractions that discretize the infinite state space defined by continuous variables into a finite set. The challenging part about abstractions is the choice made to select the representative sets and the criterion for choosing them. This choice relies entirely on the class of the properties one wishes to verify and on the structure and class of the hybrid system itself. Abstractions that can be refined are a necessary concern, as refinement allows if needed adding more information into the abstract system from the original one.

Sound and complete abstraction Figure 4.1 illustrates the exact reachable set (in grey) obtained from an initial square set X 0 . Two abstractions are proposed (finite sets of squares within the bold lines). On the left is a complete abstraction, the exact reached set of states being contained within the abstraction squares. On the right is a sound abstraction, every square of the abstraction having a nonempty intersection with the exact reached set (in the example, it is also complete, while the abstraction on the left is not sound). Take care that some authors use the opposite designation to qualify an abstraction.

X 0 X 0 For a hybrid automaton H, the general idea is to use complete abstractions, i.e., whose behaviors encompass all concrete behaviors of H, for those properties we want to verify that are universally quantified on all the behaviors (the executions) of H, and to use sound abstractions, i.e., whose behaviors all abstract some concrete behavior of H, for those properties we want to verify that are existentially quantified on the behaviors of H. Both cases correspond in practice to over-approximations and under-approximations respectively. In fact to construct the complete unsound abstraction (left), it is sufficient to have computed an over-approximation of the reachable set of states, then any square representation that contains the over-approximation is a complete abstraction. While to construct the sound and complete abstraction (right), it is necessary to have an under-approximation of the reachable set of states, any square of the abstraction representation must guarantee that it has a non-empty intersection with the underapproximation set. Consequently, we will have the insurance that if the property is proved to be satisfied by the abstraction, then it is by H. If it is proved to be unsatisfiable at the abstraction level, then we will not be able to conclude in general and will resort on a refinement of the abstraction. In this thesis where we are particularly interested in the diagnosability property, we will use exclusively complete abstractions (and thus almost always unsound, with so called spurious behaviors that do not reflect any concrete behavior) .

Abstractions using qualitative and invariant based reasoning

Using is obtained from the single landmark 0 and corresponds to the sign partition:

(-∞, 0), [0], (0, +∞), giving rise to a partition of size 3 n of R n . It is particularly interesting when applied to the valuations of the variables derivatives, as it corresponds to discretize according to the sign of the derivative, which is constant within each set of the partition, and thus to the change direction of the variable itself (decreasing, constant, increasing). The variables being continuously differentiable, it is not possible for the sign of the derivative to pass from negative to positive without crossing zero. Exploiting this feature, we obtain a scheme of the behavior of the variables called "qualitative simulation" and obtain an overview of the system behavior [START_REF] Kuipers | Qualitative reasoning: modeling and simulation with incomplete knowledge[END_REF][START_REF] Gallois | Qualitative simulation and validation of complex hybrid systems[END_REF][START_REF] Louise Travé-Massuyès | Modèles et raisonnements qualitatifs[END_REF].

Example 4.1. Consider this simple linear continuous system:

ẋ = 3x ẏ = y -1 (4.1)
Adopting the partition of the state space given by the signs of the derivatives, the abstract state space of size 9 is thus:

( ẋ > 0 ∨ ẋ < 0 ∨ ẋ = 0) ∧ ( ẏ > 0 ∨ ẏ < 0 ∨ ẏ = 0
). The transitions between the abstract states are computed according to the laws of evolution given the signs of the derivatives. The abstract state ( ẋ > 0 ∧ ẏ > 0) corresponds to the region {x, y | x > 0 ∧ y > 1} in the state space. From this state, no transition is possible to another abstract state.

Suppose we wish to verify a basic reachability property: starting from the state (1, 3) is it possible to reach the state (-5, -4)? The answer would be no, the proof is given using the previous abstraction method and inferring the property back to the original system. Such abstraction is complete: from any initial state (x 0 , y 0 ) the solutions of the differential equation system 4.1 will always satisfy the constraints imposed by the abstract system rules, i.e., the possible transitions.

Abstractions for the verification of temporal properties The above abstraction is useful to trace the future evolution of the state given the initial one to prove a safety property of avoiding an unwanted state. However it is timeoblivious, time is not captured by the abstraction. Consequently, for proving a more complex property that involves the notion of time the above abstraction is not sufficient. One needs to add time as a separate state variable and correlate the variables changes to changes in time. A timed specification can be expressed using temporal logic.

Example 4.2. Let us reconsider the same dynamics of the previous example, suppose the initial set of states X 0 such that

X 0 = {(x, y) | 1 < x < 2 ∧ 1 < y < 2 ∧
x < y} and the property F (x > y) where F is the "eventually" linear temporal logic (LTL) operator. F p, where p is a Boolean proposition, is equivalent to ∃t 0 ∈ R + , ∀t > t 0 , p = true. It is obvious that the rate at which x is increasing with respect to time is much larger than that of y. Hence, for all the initial states within X 0 the property is true. The previous abstraction method however does not capture the rate at which the derivative of x is changing and is thus useless for establishing the proof. Actually, changing the first equation in 4.1 by ẋ = 0.5x would keep the abstract system unchanged and nevertheless change the truth value of the property. In our case, the system can be written as ẋ = Ax + b where x = (x, y) T and A is the corresponding matrix. We then deduce by computing the eigenvalues of , which are 3 and 1 in our example, that the rate at which x increases is larger than the rate at which y increases, which provides a sufficient proof that the above property holds when the system is initiated from X 0 .

The previous example illustrates the case of a linear dynamics where the eigenvectors are not rotated by the linear transformation and are thus invariant for the continuous system. Therefore, taking these two vectors into account during the abstraction process is an obvious choice. However, in the more general case of nonlinear dynamics, the invariant takes a more complex form. Some technique encodes the hybrid system, the property to verify and a specific parametric form of the invariant into an SMT (Satisfiability Modulo Theories) based solver and evaluates the unknown parameters of the invariant automatically. Once computed, the invariant is incorporated to make a finer and more representative abstraction [START_REF] Gulwani | Constraint-based approach for analysis of hybrid systems[END_REF].

The finest abstraction of a hybrid automaton

Let us consider the semantics of a hybrid automaton as an infinite transition system. It is the most granular abstraction achievable whose computation is not possible in practice. We will use the finest abstraction in the next section to define a less granular abstraction, that can be computed.

The timed transition system Let S = q∈Q ({q} × Inv(q)) ⊆ S the (infinite) set of invariant satisfying states of H, S 0 = q∈Q 0 ({q} × Inv(q)) ⊆ S 0 the subset of invariant satisfying initial states and → ⊆ S × L × S the transition relation defined by one or the other condition in Definition 3.2, page 57. The semantics of H is actually given by the labeled transition system S t H = (S, S 0 , L, →), i.e., [[H]] is the set of all paths of S t H issued from an initial state. S t H , called the timed transition system of H, is thus a discretization of H with infinite sets of states and of transition labels. It just abstracts continuous flows by timed transitions retaining only information about the source, the target and the duration of each flow and constitutes the finest abstraction of H we will consider.

The timeless transition system

The timeless abstraction of S t H , called the timeless transition system of H, is obtained by ignoring also the duration of flows and thus defined as S H = (S, S 0 , Σ ∪ { }, →), obtained from S t H by replacing any timed transition (q i , x i )

d i -→ (q i+1 , x i+1 ) with d i ∈ R + by the transition (q i , x i ) - → (q i+1 , x i+1 ),

Geometric decomposition of the state space

The finest abstraction cannot be computed in practice generally. Consequently, we present finite state space decomposition of a hybrid automaton. We will then present an abstraction based on different decompositions that incorporates reachability and time constraints. Later on, we will discuss the refinement of the abstraction yielding constraints with better precision than before refinement.

Definition 4.1 (Continuous space partition). A (finite) partition P of the Euclidean space R n is a finite set of nonempty connected subsets of R n such that every point x ∈ R n is in one and only one of those subsets. We can write R n = p∈P p.

An element p of P will be referred to as a partition element and we will call it a region. For a subset E of R n , we will denote by P (E) the subset of regions of P that have a nonempty intersection with E.

The only smoothness hypothesis we will impose for the moment over a partition is that any (finite) continuous path crosses only a finite number of times each region, more precisely, ∀x : [0, 1] → R n a continuous function, ∀p ∈ P a region,

x -1 (p) is a finite union of intervals. In practice, partitions are chosen enough regular and smooth, with regions in any dimension from n to 0 such as (from simpler to more complex) rectangles, zonotopes, polytopes or defined by a set of polynomial inequalities. The choice among the different partitions is guided by the property we wish to verify. For example, consider a continuous system with dynamics F . A coarse but helpful way to obtain a high level reachability mapping would be to identify regions of the state space that conserve the sign of F . E.g., in one dimension, for all elements of the same region the derivative signs would be all either negative or positive or null. Thus, the regions would be the connected components of the three subsets p 1 , p 2 , p 3 defined by:

p 1 = {x ∈ X| ẋ > 0}, p 2 = {x ∈ X| ẋ < 0}, p 3 = {x ∈ X| ẋ = 0} (4.2)
For n dimensional systems, the regions would be the connected components of the

3 n subsets E s of R n parametrized by sign vectors s ∈ {-1, 0, +1} n : E s = {x ∈ X | ∀i, 1 ≤ i ≤ n, ẋi < 0 if s i = -1, ẋi = 0 if s i = 0, ẋi > 0 if s i = +1}.
If the considered system is a hybrid automaton, it is practical to allow different partitions in different modes. In the following, we will assume that the sets Init(q), Inv(q), G(τ ) and R(τ )(p) (for p connected subset of G(τ )) can be expressed as finite unions of connected subsets (if this is not the case, we will over-approximate parts of them). We define thus a decomposition of the hybrid state space as follows.

Definition 4.2 (Hybrid state space decomposition). Given a hybrid automaton H = (Q, X, S 0 , Σ, F, δ, Inv, G, R) and a set of partitions P, we say that P decomposes H if there is a surjective function d such that d : Q → P.

The initial and invariant sets and the guards satisfiability domains and variables reset domains are primary elements to take into consideration while abstracting. For q ∈ Q and τ = (q, σ, q ) ∈ δ, we denote the regions families d(q)(Init(q)), d(q)(Inv(q)), d(q)(G(τ )) by d Init (q), d Inv (q), d G (q, τ ) ⊆ d(q) and, for a region p ∈ d G (q, τ ), we denote d(q )(R(τ )(p ∩ G(τ ))) by d R (q , τ, p) ⊆ d(q ). When possible, we will try to define d such that Init(q), Inv(q), G(τ ) and R(τ )(p) are exactly the unions of the regions in those families (if not, those regions families overapproximate them).

Encoding hybrid automata reachability constraints

We have defined in 4.1.3 page 79, the timeless transition system S H of a hybrid automaton H as the finest timeless abstraction that can be obtained. However, in practice S H can only be computed for very restricted classes of hybrid automata.

We will define a less granular time-abstract transition system based on a set of partitions and define the relations between adjacent regions.

• Q DH = {(q, p)|q ∈ Q, p ∈ d(q)}. • Q 0 DH = {(q, p Init )|q ∈ Q 0 , p Init ∈ d Init (q)}.
• Σ DH = Σ ∪ { }.

• ((q i , p k ), σ, (q j , p l )) ∈ δ DH iff one of both is true:

-σ ∈ Σ and p k ∈ d G (q i , τ ) and p l ∈ d R (q j , τ, p k ) where τ = (q i , σ, q j ) ∈ δ.

-q i = q j and σ = and p k , p l ∈ d Inv (q i ) are adjacent regions and ∃d ∈

R * + and ∃x : [0, d] → X continuously differentiable function such that ∀t ∈ (0, d) ẋ(t) ∈ F (q i , x(t)), ∀t ∈ [0, d] x(t) ∈ Inv(q i ), x(0) ∈ p k , x(d) ∈ p l , ∃c 0 ≤ c ≤ d ∀t ∈ (0, c) x(t) ∈ p k ∀t ∈ (c, d) x(t) ∈ p l and x(c) ∈ p k ∪ p l .
The defined timeless abstract automaton encodes reachability with adjacent regions of the state space, the events in Σ witnessing mode changes and transitions representing a continuous evolution between adjacent regions in the same mode. Notice that ((q i , p k ), σ, (q j , p l )) ∈ δ DH ⇒ ∃x k ∈ p k ∃x l ∈ p l (q i , x k ) σ -→ (q j , x l ) in S H , the converse being true for σ ∈ Σ. The mapping α P defined by α P ((q, x)) = (q, p) with p ∈ d(q) and x ∈ p defines an onto timeless abstraction function α P : S → Q DH . If the flow condition F is a singleton, α P maps any transition of S H to a unique path in DH P . The coarsest timeless abstract automaton is obtained when partitions of P have all a unique region p = X and is thus (Q, Q 0 , Σ, δ), i.e., the discrete part of H without its continuous part. It corresponds to the coarsest timeless abstraction function α {{X}} ((q, x)) = q. For our previous thermostat example, this gives ({off , on}, {off }, {B on , B off }, {(off , B on , on), Abstracting with partial observations If now H is a POHA, in the same way we defined the observation of a concrete execution in Definition 3.13 we define the observation of its timeless abstraction.

Definition 4.5 (Timeless abstraction observation). Given a POHA H and h = (q 0 , p 0 ) σ 0 -→ (q 1 , p 1 )...(q i , p i ) •

σ i -→ ..., with σ i ∈ Σ ∪ { },
σ o i = σ i if σ i ∈ Σ o .
Otherwise, σ o i = ε, which is then removed from Obs(h).

Consider an execution h ∈ [[H]

] of the POHA H, h = (q 0 , x 0 )

l 0 -→ (q 1 , x 1 )...(q i , x i ) l i -→ ..., with l i ∈ Σ ∪ R + , its (timed) observation Obs(h) = x o 0 , l o 0 , x o 1 ...x o i , l o i , .
.. as in Definition 3.13, its timeless abstraction α P (h) = (q 0 , p 0 )

σ 0 -→ (q 1 , p 1 )...(q i , p i ) σ i -→ ..., with σ i ∈ Σ ∪ { },
p i = {p|x o i ∈p o } p o
the union of the projections on X o of all regions containing a value whose projection on X o is equal to x o i (assuming to simplify the same partition for each mode, as the mode may be unknown from observation). So, we notice that Obs(α P (h)) is more precise than α P (Obs(h)), as p o i ⊆ p i , which we denote by Obs(α P (h)) α P (Obs(h)) to mean that both sequences have common events and there is inclusion of the qualitative space values as subsets of X o , the valuations set corresponding to the observable variables.

Encoding hybrid automata time constraints

We are concerned with verifying temporal properties of hybrid systems and checking the diagnosability property using time constraints. For this reason, we define in this subsection, always related to a decomposition of the state space into partitions, an abstraction of the hybrid automaton as a timed automaton that partly captures the time constraints at the level of the regions. We will first introduce some intuitive ideas. Consider a partition P of the R n state space of a continuous system with arbitrary dynamics F , the set of trajectories (i.e., the continuous solution flows) entering a region p ∈ P is in one of these two cases: either at least one of the trajectories ends up trapped inside p for all future times or all of them exit p to an adjacent region within a bounded time under the continuity assumption.

In the first case, no time constraint can be associated with the region p unless a reshaping of p is applied; in the latter, it is possible to compute time constraints satisfied by all trajectories entering and leaving the region p. We will give a formal definition of the timed automaton constructed from given hybrid automaton and partitions set and then discuss some cases where a time bound can be practically computed.

Definition 4.6 (Region time interval and time bounds). Given a continuous system CS, a partition P of R n and p ∈ P one of its regions, we say that I p = [t min , t max ], with t min , t max ∈ R + ∪ {+∞}, is a region time interval of p for CS if all trajectories of the CS entering p at time t leave p at time t + t min at least and t + t max at most. t min and t max are lower and upper time bounds of p.

For a hybrid automaton, we denote the time interval relative to the region p in mode q as I (q,p) . Definition 4.7 (Decomposition-based timed abstract automaton of a hybrid automaton). Given a hybrid automaton H = (Q, X, S 0 , Σ, F, δ, Inv, G, R), a decomposition (P, d) and the timeless abstract automaton

DH P = (Q DH , Q 0 DH , Σ DH , δ DH )
of H with respect to P, we define the timed abstract automaton of H with respect to P as T H P = (Q DH , {c}, Q 0 DH , Σ DH , Inv T H , (δ DH , G T H , Y T H )) such that, ∀(q, p) ∈ Q DH with a region time interval I (q,p) = [t min , t max ]:

• Inv T H ((q, p)) = [0, t max ].
• ∀τ = ((q, p), σ, (q 1 , p 1 )) ∈ δ DH , G T H (τ ) = [t min , +∞) if σ = and p does not intersect any reset set (i.e., ∀τ = (q , σ , q

) ∈ δ DH p / ∈ d(q)(R(τ )(G(τ )))) or [0, +∞) else. and, ∀τ ∈ δ T H , Y T H (τ ) = {c}.
The timed abstract automaton adds time constraints to those states (q, p) of the timeless abstract automaton for which an interval I (q,p) is computable as nontrivial (i.e., I (q,p) = [0, +∞)), by using one local clock c (reset at 0 in each state) that measures the sojourn duration t in each state (q, p), i.e., in each region p, and coding these constraints by means of invariant and guard of c in each state.

The invariant codes the maximum sojourn duration as the upper time bound of the region p and the guard codes the minimum sojourn duration as the lower time bound of the region p when both entering and leaving the region are not the result of discrete jumps (controlled here directly for the out-transition and by requiring that p does not intersect any reset set for all possible in-transitions). In the thermostat example, consider the partition into two regions associated to the mode off given by the initial states set (off , [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF]) and by (off , [START_REF] Kilic | Diagnosability of fuzzy discrete event systems[END_REF][START_REF] Maler | Approximating continuous systems by timed automata[END_REF]). Then we take as time bounds for (off , [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF]) t min = 0 and t max = 0.12 (the exact upper bound, i.e., the time for the temperature to decrease from 90 to 80 is Log( 9 8 )). It means that we define in the timed abstract automaton Inv T H ((off , [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF])) = [0, 0.12]. A beginning of execution of the timed abstract automaton is, for example (off , [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF]) [START_REF] Kilic | Diagnosability of fuzzy discrete event systems[END_REF][START_REF] Maler | Approximating continuous systems by timed automata[END_REF]). If the flow condition F is a singleton function then the abstraction function α P defines a mapping, denoted by α t P , from S 0 rooted paths in S t H (i.e., executions of H) to executions in T H P . This mapping is trace preserving once labels are erased from executions traces in T H P and time period labels are added up between two consecutive events labels in both executions traces in S t H and in T H P . This means that, for any execution (q 0 , x 0 ) w -→ * (q i , x i ) ∈ [[H]], with w ∈ L * (where L = Σ ∪ R + ), it exists a unique execution (q 0 , p 0 ) w -→ * (q j , p j ) ∈ [[T H P ]], with w ∈ L * (where L = L ∪ { }), x 0 ∈ p 0 , q j = q i , x i ∈ p j , w |Σ = w |Σ (where |Σ is the projection of timed words on words on Σ * ) and, for any two successive events w l = w l and w m = w m of w |Σ , l <k <m ,w k = w k = l<k<m w k .

0.08 --→ (off ,
Forgetting time, i.e., removing the clock, provides a natural abstraction function α from T H P to DH P which maps an execution (q 0 , p 0 )

l 0 -→ (q 1 , p 1 )...(q i , p i ) l i -→ ..., with l i ∈ Σ∪{ }∪R + , in T H P into the execution (q 0 , p 0 ) σ 0 -→ (q 1 , p 1 )...(q i , p i ) σ i -→ ..., with σ i ∈ Σ∪{ }, in DH P , with σ i = l i if l i ∈ Σ∪{ } and continuous transitions labeled by l i = d i ∈ R + are suppressed. We have: α P = α • α t P .
Definition 4.8 (Timed abstraction observation). Given a POHA H and h = (q 0 , p 0 ) l 0 -→ (q 1 , p 1 )...(q i , p i ) l i -→ ..., with l i ∈ Σ∪{ }∪R + , an execution in T H P , i.e., a timed abstract path, the observation of h is defined as

Obs(h) = p o 0 , l o 0 , p o 1 ...p o i , l o i , ..., where • p o i is obtained by projecting p i on variables in X o . • l o i = l i if l i ∈ Σ o ∪R + . Otherwise, l o i = ε, which is then removed from Obs(h).
As for the timeless case, we can define the timed abstraction of an observation

(of an execution h ∈ [[H]]
) and we obtain: Obs(α t P (h)) α t P (Obs(h)). From another side, the abstraction function α that forgets time maps a timed abstract observation

p o 0 , l o 0 , p o 1 ...p o i , l o i , ..., with l o i ∈ Σ o ∪ R + , into the timeless ab- stract observation p o 0 , σ o 0 , p o 1 ...p o i , σ o i , ..., with σ o i ∈ Σ o , suppressing duration labels l i = d i ∈ R + . For any concrete execution h ∈ [[H]],
we have: Obs(α P (h)) = α(Obs(α t P (h))), i.e., Obs • α P = α • Obs • α t P . We now formally define a refinement operation of the previously defined abstraction. For this purpose, we construct a finer couple of discrete and timed automata by defining a more granular decomposition for regions and give the necessary assumptions to compute such refinement. By making the partition more granular in regions of interest, tighter time bounds are also obtained. The refinement is a necessary step when a proof for the verification of a property could not be made at a given abstraction level.

4.1.7 Refining the partitioning of the state space Definition 4.9 (Partition refinement). Given two partitions P and P of R n , we say that P is a refining partition of P iff ∀p ∈ P ∃p ∈ P p ⊆ p. This implies: ∀p ∈ P ∃P p ⊆ P p = p ∈P p p . Definition 4.10 (Hybrid state space decomposition refinement). Given two decompositions (P, d) and (P , d ) of a hybrid automaton H = (Q, X, S 0 , Σ, F, Inv, T ), we say that P refines P, denoted by P P, if ∀q ∈ Q d (q) is a refining partition of d(q).

Refined timeless model

Definition 4.11 (Refined timeless abstract automaton). Given a hybrid automaton H and two abstract timeless automata DH P and DH P of H with respect to two decompositions (P, d) and (P , d ) respectively, we say that DH P is a timeless refinement of DH P abstracting H if P ≺ P, which we denote by DH P ≺ DH P .

Definition 4.12 (State split operation). Given an abstract timeless automaton DH P of a hybrid automaton H, a split operation of the state (q, p) ∈ Q DH is defined by a partition {p 1 , p 2 } of p, p = p 1 p 2 , and results in two states (q, p 1 )

and (q, p 2 ) and in the refined abstract timeless automaton DH P with P obtained from P by replacing d(q) by d (q) = d(q)\{p} ∪ {p 1 , p 2 }.

The construction of DH P from DH P after a (q, p) state split is a local operation as only the transitions of δ DH having as source or as destination the state (q, p) have to be recomputed from H. In practice, the refined model is obtained by performing a finite number of state split operations. After having performed the split operations and in order for the obtained automaton to satisfy definition 4.4, it is only required to recompute some of its transitions, while inheriting the rest from DH P . Let Q split ⊆ Q DH be the set of split states and

post(Q split ) = {q ∈ Q DH | ∃q s ∈ Q split ∃(q s , σ, q) ∈ δ DH } and pre(Q split ) = {q ∈ Q DH | ∃q s ∈ Q split ∃(q, σ, q s ) ∈ δ DH }.
Then to obtain DH P it is sufficient to only recompute transitions (q, σ, q ) such that q, q ∈ Q split ∪ post(Q split ) ∪ pre(Q split ).

The onto abstraction function α P ,P : Q P DH → Q P DH defined by α P ,P ((q, p )) = (q, p) with p ⊆ p defines a trace preserving mapping α P ,P from DH P to DH P (and thus the language defined by DH P is included in the language defined by DH P ) and we have: α P = α P ,P • α P . Defining in a natural way as previously the P-abstraction α P ,P of the observation of a timeless P -abstract execution h, we obtain: Obs(α P ,P (h)) α P ,P (Obs(h)).

4.1.9 Refined timed model Definition 4.13 (Refined timed abstract automaton). Given a hybrid automaton H and two abstract timed automata T H P and T H P of H with respect to two decompositions (P, d) and (P , d ) respectively, we say that T H P is a timed refinement of T H P abstracting H if P ≺ P. We denote it similarly by T H P ≺ T H P .

Concerning the refined abstract timed automaton T H P resulting from a split of (q, p) into (q, p 1 ) and (q, p 2 ), if I (q,p) = [t min , t max ] the region time intervals I (q,p 1 ) = I (q,p 2 ) = [0, t max ] can be adopted in first approximation as they are safe, but in general new tighter time bounds are recomputed from H for the sojourn duration in the regions p 1 and p 2 . Thus, the refined timed model is obtained by a finite sequence of the two operations:

• State split: similar as before, the state split of (q, p) whose time interval is I (q,p) = [t min , t max ] yields (q, p 1 ) and (q, p 2 ). The time intervals for the new split regions are set as I (q,p 1 ) = I (q,p 2 ) = [0, t max ] (t max stays a safe upper bound of the sojourn duration but t min is reset to 0 since the split induces a distance shrink).

• Time bounds refinement: in this case, more precise time bounds are obtained for a given region of a discrete state, i.e., if I (q,p) = [t min , t max ] then I (q,p) = [t min , t max ] with t min ≥ t min and t max ≤ t max , at least one of both being a strict inequality.

The onto abstraction function α P ,P defines a trace preserving mapping α t P ,P from T H P to T H P , after trace simplification as in Theorem 4.2 and provided the time bounds used in T H P , once added for all regions p included in a given region p, are at least as tight as the time bounds used in T H P . And we have:

α t P = α t P ,P • α t P .
Finally, for any timed P -abstract execution h, we obtain: Obs(α t P ,P (h)) α t P ,P (Obs(h)).

Algorithmic computation of the abstraction

In the previous section we formally defined timeless and timed abstractions of a given hybrid automaton based on space partitioning. In this section, we present algorithmic steps to compute the timeless abstraction. Then, we discuss methods for computing the bounds of the timed abstraction. The next chapter will present a tool that applies the presented algorithms together with experimental results.

The timeless abstraction computation steps are summarized as follows and detailed next:

• For each mode q of H, compute a symbolic representation of the abstract states using qualitative reasoning rules.

• For each computed symbolic state st, evaluate the presence of a transition towards abstract states whose concretization is adjacent to the concretization of st.

• Apply a linking operation to the mode abstractions taking into account guards and resets.

For the rest of the thesis, we will instantiate the hybrid automata class to polynomial hybrid automata (page 65, Definition 3.11), hence we hold the following assumption:

Assumption 4.1. We assume that all dynamics, initial sets, invariant sets, guards and resets of the considered hybrid automaton are given by polynomials in the

Q[X] ring.
Example 4.3 (Two dimensional polynomial hybrid automaton). To illustrate the computation steps of this section we will consider the following example throughout this section. The example is purely theoretical and does not reflect a practical application.

q 0 ẋ0 = x 2 0 + x 1 ẋ1 = x 0 + x 2 1 x 0 ≥ 0 x 1 ≥ 0 q 1 ẋ0 = x 0 -x 1 ẋ1 = x 0 + x 1 x 0 ≥ 0 x 1 ≥ 0 x 2 0 + x 2 1 < 4 x 2 0 + x 2 1 > 9

Computing qualitative partitions

Partitioning rules Consider a mode q of H. We will apply the geometric decomposition seen in subsection 4.1.4 to define d(q) and compute the abstraction DH {d(q)} of q. Thus, the regions are the connected components of the 3 n subsets E s of R n parametrized by sign vectors s ∈ {-1, 0, +1} n :

E s = {x ∈ X | ∀i, 1 ≤ i ≤ n, ẋi < 0 if s i = -1, ẋi = 0 if s i = 0, ẋi > 0 if s i = +1}. Note that
in the case of polynomial dynamics, the sets conserving the sign vector are not necessarily connected, in such case we will reason over non-connected sets and use invariants (Inv(q)) to separate them. To further partition algorithmically the state-space into connected sets we refer the reader to algorithms in [START_REF] Basu | Complexity of computing semi-algebraic descriptions of the connected components of a semi-algebraic set[END_REF]. Moreover such sets are not necessarily convex. Nonetheless, for dynamics given by linear differential equations, the sign conserving sets are connected and convex.

Expressing abstract states. We use semi-algebraic sets to represent regions using (unions of) (in)equalities of polynomials over X. For example, if X contains two variables, we can express a circular set as: (xx 0 ) 2 + (yy 0 ) 2 < r 2 with x 0 , y 0 and r as given rational numbers.

Definition 4.14. A semi-algebraic set in R n is a finite union of sets defined each one by a finite number of equalities or inequalities over polynomials.

Computing the abstract states The computation is performed in the following way. For a mode q of the hybrid automaton, a stack Stack(q) is initialized with polynomials representing the initial and guard sets, incoming resets and dynamics.

The stack is then extended as follows: each polynomial from the stack is copied three times and copies are assigned +, -and null symbols. The regions expressions are obtained by symbolically computing the cross product of every element in the stack with all the other elements corresponding to different polynomials.

The result is the set of sign-conserving semi-algebraic sets. The abstract states are then labeled whether they belong to the initial set, guard condition or reset, or none of the above. The first computation step is symbolic, thus, some regions are not feasible (i.e., are empty sets). A first check is performed to eliminate all empty regions. This can be implemented by finding whether or not a set of polynomial equalities and inequalities admits a solution. The evaluation is performed using a quantifier elimination solver applying cylindrical algebraic decomposition and will be discussed in the next subsection. Abstract states whose region representation admits no solution are simply discarded from the stack. 4.2). When limiting the study zone to the specified invariant of q 0 , Inv(q 0 ) = {x 0 ≥ 0, x 1 ≥ 0}, we are left with three states (Table 4.3). Abstract States S 0

x 2 0 + x 1 = 0 S 1 x 2 0 + x 1 = 0 S 2 x 2 0 + x 1 = 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x 2 1 = ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > S 3 x 2 0 + x 1 = 0 S 4 x 2 0 + x 1 = 0 S 5 x 2 0 + x 1 = 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x 2 1 < ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > S 6 x 2 0 + x 1 = 0 S 7 x 2 0 + x 1 = 0 S 8 x 2 0 + x 1 = 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > S 9 x 2 0 + x 1 < 0 S 10 x 2 0 + x 1 < 0 S 11 x 2 0 + x 1 < 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x 2 1 = ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > S 12 x 2 0 + x 1 < 0 S 13 x 2 0 + x 1 < 0 S 14 x 2 0 + x 1 < 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x 2 1 < ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > S 15 x 2 0 + x 1 < 0 S 16 x 2 0 + x 1 < 0 S 17 x 2 0 + x 1 < 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > S 18 x 2 0 + x 1 > 0 S 19 x 2 0 + x 1 > 0 S 20 x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x 2 1 = ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > S 21 x 2 0 + x 1 > 0 S 22 x 2 0 + x 1 > 0 S 23 x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x 2 1 < ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > S 24 x 2 0 + x 1 > 0 S 25 x 2 0 + x 1 > 0 S 26 x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 >
Table 4.1: Qualitative abstract states for mode q 0 of Example 4.3

Non-empty Abstract States S 0

x 2 0 + x 1 < 0 S 1 x 2 0 + x 1 < 0 S 2 x 2 0 + x 1 < 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x > 0 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 > 4 ∧ x 2 0 + x < 4 S 3 x 2 0 + x 1 < 0 S 4 x 2 0 + x 1 < 0 S 5 x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x < 0 ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x > 4 S 6 x 2 0 + x 1 > 0 S 7 x 2 0 + x 1 > 0 S 8 x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x 2 1 < 0 ∧ x 0 + x > 0 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x > 4 S 9 x 2 0 + x 1 > 0 S 10 x 2 0 + x 1 > 0 S 11 x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x = 0 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x > 4 S 12 x 2 0 + x 1 > 0 S 13 x 2 0 + x 1 > 0 S 14 x 2 0 + x 1 = 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x 2 1 = 0 ∧ x 0 + x < 0 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x 2 1 = 4 ∧ x 2 0 + x < 4 S 15 x 2 0 + x 1 = 0 S 16 x 2 0 + x 1 = 0 S 17 x 2 0 + x 1 = 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x > 0 ∧ x 2 0 + x 2 1 > 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x = 4 S 18 x 2 0 + x 1 = 0 ∧ x 0 + x 2 1 = 0 ∧ x 2 0 + x 2 1 < 4
x 2 0 + x 1 > 0 S 9 x 2 0 + x 1 > 0 S 10 x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 0 + x > 0 ∧ x 2 0 + x 2 1 > 4 ∧ x 2 0 + x 2 1 < 4 ∧ x 2 0 + x = 4
Table 4.3: Non-empty invariant satisfying qualitative abstract states

Computing transitions between regions

We show in this section how to compute transitions between abstract states. The absence of incoming transitions to an abstract state translates by the absence of incoming trajectories to the region on the concrete level. The presence of a transition from abstract state S to S translates by the presence of some trajectories from the region of S going to the region of S after some bounded time.

For illustrative purpose, consider the set of continuous variables X to be of dimension two and let p(x, y) be a formula for which y is a function of a real variable x. The example p(x, y) = -x + y is shown in Figure 4.5. The normal Figure 4.5: Projecting the flow onto the normal vector of qualitatively chosen boundaries vector of p(x, y) is obtained by applying the partial derivatives with respect to each variable. It is not other than the gradient of p, thus points towards the direction of increasing p when a small increase of x and y occurs, in other words points towards the half plane p(x, y) > 0.

n = ∂p ∂x , ∂p ∂y = (-1, 1) (4.3)
Let us consider an ODE represented on the figure by its vector field F : ẋ = 1, ẏ = 2. A sufficient condition for which a trajectory starting in p(x, y) < 0 is able to cross to p(x, y) > 0 is that there exists a point on the boundary p(x, y) = 0 for which the vector field is pointing to p(x, y) > 0. We project the flow vector onto the normal vector and study the sign of the obtained scalar product dp. F . If there is a point (x 0 , y 0 ) for which dp. F (x 0 , y 0 ) > 0 then such a trajectory exists. In our example dp. F (x, y) = 1. If dp. F = 0 then for sure no trajectory from p(x, y) < 0 to p(x, y) > 0 is possible, but with this information alone we cannot guarantee that there is no transition from p(x, y) < 0 to p(x, y) = 0. In such case, we need to evaluate the vector field in a neighborhood around p(x, y) = 0 by studying the Jacobian matrix.

Regions defined using multiple constraints Consider our previous example and define another region boundary p 2 (x, y) = x + y. We consider all the nine connected regions formed by p 1 (x, y) op 0 ∧ p 2 (x, y) op 0 where op ∈ {<, >, =}.

To evaluate whether or not transitions are possible from a region to another, we need to evaluate the scalar product over the boundary of each region. In our example, those boundaries for the four regions of dimension two are given by two half lines. E.g., for S 0 the boundary is (p Varying normal vector In the case of polynomial hybrid automata, the direction of the normal vector over a given boundary varies with the position on the boundary. In such case dp is expressed as a polynomial.

1 (x, y) = 0∧x ≤ 0)∧(p 2 (x, y) = 0∧x ≥ 0) (see
Evaluating the flow projection onto boundaries Consequently, to evaluate the presence or not of an abstract transition, one is required to find the truth values of semi-algebraic constraints. We use a method that has been elaborated tackling this problem called Cylindrical Algebraic Decomposition (CAD). CAD was first introduced by Collins [START_REF] Collins | Quantifier elimination by cylindrical algebraic decomposition[END_REF]. We now review briefly the basic steps of this method.

Let {P (X)} be a set of polynomials over n variables with coefficients in Q. The method constructs a partition of R n where the set of polynomials {P (X)} holds a constant sign for all variables in X in every region of the computed partition. Once the decomposition is computed, it can be then used to give solutions to system of (in)-equations. The algorithmic steps are:

1. For each coordinate variable x ∈ X, (a) Find the projection on x of the intersection points of all polynomials in P (X) (i.e., solve p 1 (x) = p 2 (x)... = p n (x)).

(b) Find the zero sets of each polynomial with respect to x.

(c) Find singularity points on x for every polynomial (i.e., the function does not behave well or is not defined).

(d) Form regions on the domain of x partitioned according to the previously found sets of points and/or intervals.

2. Choose a sample point within each region, and evaluate each polynomial p(x) at each chosen point for x and symbolically for the other coordinates (variables) from X.

3. Study the sign of each p(x) at the sampled points.

4. Match the (in)-equalities required by the problem to be solved with the previously obtained table, if no match is found then the problem admits no feasible solution.

The CAD method has been proven to be doubly exponential [START_REF] Davenport | Real quantifier elimination is doubly exponential[END_REF]. However one can benefit from parallelism to alleviate the computation time, since every transition computation can be performed independently. The idea will be discussed in the next chapter.

Extending the expressiveness to rational fractions For the moment, the considered class of hybrid systems is the polynomial class. Nonetheless with some minor modifications, one can extend the abstract states and transitions computation to ODEs with rational functions. For example, given a rational fraction P (x) Q(x) , Studying the truth value of P (x) Q(x) > 0 is equivalent to studying the truth value of:

(P (x) > 0 ∧ Q(x) > 0) ∨ (P (x) < 0 ∧ Q(x) < 0) (4.4)
One can use CAD with an intermediary computation layer to allow for ODEs with rational fractions.

Example 4.5 (Transitions Computation). Let us compute the transitions between

abstract states from the previous example (Example 4.3, page 90). Consider the two adjacent regions given by abstract states S 8 and S 9 and their common boundary region given by S 10 (Table .4.3, page 94).

S 8 : x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 2 0 + x 2 1 > 4 (4.5) S 9 : x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 2 0 + x 2 1 < 4 (4.6) S 10 : x 2 0 + x 1 > 0 ∧ x 0 + x 2 1 > 0 ∧ x 2 0 + x 2 1 = 4 (4.7)
The normal vector to the boundary region is given by n = (2x 0 , 2x 1 ). The scalar product of the normal vector with the flow in mode q 0 is then:

n. F = 2x 3 0 + 2x 3 1 + 4x 0 x 1 (4.8)
The presence of a trajectory from S 9 to S 10 and from S 10 to S 8 is then given by the truth value of the following formula:

x 2 0 +x 2 1 = 4∧2x 3 0 +2x 3 1 +4x 0 x 1 > 0∧x 2 0 +x 1 > 0∧x 0 +x 2 1 > 0∧x 0 ≥ 0∧x 1 ≥ 0 (4.
9) The evaluation of formula 4.9 using CAD returns true. The same reasoning goes for evaluating the presence of transitions from S 8 to S 10 and S 10 to S 9 , the CAD evaluation of the corresponding formula gives false.

Linking the single mode abstractions

At this stage, the abstract states and transitions have been computed for one mode. The operation is repeated similarly for every mode q of H. The following operation will link the obtained mode abstractions. The linkage operation consists in expressing each guard region of a transition τ in a mode q 1 whose target mode is q 2 (or the image in q 2 of this region by the reset if the transition has a reset) according to the partition of mode q 2 . In other words, we have to compute

α d(q 2 ) (G(τ )) (or α d(q 2 ) (R(τ )(G(τ )
)) in case of reset), given α d(q 1 ) (G(τ )), and the transitions from the regions of the latter one to the regions of the first one. The operation is implemented by checking the nonemptiness of

p 1 ∩ G(τ ) ∩ p 2 ∩ Inv(q 2 ) (or R(τ )(p 1 ∩ G(τ )) ∩ p 2 ∩ Inv(q 2 )
in case of reset) for each region p 1 ∈ d(q 1 ) and each region p 2 ∈ d(q 2 ), which boils down to a satisfiability check of a system of polynomial equalities and inequalities. If satisfied, a mode change transition is thus added from region p 1 to region p 2 .

Refinement operation.

Refining the abstraction consists in adding further information from the hybrid system to obtain a more precise abstraction. The idea is to split one or more regions into several regions by adding further boundaries to the decomposition. This is applied per mode of the hybrid system. What is important to notice is that many of the previously computed transitions remain valid after a refinement operation. The refinement algorithm checks which transitions remain valid and recomputes those that require to be reevaluated. The following are the algorithmic steps to perform for a refinement operation. Consider a new boundary region B new (typically of dimension n -1) to be added to the abstraction. In order to keep the abstraction complete while incorporating the new boundary into the current partition, the following is performed:

1. Find the set of regions {R compute } from the previous decomposition that intersect B new . 2. For the set of regions {R old } that do not intersect B new , leave their incoming and outgoing transitions intact.

3. Process each region R compute intersecting B new .

• Find which boundaries (in all dimensions) of R compute intersect B new .

• Compute the newly obtained regions.

• Recompute the in and out transitions relative to those new regions as previously explained in the subsection 4.2.2.

Computing time bounds

In this subsection, we are interested in algorithmic methods to compute the time bounds of the timed abstraction. The timeless abstraction DH P provides the sets of qualitatively chosen regions with transitions towards adjacent ones. Let P be a partition of R n associated with one of the modes of H and I p = [t min , t max ] the associated region time interval of some region p ∈ P . Finding the exact minimum and maximum sojourn times is not always possible. Hence, it is rather more practical to consider upper and lower bounds of these sojourn times that keep the abstraction complete.

Definition 4.15 (Reasonable time bounds). The upper and lower bounds t min , t max associated to some region p are said to be reasonable if t min > 0 and t max = +∞, otherwise they are said unreasonable.

Some interesting points to be noted when investigating whether or not a region has reasonable time bounds:

• An unbounded region does not necessarily have unreasonable time bounds.

• A bounded region with no critical points does not necessarily have reasonable time bounds.

• A region containing only critical points has unreasonable time bounds.

• A qualitatively partitioned region (according to the sign of the derivative vector) containing no critical points does not necessarily have reasonable time bounds.

Each boundary of a region p is associated with transitions towards adjacent regions in the abstract timeless system. The transition associated to a boundary is either (inward) or (outward) or (inward and outward) towards (or from) p. For a region expressed as a semi-algebraic set given by p 1 < 0 ∧ p 2 < 0 ∧ ... ∧ p n < 0, the boundaries are B(p) = {p 1 = 0, .. Numerical simulations can be used to find approximate time bounds of p, however this is not an exact method.

Numerical estimation of the time bounds

We consider a set of points for each inward boundary in B in (p). A number of numerical simulations initialized from these points are computed and stopped when trajectories verify the equations of the abstract state neighboring any outward boundary of the region from B out (p). The exact trajectory is not guaranteed to reach an exit. Assuming the numerical trajectories reach an outward boundary, we obtain a collection of time lapses.

Choosing the maximum and minimum elements of the sample allows one to determine approximations of the maximum and minimum sojourn times. Obviously, the obtained bounds are estimated and not verified, thus the timed abstraction obtained is not necessarily complete. We propose a more suitable and accurate method for computing the time bounds.

Guard satisfying regions If the considered region p (or part of it) satisfies a mode change condition (i.e., the guard condition) from mode q to mode q while having the invariant of q satisfied within the region, the system exhibits nondeterminism between either a mode jump or staying within the mode q. This fact must be reflected by the time constraint associated to p. The dynamics within the two modes q and q must be taken into account for the region p and each associated region p in q reached after mode jump (possibly via a reset). The computation of the time bounds t min (resp. t max ) should be done for both regions p and p together as a whole by combining minimum (resp. maximum) sojourn times in p then p with a non-deterministic mode change (and possible reset), i.e., evaluating the global minimum (resp. maximum) bounds for all possible instants of mode jump, by using both dynamics of q and q . In the following, we consider the standard case of a region in absence of any guard or reset.

Computing t max

We previously defined t max as the maximum sojourn time in a region.

Consider a system of two-dimensional ODEs:

ẋ = f 1 (x, y) (4.10) ẏ = f 2 (x, y) (4.11)
The problem is summarized as follows. Consider an initial and final point in the (x, y) plane M i (x i , y i ) and M f (x f , y f ). The time lapse τ = t f -t i taken by the continuous system initially in M i at time t i to reach M f at time t f is expressed by:

τ = t f t i dt = x f x i dx f 1 (x, y) = y f y i dy f 2 (x, y) (4.12)
Computing τ exactly is not always possible since, generally speaking, the solutions x(t) and y(t) cannot be expressed in closed forms. Suppose that M i and M f are varying points respectively on the inward boundary B in and outward boundary B out . To find a safe upper bound of the maximum sojourn time, we will use a variant of flow-pipe construction. The idea is to construct a flow-pipe that will not be used to find the set of reachable states, but rather to identify the time elapsed to reach an outward boundary. The flow-pipe F low is of total duration N ∆t where ∆t is the time step and N ∈ N is to be found. F low is initialized from an inward boundary b in ∈ B in (p) of a considered region p. ContinuousTimeElapsed(B, ∆t) is a procedure computing a flow-pipe initially starting from B with a time step ∆t that was introduced in the scientific context (Chapter 2, page 29). In the latter we reviewed the existing flow-pipe computation tools that were successful in analyzing hybrid automata from linear to polynomial dynamics [START_REF] Frehse | Spaceex: Scalable verification of hybrid systems[END_REF][START_REF] Chen | Flow*: An analyzer for non-linear hybrid systems[END_REF]. To the best of our knowledge, the tools assume convex initial sets, however the qualitatively chosen boundaries can be non-convex. Thus, practical results for time bound computation will only be applied to convex qualitative regions. Algorithm termination Remind that the region p is chosen qualitatively and not containing any critical point. This assumption does not prove that the time bounds are finite, but however discards some situations where the time bounds are not finite. Consequently the qualitative partition choice eases the time bounds computation. Obviously, unless bounded by T , termination of algorithm 2 is generally not guaranteed. One can check for conditions for which finite time bounds exist and adapt the maximum time horizon T accordingly.

For the class of polynomial hybrid automata we consider, solving the equations is a well-studied procedure in non-linear optimization with constraints. The previously explained abstraction algorithms are applied to this thermostat example. The result is automatically obtained from the tool (that will be presented in Chapter 5) and is illustrated in Figure 4.8. Green states correspond to guard satisfiability, blue states are regions interpreted from the other mode and purple states are regions produced if both mode invariants were set to true. The produced abstraction graph proves that the four regions (of f, 3), (of f, 4), (on, 0) and (on, 4) of the state space in purple color are time invariants. The abstract state of the initial set [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF] is region 0 in mode of f . From state 0 only one abstract trajectory exists, a mode change is possible to region 1 in mode on and going back to mode of f is possible. The abstraction is sufficient to provide a proof that (of f, 2) and (of f, 1) are to be crossed by the system for a mode change to happen. The transitions outgoing from the blue regions are computed during the mode linkage step. Notice that the information within this abstraction are not enough to prove for example that all trajectories starting from (of f, 0) are eventually (i.e., in finite time) subject to a mode change. This can be proven however if the abstraction contains additionally time sojourn bounds expressing how much time can the system stay in a given region as we previously defined (Def. 4.7).

Application to diagnosability verification

Hybrid automata have generally an infinite state space and their semantics can be represented using infinite state machines. Thus, to verify formally their properties we will rest on using model checking over the abstraction of the hybrid system.

Model-checking can be inconclusive, in which case the abstraction must be refined.

In this section, we adapt counterexample guided abstraction refinement (CEGAR) that we previously reviewed (Chapter 2.3.5, page 40) to diagnosability verification. CEGAR was originally proposed to verify safety properties [START_REF] Edmund | Verification of hybrid systems based on counterexample-guided abstraction refinement[END_REF][START_REF] Alur | Counterexample-guided predicate abstraction of hybrid systems[END_REF].

Note that to verify safety properties, it is sufficient to check one execution at a time and verify whether the execution can reach an unsafe state. However, verifying diagnosability reveals a more complex task as one is required to simultaneously analyze two executions at a time, i.e., to verify whether or not the two executions have the same observations while only one of them contains the considered fault.

The abstraction of the hybrid automaton can be directly used to verify safety and generate an abstract counterexample when safety is violated. This is performed by state exploration of the abstraction given the abstract states of the unsafe set of states. This is not the case for diagnosability verification, in fact a transformation of the abstraction is required to find critical pairs using state exploration.

CEGAR scheme for hybrid automata diagnosability verification

Consequently, the adaptation of CEGAR to verify diagnosability of H consists in three steps described as follows and to be detailed in the next subsections:

• Abstracting a hybrid automaton using the previously elaborated method to obtain the timed automaton abstracting H.

• Diagnosability checking of a timed abstract automaton of H. Unlike safety verification, the timed abstraction cannot be directly used to check for the property to be verified and generate abstract counterexamples. This is why we use the twin plant method that transforms the timed automaton abstraction to another representation. The latter can be directly used to generate a counterexample C.E by simple state exploration when diagnosability is not verified at the abstract level.

• Validation of the C.E by checking whether the C.E is valid or spurious at the concrete level.

• Refinement of the timed abstract automaton by using a finer hybrid state space decomposition to avoid the found C.E when it is declared spurious.

Verifying diagnosability of a hybrid automaton by checking it on its abstraction is justified because if the diagnosability property is verified for an abstraction, then it is verified also for the concrete hybrid system. This can be established by showing that a concrete counterexample of diagnosability lifts up into an abstract counterexample of diagnosability. Actually, given a hybrid automaton

H = (Q, X, S 0 , Σ, F, Inv, T ), two executions h, h ∈ [[H]] such that h = (q 0 , x 0 ) l 0 -→ (q 1 , x 1 )...(q i , x i ) l i -→ ... h = (q 0 , x 0 ) l 0 -→ (q 1 , x 1 )...(q i , x i ) l i -→ ...
are called a counterexample of diagnosability in H with respect to the fault F if they satisfy the three conditions defined in Definition 3.16 (page 71), i.e., if h and h constitute a critical pair of H. We will denote each state (q i , x i ) by s i and (q i , x i ) by s i .

Theorem 4.3. Given a hybrid automaton H, a timed abstract automaton T H P of H with abstraction function α t P and a modeled fault

F in H, if F is (∆-)diagnosable in T H P then F is (∆-)diagnosable in H.
Proof. Assume that F is not ∆-diagnosable in H. Then a critical pair exists among the executions of H, thus the following holds:

∃h, h ∈ [[H]], F ∈ h and F /
∈ h and time(h, F ) ≥ ∆ and Obs(h ) = Obs(h).

From Theorem 4.2, since T H P is a timed abstraction of H with abstraction function α t P , if we denote ĥ = α t P (h) and ĥ = α t P (h ), then the following holds:

∃ ĥ, ĥ ∈ [[T H P ]], F ∈ ĥ and F / ∈ ĥ and time( ĥ, F ) ≥ ∆ and Obs( ĥ ) = Obs( ĥ).

possible diagnoses. A twin plant state is called an ambiguous one if the corresponding two pre-diagnoser states give two different diagnoses (presence for one and absence for the other of a past fault occurrence). A critical path is a path in the twin plant with at least one ambiguous state cycle. It corresponds to a critical pair and it has thus been proved that the existence of a critical path is equivalent to non-diagnosability. The twin plant method has been adapted to be applied to timed automata [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF], where a twin plant is constructed in a similar way except that the time constraints of two executions are explicitly taken into account using clock variables. The idea is to verify whether the time constraints can further distinguish two executions by comparing the occurrence time of observable events.

The definition of a critical path in the twin plant is analog, except that ambiguous state cycle is replaced by infinite time ambiguous path.

Lemma 4.1. A fault is diagnosable in a timed automaton iff its twin plant contains no critical path [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF].

For timed automata, checking diagnosability is PSPACE-complete.

Algorithmic Computation of the Twin Plant of a Timed Automaton

We review (informally) the main steps for building the twin plant of a partially observable timed automaton with a single modeled fault.

1. Make two identical copies of the timed automaton.

2. For one copy, rename the unobservable events (faulty and normal events), discrete states and clocks such that it has different names than the other copy.

3. Remove for one of the copies all transitions labeled with the copy's faulty event.

4. Compute the product of the two timed automata by forcing observable transition events to synchronize.

5. Assign the invariant of every state from the product timed automaton by composing the invariants of the merged states with the Boolean ∧ operator.

Example 4.7 (Twin plant construction example). Figure 4.10 illustrates a timed automaton with initial state q init and observable events Σ o = {a, b} and unobservable event Σ u = {u} and fault event Σ f = {f }. Under any two nominal and faulty executions of the timed automaton, the event b cannot appear at the same time.

Consequently, the timed automaton is diagnosable and contains no critical pair.

Notice that the invariants in q 1 and q F 1 play a role in determining diagnosability as b becomes an event forced to appear at necessarily different times between a non-faulty and a faulty execution. If the invariant of q 1 was for example the same as q F 1 , then the timed automaton would become non-diagnosable. If we change the guard of the transition (q 0 , f, q F 1 ) from t > 3 to t ≥ 3 then the timed automaton becomes non-diagnosable witnessed by the critical pair (h, h ) such that:

h =(q init , 0) a - → (q 0 , 0) 3 - → (q 0 , 3) u - → (q 1 , 3) b - → (q 2 , 3) h =(q init , 0) a - → (q 0 , 0) 3 - → (q 0 , 3) f - → (q F 1 , 3) b - → (q F 2 , 3)
Projecting the pair onto observations we obtain Obs(h) = Obs(h ) = 0, a,

q init q 0 t ≤ 6

q 1 t ≤ 3 q F 1 t ≤ 6 q 2 q F 2 a t := 0 u t ≤ 3 t > 3 f b b Figure 4.10: Diagnosable Timed Automaton
The twin plant is the product, synchronized on observable events, of the timed automaton with a copy of itself where the copy holds only the normal executions (those that do not contain the fault event). For the previous example, every state q is copied and denoted q , unobservable event u is copied and renamed u and clock t is copied and renamed t . The observable events a and b are synchronized, while transitions of u and u can occur asynchronously. The obtained twin plant is illustrated in Figure 4.11. Using a simple state exploration algorithm of the twin plant, we cannot find any fault labeled execution with infinite time proving the absence of critical pairs in the original timed automaton, and thus the diagnosability.

(q init , q init ) (q 0 , q 0 ) t ≤ 6 t ≤ 6 (q 1 , q 0 ) t ≤ 3 t ≤ 6 (q 1 , q 1 ) t ≤ 3 t ≤ 3 (q F 1 , q 0 ) t ≤ 6 t ≤ 6 (q 0 , q 1 ) t ≤ 6 t ≤ 3 (q F 1 , q 1 ) t ≤ 6 t ≤ 3 (q 2 , q 2 ) (q F 2 , q 2 ) a t := 0 t := 0 u t ≤ 3 t > 3 f u t ≤ 3 u t ≤ 3 b u t ≤ 3 b f t > 3 u t ≤ 3

Counterexample validation or refusal

After applying the twin plant method on a timed abstract automaton T H P of H as described in [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF], suppose that a critical pair C.E = ( ĥ, ĥ ) is returned (if not, it means that T H P , and thus H, is diagnosable). Whether we find or not two concrete executions h, h ∈ [[H]] whose abstractions by α t P are ĥ and ĥ and form a concrete critical pair decides if C.E is validated or refuted. We detail below both procedures for validation or refusal and the reasons for which, in the latter case, a critical pair can be assumed spurious.

Validating an abstract counterexample: If the returned counterexample ( ĥ, ĥ ) exists at the concrete level, there exists h, h ∈ [[H]], whose abstractions no abstract counterpart. Thus the refinement has to apply the split operation as previously described, so that preserving the abstraction while eliminating the spurious counterexample.

Spurious time constraints satisfaction: The abstract critical pair, when considered timeless, owns a concrete critical pair realization in H but none verifying the time bounds imposed by the abstract timed automaton. In this case it is not a spurious state reachability problem but a spurious timed state reachability problem. Actually the time constraints of the abstract critical pair cannot be satisfied by any concrete critical pair realizing it in H.

Spurious observation undistinguishability:

The two executions of the abstract critical pair share the same observations (observable events with their occurrence times and snapshots of the values of observable continuous variables at arrival times in each abstract state) but actually any two concrete executions realizing this critical pair in H do distinguish themselves by the observation of some observable continuous variable.

Refinement of the abstraction

If it reveals that the abstract counterexample C.E = ( ĥ, ĥ ) is spurious, then one refines the timed abstract automaton T H P to get T H P , guided by the information from C.E. The first step is analyzing C.E to identify the reasons why it is spurious (as classified previously). The idea is to avoid getting relatively close spurious abstract counterexample when applying twin plant method on the refined timed abstract automaton T H P . The refinement procedure is described as follows and will be illustrated on our example in the next subsection. 1. Suppose that C.E is refuted due to an illegal stay, i.e., the corresponding invariant is not respected. The consequence could be s reach |h|+1 = ∅, i.e., an illegal transition. To eliminate such spurious counterexample next time, one can partition the region containing ŝ|h| to get a new region representing the legal stay such that the refinement can be done based on this partition. The idea is to eliminate illegal (unobservable) transitions between the new region and others by tightening time constraints. In a similar way, one can handle spurious counterexamples with illegal transitions due to the unsatisfiability of the corresponding guards by the evolution of continuous variables, but with a legal stay this time.

Case study example

The CEGAR scheme for diagnosability checking of hybrid automata will be illustrated by the following case study example.

Example 4.8 (Fault tolerant thermostat model). We start from our thermostat example as nominal behavior and we add two faulty transitions to new faulty modes. The two observable events B on and B off allow one to witness mode changes and the continuous variable x is assumed to be observable. The system starts from

x ∈ [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF]. Two faults are modeled as unobservable events F 1 and F 2 ∈ Σ f shown in Figure 4.12. In practice, the fault F 1 models a bad calibration of the temperature sensor. As for fault F 2 , it represents a defect in the heater impacting its efficiency and is modeled by a parametric change of a constant in the expression of the first order derivative of x.

CEGAR scheme for fault F 1 Initial Abstraction: We consider an initial decomposition P = {P off , P on , P F 1 off , P F 1 on P F 2 off , P F 2 on } of the hybrid state space. Each partition P ∈ P is made up of only one region representing the reals R. Hence computing t min and t max for each region p yields I p = [0, +∞), in other words the initial abstraction contains no time constraints.

Diagnosability Check: The diagnosability check using the twin plant method gen-

off ẋ = -x x ≥ 68 on ẋ = -x + 100 x ≤ 82 off F 1 ẋ = -x x ≥ 80 on F 1 ẋ = -x + 100 x ≤ 90 off F 2 ẋ = -x x ≥ 68 on F 2 ẋ = -x + 120 x ≤ 82
x ∈ [START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF] x ≤ 70/B on --→ (off , p off )... ĥ = (off , p off )

0.1 -→ (off , p off ) F 1 -→ (off F 1 , p F 1 off ) 0.05 --→ (off F 1 , p F 1 off ) Bon --→ (on F 1 , p F 1 on ) 0.3 -→ (on F 1 , p F 1 on ) B off --→ (off F 1 , p F 1 off )...
Validation or refusal: The computation of the set of concrete executions {h} (resp.

{h }) whose abstraction is ĥ (resp. ĥ ) yields an approximation as follows: Initial Abstraction: The same as for F 1 .

{h} = (off , [
Diagnosability Check: The diagnosability check of the initial abstraction using the twin plant method generates a C.E = ( ĥ, ĥ ): ĥ = (off , p off )

0.5 -→ (off , p off ) Bon --→ (on, p on ) 0.5 -→ (on, p on ) B off --→ (off , p off )... ĥ = (off , p off ) 0.5 -→ (off , p off ) Bon --→ (on, p on ) 0.4 -→ (on, p on ) F 2 -→ (on F 2 , p F 2 on ) 0.1 -→ (on F 2 , p F 2 on ) B off --→ (off F 2 , p F 2 off )...
Validation or refusal: The computation of the set of concrete executions {h} (resp.

{h }) whose abstraction is ĥ (resp. ĥ ) yields an approximation as follows:

{h} = (off , [

Second Abstraction

Diagnosability Check: The second C.E generated from the refined twin plant is: ĥ = (off , p off 1 )

0.08 --→ (off , p off 1 ) - → (off , p off 2 ) 0.07 --→ (off , p off 2 ) Bon --→ (on, p on ) 0.5 -→ (on, p on ) B off --→ (off , p off )... ĥ = (off , p off 1 ) 0.08 --→ (off , p off 1 ) - → (off , p off 2 ) 0.07 --→ (off , p off 2 ) Bon --→ (on, p on ) 0.4 -→ (on, p on ) F 2 -→ (on F 2 , p F 2 on ) 0.1 -→ (on F 2 , p F 2 on ) B off --→ (off F 2 , p F 2 off )...

Chapter Summary

In this chapter we elaborated a method to generate an abstraction of a given hybrid automaton using qualitative reasoning. A timing of the abstraction is proposed using existing flow-pipe techniques to generate the timed automaton abstraction. An adaptation of CEGAR that was specifically used for safety verification is applied to diagnosability verification by extending results that were specific for discrete event and timed systems.

Chapter 5

Implementation and Experimental results

Automating the abstraction computation

In this chapter an implementation of a tool that applies previous algorithms from Chapter 4, Section 4.2 (page. 89) is presented. The tool automatically computes the timeless abstraction of a hybrid automaton and is implemented in C++. First, the tool architecture is presented followed by the primary classes and external dependencies. Second, we briefly explain the implementation specific procedures and present experimental results while evaluating performances. Finally, perspectives to extend the current implementation to compute the timed abstraction and perform diagnosability verification are presented and discussed.

Black box view

The input model is a polynomial hybrid automaton written in accordance to the grammar rules described in Appendix A. CAD Evaluate(string) evaluates the true or f alse nature of a CAD formula using QepCAD.

Transitions Compute given a Polynomial Partition, this function will compute the formula expressing the scalar product between the dynamics and the normal vector of some boundary while limiting the evaluated boundary to the region of the considered abstract state. The brusselator is a mathematical model used for representing chemical reactions with cyclic change of color. The dynamics are nonlinear. The model holds a single mode q with a singleton flow F given by the variables derivatives as:

ẋ0 = 1 -4x 0 + x 2 0 x 1 ẋ1 = 3x 0 -x 2 0 x 1
For illustrative purposes, two numerical simulations of the example show a clockwise rotation of the trajectories with respect to the (x 0 , x 1 ) coordinates (see selator in the first quadrant of the (x 0 , x 1 ) plane, thus we add to Inv(q) the constraints: x 0 > 0, x 1 > 0 as invariants. The system is two-dimensional, hence the computed abstraction according to flow sign vector contains 3 2 = 9 states. The tool successfully analyzes the example, the produced abstraction is shown both as an automaton view in As a result, trajectories come neither in nor out, thus no outgoing or incoming transitions are associated to state 8.

1 -4x0 + x 2 0 x1 < 0 3x0 -x 2 0 x1 < 0 2 1 -4x0 + x 2 0 x1 < 0 3x0 -x 2 0 x1 = 0 1 1 -4x0 + x 2 0 x1 < 0 3x0 -x 2 0 x1 > 0 6 1 -4x0 + x 2 0 x1 = 0 3x0 -x 2 0 x1 < 0 3 1 -4x0 + x 2 0 x1 > 0 3x0 -x 2 0 x1 < 0 7 1 -4x0 + x 2 0 x1 = 0 3x0 -x 2 0 x1 > 0 4 1 -4x0 + x 2 0 x1 > 0 3x0 -x 2 0 x1 > 0 5 1 -4x0 + x 2 0 x1 > 0 3x0 -x 2 0 x1 = 0 8 1 -4x0 + x 2 0 x1 = 0 3x0 -x 2 0 x1 = 0 (
Change of Invariant Another abstraction of the brusselator is computed with a change of the previous invariant from x 0 > 0 ∧ x 1 > 0 to true, the result is represented in Figure 5.4. Notice that new transitions that were absent appear (3 → 5) and (5 → 4). The result is correct and is due to the non-connected sets of the considered abstract states. This abstraction shows that the behavior of the system can possibly be counter-clockwise when considering the whole state space

R 2 .
Refining the abstraction Let us consider more granular regions of the previous partitions for each example. Consider adding x 1 -5 as a refining polynomial of the In this case, the half-plane expressed by x 1 -5 < 0 is added to these regions. The 0 1 -4x 0 + x 2 0 x 1 < 0 3x 0 -x 2 0 x 1 < 0 x 1 -5 < 0 2 1 -4x 0 + x 2 0 x 1 < 0 3x 0 -x 2 0 x 1 = 0 x 1 -5 < 0

1 1 -4x 0 + x 2 0 x 1 < 0 3x 0 -x 2 0 x 1 > 0 x 1 -5 < 0 13 1 -4x 0 + x 2 0 x 1 = 0 3x 0 -x 2 0 x 1 > 0 x 1 -5 < 0 6 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2 0 x 1 > 0 x 1 -5 < 0 8 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2 0 x 1 > 0 x 1 -5 = 0 7 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2 0 x 1 > 0 x 1 -5 > 0 12 1 -4x 0 + x 2 0 x 1 = 0 3x 0 -x 2 0 x 1 < 0 x 1 -5 < 0 3 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2 0 x 1 < 0 x 1 -5 < 0 5 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2 0 x 1 < 0 x 1 -5 = 0 4 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2 0 x 1 < 0 x 1 -5 > 0 10 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2 0 x 1 = 0 x 1 -5 > 0 9 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2 0 x 1 = 0 x 1 -5 < 0 11 1 -4x 0 + x 2 0 x 1 > 0 3x 0 -x 2
0 x 1 = 0 x 1 -5 = 0 14 1 -4x 0 + x 2 0 x 1 = 0 3x 0 -x 2 0 x 1 = 0 x 1 -5 < 0

Computation Time

Making use of multi-threaded programming It is important to note that the transitions computing can be parallelized, once the abstract states are computed for a single mode. For the moment this parallelization is not implemented in the presented tool. In fact, an evaluation of a set of inequalities using CAD has been proven to be doubly exponential [START_REF] Davenport | Real quantifier elimination is doubly exponential[END_REF]. Hence, parallelizing the computations will significantly reduce the computation time of the abstraction and will allow one to handle systems with large number of modes and with higher dimensions (i.e., the number of continuous variables involved).

Benchmark evaluation We use the benchmark proposed by Xin Chen in [START_REF] Chen | A benchmark suite for hybrid systems reachability analysis[END_REF] to evaluate computation time over different linear, non-linear and hybrid systems models. The computation time is illustrated in Table 5.3, page 134 and is achieved on a machine equipped with an Intel Core i5-3210M CPU operating at a 2.5 Ghz frequency. All input models are given in appendix A.2 (page 143).

Refined models computation time For some of the previously considered examples from the benchmark, we applied successive refinement steps to obtain a more granular abstraction. The refining polynomials were chosen randomly. The computation time of the refined models and the number of refinement steps (i.e., number of added polynomials for all modes) are illustrated in Table 5.4 (page 135).

Fail reasons Fail (1) occurred with one of the transition computation at the level of the quantifier elimination solver with no specific error. Fail (2) occurred due to the lack of extra cells needed for the computation. In fact the number of cylindrical algebraic decomposition cells in QepCAD is capped. From the first transition computation of Biology Model 1, the number of required cells exceeded the maximum cap.

Extending the tool with optimization libraries

Once the qualitative abstraction is computed, the tool can optionally call a nonlinear optimization library Nlopt to perform optimization operations over the partitioned regions.

Computing V min and V max An important operation that can be performed is computing the maximum and minimum values of the first order derivatives of each continuous variables. After the discrete abstraction of H is computed, the user can choose to compute V min and V max . Similarly to the transitions between regions computation, the computation of the minimal and maximal values of ẋ denoted respectively V min and V max can be parallelized as well. The tool interfaces with the Nlopt library and uses existing algorithms to determine safe upper and lower bounds of V min and V max with a tolerated error. The computed values will refine the abstraction and can be represented using rectangular automata. We were interested in verifying a given formal safety property on a hybrid system, based on discrete abstractions of this system, for which checking this property is decidable and which guarantee that the property is satisfied at the concrete hybrid level if it is satisfied at the abstract level. We focused on the diagnosability property, for its importance in safety analysis at design stage and the challenge it gives rise to. We presented elements from the literature regarding hybrid automata abstractions, however few works handle diagnosability verification, as this property deals with a pair of trajectories and partial observations of the system and is thus more complex to check than reachability. In order to handle time constraints at the abstract level, we chose abstractions of the hybrid automaton as timed automata, related to a decomposition of the state space into geometric regions, the abstract time constraints coming from the estimation of the sojourn time of trajectories in each region. Thus the abstractions over-approximate the regions of interest to which are added time constraints obtained from the dynamics of the concrete system. We adapted a CEGAR scheme for hybrid systems diagnosability verification, based on the counterexample provided at the abstract level by the twin plant based diagnosability checking when diagnosability is proved to be unsatisfied. We presented situations for which the produced counterexample is spurious and a refinement in finer regions and tighter time constraints is then required. A tool prototype that implements the qualitative simulation algorithm of a given hybrid automaton (with at most polynomial dynamics in terms of expressiveness) have been developed and tested over examples.

6.2 Comparison with the existing literature where the orientation whether inward or outward is reflected in the abstraction over qualitatively partitioned regions. This is justified as some properties can only be proved by taking all aspects of the flow orientation into account (recall the brusselator example direction of rotation). In our work we propose to combine existing flow-pipe computation techniques with finite state abstractions to obtain a more representative, timed abstraction.

Diagnosability verification

Works of A. Grastien [START_REF] Grastien | Solving diagnosability of hybrid systems via abstraction and discrete event techniques[END_REF] In the abstraction method we previously elaborated, time constraints are used explicitly. When an abstraction refinement is required, tighter time bounds are obtained over the new regions of the refined small. This will ensure theoretical termination of the algorithm, as the number of refinement steps to reach the precision will then be finite. And this is actually justified in practice because both model parameters and observations cannot be infinitely accurate, thus the value for the precision would come from the precision of the model parameters and of the measurements, in space and time.

• In the same spirit, one interesting future work would be to demonstrate a bisimulation relation between the concrete model and the final refined abstract model when considering this minimal precision imposed by the model and the sensors, where the termination of the refinement can thus be guaranteed. In other words, theoretically, we could always deduce the right verdict, either the system is diagnosable or it is not diagnosable with respect to a given minimal precision.

• Another promising aspect of diagnosability verification is to study the potential of this approach for deducing at design stage minimal concrete sets of observations (which events/continuous variables to observe, i.e., which sensors, and at which observation times, e.g., sampling periods of sensors) for which the system is diagnosable (assuming it would be diagnosable if observation was total). This includes both suppressing sensors placement (if not useful otherwise) while keeping existing diagnosability or adding sensors to make diagnosable a non-diagnosable system [START_REF] Briones | Optimizing the system observability level for diagnosability[END_REF].

• We would like as well to study the application of the approach to the problem of active diagnosis. The latter supposes that the system is controllable via actions at execution time. When some actions are performed the future evolution of the system is changed. If the system is not diagnosable, a controller can be synthesized that forces the system to stay within the diagnosable area of execution. The problem was studied for systems modeled as automata [START_REF] Haar | Optimal constructions for active diagnosis[END_REF].

• Extending the abstraction combined with model checking approach to other formal properties such as predictability seems promising. Predictability is a property of the model, if satisfied then it is possible to predict in advance the future unavoidable occurrence of a fault, given some sequence of observations.

Tool perspectives

• Interfacing the current tool prototype with existing flow-pipe computation tools to automate the computations of the time bounds of the timed abstraction and for validating/refuting a given counter-example is a crucial step to extend the existing prototype. We plan in particular to use and extend existing tools for timed automata model checking and for over-approximation reachability at the continuous level. We want to investigate also the usage of SMT solvers [START_REF] Cimatti | SMT-based scenario verification for hybrid systems[END_REF][START_REF] Cimatti | HyComp: An SMT-based model checker for hybrid systems[END_REF], in particular with theories including ODEs [START_REF] Gao | Satisfiability modulo ODEs[END_REF], to deal simultaneously with discrete and continuous variables.

• We wish to implement a split of the sign preserving regions, which for the moment can have non-connected components (in the case of polynomial dynamics) to have sign preserving regions with only connected sets. This is feasible in practice, in fact using results from the literature [START_REF] Heintz | Description of the connected components of a semialgebraic set in single exponential time[END_REF] and known theorems such as, Theorem 6.1. Every semialgebraic set has finitely many connected components which are semialgebraic. Every semialgebraic set is locally connected.

the obtained abstraction by partitioning the state-space into connected components is guaranteed to stay finite.

• It is also important to interface the tool with a timed abstraction diagnosability model checker which given a fault-modeling partially observable timed automaton, computes the corresponding twin plant and generates (∆)critical pairs (such a model checker has been developed at LRI, implemented with the SMT solver Z3). Once implemented it can be interfaced with the current prototype tool to perform CEGAR for verifying automatically diagnosability.

• Implementing a state split strategy guided by a validated counterexample is as well a practical and useful step to perform. Thus T is infinite, the equilibrium point is never reached. This reasoning can be extended to dimension n by evaluating r ṙ and using spherical (or hyperspherical) coordinates and to polynomial with real exponents. We can take an example of square root, for instance ẋ = √ x and demonstrate the time T is finite, then the equilibrium is reached.

Infinite number of null derivatives. Studying a case where at least one derivative along an axis takes an infinite number of null values in a connected set can be done by extending the previous method. For the particular class of continuous systems where the dynamics are only allowed multi-affine function form, [START_REF] Maler | Approximating continuous systems by timed automata[END_REF] showed how it is possible to capture time constraints by decomposing the infinite state space R n into hypercubes and evaluate the time elapsed between entering and exiting each cube by bounding the dynamics.

Brusselator time bounds. For the Example 5.1 (page 127) of the brusselator dynamics, which is a repeller case around the point M 0 = (1, 3), consider the ring set R that excludes M 0 such that R = {(x 0 , x 1 ) | 0.09 < (-1 + x 0 ) 2 + (-3 + x 1 ) 2 < 0.5625}. Let v = ẋ0 2 + ẋ1 2 then v 2 = (1-4x 0 +x 2 0 x 1 ) 2 +(3x 0 -x 2 0 x 1 ) 2 and, using a solver, we compute a lower bound v 2 low = 0.0051 of v 2 . It has been proven that all trajectories initially in S 0 = R 2 \ {M 0 } converge towards a fixed orbit of the phase plane contained within R. Suppose we split the region R into two connected sets R 1 and R 2 such that R = R 1 R 2 , for each of which the maximal sojourn duration t max is a positive real constant. This is possible since v admits a lower bound v low . This states that all trajectories initiated from S 0 will cross R 1 and R 2 sequentially infinitely often. In practice, the presence of the system in either R 1 or R 2 can correspond to two different visible colors of the chemical reaction. Abstract: Hybrid systems are complex systems that combine both discrete and continuous behaviors. Verifying behavioral or safety properties of such systems, either at design stage or on-line is a challenging task. Actually, computing the reachable set of states of a hybrid system is undecidable. One way to verify those properties over such systems is by computing discrete abstractions and inferring them from the abstract system back to the original system. We are concerned with abstractions oriented towards hybrid systems diagnosability checking. Our goal is to create discrete abstractions in order to verify if a fault that would occur at runtime could be unambiguously detected in finite time by the diagnoser. This verification can be done on the abstraction by classical methods developed for discrete event systems, which provide a counterexample in case of nondiagnosability. The absence of such a counterexample proves the diagnosability of the original hybrid system. In the presence of a counterexample, the first step is to check if it is not a spurious effect of the abstraction and actually exists for the hybrid system, witnessing thus non-diagnosability. Otherwise, we show how to refine the abstraction and continue the process of looking for another counterexample.

Université Paris-Saclay Espace Technologique / Immeuble Discovery Route de l'Orme aux Merisiers RD 128 / 91190 Saint-Aubin, France

tion 2 .

 2 1 presents model driven engineering and verification. Section 2.2 reviews the literature concerned with qualitative reasoning and simulation. Section 2.3 addresses hybrid systems modeling and verification techniques. The last section summarizes existing tools and challenges in the hybrid systems verification domain. The objective of the thesis is the study of abstraction techniques of hybrid systems using qualitative principles and their application to diagnosability verification. For this reason, it is important to review the concerned literature and existing techniques presented in this chapter. Consequently the literature addressing qualitative reasoning principles is presented. The latter are used in the proposed abstraction technique. Moreover, existing hybrid systems verification techniques are reviewed to bring forward what the elaborated qualitative abstraction can complement and for comparison purposes. Works addressing diagnosability of discrete event, timed and hybrid systems are recalled; in fact the proposed diagnosability verification technique uses and extends some of the thesis works from the presented scientific context.

  all of the following are met: f is continuous on [a, b]; f is continuously differentiable on (a, b) with values in R and f d (a) and f g (b) exist in R (when defined, i.e., when a or f (a) is finite and the same with b); the set of critical points of f in any bounded interval of [a, b] has only finitely many connected components;

Figure 2 . 1 :

 21 Figure 2.1: Graph of a function labeled with the minimum set of landmarks and time-distinguished points

Definition 2 . 5 (

 25 Qualitative Behavior). The qualitative behavior of f on [a, b] is the sequence of qualitative states obtained by alternating timed-distinguished points

Example 2 . 2 Figure 2 . 2 :

 2222 Figure 2.2: Two tanks system

Figure 2 . 3 :

 23 Figure 2.3: Qualitative model of the U-Tube example

Figure 2 . 4 :

 24 Figure 2.4: Forward and backward flow-pipe computation for safety verification

Figure 2 . 6 :

 26 Figure 2.6: Flow-pipe computation versus numerical simulations

Figure 2 . 7 :

 27 Figure 2.7: Hybrid automata abstraction scheme combined with model checking

Figure 2 . 8 :

 28 Figure 2.8: Three abstract states defined via predicates and linked via flow-pipe computation

Theorem 2 . 1 .

 21 Given a hybrid automaton H, a discrete automaton DA which is an abstraction of H with abstraction function α, let B ⊂ S, and B = { b | ∃b ∈ B : b = α(b)}. Then DA |= AG¬ B implies H |= AG¬B.

Example 2 . 6 (

 26 Hybrid Program). Hybrid programs are an equivalent representation method of hybrid automata. To illustrate a hybrid program, let us consider the verification task of a simple train control system. The example is present in Keymaera. The goal is to verify that the train at location z never bypasses the movement authority (MA) by a distance SB in order to avoid collisions with other train. In dL logic, this is expressed by a hybrid program where a is the acceleration of the train, b is the train braking constant and c is an acceleration constant such that: ET CS ≡ if (MAz < SB) then a := -b else a := c z = a • The ETCS program consists of two parts, a control part ctrl (verifying a guard condition with a reset) and a continuous applied dynamic drive. When embedded into an actual train, the ET CS program must repeat itself periodically. This is represented by assigning the Kleene star to the sequence: ET CS ≡ (ctrl; drive) * . The star refers to continuous repetition of the sequence ctrl; drive of hybrid programs with respect to time.

Figure 3 . 1 : 1 -

 311 Figure 3.1: 1-dimensional hybrid automaton modeling a thermostat

Figure 3 . 2 :

 32 Figure 3.2: Thermostat behavior for: (a) Mode off , (b) Mode on

  (off , 81)... is valid for the thermostat (Example 3.1), thus h ∈ [[H]]. The trace of an execution h, i.e.,

  This definition is identical to Definition 2.6, except that now any state is considered final. The semantics [[D]] of D is given by the set of sequences (called paths) made up of successive states transitions labeled by events and rooted in an initial state. It has a finite representation. The trace of such a path is the word in Σ (Σ ω for infinite paths) whose letters are the successive labels of the path. Definition 3.4 (Continuous systems (CS)). It is the case where there is no discrete part. Thus, an n-dimensional continuous system (CS) is a particular hybrid automaton C with only one mode (|Q| = 1) and Σ, T = ∅ (and thus δ, G, R too).It can thus be denoted as C = (X, S 0 , F, Inv) with S 0 ⊆ Inv.The semantics [[C]] of C is the set of all time labeled sequences of continuous states, rooted in an initial state, corresponding to the continuous transitions constrained by the dynamics F and the invariant set Inv. Its representation is infinite.

Definition 3 . 6 (

 36 Rectangle of dimension n). A rectangle I of dimension n is a product of n intervals I i = (a i , b i ) whose endpoints (that may belong or not to the interval) are in {R ∪ ±∞} I = Π 1 i n I i (3.1)

  ẏ = a x + b y + c xy + d (3.4) where a, b, c, d, a , b , c , d ∈ R. Definition 3.10 (Multi-Affine Hybrid Automata (MAA)). A multi-affine hybrid automaton (MAA) is a hybrid automaton M A = (Q, X, S 0 , Σ, F, δ, Inv, G, R) for

2 Figure 3 . 4 :

 234 Figure 3.4: Graphical representation of the switched buffer hybrid system example

Definition 3 . 12 (

 312 Partially observable hybrid automaton (POHA)). A partially observable hybrid automaton (POHA) is a hybrid automaton H (Def.3.1, page. 53)

Proposition 3 . 2 .Theorem 3 . 1 (

 3231 A fault F is diagnosable in a partially observable timed automaton T iff there is no +∞-critical pair in [[T ]] with respect to F . Diagnosability check of timed automata). Checking diagnosability of a partially observable timed automaton T is PSPACE-complete.

Figure 4 . 1 :

 41 Figure 4.1: Square abstraction of a continuous evolution: complete unsound abstraction (left), sound and complete abstraction (right)

Definition 4 . 3 (

 43 Adjacent regions). Two distinct regions p 1 , p 2 of a partition P of R n are adjacent if one intersects the boundary of the other: p 1 ∩ p 2 = ∅ or p 1 ∩ p 2 = ∅, where p refers to the closure of p. Definition 4.4 (Decomposition-based timeless abstract automaton of a hybrid automaton). Given a hybrid automaton H = (Q, X, S 0 , Σ, F, Inv, T ) and a decomposition (P, d) of H, we define the timeless abstract (finite) automaton of H with respect to P as DH P = (Q DH , Q 0 DH , Σ DH , δ DH ) with:

(

  on, B off , off )}) and the abstraction of the execution h given previously (3.1.4) is just off Bon --→ on B off --→ off ...

Theorem 4 . 1 (

 41 Timeless abstraction completeness). Given a decomposition P of H, any concrete behavior of H is timeless abstracted into a Q 0 DH rooted path in DH P and any transition of DH P abstracts a part of a concrete behavior of H. If the flow condition F is a singleton function then the timeless abstraction function α P defines a trace preserving mapping (still denoted by α P ) from S 0 rooted paths in S H (i.e., timeless executions of H) to Q 0 DH rooted paths in DH P and thus the language defined by S H is included in the language defined by DH P .Obviously, a path in DH P does not abstract in general a concrete behavior of H (as the behaviors parts abstracted by the individual transitions do not connect in general) which expresses that abstraction creates spurious behavior.

  Figure 4.2 illustrates a parallelogram abstraction. Two concrete trajectories h and h are abstracted by two abstract paths respectively p 1 → p 2 and p 2 → p 3 ; however the abstract path p 1 → p 2 → p 3 admits no feasible concrete trajectory.

3 (p 1 ; p 2 )(p 2 ; p 3 )Figure 4 . 2 :

 3122342 Figure 4.2: Abstraction spurious effect: every concrete trajectory is covered by an abstract trajectory but the opposite does not necessarily hold.

Theorem 4 . 2 (

 42 Timed abstraction completeness). Given a decomposition P of H, any concrete behavior of H is timed abstracted into an execution in T H P .

Figure 4 . 3 :

 43 Figure 4.3: Polynomial hybrid automaton example

Example 4 . 4 (

 44 Computing an initial qualitative partition). Applying the previous steps for the considered example (Example 4.3, page 90), the initial partition of mode q 0 (whose null-clines and guard boundary are shown on Figure 4.4) contains the abstract states represented in Table 4.1. The empty regions check eliminates 8 regions and we are left with 18 abstract states (Table

Figure 4 . 4 :

 44 Figure 4.4: Qualitative partition of mode q 0

  Figure 4.6).

Figure 4 . 6 :

 46 Figure 4.6: Flow projection onto regions defined using multiple constraints

Assumption 4 . 3 .

 43 The considered region p does not intersect any guard or reset set.

Example 4 . 6 (

 46 Temperature regulator). Consider again the temperature regulator, or thermostat (see Figure 3.1). The continuous behavior of each mode is illustrated in Figure 4.7.

Figure 4 . 7 :

 47 Figure 4.7: Thermostat phase plane with randomly generated numerical simulations: (a) Mode of f , (b) Mode on

(Mode on, Region 2

 2

Figure 4 . 8 : 12 80 and reaching 70 :(

 48128070 Figure 4.8: Thermostat qualitative abstraction: (a) Mode off , (b) Mode on

Figure 4 . 9 :

 49 Figure 4.9: Timed abstraction of the thermostat system (a) Mode on, (b) Mode off

Figure 4 . 11 :

 411 Figure 4.11: Twin plant of a diagnosable timed automaton

Figure 4 . 15 - 3 -

 4153 Figure 4.12: 1-dimensional hybrid automaton modeling a faulty thermostat

Figure 5 . 2 )Figure 5 . 2 :

 5252 Figure 5.2). As a first simulation, we are interested in the behavior of the brus-

Figure 5 . 3 .

 53 a and in the continuous space view in Figure 5.3.b. The qualitative simulation shows what behavior of the system is impossible and what behavior is possible. Using a numerical simulator (or computing an

  0

Figure 5 . 3 :

 53 Figure 5.3: Brusselator computed abstraction with Inv(q) = (x 0 > 0 ∧ x 1 > 0) (a) Automaton view (b) Continuous space view

Figure 5 . 4 :

 54 Figure 5.4: Brusselator computed abstraction with Inv(q) = true (a) Automaton view (b) Continuous space view

Figure 5 . 5 :

 55 Figure 5.5: Adding a refining polynomial to a previous decomposition

Figure 5 . 6 :

 56 Figure 5.6: Refined Brusselator Abstraction Automaton View

Table 5 . 3 :

 53 Computation time of the timeless abstraction for different models

6. 2 . 1

 21 Hybrid Automata AbstractionWorks of A. Tiwari[START_REF] Tiwari | Abstractions for hybrid systems[END_REF] The works of Tiwari introduced qualitative reasoning to hybrid automata verification. The broad class of hybrid automata is considered and experimentation is provided through examples and case study. Our work further instantiates the framework to the specific class of polynomial hybrid automata and considers partitions of the state space using semi-algebraic sets. Feasibility and applicability in practice of the qualitative simulation is shown by the tool implementation and a manual refinement of the abstraction is implemented.Works of C. Sloth [60]Sloth elaborated abstraction methods of hybrid automata represented as timed automata. In his work, inductive invariants are considered and form a basis of the abstraction technique. Consequently, he considers regions of interest for which the projections of the flow to boundaries are always oriented inward, making the region an invariant. This is not the case in our work,

1 +

 1 cos 2 (θ)(1 -rcos(θ)))

Titre:

  Modélisation et Simulation Qualitatives des Systèmes Hybrides Mots clés: Automates Hybrides, Abstraction, Raisonnement Qualitative, Diagnosticabilité. Résumé: Les systèmes hybrides sont des systèmes complexes qui combinent un double comportement continu et discret. La vérification des propriétés comportementale comme la sûreté de ces systèmes, depuis la modélisation ou durant leur exécution en ligne, est une tâche difficile. En effet, calculer l'ensemble des états atteignables par un système hybride est indécidable. Une façon de vérifier ces propriétés est de calculer des abstractions discrètes et d'inférer le résultat obtenu du système abstrait vers le système d'origine. Dans ce travail on est concerné par des abstractions orientées pour vérifier la diagnosticabilité d'un système hybride donné. Notre objectif est de créer des abstractions discrètes pour vérifier si une faute qui peut survenir du-rant l'exécution du système peut être détecter sans ambiguïté en un temps borné par le diagnostiqueur. La vérification est effectuée sur l'abstraction en utilisant des méthodes classiques, développées pour les systèmes à évènements discrets qui fournissent un contreexemple si le système n'est pas diagnosticable. L'absence d'un tel contre-exemple prouve la diagnosticabilité du système original. En présence d'un contre-exemple, la première étape consiste à vérifier si le contre-exemple est un artefact résultant de l'abstraction et existe au niveau du système hybride, témoignant ainsi de la non-diagnosticabilité du système. Dans le cas-contraire, on montre comment raffiner l'abstraction et continuer à rechercher un autre contre-exemple. Title: Modeling and Qualitative Simulation of Hybrid Systems Keywords: Hybrid Automata, Abstraction, Qualitative Reasoning, Diagnosability.

Table 2 .

 2

1: Initial qualitative state

  .2). The applied rules rely on the continuously differentiable assumption for each variable. The successor state is valid for the open time interval (t 0 , t 1 ) where t 1 is the next time-distinguished point.

		Qualitative Variable	q val	q dir
			H A		(0, H Amax ) -
			H B		(0, H Bmax ) +
			P A		(0, +∞)	-
			P B		(0, +∞)	+
			P AB		(0, +∞)	-
			f lowAB	(0, +∞)	-
		Table 2.2: Successor qualitative state
	still not reached, thus the current model can represent the spilling effect of water
	from tank B (QS 3 , Table 2.3). Thus, many next qualitative states are possible,
	the transition system obtained from a qualitative simulation is not deterministic.
	Qualitative Variable	q val	QS 1	Branched Qualitative States QS 2	QS 3
	At t 1 , different qualitative states are possible. Either an equilibrium is reached
	with f lowAB being null, or f lowAB continues to decrease. In the first case, there
	are two possibilities, either the tank B is filled at the same time the equilibrium is
	reached (QS 1 , Table 2.3), or B is only partially filled while reaching the equilibrium
	(QS 2 , Table 2.3). In the second case, tank B is fully filled but the equilibrium is

  then any arbitrary precision can be computed by increasing the Taylor polynomial order.

	Hybrid Automaton H	Abstraction Function α
			Abstract System A
	Undecidable state reachability
			Model Checking Algorithm
	Verdict Analysis and Inference Rules	Guaranteed Termination

  qualitative principles Let us apply qualitative based reasoning to abstract continuous change (reviewed in 2.2, page 17). Given a set of ODEs, the infinite state space of the continuous variables is discretized into a finite set. The discretization of R n is often achieved by rectangles, i.e., is built by product from a discretization of R. And this one is obtained by fixing a finite number of (ratio-

nal) landmarks l i , resulting in a finite partition in terms of open intervals (l i , l i+1 ) (with possibly infinite endpoints) and singleton intervals [l i ], allowing what is called absolute order of magnitude reasoning. The coarsest partition (except R itself)

  that can be considered as a silent transition. It has infinite set of states but finite set of transitions labels. It constitutes the finest timeless abstraction of H we will consider. Proposition 4.1 (Correctness and completeness of the semantics). Any concrete behavior of H is timed (resp. timeless) abstracted into an S 0 rooted path in S t H (resp. S H ). Conversely, any path in S t H (resp. S H ) that alternates continuous and discrete transitions (in particular any single transition) abstracts a part of a concrete behavior of H and, if the flow dynamics F is a singleton function (i.e., deterministic derivative), any S 0 rooted path in S t H (resp. S H ) abstracts a concrete behavior of H. In this latter case, there is thus no spurious abstract behavior in S t H (resp. S H ), which expresses faithfully the behavior of H.

  a timeless abstract path in DH P , the observation of h is defined as Obs(h) = p o 0 , σ o 0 , p o 1 ...p o i , σ o i , ..., where • p o i is obtained by projecting p i on variables in X o .

  as in Theorem 4.1 (assuming F a singleton) and the observation of this last one Obs(α P (h)) = p o 0 , σ o 0 , p o 1 ...p o i , σ o i , ... as in Definition 4.5. We could try to define the timeless abstraction of the observation Obs(h). A natural definition would be α P (Obs(h)) = p 0 , σ o 0 , p 1 ...p i , σ o i , ..., with σ o i = l o i if l o i ∈ Σ o (and = , which is removed, otherwise), i.e., the same σ o

i 's as in Obs(α P (h)), and

Table 4 .

 4

	2: Qualitative abstract states after empty regions check
	Non-empty Abstract States
	S 8

  ., p n = 0}. Let B in (p) be the set of inward boundaries towards p, B out (p) be the set of outward boundaries from p and B in/out (p) be the set of inward and outward boundaries towards (or from) p. The sign based timeless abstraction allows one to differentiate between regions containing only critical points and those that do not contain any critical point (the number of critical points in any region is finite as the number of zeros of a polynomial is finite). Regions containing only critical points are assigned a maximum and minimum sojourn time t min = t max = +∞. Consequently, for the following the time bound computation concerns regions containing no critical points.Assumption 4.2. The considered region p contains no critical points.

  Algorithm 2 is applied to obtain t max of a region p. input : set B in (p) of inward boundaries of a region p, time horizon T output: a safe over-approximating time bound t max of p for b in ∈ B in (p) do t max i ← 0; while t max i < T do F low ← ContinuousTimeElapsed(b in , ∆t); t max i ← t max i + ∆t; if (F low ∩ p = ∅) then break; end if (t max i ≥ T ) then return "max reached"; end return Maximum (t max i );

	Algorithm 2: Computing a safe time bound of a region

2 .

 2 Suppose that the refutation of C.E is due to different observations from s |h|+1 and s |h |+1 without reachability problem. The idea is to calculate the exact moment, denoted t spurious , before which it is still possible to get the same observations while after it the observations will diverge. With t spurious , one can partition ŝ|h|+1 and ŝ |h |+1 to get a new region whose legal stay is limited by t spurious and transition to another region gives birth to a new refined observation by means of an observable continuous variable if any.

  The concrete state computations show that it is not possible to stay 0.05 time units in mode off F 1 as the temperature reached would be[START_REF] Lee | The past, present and future of cyber-physical systems: A focus on models[END_REF][START_REF] Liu | Safe diagnosability of stochastic discrete-event systems[END_REF] violating the invariant

	80, 90])	0.15 --→ (off , [69, 77])	Bon --→ (on, [69, 70])...
	{h } = (off , [80, 90])	0.1 -→ (off , [72, 81])	F 1 -→ (off F 1 , [80, 81])	0.05 --→
	(off F 1 , [76, 77] : invalid)

x ≥ 80. The C.E is thus refuted.

Refinement of the state space:

The refinement aims at eliminating the previous spurious C.E. From this C.E, it is possible to compute the exact time constraint for staying in mode off F 1 and then triggering the transition B on and refine the hybrid state space accordingly. Once refined, the new abstraction should not contain similar counterexamples. The validation process reveals that all trajectories entering mode off F 1 with x ∈

[START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Matveev | Qualitative Theory of Hybrid Dynamical Systems[END_REF]

cannot stay more than t max = 0.0124 time units but it is possible for some trajectories to instantaneously change from off to off F 1 to on F 1 in which case t min = 0, thus I (off F 1 ,

[START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Matveev | Qualitative Theory of Hybrid Dynamical Systems[END_REF]

) = [0, 0.0124]. The refined abstraction would carry this new information by updating the partition of mode off F 1 , from R to (-∞, 80)

[START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Matveev | Qualitative Theory of Hybrid Dynamical Systems[END_REF]

(81, +∞), thus ensuring that all future generated counterexamples would satisfy this constraint.

CEGAR scheme for fault F 2

  This C.E is refuted due to illegal stay in the mode off violating the corresponding invariant. In other words the trajectories are not feasible: if the system stays in mode off for 0.5 time units then the state invariant is no longer true. Thus, if B on is observed then the duration of stay in off should be smaller.

	80, 90])	0.5 -→ (off , [48.5, 54.58] : invalid)
	{h } = (off , [80, 90])	0.5 -→ (off , [48.5, 54.58] : invalid)

Refinement of the state space: To prevent future similar spurious counterexamples, a refinement is applied to the initial abstraction. The refined model considers new regions in mode off : p off 1 = [80, 90] (initial region) and p off 2 = [68, 80) (legal region). The computation of the time intervals relative to each region are:

I (off ,

[START_REF] Kilic | Diagnosability of fuzzy discrete event systems[END_REF][START_REF] Maler | Approximating continuous systems by timed automata[END_REF]

) = [0, 0.16] and I (off ,

[START_REF] Maler | Approximating continuous systems by timed automata[END_REF][START_REF] Pencolé | A chronicle-based diagnosability approach for discrete timed-event systems: Application to web-services[END_REF]

) = [0, 0.12]. The refined abstraction will encode these time constraints and ensure that a set of similar counterexamples (including this one) are eliminated. Regions that are not reachable will be eliminated, such as [0, 68).

  Validation or refusal: Note that the continuous transitions in the second C.E respect the temporal constraints added during the refinement based on the first C.E. The corresponding concrete approximate executions of this C.E are:In this case, this second C.E is also considered as spurious because, given the time constraints, the two trajectories are different in the observations of x in the hybrid system since the last regions are disjoint, i.e.,[80.5, 81.8] ∩ [82.9, 83.7] = ∅. And also the invariant x ≤ 82 in on F 2 is violated.Refinement of the state space: The counterexample analysis could identify the time boundary t spurious , up to which the observations could be the same for at least two concrete trajectories, and after which the critical pair becomes spurious.In our example, suppose the fault occurred at t f where x ∈ [a, b], then t spurious is the time instant from which faulty and nominal sets of trajectories are disjoint:

	{h} = (off , [80, 90])	0.15 --→ (off , [69, 77])		Bon --→ (on, [69, 70])	0.5 -→ (on, [80.5, 81.8])...
	{h } = (off , [80, 90])	0.15 --→ (off , [69, 77])	Bon --→ (on, [69, 70])	0.4 -→ (on, [79, 79.9])	F 2 -→
	(on F 2 , [79, 79.9])	0.1 -→ (on F 2 , [82.9, 83.7])...
			t spurious = ln	b -a + 20 20	+ t f	(4.16)

For the second spurious C.E, t f = 0.4 and t spurious -t f = 0.044. The two concrete nominal and faulty executions originating from (on,

[79, 79.9]

) will be in the following temperature range after 0.044 time units: x ∈ [79.

90, 80.7]

in the mode on and x ∈ [80.7, 81.6] in the mode on F 2 . Hence, at any future time, the observations are different. By incorporating the time constraint in the refined abstraction, we ensure that counterexamples that are spurious because of disjoint observations including the previous one cannot be generated again. For the sake of simplicity, we analyzed the two faults separately. One more sophisticated strategy is to analyze the next fault based on the refined abstraction obtained from the analysis of the precedent fault.

Table 5 .

 5 1. The tool takes the file [name].model and performs the abstraction procedure if no model parsing errors are detected. Tables 5.1 and 5.2 present the main classes and methods used in the tool. 1: Main Classes of the Abstraction Tool

	The input file contains the different components of a hybrid automaton model H:
	• A list of hybrid automaton modes
	• A list of ODE's relative to each mode

Table 5 .

 5

	2: Main Methods of the Abstraction Tool

Table 5 .

 5

	4: Applying refinement steps with computation time

Acknowledgements

Proposition 4.2 (Sojourn bounds). A sufficient but not necessary condition for the region p to have finite time bounds (t max finite, thus nonnegative real) is that ∃i 1 ≤ i ≤ n ∀x ∈ p ẋi = 0, where p is the closure of p.

If the condition in proposition 4.2 is verified over p for a dimension i then all trajectories should respect finite time bounds for staying in the region p. On the other hand, a trajectory making a finite number of orbital spins once inside p then exiting p does not satisfy this condition while having finite time bounds. One way to look for a finite time bound is to refine the partition with the objective that the regions become small enough for the condition to hold for each of them. If the derivatives along each axis take each a finite number of null values inside the partition, but never all at the same time, there is no problem with refining the partition to have each null derivative point alone in one region. In the other cases, a further discussion on critical points is presented in Appendix B.

Note that the t max computed by Algorithm 2 is only valid for those trajectories that from a B in (p) are guaranteed to exit by a B out (p). This happens because the flow-pipe is an over-approximation and some trajectories staying in p with t max = +∞ may exist. To deal with such trajectories, one can combine under and over-approximations to obtain faithful time bounds whether it is the maximum or minimum sojourn time.

Computing t min

As previously defined, t min corresponds to the minimum sojourn time in a state.

Consequently, if any inward and outward boundaries of the region p have an intersection then we associate a null value to t min . Thus, one can associate t min to a specific entry boundary B in instead of the whole region. A simple way to compute a lower bound of the time passed in p by all the trajectories, is to consider the minimal distance between B in and B out expressed as:

Consequently, ( ĥ, ĥ ) is a critical pair of T H P , which establishes thus a counterexample of diagnosability in T H P : C.E = ( ĥ, ĥ ). By contradiction, this proves the result.

Algorithm 3 illustrates the CEGAR scheme adaptation for hybrid automata diagnosability verification.

input : Hybrid Automaton := H; Considered Fault := F ; Precision := (integer, maximum number of refinements) precision output:

Twin plant based diagnosability checking

Diagnosability checking of a discrete event system, modeled as an automaton, based on the twin plant method [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete-event systems[END_REF][START_REF] Yoo | Polynomial-time verification of diagnosability of partially observed discrete-event systems[END_REF] is polynomial in the number of states (actually it has been proved it is NLOGSPACE-complete [START_REF] Rintanen | Diagnosers and diagnosability of succinct transition systems[END_REF]). The idea is to construct a non-deterministic automaton, called pre-diagnoser or verifier, that preserves only all observable information and appends to every state the knowledge about past fault occurrence. The twin plant is then obtained by synchronizing the pre-diagnoser with itself based on observable events to get as paths in the twin plant all pairs of executions with the same observations in the original system. Each state of the twin plant is a pair of pre-diagnoser states that provide two by α t P (according to Theorem 4.2) are ĥ, ĥ , and which form a critical pair. This concrete pair is a witness of non-diagnosability of the hybrid automaton H.

In practice, validating the counterexample involves computing reachable sets of states. As we have seen, computing the exact set is not possible, one uses computations of safe over-approximations instead, such as using ellipsoids and zonotopes for complex dynamics or hyper-cubes for simpler ones [START_REF] Althoff | Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes[END_REF][START_REF] Botchkarev | Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations[END_REF]. Two flowpipes are computed with pre-defined time horizons T and T such that T = time( ĥ) and T = time( ĥ ). The flow-pipes trace what is dictated by the counterexample.

Suppose that ĥ is the fault carrying execution of the counterexample, then the verification of ∆-diagnosability will translate by the flow-pipe tracing ĥ to be of duration at least ∆ in the faulty mode.

If the counterexample is not validated, the abstract counterexample C.E is said spurious and becomes refuted.

Refuted counterexample: In case of spurious C.E = ( ĥ, ĥ ), the idea is

, that abstract by α t P into finite prefixes of ĥ, ĥ and such that Obs(h) = Obs(h ). The fact they cannot be

In this case, s reach |h|+1 and s reach |h |+1 are returned, that represent the two sets of reachable concrete states that are the first ones to disagree with the abstract C.E. We summarize below the reasons resulting in the C.E being spurious.

Spurious state reachability: There is no concrete execution in H whose abstraction is one of ĥ or ĥ , as one of the set of states of H whose abstraction is an abstract state ŝi or ŝ i is not reachable in H starting from the initial states of H. Note that care will have to be taken when refining T H P (see next subsection). E.g., a possible case is that there exists two executions (h, h ) reaching (s 1 , s 1 ) and then (s 2 , s 2 ) but not reaching (s 3 , s 3 ) (and none passing by (s 1 , s 1 ) and (s 2 , s 2 ) reaches (s 3 , s 3 )), and two other executions (u, u ) reaching (s 2 , s 2 ) from (s, s ) = (s 1 , s 1 ), with α t P (s) = α t P (s 1 ) and α t P (s ) = α t P (s 1 ), and then reaching (s 3 , s 3 ), all with time periods compatible to those of the abstract executions. If the refined model simply eliminated the transition from ŝ2 to ŝ3 or from ŝ 2 to ŝ 3 then it could no longer be considered an abstraction of H, since some concrete execution in H would have

Tool Architecture

The tool architecture is presented in Figure 5.1. Execution flow shows how the applied algorithms are sequenced. The required libraries for each step of the computation are also mentioned. First, a parsing operation is applied to a given input model satisfying the previously presented grammar. Second, the state partitioning algorithm is applied to discretize the state space into qualitative regions. Then transitions are evaluated from every qualitative region with its adjacent neighbors.

The obtained partitioning and transition evaluation results are then saved graphically as a finite state machine graph. At this point of the execution, the user can choose or not to compute the maximum and minimum first order derivatives of Ẋ in each partitioned region. The latter can in some situations be used to deduce the minimum and maximum sojourn times combined with the crossing distances of each region.

The following freely available libraries and solvers are required by the tool:

• QepCAD a Quantifier Elimination applying Cylindrical Algebraic Decomposition solver;

• Nlopt a non linear optimization library;

• Boost libraries for parsing inputs and generating outputs using regular expressions;

• Graphviz and Matplotlib for plotting and visualization.

Input: Hybrid

Chapter Summary

In this chapter we presented a tool that automatically performs the qualitative simulation of a given non-linear polynomial hybrid automaton given as input. The performed operations can be summarized in two steps: first the computation of the partitions relative to each mode of the hybrid automaton, second the computation of the transitions between each region of the obtained partition. The tool was tested over several examples to evaluate performances.

decomposition. The proposed abstraction method hence differs from the one proposed by Grastien. In [START_REF] Grastien | Solving diagnosability of hybrid systems via abstraction and discrete event techniques[END_REF], the abstraction consists in retaining some properties of the continuous dynamics, namely mode distinguishability and ephemerality, which are directly checked on the concrete hybrid system when necessary. On the contrary, in our approach the abstractions refer directly to the continuous state space and the continuous dynamics are interpreted with increasing levels of granularity, which results in finer and finer state space decompositions to which time constraints are associated. These abstractions take the form of timed automata.

Works of M. Beneditto [START_REF] Di Benedetto | Verification of hybrid automata diagnosability by abstraction[END_REF] Beneditto proposes a timed abstraction to verify diagnosability. The abstraction used is a durational graph, that measures the elapsed time of a trajectory from an initial set until a mode change condition is hit. In our method, the abstraction we use is one that first can be refined, and second is computed qualitatively over partitioned regions. The diagnosability verification is proven via the absence of critical pairs.

Perspectives

Our thesis work draws many perspectives. The first direct perspective is to elaborate automated rules to implement the refinement strategies by analysis of a diagnosability counterexample given the reasons we previously explained.

Diagnosability specific perspectives

• We wish to extend the diagnosability verification algorithm by attributing an -precision, for arbitrary small constant (for a given metrics to be defined), for hybrid automata, guaranteeing the refinement loop termination when the defined precision is achieved. In fact, up to now, we assume a continuous domain for both the values and the time stamps of the observable variables without taking into account sensors precision, i.e., the minimal intervals (of value and of time) that can be captured. This is the reason why our current algorithm may not terminate, due to an infinite refinement process. A fundamental and essential future work perspective is to provide a general algorithm for diagnosability verification with -precision [START_REF] Kim | Computing bounded epsilon-reach set with finite precision computations for a class of linear hybrid automata[END_REF], for arbitrary

Appendix A Tool Grammar and Models

A.1 Tool Grammar

A.2.8 Bouncing Ball

Mode q 0 : ẋ0 = x 1 ẋ1 = -10

Inv(q 0 ) = {x 0 > 0} Transitions: From q 0 to q 0 guarded by G : x 0 < 0.

A.2.9 Combined Brusselator

Mode q 0 : ẋ0

Transitions: From q 0 to q 1 guarded by G :

Transitions: From q 1 to q 0 guarded by G : x 0 < x 1 .

Appendix B Discussion on critical points

Finite number of critical points The derivatives along each coordinate are all null at the same time in a finite number of points X eq of region p, we repartition p such that each new region p i has exactly one point of X eq on its boundary. In one dimension, suppose the null derivative point is at x eq and the initial value of x(t) is x 0 . The time, which we denote by T , taken by the continuous variable x(t) to cross from x 0 to x eq can in some cases be finite. If ẋ is of the form x k where k ∈ R, then by studying T in a neighborhood around k = 1 we obtain: T is convergent if k < 1. Thus a time bound can be computed for all dynamics of the form ẋ = x k with k < 1, for example for the square root ẋ = √ x. In two dimensions, let r be the distance from the equilibrium point M eq (x eq , y eq ) to a point M (x, y) which is initially in region p. Let X = x eq -x and Y = y eq -y.

Since r 2 = X 2 + Y 2 then 2r ṙ = 2X Ẋ + 2Y Ẏ and if ṙ = 0 the time to reach M eq is :

Example B.1. Consider the two dimensional continuous system ẋ = -x 2 and ẏ = -y where (x, y) ∈ R + × R + . The equilibrium point is M eq (0, 0). In polar coordinates x = rcos(θ) and y = rsin(θ), then r ṙ = x ẋ + y ẏ = -x 3 -y 2 = -x 2 -y 2 + x 2 -x 3 = -r 2 + x 2 (1 -x) = r 2 (-1 + cos 2 (θ)(1 -rcos(θ))). In a