Abstractions Refinement for Hybrid Systems Diagnosability Analysis

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 such as state reachability, diagnosability, and predictability or on-line such as fault detection and isolation, is a challenging task. Actually, computing the reachable set of states of a hybrid system is an undecidable matter due to the infinite state space of continuous systems. 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. In this chapter, we are concerned with abstractions oriented towards hybrid systems diagnosability checking. Our goal is to create discrete abstractions in order to verify, at design stage, if a fault that would occur at runtime could be unambiguously detected in finite time (or within a given finite time bound for bounded diagnosability) 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 non-diagnosability. 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, guided by the elimination of the counterexample, and continue the process of looking for another counterexample until either a final result is obtained or we reach an inconclusive verdict. We make use of qualitative modeling and reasoning to compute discrete abstractions and we define several refinement strategies. Abstractions as timed automata are particularly studied as they allow one to handle time constraints that can be captured at a qualitative level from the hybrid system.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

11.1 Introduction

The increasing complexity of systems makes it challenging to detect and isolate faults. Hybrid systems are no exception, combining both discrete and continuous behaviors. Verifying behavioral or safety properties of such systems, either at design stage such as state reachability, diagnosability, and predictability or on-line such as fault detection and isolation is a challenging task. Actually, computing the reachable set of states of a hybrid system is an undecidable matter due to the infinite state space of continuous systems. 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. Methods have been proposed for diagnosability verification for continuous and discrete systems separately, few of them handle hybrid automata [21, 35, 62]. Diagnosability is a property describing the system ability to determine whether a fault has effectively occurred based on the observations, which has received considerable attention in the literature [16, 32, 48, 52, 53, 60]. However, most of the existing works are applied on discrete event systems.

In this chapter, we are concerned with abstractions oriented towards hybrid systems diagnosability checking. Our goal is to create discrete abstractions in order to verify, at design stage, if a fault that would occur at runtime 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, we show how to refine the abstraction, guided by the elimination of the counterexample, and continue the process of looking for another counterexample until either a final result is obtained or we reach an inconclusive verdict. We make use of qualitative modeling and reasoning to compute discrete abstractions and we define several refinement strategies. Abstractions as timed automata are particularly studied as they allow one to capture qualitative temporal constraints [10, 13]. The chapter is organized as follows. We first present the hybrid automata formalism and define diagnosability for hybrid systems. We then introduce a formal framework for constructing hybrid automata abstractions while defining the refinement relation. Lastly, we detail the counterexample guided abstraction refinement (CEGAR) scheme adapted for diagnosability verification and a case study example illustrating this scheme.

11.2 Hybrid Dynamical Systems

In this section, we start with a brief general description of hybrid systems and then move on to propose a formal representation framework for hybrid automata that is adopted throughout the chapter. Later on, we provide an example of a practical system modeled as a hybrid automaton. Lastly, we introduce various classes of hybrid automata, among which timed automata are our primary interest.

11.2.1 Hybrid Automata Definition

Hybrid systems are dynamical systems that include discrete and continuous behaviors [38]. Hybrid automaton (HA) is a mean to model such systems; it is an infinite state machine frequently used for this purpose among the scientific community. 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 $\mathbb {R}^n$.

Definition 1 (Hybrid Automaton (HA))

An n-dimensional hybrid automaton (HA) is a tuple H = (Q, X, S ₀, Σ, 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 continuously differentiable functions of time), whose valuations set $\mathbf {X} \subseteq \mathbb {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 ₀ ⊆ S is the set of initial states. If unique, the initial state is noted (q ₀, x ₀).

• Σ is a finite set of events.

• $F: S \rightarrow 2^{\mathbb {R}^n}$ is a mapping assigning to each state (q, x) ∈ S a set $F(q,\mathbf {x}) \subseteq \mathbb {R}^n$ constraining the time derivative $\dot {\mathbf {x}}$ of the continuous part of the mode q by $\dot {\mathbf {x}} \in F(q,\mathbf {x})$. If there is no uncertainty on the derivative, then F is a function $S \rightarrow \mathbb {R}^n$ specifying the flow condition $\dot {\mathbf {x}} = F(q,\mathbf {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 value of the continuous part of the state while the discrete part is q. We require, for all q ∈ Q, that {x∣(q, x) ∈ S ₀}⊆ 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. Hybrid systems are typically represented as finite automata with (discrete, i.e., modes) states Q, initial states Q ₀ = {q ∈ Q∣∃x ∈ Inv(q) (q, x) ∈ S ₀} and transitions δ defined by δ = {(q, σ, q ^′) ∈ Q × Σ × Q∣∃x, x ^′ (q, x, σ, q ^′, x ^′) ∈ T}. To each state q ∈ Q ₀ is associated an initial (continuous) nonempty set Init(q) = {x ∈ Inv(q)∣(q, x) ∈ S ₀}. 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(\tau ): G(\tau ) \rightarrow 2^{Inv{(q^\prime )}}$ 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 ₀, Σ, F, δ, Inv, G, R) and we have: ∀(q, x), (q ^′, x ^′) ∈ S, ∀σ ∈ Σ, ((q, x, σ, q ^′, x ^′) ∈ T ⇔ τ = (q, σ, q ^′) ∈ δ ∧x ∈ G(τ) ∧x ^′∈ R(τ)(x)).

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 ₀), F(q) and Inv(q) indicate then predicates whose free variables are respectively from X, $X \times \dot {X}$ and X and Init(q)(x), $F(q)(\mathbf {x},\dot {\mathbf {x}})$ and Inv(q)(x) being true means respectively x ∈ Init(q), $\dot {\mathbf {x}} \in F(q,\mathbf {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.

Guards in any mode q will be assumed non-intersecting: ∀q ∈ Q, ∀τ ₁ = (q, σ ₁, q ₁) ∈ δ, ∀τ ₂ = (q, σ ₂, q ₂) ∈ δ, (τ ₁ ≠ τ ₂ ⇒ G(τ ₁) ∩G(τ ₂) = ∅). Thus, at any moment of its continuous evolution in a mode q, the system may jump to at most one another 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 non-deterministic.

11.2.2 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 a hybrid automaton is used for modeling a system.

Example 1

A simple thermostat system maintains the temperature of an object quasi-constant by turning on and off a heater device. In practice such system contains at least, a temperature sensor, a heater device and logic control electronic circuits. The circuitry decides, given the actual measured temperature of the object, to activate or not the heater. A hybrid automaton H = (Q, X, S ₀, Σ, F, δ, Inv, G, R) models the behavior of such system (see graphical representation on Fig. 11.1):

• Q = {on, off}, X = {x}, S ₀ = (off, [80, 90])

• Σ = {B _on , B _off }, $F(on) = \{\dot {x} = -x+100\}$, $F(off) = \{\dot {x}= -x \}$

• δ = {τ ₁ = (off, B _on , on), τ ₂ = (on, B _off , off)}, Inv(off) = x ≥ 68, Inv(on) = x ≤ 82

• G(τ ₁) = x ≤ 70, G(τ ₂) = x ≥ 80, R(τ ₁) = R(τ ₂) = (x = x ^′)

The assigned hybrid automaton H is one dimensional, where x represents the sensed temperature.

Fig. 11.1

One-dimensional hybrid automaton modeling a thermostat

11.2.3 Hybrid Automata Semantics

We denote by q ₀, q ₁, … the modes of Q, and by x ₁, x ₂, …, x _n the variables of X.

Definition 2 (Hybrid Automaton Semantics)

The semantics of a hybrid automaton H, denoted by [[H]], is the set of all executions, which are labeled sequences of states from S with labels in $L = \varSigma \cup \mathbb {R}_+$: $(q_0,\mathbf {x}_0 ) \xrightarrow {l_0} (q_1, \mathbf {x}_1) \ldots (q_i, \mathbf {x}_i) \xrightarrow {l_i} \ldots$ such that (q ₀, x ₀) ∈ S ₀ and, for any two successive states $(q_i, \mathbf {x}_i) \xrightarrow {l_i} (q_{i+1}, \mathbf {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 \in \mathbb {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 $\forall t \in (0, d_i) \dot {x}(t) \in 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 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) \xrightarrow {0.15} (off,69) \xrightarrow {B_{on}} (on,69) \xrightarrow {0.5} (on,81) \xrightarrow {B_{off}}(off,81)\ldots$ is valid for the thermostat example (Fig. 11.1), thus h ∈ [[H]]. The trace of an execution h, i.e., 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) \in \mathbb {R}_+ \cup \{+\infty \}$, which is calculated as the sum of all time periods in the trace of h: $time(h)=\sum d_i$.

Let $\overline {S} = \bigcup _{q \in Q} (\{q\} \times Inv(q)) \subseteq S$ the (infinite) set of invariant satisfying states of H, $\overline {S}_0 = \bigcup _{q \in Q_0} (\{q\} \times Inv(q)) \subseteq S_0$ the subset of invariant satisfying initial states and $\rightarrow \subseteq \overline {S} \times L \times \overline {S}$ the transition relation defined by one or the other condition in Definition 2. The semantics of H is actually given by the labeled transition system $S_H^t={(\overline {S},\overline {S}_0,L,\rightarrow )}$, i.e., [[H]] is the set of all paths of $S_H^t$ issued from an initial state. $S_H^t$, 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 abstraction of $S_H^t$, called the timeless transition system of H, is obtained by ignoring also the duration of flows and thus defined as $S_H=(\overline {S},\overline {S}_0,\varSigma \cup \{\epsilon \},\rightarrow )$, obtained from $S_H^t$ by replacing any timed transition $(q_i, \mathbf {x}_i) \xrightarrow {d_i} (q_{i+1}, \mathbf {x}_{i+1})$ with $d_i \in \mathbb {R}_+$ by the ε transition $(q_i, \mathbf {x}_i) \xrightarrow {\epsilon } (q_{i+1}, \mathbf {x}_{i+1})$, that can be considered as a silent transition. It has infinite set of states but finite set of transition labels. It constitutes the finest timeless abstraction of H we will consider.

Theorem 1 (Correction and Completeness of the Semantics)

Any concrete behavior of H is timed (resp. timeless) abstracted into an $\overline {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 F is a singleton function (i.e., deterministic derivative), any $\overline {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.

11.2.4 Hybrid Automata Classes and Particular Cases

Definition 3 (Discrete Automaton (DA))

It is the case where there is no continuous part. Thus, a (finite) discrete automaton (DA) is a tuple D = (Q, Q ₀, Σ, δ) where Q is a finite set of discrete states (modes), Q ₀ ⊆ Q is the set of initial states, Σ is a finite set of events, and δ ⊆ Q × Σ × Q is a set of transitions of the form τ = (q, σ, q′).

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. The trace of such a path is the word in Σ ^⋆ whose letters are the successive labels of the path.

Definition 4 (Continuous System (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 ₀, F, Inv) with S ₀ ⊆ 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 of a hybrid automaton, constrained by the dynamics F and the invariant set Inv.

The form of the dynamics F determines primarily the class of the hybrid automaton. The rectangular class, for which the dynamics valuations are a cartesian product of intervals, lies on the boundary of the decidability over reachability problem with some restrictions [39]. We will present some classes of hybrid automata starting from the particular to the more general classes.

Timed Automata

We are particularly interested in timed automata, a class of hybrid automata where the continuous variables x _i , 1 ≤ i ≤ n, with values in $\mathbb {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 \in \mathbb {R}_+$ (at the theoretical level because, in practice, $\mathbb {Q}$ is used instead of $\mathbb {R}$ for computer implementation reasons) and op is one of the operators <, ≤, =, ≥, > , or a finite conjunction of primitive constraints. The satisfiability set of a constraint is thus a rectangle in $\mathbb {R}_+^n$, i.e., the product of n intervals of the half real line $\mathbb {R}_+$, and we will identify C(X) to the set of rectangles.

Definition 5 (Timed Automaton (TA))

A timed automaton (TA) is a hybrid automaton T = (Q, X, S ₀, Σ, F, δ, Inv, G, R) such that:

• $\mathbf {X} = \mathbb {R}_+^n$.

• S ₀ = Q ₀ ×{0}.

• ∀q ∈ Q F(q, .) = 1, which means that the dynamics of clocks evolution in each mode q is given by $\dot {x}_i = 1$.

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

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

• ∀τ ∈ δ∃Y (τ) ⊆ X∀x ∈ G(τ)R(τ)(x) = {x ^′} with $\mathbf {x}^\prime _i = 0$ if x _i  ∈ Y (τ) and $\mathbf {x}^\prime _i = \mathbf {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 ₀, Σ, Inv, (δ, G, Y )). The semantics of T as a hybrid automaton, given by Definition 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,\mathbf {x}_0 ) \xrightarrow {d_1} (q_0, \mathbf {x}_0+d_1) \xrightarrow {\sigma _1} (q_1, \mathbf {x}_1) \xrightarrow {d_2} \ldots$ whose trace trace(h) is the timed word $d_1 \sigma _1 d_2 \ldots \in \mathbb {R}_+(\varSigma \mathbb {R}_+)^*$ and duration is $time(h)=\sum d_i$.

The class of timed automata is particularly interesting as the reachability and language emptiness problems are decidable for that class [2]. Actually, decidability still holds for the larger class of rectangular automata (RA), where the unique flow condition F(., .), the same for all modes, is given by a rectangle in $\mathbb {R}^n$ (instead of the singleton 1), Init(q) is a bounded rectangle and $R(\tau )(\mathbf {x}) = \{\mathbf {x}^\prime \mid \mathbf {x}^\prime _i \in I_i$ if x _i  ∈ Y and $\mathbf {x}^\prime _i = \mathbf {x}_i$ else}, where the I _i ’s are bounded intervals depending only on τ [38]. And thus holds for the subclass of singular automata, where the flow rectangle is reduced to a singleton, whose timed automata are a particular case.

But decidability does not hold any more if the flow condition is allowed to change from one mode to another one. The simplest example of this is the generalization of timed automata where we allow the presence of stopwatches. A stopwatch is a clock which can switch from active (turned on) to inactive (turned off), or vice versa, when transiting between two modes. The generalized flow condition is thus given by: ∀q ∈ Q ∃c ∈{0, 1}ⁿ F(q, .) = c, which means that the dynamics of clocks evolution in each mode q is given by $\dot {x}_i = 1$ for those clocks active in q and $\dot {x}_i = 0$ for those clocks inactive in q. Thus, during inactivity, a stopwatch holds its last valuation when it was active (or 0 in case of reset). It happens that reachability decidability does not hold for a generalized timed automaton if only one clock is allowed to be a stopwatch, i.e., when the flow conditions are not independent of the mode (and thus also for the more general classes of multisingular automata, where the flow singletons depend on the mode, and of the multirectangular automata, where the flow rectangles depend on the mode). 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 multi-rectangular 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. Another case where decidability is lost in general for a hybrid system (but not for a timed automaton, for which it does not change the expressivity) is when the set C(X) of constraints is extended to contain primitive constraints of the form (x _i  − x _j ) op c _ij , i.e., if variables are not pairwise independent (and thus also for the class of triangular automata which generalize rectangular automata by adding such constraints). Linear automata generalize both multirectangular and triangular automata by allowing sets F(q), Init(q), Inv(q), G(τ) to be any convex polyhedra in $\mathbb {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.

11.3 Diagnosability of Hybrid Dynamical Systems

We will now introduce the model of hybrid systems that is used for diagnosability analysis and remind some methods from the literature aimed at verifying this property.

11.3.1 Hybrid System Model for Diagnosability Analysis

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 system ability to determine without ambiguity whether a fault of a given type has effectively occurred based on the observations. Diagnosability analysis has already received considerable attention in the literature over latest decades. However, most of the existing works refer to discrete event systems [16, 32, 34, 48, 52, 53, 60] with stochastic and fuzzy variants [41, 44, 54] or continuous systems [5, 15, 47, 57]. Diagnosability was also studied in the framework of decentralized and distributed architectures [46, 49, 50, 59].

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.

As a first step, Travé-Massuyès et al. [56] proved that the existing definitions of diagnosability for discrete event systems and for continuous systems can be stated as a property of the system fault signatures, and a unified definition of diagnosability was established. However hybrid system diagnosability was not considered.

Among the contributions concerned with hybrid diagnosability, we can mention [11] that slightly modified the classical necessary and sufficient condition for diagnosability of a discrete event system of [52] and expressed it in terms of reachability. Reference [29] 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 [19], diagnosability is expressed in terms of mode discernability (also called distinguishability by other authors) and is only based on the continuous dynamics.

Reference [8] 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 [33] for every mode, Bayoudh et al. [8] introduced the concept of mode signature which refines the classical concept of fault signature. Mode signatures determine mode distinguishability. The key idea of [8] 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 [8] later consolidated in [6] can be compared to the approach proposed in [22, 23] which uses fault signatures to capture the continuous dynamics. The fault signatures of [22, 23] 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 [6, 8] 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 [27]. Its originality relies in that it proposes a way to integrate these methods with equally standard methods of the DES diagnosis field [63]. Bayoudh et al. [6, 8] adopt the diagnoser approach [52] because it has the advantage to also support straightforwardly online diagnosis. Diene et al. [25] 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 [26] as a first piece of work in this direction. Later, Grastien et al. [35] 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, Grastien et al. [35] 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 [35] and also [24], 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.

This is why this chapter reviews different ways of abstracting hybrid automata in the next section, then elaborates from the diagnosability procedure proposed in [35] that uses the counterexample guided abstraction refinement (CEGAR) as initially introduced in [3, 28]. The algorithmic basis refers to CEGAR considering that the verification problem for even very simple hybrid systems is undecidable [39]. The method abstracts the hybrid automaton and then refines the abstraction while being guided by a diagnosability counterexample found at this abstract level. A first discrete abstraction of the hybrid system is computed, diagnosability is then verified using classical discrete methods. The verification could either yield the abstraction as diagnosable, which infers the diagnosability property back to the hybrid system, or non-diagnosable with a generated counterexample that validates this decision. The produced counterexample is either present in the original system in which case the hybrid system is not diagnosable, or it is a spurious effect of the abstraction. In the latter case, the counterexample is analyzed and the current abstraction is refined according to this analysis and the diagnosability verification task is iterated.

11.3.2 Observations and Faults

Remind that diagnosability is a system property allowing one to determine with certainty, at the design stage, a fault occurrence, based on 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 our thermostat system in Fig. 11.1, transitions B _on , B _off and temperature x are assumed to be observable. For what concerns faults, we will suppose that they are modeled, as for discrete event systems, by some unobservable discrete jumps, 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.

Definition 6 (Partially Observable Hybrid Automaton (POHA))

A partially observable hybrid automaton (POHA) is a hybrid automaton H according to Definition 1 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 7 (Execution (Timed) Observation)

Given an execution h ∈ [[H]] of a POHA H, $h=(q_0,\mathbf {x}_0 ) \xrightarrow {l_0} (q_1, \mathbf {x}_1) \ldots (q_i, \mathbf {x}_i) \xrightarrow {l_i} \ldots$, with $l_i \in \varSigma \cup \mathbb {R}_+$, the (timed) observation of h is defined as $Obs(h)=\mathbf {x}_0^o, l_0^o, \mathbf {x}_1^o \ldots \mathbf {x}_i^o, l_i^o, \ldots$, where:

• $\mathbf {x}_i^o$ is obtained by projecting x _i on variables in X _o .

• $l_i^o=l_i$ if $l_i\in \varSigma _o\cup \mathbb {R}_+$. Otherwise, $l_i^o=\varepsilon$, 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 $\mathbf {x}_i^o$. 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 $S^t_H$. Defining its observation at the level of its timeless transition system S _H is similar, with l _i  ∈ Σ ∪{ε} and $l_i^o=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 $\mathbf {x}_i^o$ of observable variables at each transition step as an ordered sequence without any occurrence time attached.

11.3.3 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. 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. However, this framework can be extended in a straightforward way such that a number of different faults can be considered simultaneously. Now we adapt to hybrid systems the diagnosability definition [52] 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,\mathbf {x}_0 ) \xrightarrow {l_0} (q_1, \mathbf {x}_1) \ldots (q_i, \mathbf {x}_i)$, the set of post-executions of h in [[H]] is defined as $[[H]]/h=\{h^\prime =(q_i, \mathbf {x}_i)\xrightarrow {l_i}\ldots \mid h.h^\prime \in [[H]]\}$, where h.h ^′ is obtained by merging the final state of h and the first state of h ^′, both should be the same.

Definition 8 ((Δ-)Faulty Executions)

Given a hybrid automaton H and F a fault event, a faulty execution is an execution h ∈ [[H]] such that F ∈ trace(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) fault F in h by time(h, F) = time(h ^′). Given a positive real number $\triangle \in \mathbb {R}^*_+$, we say that at least Δ time units pass after the first occurrence of F in h, or, in short, that h is Δ-faulty, if time(h, F) ≥ Δ.

Definition 9 (Hybrid Automaton (Time Bounded and Unbounded) Diagnosability)

Given $\triangle \in \mathbb {R}^*_+$, a fault F is said △-diagnosable in a POHA H iff (we abbreviate F ∈ trace(h) by F ∈ h)

$$\displaystyle \begin{aligned} \begin{array}{rcl} &\displaystyle &\displaystyle \forall h\in [[H]] (h \varDelta\text{-faulty}\ \\ &\displaystyle &\displaystyle \quad \Rightarrow \forall h^\prime\in [[H]] (Obs(h^\prime)=Obs(h)\Rightarrow F\in h^\prime)). \end{array} \end{aligned} $$

i.e.,

$$\displaystyle \begin{aligned} \begin{array}{rcl} &\displaystyle &\displaystyle \forall h^F\in [[H]] \forall h\in [[H]]/h^F (time(h)\ge \triangle\\ &\displaystyle &\displaystyle \quad \Rightarrow \forall h^\prime\in [[H]] (Obs(h^\prime)=Obs(h^F.h)\Rightarrow F\in h^\prime)). \end{array} \end{aligned} $$

A fault F is said diagnosable in H iff

$$\displaystyle \begin{aligned} \exists \triangle\in \mathbb{R}^*_+ (F \triangle{-}{\mathrm{diagnosable}}\ {\mathrm{in}}\ H). \end{aligned} $$

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 10 (△-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) ≥△.

Theorem 2

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).

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 [7, 9, 20, 21, 35]. 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 [58] that for timed automata the existence of arbitrarily long time after F faulty executions implies the existence of a + ∞-faulty execution (extending the definition above to △ = +∞) and thus that non-diagnosability is witnessed by the existence of a + ∞-critical pair and its checking is PSPACE-complete.

Theorem 3

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

We will rest on this result as diagnosability checking of a POHA H will be done on a time automaton T abstracting H.

11.4 Abstracting Hybrid Automata

For continuous systems, verifying the most basic properties such as “Is this state reachable?” is not decidable, due in particular to the uncountability of continuous domains [37]. A fortiori, for a hybrid system, a simple computation of the reachable set of states starting from an initial state is not a decidable matter except for few unpractical classes [39]. This is why a common practice is to partition infinite domains into a finite number of subsets, abstracting the system behavior in each of those subsets. The abstraction of the domain into representative sets is usable in computations to possibly reason about the infinite domain. In this section, we thus focus on abstractions that discretize the infinite state space defined by continuous variables into finite sets. We show the targeted class of properties we wish to verify. As our study considers abstractions of complex hybrid dynamical systems for diagnosability analysis, it is therefore crucial to first introduce abstractions for continuous dynamical systems which are a particular case of hybrid dynamical systems. Utilizing these abstractions, we aim at verifying temporal properties and bounding the time for fault detection and isolation. Abstractions retain less but important information regarding a property that we wish to verify about a complex system. Due to the uncountability of the continuous state space domain, verifying simple properties of continuous and more generally hybrid systems via abstraction becomes challenging. 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 of the hybrid system itself. Here, we are interested in hybrid systems abstraction aimed towards diagnosability checking. Abstractions that can be refined if necessary are of our concern, as refinement allows adding more information into the abstracted system while being always guided by the property to check. In this section, we will discuss abstractions in general and focus on those that capture time constraints in particular.

11.4.1 Different Abstraction Strategies

Using Qualitative Principles

We first take a look at abstractions using qualitative concepts. Given a set of ODEs, these concepts classically discretize the infinite state space of the continuous variables into finite sets. The discretization of $\mathbb {R}^n$ is often achieved by rectangles, i.e., is built by product from a discretization of $\mathbb {R}$. And this one is obtained by fixing a finite number of (rational) 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 $\mathbb {R}$ itself) is obtained from the single landmark 0 and corresponds to the sign partition: (−∞, 0), [0], (0, +∞), giving rise to a partition of size 3ⁿ of $\mathbb {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, it is possible to draw a rough scheme of the behavior of the variables called “qualitative simulation” in the literature and to obtain a loose overview about how the system will behave [30, 43, 55].

Example 2

Consider this simple linear continuous system:

$$\displaystyle \begin{aligned} \begin{aligned} {} \dot{x} &= 3x \\ \dot{y} &= y-1 \end{aligned}\end{aligned} $$

(11.1)

Adopting the partition of the state space given by the signs of the derivatives, the abstract state space of size 9 is thus: $(\dot {x}>0 \vee \dot {x}<0 \vee \dot {x} =0) \wedge (\dot {y}>0 \vee \dot {y} <0 \vee \dot {y} = 0 )$. The transitions between the abstract states are computed according to the laws of evolution given the signs of the derivatives. The abstract state $(\dot {x} > 0 \wedge \dot {y} >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 sound: from any initial state (x ₀, y ₀) the solutions of the differential equation system (11.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 partitions the state space into sets with a constant sign of the derivative. This 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. Nonetheless, for proving a more complex property that involves the notion of time, classically expressed using temporal logic, 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.

Example 3

We consider the same continuous system and suppose the initial set of states I such that I = {(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. Fp, where p is a Boolean proposition, is equivalent to $\exists t_0 \in \mathbb {R}^+, \forall 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 I 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 (11.1) by $\dot {x} = 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 $\dot {\mathbf {x}} = A\mathbf {x}+\mathbf {b}$ where x = (x, y)^T and A is the corresponding matrix. We then deduce by computing the eigenvalues of A 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 I.

The previous example illustrates the simple 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 [36].

11.4.2 Geometric Decomposition of the State Space

We now introduce 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, in the next section, we will discuss the refinement of the abstraction yielding constraints with better precision than before refinement.

Definition 11 (Continuous Space Partition)

A (finite) partition P of the Euclidean space $\mathbb {R}^n$ is a finite set of nonempty connected subsets of $\mathbb {R}^n$ such that every point $x \in \mathbb {R}^n$ is in one and only one of those subsets. We can write $\mathbb {R}^n = \biguplus _{ p\in 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 $\mathbb {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, $\forall x: [0,1] \rightarrow \mathbb {R}^n$ a continuous function, ∀p ∈ P a region, x ⁻¹(p) is a finite union of intervals. In practice, partitions are chosen enough regular and smooth, with regions in any dimension from 1 to n 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 ₁, p ₂, p ₃ defined by:

$$\displaystyle \begin{aligned} p_1 = \{\mathbf{x} \in \mathbf{X}| \dot{x}>0\}, p_2 = \{\mathbf{x}\in \mathbf{X}| \dot{x} <0\}, p_3 = \{\mathbf{x}\in \mathbf{X}|\dot{x}=0\} \end{aligned} $$

(11.2)

For n dimensional systems, the regions would be the connected components of the 3ⁿ subsets E _s of $\mathbb {R}^n$ parametrized by sign vectors s ∈{−1, 0, +1}ⁿ: $E_s = \{\mathbf {x} \in \mathbf {X} \mid \forall i, 1 \le i \le n, \dot {\mathbf {x}}^i<0\ \text{if } s^i = -1, \dot {\mathbf {x}}^i=0\ \text{if } s^i = 0, \dot {\mathbf {x}}^i>0\ \text{if } s^i = +1\}$.

Example 4 (The Brusselator)

We now illustrate some of the introduced concepts on a mathematical model used for representing chemical reactions: the brusselator whose dynamics is nonlinear. Consider a two-dimensional continuous system C = (X, S ₀, F, Inv) such that X = {x, y} are two continuously differentiable variables and F given by [4]:

$$\displaystyle \begin{aligned} \begin{aligned} &\dot{x} = 1 - (b + 1)x + ax^2y \\ &\dot{y} = bx - ax^2y {} \end{aligned} \end{aligned} $$

(11.3)

where $a, b\in \mathbb {R}$ are two real constants. The stationary point for which $\dot {x} = \dot {y} = 0$ is $M_0(1, \frac {b}{a})$. If b < a + 1, then M ₀ is an attractor and all trajectories converge towards M ₀; if b > a + 1 then it is a repeller and all trajectories close to M ₀ converge towards an orbit. We consider two cases where b = 1, a = 2 and b = 3, a = 1 illustrated respectively in Fig. 11.2a, b. To characterize the dynamic behavior qualitatively as in Eq. (11.2), consider a partition P yielding nine regions p ₁, …, p ₉ illustrated in the repeller case in Fig. 11.3 [30].

Fig. 11.2

Brusselator phase plane: (a) Attractor, (b) Repeller

Fig. 11.3

Qualitative partitioning of the state space

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 12 (Hybrid State Space Decomposition)

Given a hybrid automaton H = (Q, X, S ₀, Σ, F, δ, Inv, G, R) and a set $\mathfrak {P}$ of partitions of the valuations set of X, $\mathbf {X} \subseteq \mathbb {R}^n$, we say that $\mathfrak {P}$ decomposes H if there is an onto function $d: Q \rightarrow \mathfrak {P}$ which associates to each q ∈ Q a partition $d(q) \in \mathfrak {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 over-approximate them).

11.4.3 Encoding Hybrid Automata Reachability Constraints

We have defined in Sect. 11.2.3, 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.

Definition 13 (Adjacent Regions)

Two distinct regions p ₁, p ₂ of a partition P of $\mathbb {R}^n$ are adjacent if one intersects the boundary of the other: $p_1 \cap \overline {p_2} \neq \emptyset$ or $\overline {p_1} \cap p_2 \neq \emptyset$, where $\overline {p}$ refers to the closure of p.

Definition 14 (Decomposition-Based Timeless Abstract Automaton of a Hybrid Automaton)

Given a hybrid automaton H = (Q, X, S ₀, Σ, F, Inv, T) and a decomposition $(\mathfrak {P},d)$ of H, we define the timeless abstract (finite) automaton of H with respect to $\mathfrak {P}$ as $DH_{\mathfrak {P}} = (Q_{DH}, Q_{0_{DH}},\varSigma _{DH}, \delta _{DH})$ with:

• Q _DH  = {(q, p)|q ∈ Q, p ∈ d(q)}.

• $Q_{0_{DH}}= \{(q, p_{Init})| q \in Q_0, p_{Init} \in d_{Init}(q) \}$.

• Σ _DH  = Σ ∪{ε}.

• ((q _i , p _k ), σ, (q _j , p _l )) ∈ δ _DH iff one of both is true:

  • q _i  ≠ q _j and σ ∈ Σ and p _k  ∈ d _G (q _i , τ) and p _l  ∈ d _R (q _j , τ, p _k ) where τ = (q _i , σ, q _j ) and ∃t = (q _i , x, σ, x ^′, q _j ) ∈ T such that x ∈ p _k and x ^′∈ p _l .

  • q _i  = q _j and σ = ε and p _k , p _l  ∈ d _Inv (q _i ) are adjacent regions and $\exists d \in \mathbb {R}_+^*$ and ∃x : [0, d] →X continuously differentiable function such that $\forall t \in (0,d)\ \dot {x}(t) \in 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), \sigma , (q_j,p_l)) \in \delta _{DH} \Rightarrow \exists \mathbf {x}_k \in p_k\ \exists \mathbf {x}_l \in p_l\ (q_i, \mathbf {x}_k) \xrightarrow {\sigma } (q_j, \mathbf {x}_l)$ in S _H , the converse being true for σ ∈ Σ. The mapping $\alpha _{\mathfrak {P}}$ defined by $\alpha _{\mathfrak {P}}((q,\mathbf {x})) = (q,p)$ with p ∈ d(q) and x ∈ p defines an onto timeless abstraction function $\alpha _{\mathfrak {P}}: \overline {S} \rightarrow Q_{DH}$. If the flow condition F is a singleton, $\alpha _{\mathfrak {P}}$ maps any transition of S _H to a unique path in $DH_{\mathfrak {P}}$. The coarsest timeless abstract automaton is obtained when partitions of $\mathfrak {P}$ have all a unique region p = X and is thus (Q, Q ₀, Σ, δ), 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), (on, B _off , off)}) and the abstraction of the execution h given previously (11.2.3) is just $off \xrightarrow {B_{on}} on \xrightarrow {B_{off}} off\ldots$

Theorem 4 (Timeless Abstraction Completeness)

Given a decomposition $\mathfrak {P}$ of H, any concrete behavior of H is timeless abstracted into a $Q_{0_{DH}}$ rooted path in $DH_{\mathfrak {P}}$ and any transition of $DH_{\mathfrak {P}}$ abstracts a part of a concrete behavior of H. If the flow condition F is a singleton function then the timeless abstraction function $\alpha _{\mathfrak {P}}$ defines a trace preserving mapping (still denoted by $\alpha _{\mathfrak {P}}$ ) from $\overline {S}_0$ rooted paths in S _H (i.e., timeless executions of H) to $Q_{0_{DH}}$ rooted paths in $DH_{\mathfrak {P}}$ and thus the language defined by S _H is included in the language defined by $DH_{\mathfrak {P}}$.

Obviously, a path in $DH_{\mathfrak {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 behaviors.

If now H is a POHA, in the same way we defined the observation of a concrete execution in Definition 7 we define the observation of its timeless abstraction.

Definition 15 (Timeless Abstraction Observation)

Given a POHA H and $h=(q_0,p_0 ) \xrightarrow {\sigma _0} (q_1, p_1) \ldots (q_i, p_i) \xrightarrow {\sigma _i} \ldots$, with σ _i  ∈ Σ ∪{ε}, a timeless abstract path in $DH_{\mathfrak {P}}$, the observation of h is defined as $Obs(h)=p_0^o, \sigma _0^o, p_1^o \ldots p_i^o, \sigma _i^o, \ldots$, where

• $p_i^o$ is obtained by projecting p _i on variables in X _o .

• $\sigma _i^o=\sigma _i$ if σ _i  ∈ Σ _o . Otherwise, $\sigma _i^o=\varepsilon$, which is then removed from Obs(h).

Consider an execution h ∈ [[H]] of the POHA H, $h=(q_0,\mathbf {x}_0 ) \xrightarrow {l_0} (q_1, \mathbf {x}_1) \ldots (q_i, \mathbf {x}_i) \xrightarrow {l_i} \ldots$, with $l_i \in \varSigma \cup \mathbb {R}_+$, its (timed) observation $Obs(h)=\mathbf {x}_0^o, l_0^o, \mathbf {x}_1^o \ldots \mathbf {x}_i^o, l_i^o, \ldots$ as in Definition 7, its timeless abstraction $\alpha _{\mathfrak {P}}(h)=(q_0,p_0) \xrightarrow {\sigma _0} (q_1, p_1) \ldots (q_i, p_i) \xrightarrow {\sigma _i} \ldots$, with σ _i  ∈ Σ ∪{ε}, as in Theorem 4 (assuming F a singleton) and the observation of this last one $Obs(\alpha _{\mathfrak {P}}(h))=p_0^o, \sigma _0^o, p_1^o \ldots p_i^o, \sigma _i^o, \ldots$ as in Definition 15. We could try to define the timeless abstraction of the observation Obs(h). A natural definition would be $\alpha _{\mathfrak {P}}(Obs(h))=p_0^\prime , \sigma _0^o, p_1^\prime \ldots p_i^\prime , \sigma _i^o, \ldots$, with $\sigma _i^o=l_i^o$ if $l_i^o \in \varSigma _o$ (and = ε, which is removed, otherwise), i.e., the same $\sigma _i^o$’s as in $Obs(\alpha _{\mathfrak {P}}(h))$, and $p_i^\prime =\biguplus _{\{p|\mathbf {x}_i^o\in 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 $\mathbf {x}_i^o$ (assuming to simplify the same partition for each mode, as the mode may be unknown from observation). So, we notice that $Obs(\alpha _{\mathfrak {P}}(h))$ is more precise than $\alpha _{\mathfrak {P}}(Obs(h))$, as $p_i^o \subseteq p_i^\prime$, which we denote by $Obs(\alpha _{\mathfrak {P}}(h)) \sqsubseteq \alpha _{\mathfrak {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.

11.4.4 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 $\mathbb {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 16 (Region Time Interval and Time Bounds)

Given a continuous system CS, a partition P of $\mathbb {R}^n$ and p ∈ P one of its regions, we say that I _p  = [t _min , t _max ], with $t_{min}, t_{max} \in \mathbb {R}_+ \cup \{+\infty \}$, 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 17 (Decomposition-Based Timed Abstract Automaton of a Hybrid Automaton)

Given a hybrid automaton H = (Q, X, S ₀, Σ, F, δ, Inv, G, R), a decomposition $(\mathfrak {P},d)$ and the timeless abstract automaton $DH_{\mathfrak {P}} = (Q_{DH}, Q_{0_{DH}}, \varSigma _{DH}, \delta _{DH})$ of H with respect to $\mathfrak {P}$, we define the timed abstract automaton of H with respect to $\mathfrak {P}$ as $TH_{\mathfrak {P}} =(Q_{DH},\{c\}, Q_{0_{DH}}, \varSigma _{DH}, Inv_{TH}, (\delta _{DH}, G_{TH}, Y_{TH}))$ such that, ∀(q, p) ∈ Q _DH with a region time interval I _(q,p) = [t _min , t _max ]:

• Inv _TH ((q, p)) = [0, t _max ].

• ∀τ = ((q, p), σ, (q ₁, p ₁)) ∈ δ _DH , G _TH (τ) = [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, ∀τ ∈ δ _TH , Y _TH (τ) = {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 non-trivial (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, [80, 90]) and by (off, [68, 80)). Then we take as time bounds for (off, [80, 90]) 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(\frac {9}{8})$). It means that we define in the timed abstract automaton Inv _TH ((off, [80, 90])) = [0, 0.12]. A beginning of execution of the timed abstract automaton is, for example, $(off,[80,90]) \xrightarrow {0.08} (off,[68,80])$.

Theorem 5 (Timed Abstraction Completeness)

Given a decomposition $\mathfrak {P}$ of H, any concrete behavior of H is timed abstracted into an execution in $TH_{\mathfrak {P}}$ . If the flow condition F is a singleton function then the abstraction function $\alpha _{\mathfrak {P}}$ defines a mapping, denoted by $\alpha ^t_{\mathfrak {P}}$ , from $\overline {S}_0$ rooted paths in $S^t_H$ (i.e., executions of H) to executions in $TH_{\mathfrak {P}}$ . This mapping is trace preserving once ε labels are erased from executions traces in $TH_{\mathfrak {P}}$ and time period labels are added up between two consecutive events labels in both executions traces in $S^t_H$ and in $TH_{\mathfrak {P}}$ . This means that, for any execution , with w ∈ L ^∗ (where $L = \varSigma \cup \mathbb {R}_+$ ), it exists a unique execution $(q_0, p_0) {\xrightarrow {w^{\prime }}{ }_{\ast }} (q_j,p_j) \in {[}{[}TH_{\mathfrak {P}}{]}{]}$ , with w ^′∈ L ^′∗ (where L ^′ = L ∪{ε}), x ₀ ∈ p ₀ , q _j  = q _i , x _i  ∈ p _j , $w^{\prime }_{\scriptstyle {\vert \varSigma }} = w_{\scriptstyle {\vert \varSigma }}$ (where |Σ is the projection of timed words on words on Σ ^∗ ) and, for any two successive events $w_l = w^{\prime }_{l'}$ and $w_m = w^{\prime }_{m'}$ of w _|Σ , $\sum _{l'<k'<m',w^{\prime }_{k'} \neq \epsilon } w^{\prime }_{k'} = \sum _{l<k<m} w_k$.

Forgetting time, i.e., removing the clock, provides a natural abstraction function α from $TH_{\mathfrak {P}}$ to $DH_{\mathfrak {P}}$ which maps an execution $(q_0,p_0 ) \xrightarrow {l_0} (q_1, p_1) \ldots (q_i, p_i) \xrightarrow {l_i} \ldots$, with $l_i \in \varSigma \cup \{\epsilon \}\cup \mathbb {R}_+$, in $TH_{\mathfrak {P}}$ into the execution $(q_0,p_0 ) \xrightarrow {\sigma _0} (q_1, p_1) \ldots (q_i, p_i) \xrightarrow {\sigma _i} \ldots$, with σ _i  ∈ Σ ∪{ε}, in $DH_{\mathfrak {P}}$, with σ _i  = l _i if l _i  ∈ Σ ∪{ε} and continuous transitions labeled by $l_i = d_i \in \mathbb {R}_+$ are suppressed. We have: $\alpha _{\mathfrak {P}} = \alpha \circ \alpha ^t_{\mathfrak {P}}$.

Definition 18 (Timed Abstraction Observation)

Given a POHA H and $h=(q_0,p_0 ) \xrightarrow {l_0} (q_1, p_1) \ldots (q_i, p_i) \xrightarrow {l_i} \ldots$, with $l_i \in \varSigma \cup \{\epsilon \}\cup \mathbb {R}_+$, an execution in $TH_{\mathfrak {P}}$, i.e., a timed abstract path, the observation of h is defined as $Obs(h)=p_0^o, l_0^o, p_1^o \ldots p_i^o, l_i^o, \ldots$, where

• $p_i^o$ is obtained by projecting p _i on variables in X _o .

• $l_i^o=l_i$ if $l_i\in \varSigma _o\cup \mathbb {R}_+$. Otherwise, $l_i^o=\varepsilon$, 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(\alpha ^t_{\mathfrak {P}}(h)) \sqsubseteq \alpha ^t_{\mathfrak {P}}(Obs(h))$.

From another side, the abstraction function α that forgets time maps a timed abstract observation $p_0^o, l_0^o, p_1^o \ldots p_i^o, l_i^o, \ldots$, with $l_i^o\in \varSigma _o\cup \mathbb {R}_+$, into the timeless abstract observation $p_0^o, \sigma _0^o, p_1^o \ldots p_i^o, \sigma _i^o, \ldots$, with $\sigma _i^o\in \varSigma _o$, suppressing duration labels $l_i = d_i \in \mathbb {R}_+$. For any concrete execution h ∈ [[H]], we have: $Obs(\alpha _{\mathfrak {P}}(h)) = \alpha (Obs(\alpha ^t_{\mathfrak {P}}(h)))$, i.e., $Obs\circ \alpha _{\mathfrak {P}} = \alpha \circ Obs\circ \alpha ^t_{\mathfrak {P}}$.

11.4.5 Computing Time Bounds

In this subsection, we present and discuss some situations for which time bounds can be computed for the continuous evolution of the hybrid system. In the following, CS is a continuous system, and P is a partition of $\mathbb {R}^n$, p ∈ P and I _p  = [t _min , t _max ] the associated region time interval of p.

Proposition 1 (Sojourn Bounds)

A sufficient but not necessary condition for the region p to have finite time bounds (t _max finite, thus real nonnegative constant) is that $\exists i\ 1\leq i\leq n \quad \forall \mathbf {x} \in \overline {p} \quad \dot {\mathbf {x}_i} \neq 0$.

If the condition in Proposition 1 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. This idea will be developed in Sect. 11.5. 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, we present now some examples for which a time bound can be nevertheless obtained.

Finite Number of Equilibrium Points

The derivatives along each coordinate are null in a finite number of points X _eq at the same time, 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 ₀. The time, which we denote by $\mathcal {T}$, taken by the continuous variable x(t) to cross from x ₀ to x _eq can in some cases be finite. If $\dot {x}$ is of the form x ^k where $k\in \mathbb {R}$, then by studying $\mathcal {T}$ in a neighborhood around k = 1 we obtain:

$$\displaystyle \begin{aligned} \mathcal{T} = \int_{0}^{t_{eq}} \, \mathrm{d}t = \int_{x_0}^{x_{eq}} \frac{1}{\dot{x}} \, \mathrm{d}x = \int_{x_0}^{0} \frac{1}{x^k} \, \mathrm{d}x = \left[\frac{x^{-k+1}}{(-k+1)}\right]_{x_0}^{0} \end{aligned} $$

(11.4)

$\mathcal {T}$ is convergent if k < 1. Thus a time bound can be computed for all dynamics of the form $\dot {x} = x^k$ with k < 1, for example for the square root $\dot {x} = \sqrt {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 ² = X ² + Y ² then $2r\dot {r} = 2 X \dot {X} + 2 Y \dot {Y}$ and if $\dot {r} \neq 0$ the time to reach M _eq is :

$$\displaystyle \begin{aligned} \mathcal{T} = \int_{0}^{t_{eq}} \, \mathrm{d}t = \int_{r_0}^{0} \frac{1}{\dot{r}} \, \mathrm{d}r = \int_{r_0}^{0} \frac{r}{X\dot{X}+ Y\dot{Y}} \, \mathrm{d}r \end{aligned} $$

(11.5)

Example 5

Consider the two dimensional continuous system $\dot {x} = -x^2$ and $\dot {y} = -y$ where $(x,y) \in \mathbb {R}^+ \times \mathbb {R}^+$. The equilibrium point is M _eq (0, 0). In polar coordinates $x = r \cos {}(\theta )$ and $y = r \sin {}(\theta )$, then $r \dot {r} = x\dot {x} + y\dot {y} = -x^3 -y^2 = -x^2 -y^2 + x^2 -x^3 = -r^2 + x^2(1-x) = r^2(-1 + \cos ^2(\theta )(1 - r\cos {}(\theta )))$. In a neighborhood around (0, 0):

$$\displaystyle \begin{aligned} \mathcal{T} = \int_{r_0}^{0} \frac{1}{r(-1 + \cos^2(\theta)(1 - r\cos{}(\theta)))} \, \mathrm{d}r \geq \int_{r_0}^{0} \frac{-1}{r} \, \mathrm{d}r \end{aligned} $$

(11.6)

Thus $\mathcal {T}$ is infinite, the equilibrium point is never reached. This reasoning can be extended to dimension n by evaluating $r\dot {r}$ and using spherical (or hyperspherical) coordinates and to polynomial with real exponents. We can take an example of square root, for instance $\dot {x} = \sqrt {x}$ and demonstrate the time $\mathcal {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, Maler and Batt [45] showed how it is possible to capture time constraints by decomposing the infinite state space $\mathbb {R}^n$ into hypercubes and evaluate the time elapsed between entering and exiting each cube by bounding the dynamics.

Brusselator Time Bounds For our Example 4 of the brusselator dynamics, consider, for the repeller case with b = 3, a = 1, a ring set R that excludes M ₀ such that R = {(x, y)∣(−1 + x)² + (−3 + y)² > 0.09 ∧ (−1 + x)² + (−3 + y)² < 0.5625}. Let $v = \sqrt {\dot {x}^2 + \dot {y}^2}$ then v ² = (1 − 4x + x ² y)² + (3x − x ² y)² and, using a solver, we compute a lower bound $v^2_{low} = 0.0051$ of v ². It has been proven that all trajectories initially in $S_0 = \mathbb {R}^2 \setminus \{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 ₁ and R ₂ such that $R = R_1 \biguplus 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 ₀ will cross R ₁ and R ₂ sequentially infinitely often. In practice, the presence of the system in either R ₁ or R ₂ can correspond to two different visible colors of the chemical reaction.

11.5 Hybrid Automata Abstraction Refinement

We will now explain and formalize the refinement process 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 for the CEGAR scheme, it is a required step when a proof for the verification of a property could not be made at a given abstraction level.

Definition 19 (Partition Refinement)

Given two partitions P and P′ of $\mathbb {R}^n$, we say that P′ is a refining partition of P iff ∀p′∈ P′ ∃p ∈ P p′⊆ p. This implies: $\forall p \in P\ \exists P^{\prime }_{p} \subseteq P'\ p = \biguplus _{p' \in P^{\prime }_{p}} p'$.

Definition 20 (Hybrid State Space Decomposition Refinement)

Given two decompositions $(\mathfrak {P},d)$ and $(\mathfrak {P}',d')$ of a hybrid automaton H = (Q, X, S ₀, Σ, F, Inv, T), we say that $\mathfrak {P}'$ refines $\mathfrak {P}$, denoted by $\mathfrak {P}'\preceq \mathfrak {P}$, if ∀q ∈ Q d′(q) is a refining partition of d(q).

11.5.1 Refined Timeless Model

Definition 21 (Refined Timeless Abstract Automaton)

Given a hybrid automaton H and two abstract timeless automata $DH_{\mathfrak {P}}$ and $DH_{\mathfrak {P}^\prime }$ of H with respect to two decompositions $(\mathfrak {P},d)$ and $(\mathfrak {P}',d')$ respectively, we say that $DH_{\mathfrak {P}^\prime }$ is a timeless refinement of $DH_{\mathfrak {P}}$ abstracting H if $\mathfrak {P}'\prec \mathfrak {P}$, which we denote by $DH_{\mathfrak {P}^\prime }\prec DH_{\mathfrak {P}}$.

Definition 22 (State Split Operation)

Given an abstract timeless automaton $DH_{\mathfrak {P}}$ of a hybrid automaton H, a split operation of the state (q, p) ∈ Q _DH is defined by a partition {p ₁, p ₂} of p, $p= p_1 \biguplus p_2$, and results in two states (q, p ₁) and (q, p ₂) and in the refined abstract timeless automaton $DH_{\mathfrak {P}'}$ with $\mathfrak {P}'$ obtained from $\mathfrak {P}$ by replacing d(q) by d′(q) = d(q)∖{p}∪{p ₁, p ₂}.

The construction of $DH_{\mathfrak {P}'}$ from $DH_{\mathfrak {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 14, it is only required to recompute some of its transitions, while inheriting the rest from $DH_{\mathfrak {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_{\mathfrak {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 $\alpha _{\mathfrak {P}',\mathfrak {P}}: Q_{DH}^{\mathfrak {P}'} \rightarrow Q_{DH}^{\mathfrak {P}}$ defined by $\alpha _{\mathfrak {P}',\mathfrak {P}}((q,p')) = (q,p)$ with p′⊆ p defines a trace preserving mapping $\alpha _{\mathfrak {P}',\mathfrak {P}}$ from $DH_{\mathfrak {P}'}$ to $DH_{\mathfrak {P}}$ (and thus the language defined by $DH_{\mathfrak {P}'}$ is included in the language defined by $DH_{\mathfrak {P}}$) and we have: $\alpha _{\mathfrak {P}} = \alpha _{\mathfrak {P}',\mathfrak {P}} \circ \alpha _{\mathfrak {P}'}$. Defining in a natural way as previously the $\mathfrak {P}$-abstraction $\alpha _{\mathfrak {P}',\mathfrak {P}}$ of the observation of a timeless $\mathfrak {P}'$-abstract execution h, we obtain: $Obs(\alpha _{\mathfrak {P}',\mathfrak {P}}(h)) \sqsubseteq \alpha _{\mathfrak {P}',\mathfrak {P}}(Obs(h))$.

11.5.2 Refined Timed Model

Definition 23 (Refined Timed Abstract Automaton)

Given a hybrid automaton H and two abstract timed automata $TH_{\mathfrak {P}}$ and $TH_{\mathfrak {P'}}$ of H with respect to two decompositions $(\mathfrak {P},d)$ and $(\mathfrak {P'},d')$ respectively, we say that $TH_{\mathfrak {P'}}$ is a timed refinement of $TH_{\mathfrak {P}}$ abstracting H if $\mathfrak {P}'\prec \mathfrak {P}$. We denote it similarly by $TH_{\mathfrak {P'}}\prec TH_{\mathfrak {P}}$.

Concerning the refined abstract timed automaton $TH_{\mathfrak {P}'}$ resulting from a split of (q, p) into (q, p ₁) and (q, p ₂), 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 ₁ and p ₂. 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 ₁) and (q, p ₂). 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^{\prime }_{(q,p)}= [t^{\prime }_{min},t^{\prime }_{max}]$ with $t^{\prime }_{min}\ge t_{min}$ and $t^{\prime }_{max}\le t_{max}$, at least one of both being a strict inequality.

The onto abstraction function $\alpha _{\mathfrak {P}',\mathfrak {P}}$ defines a trace preserving mapping $\alpha ^t_{\mathfrak {P}',\mathfrak {P}}$ from $TH_{\mathfrak {P}'}$ to $TH_{\mathfrak {P}}$, after trace simplification as in Theorem 5 and provided the time bounds used in $TH_{\mathfrak {P}'}$, once added for all regions p′ included in a given region p, are at least as tight as the time bounds used in $TH_{\mathfrak {P}}$. And we have: $\alpha ^t_{\mathfrak {P}} = \alpha ^t_{\mathfrak {P}',\mathfrak {P}} \circ \alpha ^t_{\mathfrak {P}'}$. Finally, for any timed $\mathfrak {P}'$-abstract execution h, we obtain: $Obs(\alpha ^t_{\mathfrak {P}',\mathfrak {P}}(h)) \sqsubseteq \alpha ^t_{\mathfrak {P}',\mathfrak {P}}(Obs(h))$.

11.5.3 Refinement Guided by Reachability Analysis

We give here some general mathematical properties, in particular about conservation of the connectivity property of the regions when following the solution flow, that are useful for the refinement process when guided by the dynamics of the hybrid system and reachability conditions.

Reachability from a Connected Set

Let CS = (X, S ₀, F, Inv) be a continuous system with deterministic flow condition $F:\mathbf {X} \rightarrow \mathbb {R}^n$ and $\mathbf {K} \subset \mathbb {R}^n$ a set, such that the following hypotheses are verified:

• K is a connected and bounded closed (i.e., compact) set and ∀x ∈K, F(x) ≠ 0.

• The flow solution function x(t, x ₀) initially starting at t = 0 from x ₀ ∈K is continuous with respect to x ₀ ∈K and of class C ¹ with respect to the time t (this property is true in the case of polynomial dynamics).

With these hypotheses, trajectories issued from x ₀ are continuous with respect to x ₀ (proof can be made using the uniform continuity deduced from the continuity as K is a compact set).

Let y be a reachable element from K and x(t) the trajectory reaching y at time t ₀. We define the successor trajectory post(y) and the predecessor trajectory pre(y) by:

$$\displaystyle \begin{aligned} post(\mathbf{y}) = \{\mathbf{x}\in \mathbf{X} \mid \exists t > t_0 \mathbf{x} = x(t) \} pre(\mathbf{y}) = \{\mathbf{x}\in \mathbf{X} \mid \exists 0 < t < t_0 \mathbf{x} = x(t) \}\end{aligned} $$

(11.7)

We extend this definition to the set K:

$$\displaystyle \begin{aligned} post(\mathbf{K}) = \underset{{k \in \mathbf{K}}}{{\bigcup}}post(k) \quad pre(\mathbf{K}) = \underset{{k \in \mathbf{K}}}{{\bigcup}}pre(k) \end{aligned} $$

(11.8)

With continuity argument from the hypotheses, we have the following result.

Theorem 6

post(K) and pre(K) are connected sets.

This result shows that our connectivity property assumed for all regions is conservative along trajectories (backward and forward) issued from set K.

Reachability from Initial State to Guard Set

Let H be a hybrid automaton with polynomial dynamics and X ₀ = {x∣(q ₀, x) ∈ S ₀} the set of its initial states in a mode q ₀. We suppose we have built an abstract automaton of H with respect to a given partition. By construction of this partition, we consider that for each region p, all incoming trajectories must exit and become outgoing trajectories after having passed a bounded time in p. Then we can define in(p) as the set of all trajectories restricted to p, which is equal to post(X ₀) ∩ p. We define also the subset pre(p) of the incoming points of in(p) and the subset post(p) of the outgoing points of in(p). It can be demonstrated that pre(p), in(p), and post(p) are unions of a finite number of connected sets. The proof can be made by induction starting from the initial set assumed to be defined by convex linear predicates and using the fact the dynamics is polynomial.

If we consider a guard set G(τ), assumed to be a convex linear predicate set, the set of outgoing points of the trajectories crossing p and verifying this guard is post(p) ∩ G(τ) and it can be proved that this set is again a union of a finite number of connected sets. So the time passed by a trajectory inside p with outgoing points verifying G(τ) can be represented by a union of finite number of intervals, as internal trajectories form a union of finite number of connected sets (the set of instants passed in trajectories belonging to a connected set is a time interval if the trajectories are continuous). Outside this union of time intervals for internal trajectories in p, the guard G(τ) cannot be verified by outgoing points. This analysis will provide important results for the diagnosability verification.

Brusselator Example

This result applies to the polynomial dynamics of the brusselator, more specifically the two defined regions R ₁ and R ₂ corresponding to the color change of the system. We consider the repeller case of the brusselator as a discrete hybrid mode. With the previous result, we demonstrate that any inconsistency in observing the color change within the computed maximal time bound could be diagnosed with a change of the current repellor mode. If we model the fault as a discrete jump to the attractor case, the observations in terms of color change are sufficient to diagnose this fault, since in the attractor case all trajectories converge asymptotically to M ₀, thus there is no color change.

11.6 CEGAR Adaptation for Diagnosability Verification

Since hybrid systems have an infinite state space due to continuous dynamics, verifying formally their properties often rests on using ordinary model checking together with a finite-state abstraction. Model-checking can be inconclusive, in which case the abstraction must be refined. In this section, we adapt counterexample guided abstraction refinement (CEGAR) that was originally proposed to verify safety properties [3, 28].

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. 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.

In our abstraction method, time constraints are used explicitly. When an abstraction refinement is required, tighter time bounds are obtained over the new regions of the refined decomposition. The proposed abstraction method hence differs from the one proposed in [35]. In [35], the abstraction consists in retaining 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.

The adaptation of CEGAR to verify diagnosability of a hybrid automaton H consists in three steps described as follows and to be detailed in the next subsections:

• Diagnosability checking of a timed abstract automaton of H using the twin plant method, which generates a counterexample C.E when diagnosability is not verified.

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

• Refinement of the timed abstract automaton by using a finer hybrid state space decomposition.

11.6.1 CEGAR Scheme for Hybrid Automata Diagnosability Verification

Verifying diagnosability of a hybrid automaton by checking it on abstractions of this automaton 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 ₀, Σ, F, Inv, T), two executions h, h ^′∈ [[H]], $h =(q_0,\mathbf {x}_0 ) \xrightarrow {l_0} (q_1, \mathbf {x}_1) \ldots (q_i, \mathbf {x}_i) \xrightarrow {l_i} \ldots$, $h^\prime =(q_0^\prime ,\mathbf {x}_0^\prime ) \xrightarrow {l_0^\prime } (q_1^\prime , \mathbf {x}_1^\prime ) \ldots (q_i^\prime , \mathbf {x}_i^\prime ) \xrightarrow {l_i^\prime } \ldots$ are called a counterexample of diagnosability in H with respect to the fault F if they satisfy the three conditions defined in Definition 10, 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^\prime ,\mathbf {x}_i^\prime )$ by $s_i^\prime$. We assume that the flow condition F is a singleton function (deterministic). Then, from Theorem 5, given a timed abstract automaton $TH_{\mathfrak {P}}$ of H with abstraction function $\alpha ^t_{\mathfrak {P}}$, h and h ^′ are mapped by $\alpha ^t_{\mathfrak {P}}$ into executions $\hat {h}, \hat {h}^\prime \in [[TH_{\mathfrak {P}}]]$, $\hat {h}=\hat {s}_0 \xrightarrow {\hat {l}_0} \hat {s}_1 \ldots \hat {s}_i\xrightarrow {\hat {l}_i} \ldots$, $\hat {h}^\prime =\hat {s}_0^\prime \xrightarrow {\hat {l}_0^\prime } \hat {s}_1^\prime \ldots \hat {s}_i^\prime \xrightarrow {\hat {l}_i^\prime } \ldots$ and, as (h, h ^′) is a critical pair in H with respect to F, so is $(\hat {h},\hat {h}^\prime )$ in $TH_{\mathfrak {P}}$, which establishes thus a counterexample of diagnosability in $TH_{\mathfrak {P}}$: $C.E = (\hat {h},\hat {h}^\prime )$. This proves the following result.

Theorem 7

Given a hybrid automaton H with singleton flow condition, a timed abstract automaton $TH_{\mathfrak {P}}$ of H with abstraction function $\alpha ^t_{\mathfrak {P}}$ and a modeled fault F in H, if F is diagnosable in $TH_{\mathfrak {P}}$ then F is diagnosable in H.

Now, with this result, Algorithm 1 illustrates the CEGAR scheme adaptation for hybrid automata diagnosability verification.

Algorithm 1 CEGAR scheme for hybrid automata diagnosability verification

11.6.2 Twin Plant Based Diagnosability Checking

Diagnosability checking of a discrete event system, modeled as an automaton, based on the twin plant method [40, 61] is polynomial in the number of states (actually it has been proved it is NLOGSPACE-complete [51]). 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 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 [58], 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 1

A fault is diagnosable in a timed automaton iff its twin plant contains no critical path [ 58 ].

For timed automata, checking diagnosability is PSPACE-complete.

11.6.3 Counterexample Validation or Refusal

After applying the twin plant method on a timed abstract automaton $TH_{\mathfrak {P}}$ of H as described in [58], suppose that a critical pair $C.E = (\hat {h},\hat {h}')$ is returned (if not, it means that $TH_{\mathfrak {P}}$, and thus H, is diagnosable). Whether we find or not two concrete executions h, h ^′∈ [[H]] whose abstractions by $\alpha ^t_{\mathfrak {P}}$ are $\hat {h}$ and $\hat {h'}$ 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.

Validated Counterexample

If it exists h, h ^′∈ [[H]], whose abstractions by $\alpha ^t_{\mathfrak {P}}$ (according to Theorem 5) are $\hat {h},\hat {h'}$ and such that Obs(h) = Obs(h ^′), then (h, h ^′) constitutes a concrete counterexample realizing C.E and proves thus the non-diagnosability of H. If not, the abstract counterexample C.E is said spurious. In practice, this step involves computing reachable sets of states using safe over approximations such as ellipsoids and zonotopes for complex dynamics or hypercubes for simpler ones [1, 12]. Obviously, due to inherent undecidability of reachability problem at the concrete level of the hybrid automaton, it can happen that a concrete critical pair realizing C.E does actually exist but this existence will not be proved and C.E will be declared spurious, with new chance to discover a concrete critical pair at the next refinement loop.

Refuted Counterexample

In case of spurious $C.E = (\hat {h},\hat {h}')$, the idea is to construct longest finite executions h, h ^′∈ [[H]], that abstract by $\alpha ^t_{\mathfrak {P}}$ into finite prefixes of $\hat {h},\hat {h}'$ and such that Obs(h) = Obs(h ^′). The fact they cannot be extended means that $\forall \overline {h} \in [[H]]/h$, $\overline {h^\prime } \in [[H]]/h^\prime$ one step executions, either (i) $\hat {s}_{\lvert h \rvert +1}\neq \alpha ^t_{\mathfrak {P}}(s_{\lvert h \rvert +1})$ (or $\hat {s}^\prime _{\lvert h^\prime \rvert +1}\neq \alpha ^t_{\mathfrak {P}}(s^\prime _{\lvert h^\prime \rvert +1})$) or (ii) $\hat {l}_{\lvert h \rvert }\neq l_{\lvert h \rvert }$ (or $\hat {l}_{\lvert h \rvert }^\prime \neq l_{\lvert h \rvert }^\prime$) or (iii) $Obs(\overline {h})\neq Obs(\overline {h^\prime })$. In this case, $s_{\lvert h \rvert +1}^{reach}$ and $s_{{\lvert h^\prime \rvert }+1}^{\prime reach}$ 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 $\hat {h}$ or $\hat {h}^\prime$, as one of the set of states of H whose abstraction is an abstract state $\hat {s}_i$ or $\hat {s}_i^\prime$ is not reachable in H starting from the initial states of H. Note that care will have to be taken when refining $TH_{\mathfrak {P}}$ (see next subsection). E.g., a possible case is that there exist two executions (h, h ^′) reaching $(s_1,s_1^\prime )$ and then $(s_2, s_2^\prime )$ but not reaching $(s_3,s_3^\prime )$ (and none passing by $(s_1,s_1^\prime )$ and $(s_2, s_2^\prime )$ reaches $(s_3,s_3^\prime )$), and two other executions (u, u ^′) reaching $(s_2,s_2^\prime )$ from $(s,s^\prime )\neq (s_1,s_1^\prime )$, with $\alpha ^t_{\mathfrak {P}}(s)=\alpha ^t_{\mathfrak {P}}(s_1)$ and $\alpha ^t_{\mathfrak {P}}(s^\prime )=\alpha ^t_{\mathfrak {P}}(s_1^\prime )$, and then reaching $(s_3,s_3^\prime )$, all with time periods compatible to those of the abstract executions. If the refined model simply eliminated the transition from $\hat {s}_2$ to $\hat {s}_3$ or from $\hat {s}_2^\prime$ to $\hat {s}_3^\prime$ then it could no longer be considered an abstraction of H, since some concrete execution in H would have 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.

11.6.4 Refinement of the Abstraction

If it reveals that abstract counterexample $C.E = (\hat {h},\hat {h}^\prime )$ is spurious, then one refines the timed abstract automaton $TH_{\mathfrak {P}}$ to get $TH_{\mathfrak {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 $TH_{\mathfrak {P'}}$. The refinement procedure is described as follows and will be illustrated on our example in the next section.

• 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_{\lvert h \rvert +1}^{reach}=\emptyset$, i.e., an illegal transition. To eliminate such spurious counterexample next time, one can partition the region containing $\hat {s}_{\lvert h \rvert }$ 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.

• 2. Suppose that the refutation of C.E is due to different observations from $s_{\lvert h \rvert +1}$ and $s_{{\lvert h^\prime \rvert }+1}^\prime$ 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 $\hat {s}_{\lvert h \rvert +1}$ and $\hat {s}_{\lvert h^\prime \rvert +1}^\prime$ 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.

11.7 Case Study Example

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

Example 6 (Fault Tolerant Thermostat Model)

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 ∈ [80, 90]. Two faults are modeled as unobservable events F ₁ and F ₂ ∈ Σ _f shown in Fig. 11.4. In practice, the fault F ₁ models a bad calibration of the temperature sensor. As for fault F ₂, 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.

Fig. 11.4

One-dimensional hybrid automaton modeling a faulty thermostat

CEGAR Scheme for Fault F ₁

Initial Abstraction We consider an initial decomposition $\mathfrak {P}= \{P_{off}, P_{on},P_{off}^{F_1}, P_{on}^{F_1}\\ P_{off}^{F_2}$, $P_{on}^{F_2}\}$ of the hybrid state space. Each partition $P \in \mathfrak {P}$ is made up of only one region representing the reals $\mathbb {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 generates a counterexample $C.E = (\hat {h}, \hat {h'})$ such that:

$$\displaystyle \begin{aligned} \begin{aligned} &\hat{h} = (off,p_{off}) \xrightarrow{0.15} (off,p_{off}) \xrightarrow{Bon} (on,p_{on})\xrightarrow{0.3} (on,p_{on}) \xrightarrow{B_{off}} (off, p_{off}) \ldots \\ &\hat{h'} = (off,p_{off}) \xrightarrow{0.1} (off,p_{off}) \xrightarrow{F_1} (off^{F_1}, p_{off}^{F_1}) \xrightarrow{0.05} (off^{F_1}, p_{off}^{F_1}) \xrightarrow{B_{on}} \\ & \qquad (on^{F_1}, p_{on}^{F_1}) \xrightarrow{0.3} (on^{F_1}, p_{on}^{F_1}) \xrightarrow{B_{off}} (off^{F_1}, p_{off}^{F_1}) \ldots \end{aligned} \end{aligned} $$

Validation or Refusal The computation of the set of concrete executions {h} (resp. {h′}) whose abstraction is $\hat {h}$ (resp. $\hat {h'}$) yields an approximation as follows:

$$\displaystyle \begin{aligned} \begin{aligned} &\{h\} = (off,[80,90]) \xrightarrow{0.15} (off,[69,77]) \xrightarrow{Bon} (on,[69,70]) \ldots \\ &\{h'\} = (off,[80,90]) \xrightarrow{0.1} (off,[72,81]) \xrightarrow{F_1} (off^{F_1},[80,81]) \xrightarrow{0.05} \\ &\qquad \quad (off^{F_1},[76,77]:invalid) \end{aligned} \end{aligned} $$

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 [76,77] violating the invariant 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 ∈ [80, 81] 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},[80,81])} = [0,0.0124]$. The refined abstraction would carry this new information by updating the partition of mode $off^{F_1}$, from $\mathbb {R}$ to (−∞, 80) ⊎ [80, 81] ⊎ (81, +∞), thus ensuring that all future generated counterexamples would satisfy this constraint.

CEGAR Scheme for Fault F ₂

Initial Abstraction The same as for F ₁.

Diagnosability Check The diagnosability check of the initial abstraction using the twin plant method generates a $C.E = (\hat {h}, \hat {h'})$:

$$\displaystyle \begin{aligned} \begin{aligned} &\hat{h} = (off,p_{off}) \xrightarrow{0.5} (off,p_{off}) \xrightarrow{B_{on}} (on,p_{on})\xrightarrow{0.5} (on,p_{on}) \xrightarrow{B_{off}} (off, p_{off}) \ldots \\ &\hat{h'} = (off,p_{off}) \xrightarrow{0.5} (off,p_{off}) \xrightarrow{B_{on}} (on,p_{on}) \xrightarrow{0.4} (on, p_{on}) \xrightarrow{F_2} (on^{F_2}, p_{on}^{F_2}) \xrightarrow{0.1}\\ &\qquad (on^{F_2}, p_{on}^{F_2}) \xrightarrow{B_{off}}(off^{F_2}, p_{off}^{F_2}) \ldots \end{aligned} \end{aligned} $$

Validation or Refusal The computation of the set of concrete executions {h} (resp. {h′}) whose abstraction is $\hat {h}$ (resp. $\hat {h'}$) yields an approximation as follows:

$$\displaystyle \begin{aligned} \begin{aligned} \{h\} = (off,[80,90]) \xrightarrow{0.5} (off,[48.5,54.58]:invalid) \\ \{h'\} = (off,[80,90]) \xrightarrow{0.5} (off,[48.5,54.58]:invalid) \end{aligned} \end{aligned} $$

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.

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,[68,80))} = [0, 0.16] and I _{(off,[80,90])} = [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).

Second Abstraction

Diagnosability Check The second C.E generated from the refined twin plant is:

$$\displaystyle \begin{aligned} \begin{aligned} \hat{h} &= (off,p_{{off}_1}) \xrightarrow{0.08}(off,p_{{off}_1}) \xrightarrow{\epsilon} (off,p_{{off}_2})\xrightarrow{0.07} (off,p_{{off}_2}) \xrightarrow{B_{on}} (on,p_{on})\\ &\xrightarrow{0.5} (on,p_{on}) \xrightarrow{B_{off}}(off, p_{off}) \ldots \\ \hat{h'} &=(off,p_{{off}_1}) \xrightarrow{0.08}(off,p_{{off}_1}) \xrightarrow{\epsilon} (off,p_{{off}_2}) \xrightarrow{0.07} (off,p_{{off}_2})\xrightarrow{B_{on}} (on,p_{on})\\ &\xrightarrow{0.4} (on, p_{on}) \xrightarrow{F_2}(on^{F_2}, p_{on}^{F_2}) \xrightarrow{0.1} (on^{F_2}, p_{on}^{F_2}) \xrightarrow{B_{off}} (off^{F_2}, p_{off}^{F_2}) \ldots \end{aligned} \end{aligned} $$

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:

$$\displaystyle \begin{aligned} \begin{aligned} \{h\} &= (off,[80,90]) \xrightarrow{0.15} (off,[69,77]) \xrightarrow{B_{on}} (on,[69,70])\xrightarrow{0.5} (on,[80.5,81.8])\ldots\\ \{h'\} &= (off,[80,90]) \xrightarrow{0.15} (off,[69,77]) \xrightarrow{B_{on}} (on,[69,70])\xrightarrow{0.4} (on,[79,79.9])\\ &\xrightarrow{F_2} (on^{F_2},[79,79.9]) \xrightarrow{0.1}(on^{F_2}, [82.9,83.7])\ldots \end{aligned} \end{aligned} $$

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] = ∅.

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:

$$\displaystyle \begin{aligned} t_{spurious} = \ln \left(\frac{b-a+20}{20}\right) + t_f \end{aligned} $$

(11.9)

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.

11.8 Conclusion

In this chapter, 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.

This preliminary work draws many perspectives. First of all, we have to develop refinement strategies by analysis of the counterexample and progress in the (partial) automation of the whole process and the integration of the algorithms for abstract diagnosability checking, for validation of the counterexample and for refinement. 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 [17, 18], in particular with theories including ODEs [31], to deal simultaneously with discrete and continuous variables. Moreover, we plan to apply this approach to other formal safety properties such as predictability, which guarantees to predict in advance the future unavoidable occurrence of a fault given some sequence of observations. With all this, we will be able to tackle real applications and get deeper experimental results.

Another promising aspect is the potential of this approach to deduce minimal concrete sets of observations for which the system is diagnosable. These observations specify a minimal (for set inclusion) needed set of events and continuous variables for which the system is diagnosable. If one element of this set is not considered as observable, the system becomes non-diagnosable. Thus, such a minimal set draws the boundary between the diagnosable and non-diagnosable systems [14] from the point of view of their observability.

Up to now we assume a continuous domain for both the values and the time stamps of the observable variables without taking into account sensor capability, i.e., the minimal interval (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 [42], for ε arbitrary small (for a given metric to be defined). 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 bi-simulation 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.