# An Approximation-based Incremental SMT Approach for Diagnosability Analysis of Real-Time Systems

Lulu He, Philippe Dague, Lina Ye

► To cite this version:

Lulu He, Philippe Dague, Lina Ye. An Approximation-based Incremental SMT Approach for Diagnosability Analysis of Real-Time Systems. Discrete Event Dynamic Systems, 2025, 35 (3), pp.267-299. 10.1007/s10626-025-00420-x. hal-05073025v2

HAL Id: hal-05073025

https://hal.science/hal-05073025v2

Submitted on 19 Sep 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# An approximation-based incremental SMT approach for diagnosability analysis of real-time systems

Lulu He<fnref n="1" /> · Philippe Dague<fnref n="2" />, Lina Ye<fnref n="2" />,<fnref n="3" />

Received: 19 December 2022 / Accepted: 10 July 2025 / Published online: 23 August 2025
© The Author(s) 2025

## Abstract

In this article, we focus on improving the efficiency of diagnosability checking for real-time systems modeled as timed automata. Inspired by a recently introduced extension of the classic CEGAR (CounterExample-Guided Abstraction Refinement) algorithm, namely the RECAR (Recursive Explore and Check Abstraction Refinement) algorithm, we propose new RECAR-like algorithms that combine over-approximation and under-approximation techniques. We use CEGAR to quickly terminate the refinement loop by over-approximation and under-approximation, in the case where the original formula is respectively satisfiable or unsatisfiable, and then show the soundness of our RECAR-like approach applied to an arbitrary formula. We define then several types of parameterized over- and under-approximations along with refinement strategies for the diagnosability problem. Finally, we evaluate the effectiveness of our method and its implementation with the Z3 SMT solver on different benchmarks by comparing it to the direct method without approximation shortcuts.

**Keywords** Diagnosability · Timed automata · Approximations · CounterExample-guided abstraction refinement (CEGAR) · Satisfiability modulo theories (SMT)

<figure><img src="image_2.png" /></figure>

<footnote>Lulu He and Lina Ye contributed equally to this work.</footnote>

<footnote>Philippe Dague
philippe.dague@universite-paris-saclay.fr</footnote>

<footnote>Lulu He
hell@czu.cn</footnote>

<footnote>Lina Ye
lina.ye@centralesupelec.fr</footnote>

<footnote n="1">¹ Changzhou Institute of Technology, No. 666 Liaohe Road, Xinbei District, Changzhou City, Jiangsu Province 213032, China</footnote>

<footnote n="2">² Laboratoire Méthodes Formelles, Université Paris-Saclay, CNRS, ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette 91190, France</footnote>

<footnote n="3">³ CentraleSupélec Paris-Saclay, 3 rue Joliot-Curie, Gif-sur-Yvette 91190, France</footnote>
# 1 Introduction

Work on diagnosability has mainly focused on discrete event systems, first timeless, classically modeled as finite state automata (Sampath et al. 1995), then real-time, classically modeled as timed automata (Tripakis 2002). It has been shown that any pair of sufficiently long trajectories (in distance or duration) sharing the same observation, one of which is faulty and the other normal (called a (timed) critical pair), constitutes a witness of non-diagnosability. Thus checking diagnosability boils down to checking the non-existence of a critical pair, for which methods have been developed.

The problem of verifying the diagnosability of discrete event systems has been shown to belong to class P for finite state automata (Jiang et al. 2001) and to become PSPACE-complete for timed automata (Tripakis 2002). The combination of Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) methods has proved to be a very successful practical approach to solving certain NP-complete problems, achieving good results in this case. Nevertheless, scalability is not guaranteed and timed automata of too large a size cannot be handled. As the recently introduced RECAR (Recursive Explore and Check Abstraction Refinement) framework (Lagniez et al. 2017), an extension of the well-known CEGAR (CounterExample-Guided Abstraction Refinement) algorithm (Clarke et al. 2000), seems promising for dealing with problems beyond NP, in particular PSPACE-complete problems, we decided to investigate the use of RECAR to check the diagnosability of real-time systems modeled as timed automata.

CEGAR is an incremental method for deciding the satisfiability of formulas, for example in classical propositional logic, based on the use of abstractions, i.e., under-approximations (less constrained and therefore with more solutions), of the original formula. It provides a shortcut when the approximate formula proves unsatisfiable, since this also the case for the original formula. In the case of satisfiability, the counterexample is checked to determine whether it is a real solution for the original formula or a spurious solution, in which case the abstraction is refined to avoid this spurious solution and the process is repeated. The method works in the same way using over-approximations (more constrained and therefore with fewer solutions) by exchanging the SAT and UNSAT cases (and thus the analysis of a SAT instance by the analysis of the UNSAT core). From preliminary experiments applied to diagnosability verification, we found that CEGAR-over does not give good results for unsatisfiable problems, while CEGAR-under does not give good results for satisfiable problems, and that one way of solving this problem is to alternate between over- and under-approximations. The RECAR approach precisely combines the two types of approximation.

Therefore, in order to check the bounded diagnosability of real-time systems, we propose a RECAR-like approach, which includes refinement iteration steps that can switch between CEGAR-over and CEGAR-under by estimating how easy it is to check the next refinement or to use another type of approximation. In each iteration step, CEGAR begins by refining the formula that was last processed by CEGAR of the same type.

This paper is organized as follows. Section 2 recalls the diagnosability checking problem for timed automata. Section 3 presents CEGAR with over-approximations and the corresponding refinement determined by three modifiable parameters for the diagnosability checking problem. Symmetrically, Section 4 presents CEGAR with under-approximations and the corresponding refinement determined by two modifiable parameters, and also defines the *semi-equivalence* of observations instead of equivalence as an under-approximation.

<figure><img src="image_3.png" /></figure>
Section 5 proposes a RECAR-like algorithm alternating CEGAR-over and CEGAR-under, defining a switch function SF to decide whether to switch from one type of approximation to the other. Section 6 shows how to encode modifiable parameters in SMT to support the incremental processing of refinements and presents the refinement strategies adopted. Section 7 presents the construction of a scalable benchmark and the experimental results of the CEGAR and RECAR-like algorithms on several of its instances. Section 8 analyzes these results and determines that the key factor in complexity and hence non-efficiency is the length of the critical pair sought, which cannot be improved with our under-approximations for UNSAT problems. Section 10 concludes and outlines prospects for future research.

## 2 Preliminaries: diagnosability of timed automata

In this section, we review the definition of timed automata (TA) and the principle of diagnosability checking.

TA provides a framework for modeling and verifying real-time discrete event systems (Alur and Dill 1994). A TA is essentially a finite automaton, i.e., with a finite set of states and a finite set of labeled transitions between them, extended with a finite set of real-valued variables modeling the clocks. During the run of a TA, the clock values are initialized to zero on start-up in the initial state, and then all increase at the same rate. The clock values can be compared with constants or with each other. These comparisons form guards that can enable or disable instantaneous transitions and, in so doing, limit the possible behaviors of the TA. In addition, clocks can also be reset to zero during certain transitions.

Before introducing the formal definition of TA, we first present the set of possible clock constraints considered in this paper. The time constraints discussed here constitute the set of so-called diagonal constraints, formally described as:

$$g ::= true \mid x \bowtie c \mid x - y \bowtie c \mid g \land g, \\ \text{where } x, y \text{ are clock variables, } c \text{ is a constant and } \bowtie \in \{<, \leq, =, \geq, >\}.$$

Note that a TA allowing such clock constraints is exponentially more concise than its classical variant with only diagonal-free constraints (where the comparison can only be made between a clock value and a constant), but both have the same expressiveness. Let X be a finite set of clock variables. A clock valuation on X is a function $v: X \to R$, where R represents the set $\mathbb{R}_+$ of non-negative real numbers (in fact, for implementation purposes, the set $\mathbb{Q}_+$ of non-negative rational numbers is used to have an exact computational representation). The set of all clock valuations on X is denoted $R^X$ and the set of time constraints on X is denoted $C(X)$, where such a constraint is given by a collection of clock constraints. If a clock valuation $v$ satisfies the time constraint $g$, then it is denoted by $v \models g$. In the following, we denote $[[g]]$ the set of clock valuations that satisfy $g$, i.e., $[[g]] = \{v \in R^X | v \models g\}$.

The definition of a timed automaton is as follows.

**Definition 1** (Timed Automaton) A timed automaton (TA) is a tuple $A = (Q, \Sigma, X, \delta^X, q_0, I)$, where:

* $Q$ is a finite set of states;
• Σ is a finite set of events;

• X is a finite set of clock variables;

• $\delta^X \subseteq Q \times \mathbb{C}(X) \times \Sigma \times 2^X \times Q$ is a finite set of transitions;

• $q_0 \in Q$ is the initial state;

• $I: Q \to \mathbb{C}(X)$ is a function that assigns invariants to states, with $0 \in [I(q_0)]$.

It is assumed that $A$ is only partially observable, i.e., the set of events is divided into three disjoint parts: $\Sigma = \Sigma_o \uplus \Sigma_u \uplus \Sigma_f$, where $\Sigma_o$ is the set of observable (normal) events, $\Sigma_u$ is the set of unobservable normal events and $\Sigma_f$ the set of (unobservable) fault events.

In the example shown in Fig. 1, $x$ is a clock variable used to impose a certain period between events, or to restrict the possible time during which one is allowed to stay in certain states. For example, $(q_0, x > 1, o1, \{x\}, q_1) \in \delta^X$ means that event $o1$ can only occur when guard $x > 1$ is satisfied, i.e., the clock value is greater than 1, resulting in an instantaneous change of state from $q_0$ to $q_1$ and simultaneous resetting of clock $x$ to 0. We also refer to this transition as $q_0 \xrightarrow[x:=0]{x>1;o1}$ $q_1$. Furthermore, $I(q_1) = x < 6$ requires that we can only stay in the state $q_1$ when the clock value is smaller than 6. In other words, when the invariant ceases to be satisfied, one is obliged to leave the corresponding state.

We call a state with clock valuation an extension state, i.e., $(q, v)$ with $q \in Q$ and $v \in R^X$. If $t \in R$, the valuation $v + t$ is defined by $(v + t)(x) = v(x) + t, \forall x \in X$. Suppose $X' \subseteq X$, we denote by $v[X' \leftarrow 0]$ the valuation such that $\forall x \in X'$, $v[X' \leftarrow 0](x) = 0$ and $\forall x \in X \setminus X'$, $v[X' \leftarrow 0](x) = v(x)$. A TA gives rise to an infinite system of transitions with two types of transitions between extension states. One is a *time* transition representing the passage of time in the same state $q$, during which the invariant $inv = I(q)$ for $q$ must always be respected. The other is a *discrete* transition arising from a labeled transition $(q, g, \sigma, r, q')$ for TA, associated with an event $\sigma$, which is triggered (a necessary condition being that the guard $g$ is satisfied) and must be executed instantaneously, i.e., the clock valuation cannot be modified by the transition itself, but only by resetting the clock variables belonging to $r$ to 0, if any. In what follows, both are denoted $(q, v) \xrightarrow{\nu} (q', v')$, where $\nu \in \Sigma \cup R$. Thus, if $\nu \in \Sigma$, then $v$ must satisfy the guard $g$ in the corresponding TA transition and $v' = v[r \leftarrow 0]$ for $r$ clock variables reset to 0 in this transition, if any. Otherwise, if $\nu \in R$, then $q' = q$ and $v' = v + \nu$, where any $v + t$, for $0 \le t \le \nu$, must satisfy the invariant $inv$ associated with state $q$.

Given $A$ a TA, a sequence of such transitions $(q_0, v_0 = 0) \xrightarrow{\nu_1} (q_1, v_1) \dots \xrightarrow{\nu_n} (q_n, v_n)$ is a feasible execution in $A$ if $\forall i \in \{0, \dots, n-1\}$, $(q_i, v_i) \xrightarrow{\nu_{i+1}} (q_{i+1}, v_{i+1})$ is either a time or a discrete transition. The word $\nu_1 \dots \nu_n \in (\Sigma \cup R)^*$ is then called a (finite) *timed automaton*.

<figure><img src="image_4.png" /><figcaption>**Fig. 1** A system example modeled by a timed automaton</figcaption></figure>
trajectory or run. This extends to infinite sequences and trajectories. The set of finite (resp., infinite) timed trajectories for A is denoted $L(A)$ (resp., $L^\omega(A)$). By summing successive time periods and inserting a zero time period between two successive events, we can always assume that between two successive events there is exactly one time period, i.e., time periods and events alternate in a timed trajectory, which, if finite, belongs thus to $(R\Sigma)^*R$. For $\rho$ a timed trajectory, we denote by $time(\rho) \in R \cup \{+\infty\}$ the total duration of $\rho$, i.e., $time(\rho) = \sum_{\nu_i \in R \land \nu_i \in \rho} \nu_i$. The set of time-infinite timed trajectories, included in $L^\omega(A)$, is denoted $L^\infty(A)$. We define a projection operator $P$ for TA as follows. Given a timed trajectory $\rho$ and a set of events $\Sigma' \subseteq \Sigma$, $P(\rho, \Sigma')$ is the timed trajectory obtained by deleting from $\rho$ all events not in $\Sigma'$ and adding the periods between successive events in the resulting sequence. For example, if $\rho = 2o13u2o23o1$, then $P(\rho, \{o1, o2\}) = 2o15o23o1$. In the following, we simply note $P(\rho)$ the projection of the timed trajectory $\rho$ onto observable events, i.e., $P(\rho) = P(\rho, \Sigma_o) \in (R\Sigma_o)^*R$ if $\rho$ is finite.

In order to check the diagnosability property, we make the usual assumptions for TA about the system’s time aliveness and the need to observe all time-infinite behaviors.

**Assumption 1** (Timed living system) TA A is timed living (or well-timed), i.e., for any reachable state, there is a time-infinite timed trajectory from that state.

**Assumption 2** (Timed observably living system) The TA A is timed observably living, i.e., it has no time-infinite execution from a reachable state without observable events, and therefore any time-infinite timed trajectory has an infinite number of occurrences of observable events.

In particular, these assumptions imply that the system cannot stay infinitely long in the same state without a discrete transition and that $L^\omega(A) \subseteq (R\Sigma)^\omega$ and $P(L^\omega(A)) \subseteq (R\Sigma_o)^\omega$. We are reformulating a useful concept originally introduced by Tripakis (2002).

**Definition 2** (Δ-faulty runs) Given A a TA, let $\rho = \nu_1\nu_2\dots$ be a timed trajectory; $\rho$ is faulty if, for some $i \in \{1, \dots, \}$, $\nu_i = F$. Then let $j$ be the smallest $i$ such that $\nu_i = F$ and let $\rho' = \nu_{j+1}\dots$. We designate the period from (the first occurrence of) fault F in $\rho$ by $time(\rho, F) = time(\rho')$. If $time(\rho, F) > \Delta$, where $\Delta \in R$, we say that more than $\Delta$ time units elapse after the first occurrence of F in $\rho$, or, in short, that $\rho$ is Δ-faulty.

For example, for the timed trajectory $\rho = 2o15o21.01F0.98o13o13 o10$ of the system in Fig. 1, we have $time(\rho, F) = 6.98$ and so $\rho$ is 6.9-faulty but not 7-faulty or even 6.98-faulty.

Note that we have chosen in the definition $> \Delta$ instead of $\ge \Delta$ because some technical aspects of the encoding become easier (in particular, a Δ-faulty run can then be assumed finite since such an infinite run has a finite run as its prefix), but there is no difference in substance for what follows, since a Δ-faulty run (for $>$) is Δ-faulty (for $\ge$) and a Δ-faulty run (for $\ge$) with $\Delta > 0$ is Δ'-faulty (for $>$) for all $\Delta' < \Delta$.

We now define the property of Δ-diagnosability (resp., diagnosability) for TA, which, when satisfied, means that any Δ-faulty run (resp., any faulty run with a sufficiently long time after the first occurrence of the fault) can be distinguished by observation from any normal run, i.e., the two runs have distinct projections onto observable events (or equivalently, any run sharing an identical observation with the faulty run is itself faulty). This definition
thus generalizes to TA that of k-diagnosability (resp., diagnosability) for simple automata, where $k \in \mathbb{N}$ and a k-faulty run has a length after the occurrence of the fault longer than k. It allows more systems to be diagnosable as the projection onto observable events is not limited to the ordered sequence of occurrences of these events, but includes also the durations between these occurrences.

**Definition 3** (Diagnosability of TA) Given a TA A and a fault F:

1. given $\Delta \in R$, F is $\Delta$-diagnosable in A if and only if

$$ \begin{array}{l} \forall \rho \in L(A)(\rho\Delta - \text{faulty} \Rightarrow \\ \forall \rho' \in L(A)(P(\rho) = P(\rho') \Rightarrow F \in \rho')). \end{array} $$

2. F is diagnosable in A if and only if

$$ \exists \Delta \in R \text{ such that } F \text{ is } \Delta\text{-diagnosable in } A. $$

As usual, in order to avoid exponential complexity in the number of faults, we deal with faults one by one (the others then being considered unobservable normal events notwithstanding), and we can therefore assume a single fault (with multiple occurrences), i.e., $\Sigma_f = \{F\}$.

For example, let's consider the system modeled by the TA in Fig. 1. The system has both faulty runs (where F occurs) and normal runs. Indeed, in all runs, observable events occur in the same order, i.e., $o1.o2.o1^*$. Thus, in the absence of time constraints (as in the case of an automaton), the system could be non-diagnosable. However, in faulty runs, the duration between successive observable events $o2$ and $o1$ is less than 2 (time units), whereas in normal runs, this duration is greater than 2. So, a diagnoser observing $o2$ and then $o1$, and measuring the time between the two, can say with certainty whether or not a fault has occurred. Now, as $o1$ occurs at most one time unit after F, this means that the system is 1-diagnosable and so is diagnosable (but is not $\Delta$-diagnosable for any $\Delta < 1$ because then there is a $\Delta$-faulty run with no occurrence of $o1$ after F).

We can clearly see that the addition of time constraints sometimes makes a non-diagnosable system diagnosable by distinguishing by temporal observation (for example, by different durations between two successive observable events) a faulty trajectory and a normal trajectory that have the same observation in the untimed framework.

In the untimed framework, a critical pair is a pair of trajectories, one faulty, the other normal, sharing the same sequence of occurrences of observable events. If the faulty trajectory has a length after fault occurrence longer than k (resp., infinite), the critical pair testifies to non-k-diagnosability (resp., non-diagnosability) in automata. Now, the analog in the timed framework of a critical pair, called a *timed critical pair*, is defined as follows.

**Definition 4** (Timed critical pair) Given a TA A, the fault under consideration F and $\Delta \in R$, two timed trajectories $\rho_F, \rho$ are called a (timed) $\Delta$-critical pair ($\Delta$-CP), denoted by $\rho_F \approx_{\Delta} \rho$ (resp., a (timed) $\infty$-critical pair ($\infty$-CP), denoted by $\rho_F \approx_{\infty} \rho$), if the following conditions are met: 1) $\rho_F$ contains F and $\rho$ does not; 2) $\rho_F$ is $\Delta$-faulty (resp., $\text{time}(\rho_F) = +\infty$); 3) $P(\rho_F) = P(\rho)$.
Note that, in a $\Delta$-$CP$, $\rho_F$ can be assumed finite, and so can $\rho$, and, in an $\infty$-$CP$, $\rho_F$ and $\rho$ are necessarily infinite and $time(\rho) = +\infty$.

For example, in the system shown in Fig. 1, consider $\rho_F = 2\text{015}\text{o21.01F0.98}$ and $\rho = 2\text{013u2o21.99}$. We have $P(\rho_F) = P(\rho) = 2\text{015}\text{o21.99}$ and therefore $\rho_F \approx_{0.9} \rho$. But there is no $\rho_F$, $\rho$ with $\rho_F \approx_1 \rho$. Now, suppose that, in the system, both the invariant in state $q_4$ and the guard of the transition from $q_4$ to $q_6$ are relaxed from $x < 2$ to $x < 2.1$. Consider $\rho_F = 2\text{015}\text{o21.01F1(o13)}^\infty$ and $\rho = 2\text{013u2o22.01(o13)}^\infty$. We have $P(\rho_F) = P(\rho) = 2\text{015}\text{o22.01(o13)}^\infty$ and therefore $\rho_F \approx_\infty \rho$.

It is obvious from Definitions 3 and 4 that the existence of a $\Delta$-$CP$ is equivalent to non-$\Delta$-diagnosability and that the existence of an $\infty$-$CP$ violates the diagnosability for TA, and the converse was also proved by Tripakis (2002).

**Theorem 1 (Criterion of diagnosability)** Given A a TA, F is $\Delta$-diagnosable (resp., diagnosable) in A if and only if there is no $\Delta$-$CP$ (resp., $\infty$-$CP$) with respect to F in A.

Thus, checking the diagnosability of TA consists in verifying the non-existence of timed critical pairs.

Since we will be relying on bounded model checking methods and finite formulas, we will only consider finite critical pairs and thus $\Delta$-diagnosability checking. For a duration $\Delta$ given and a length bound $B$ given, the verification of bounded $\Delta$-diagnosability for TA consists in checking the non-existence of a $\Delta$-critical pair of length (i.e., the maximum length of the two trajectories) at most $B$. However, it is not difficult to code a finite critical pair in logic: we have followed the SAT coding presented in (Grastien et al. 2007; Rintanen and Grastien 2007) for succinct transition systems, which we have extended to TA using the Z3 SMT solver with Linear Real Arithmetics (LRA) theory to handle time constraints. In this way, we can represent the search for a $\Delta$-$CP$, and thus the bounded $\Delta$-diagnosability problem, as the satisfiability problem of a parameterized formula $CP(B, \Delta, \delta^X, \Sigma_o)$, where $B$, the bound parameter, and $\Delta$, the diagnosability parameter, are given by the user, $\delta^X$ is the set of transitions of the TA modeling the system, i.e., the search space of the SMT solver, and $\Sigma_o$ the observable events. All these parameters will be modifiable in the different approximations during the diagnosability check with the CEGAR algorithm.

### 3 CEGAR-over for bounded diagnosability analysis of RTS

As mentioned in the introduction, CEGAR is a framework that makes it easy to use over- or under-approximations to solve problems that are generally too complex to tackle directly. It is widely used in a large number of decision problems. There are two types of CEGAR methods, depending on the type of approximation used.

Figure 2 shows the CEGAR-over framework for the bounded $\Delta$-diagnosability checking problem. It receives as input the original formula $\phi = CP(B, \Delta, \delta^X, \Sigma_o)$, representing a finite parameterized candidate critical pair, and over-approximates it to $\psi$ first, then calls up a solver (the Z3 SMT solver in our case) to check whether $\psi$ is satisfiable. If so, we can conclude that $\phi$ is satisfiable, i.e., the existence of a $\Delta$-critical pair, and therefore non-$\Delta$-diagnosability. Otherwise, $\psi$ is refined (under-approximated, while remaining an over-approximation of $\phi$) to make it closer to $\phi$, until it is satisfiable, or until the refined
<figure><img src="image_5.png" /><figcaption>**Fig. 2** CEGAR-over for diagnosability checking</figcaption></figure>

over-approximation is equisatisfiable to $\phi$, denoted here as $\psi = \phi$ as in our case we will limit equisatisfiability to equality, in which case we can conclude that $\phi$ is unsatisfiable and therefore the system $\Delta$-diagnosable (within the length bound $B$).

Figure 3 shows that successive over-approximations get closer and closer to the original problem ($\subseteq$ meaning the entailment of formulas or the inclusion of their models, and $refine^i(\hat{\phi})$ representing the $i^{th}$ refinement of $\hat{\phi}$).

CEGAR-over is sound and complete if the refinement process ends (subject to a sound and complete solver and satisfiability-preserving refinement). In general, refinement is guided by an analysis of the UNSAT core in order to eliminate the reasons that led to an unsatisfiability result. In our case, we define the refinement function as a change in the values of certain parameters of the input formula. As the possible values for these changes turn out to be finite, the refinement process will always end (if the solver completes within the allotted time) by reaching the original formula at worst.

We denote the general parameterized current formula by the refinement process as $\psi = CP(L, D, T, O)$, where $L$ is the current length bound and $D$ the current time after fault occurrence in the current critical pair being searched, $T$ the current transition set and $O$ the current observable event set of the current search space. Thus, the initial problem corresponds to: $L = B, D = \Delta, T = \delta^X, O = \Sigma_o$. We will now bring three of these parameters into play to define over-approximations and their refinements:

*   **Length bound $L$.** Decreasing $L$ down to $L' < L$, i.e., requiring a shorter length bound for critical pairs, defines an over-approximation $\psi' = CP(L', D, T, O)$ of $\psi$, which is refined if necessary to $\psi'' = CP(L'', D, T, O)$ by increasing $L'$ up to $L''$ with $L' < L'' \le L$.

*   **Transition set $T$.** Reducing $T$ to $T' \subset T$, i.e., using only part of the system's transitions to construct a critical pair, defines an over-approximation $\psi' = CP(L, D, T', O)$ of $\psi$, which is refined if necessary to $\psi'' = CP(L, D, T'', O)$ by extending $T'$ to $T''$ with $T' \subset T'' \subseteq T$.

*   **Set of observable events $O$.** Extending $O$ to $O' \supset O$, i.e., transforming certain unobservable events into observable events, which requires more constraints to be satisfied be-

<caption>**Fig. 3** Over-approximation refinement process</caption>

$$ \phi \xrightarrow{\text{over-approximation}} \hat{\phi} \subseteq \text{refine}^1(\hat{\phi}) \subseteq \text{refine}^2(\hat{\phi}) \subseteq \dots \subseteq \text{refine}^n(\hat{\phi}) = \phi $$
tween the faulty and normal trajectories of a critical pair, defines an over-approximation $\psi' = CP(L, D, T, O')$ of $\psi$, which is refined if necessary to $\psi'' = CP(L, D, T, O'')$ by reducing $O'$ to $O''$ with $O' \supset O'' \supset O$.

Clearly, the three parameters can be combined, and a general over-approximation of $\psi$ is therefore defined as $\psi' = CP(L', D, T', O')$ with $L' \le L, T' \subseteq T, O' \supseteq O$, at least one of the inequalities being strict. And a general refinement (under-approximation) of $\psi'$ that remains an over-approximation of $\psi$ is defined as $\psi'' = CP(L'', D, T'', O'')$ with $L' \le L'' \le L, T' \subseteq T'' \subseteq T, O' \supseteq O'' \supseteq O$, at least one of the inequalities between the parameters of $\psi'$ and $\psi''$ being strict. Since the possible values of $L''$ (increasing integers from $L'$ to $L$), $T''$ (increasing subsets of the finite set $T$ containing $T'$), and $O''$ (decreasing subsets of the finite set $O'$ containing $O$) are all finite in number, the refinement process always terminates, reaching at worst $\psi$. The finite number of possible refinements (from $\psi'$ to $\psi$ if necessary) is in fact bounded above by $(L - L') + (|T| - |T'|) + (|O'| - |O|)$. Note that we do not use the parameter $D$ (time after fault) to define an over-approximation by increasing it, as the problem turns out to be even more complex to solve and would generally require a larger $L$.

The above analysis can be summed up as follows.

**Lemma 2 (Diagnosability checking with over-approximations)**

1. (Over-approximation) Given a current formula $\psi = CP(L, D, T, O)$ representing a parameterized D-CP of length at most $L$ built from set of transitions $T \subseteq \delta^X$ and set of observable events $O \supseteq \Sigma_o$, the formula $\hat{\psi} = CP(L^0, D, T^0, O_+^0)$ with $L^0 \le L, T^0 \subseteq T, O_+^0 \supseteq O$ (at least one of the inequalities being strict) defines an over-approximation of $\psi$.

2. (Refinement process) Any sequence of formulas $\psi^n = CP(L^n, D, T^n, O_+^n)$, $n > 0$, with $L^0 \le L^n \le L^{n+1} \le L, T^0 \subseteq T^n \subseteq T^{n+1} \subseteq T, O_+^0 \supseteq O_+^n \supseteq O_+^{n+1} \supseteq O$ (at least one of the inequalities between the parameters of $\psi^n$ and $\psi^{n+1}$ being strict) defines a general refinement process of $\hat{\psi}$, $\psi^n = refine^n(\hat{\psi})$, i.e., each $\psi^n$ is an under-approximation of $\hat{\psi}$ which remains an over-approximation of $\psi$, and $\psi^{n+1}$ is an under-approximation of $\psi^n$.

3. (Finiteness) This process is necessarily finite, bounded above by $L + |T| + |\Sigma_u|$, reaching at worst formula $\psi$, and is a sound and complete procedure for checking $\psi$ satisfiability, regardless of the strategy for choice of $L^n, T^n, O_+^n$.

Algorithm 1 provides pseudo-code for an example of refinement in the over-approximation process: here, only one parameter is refined each time: either the current length bound is increased by one, or a certain number (at most 10% of the total number of transitions) of new transitions, chosen at random, are added to the current transition set, or an unobservable event, chosen at random, which has been considered observable in the current set of observable events, is removed from this set.
<caption>**Algorithm 1 Refinement in over-approximation**</caption>

**input** : problem *CP(L, D, T, O)* solved by over-approximation
*ψ*<sup>*n*</sup> formula coding *n*<sup>*th*</sup> refinement *CP(L<sup>*n*</sup>, D, T<sup>*n*</sup>, O<sub>+</sub><sup>*n*</sup>)
**output**: Refine(*ψ*<sup>*n*</sup>)
result ← ChoiceParameterToRefine(L<sup>*n*</sup>, T<sup>*n*</sup>, O<sub>+</sub><sup>*n*</sup>)
**if** result = L<sup>*n*</sup> **then**
  **return** Refine(*ψ*<sup>*n*</sup>) = *CP(L*<sup>*n*</sup> + 1, *D*, *T*<sup>*n*</sup>, O<sub>+</sub><sup>*n*</sup>)
**else**
  **if** result = T<sup>*n*</sup> **then**
    *T'* ← Random(*|T|*div*10, *T*\*T<sup>*n*</sup>)
    **return** Refine(*ψ*<sup>*n*</sup>) = *CP(L*<sup>*n*</sup>, *D*, *T*<sup>*n*</sup> ∪ *T'*, O<sub>+</sub><sup>*n*</sup>)
  **else**
    **if** result = O<sub>+</sub><sup>*n*</sup> **then**
      *o* ← Random(*O*<sub>+</sub><sup>*n*</sup>\*O)
      **return** Refine(*ψ*<sup>*n*</sup>) = *CP(L*<sup>*n*</sup>, *D*, *T*<sup>*n*</sup>, O<sub>+</sub><sup>*n*</sup>\*{*o*})
    **end**
  **end**
**end**

Note that, in the current development of our method for over-approximation, we retain
from the CEGAR algorithm only the idea of a refinement process, with no analysis of the
result in the event of unsatisfiability. The reasons for this are that the analysis of the UNSAT
core is a difficult task (compared with that of a SAT solution), particularly in our framework
where we require the various refined problems to be parameterized instances of a single
critical pair search problem (identifying whether the cause of unsatisfiability is an *L* too
small or a *T* not large enough or an *O* too large, in order to guide the next choice, is unclear),
and that, as we shall see, the experimental results of this process are globally satisfactory.

4 CEGAR-under for bounded diagnosability analysis of RTS

The CEGAR-under framework for the bounded Δ-diagnosability checking prob-
lem is given in Fig. 4. It receives as input the original parameterized formula
$\phi = CP(B, \Delta, \delta^X, \Sigma_o)$ and under-approximates it to $\chi$, then calls the SMT solver to
check whether $\chi$ is unsatisfiable. If so, we can conclude that $\phi$ is unsatisfiable, i.e., the

<figure><img src="image_6.png" /><figcaption>**Fig. 4** CEGAR-under for diagnosability checking</figcaption></figure>
non-existence of a Δ-critical pair, and hence the bounded Δ-diagnosability (within the given length bound B). Otherwise, χ is refined (over-approximated, while remaining an under-approximation of φ) to make it closer to φ, until it is unsatisfiable, or until the refined under-approximation is equisatisfiable to φ, denoted χ = φ as we will only consider equality, in which case we can conclude that φ is satisfiable and thus the system non-Δ-diagnosable.

Figure 5 shows that successive under-approximations get closer and closer to the original problem.

CEGAR-under is sound and complete when the refinement process ends. In general, refinement is guided by the solution found (after checking that it is not a true solution for the initial formula, in which case this formula is satisfiable) so as to eliminate it. In our case, we will require each refined formula to have the same form as the input formula, with different values for its parameters and we will therefore define the refinement function as a change in the values of some of these parameters. Either the possible values for these changes are finite, or we will choose only a finite number of them (see below), so that the refinement process will always end with, at worst, the original formula.

Given the formula $\chi = CP(L, D, T, O)$, we bring in two of the parameters to define the under-approximations and their refinements:

* *Time after fault occurrence D.* Decreasing *D* to *D'* < *D*, requiring a smaller minimal time after fault in the faulty trajectory of a critical pair that is therefore less constrained, defines an under-approximation $\chi' = CP(L, D', T, O)$ of $\chi$, which is refined if necessary to $\chi'' = CP(L, D'', T, O)$ by increasing $D'$ up to $D''$ with $D' < D'' \le D$.

* *Set of observable events O.* Reducing *O* to *O'* ⊂ *O*, i.e., transforming certain observable events into unobservable events, reducing the number of constraints to be met between the faulty and normal trajectories of a critical pair, defines an under-approximation $\chi' = CP(L, D, T, O')$ of $\chi$, which is refined if necessary to $\chi'' = CP(L, D, T, O'')$ by extending $O'$ to $O''$ with $O' \subset O'' \subseteq O$.

There are an infinite number of $D''$ such that $D' < D'' \le D$, and therefore an infinite number of possible refinements using the time after fault occurrence. We will only allow a discrete set of values for this parameter, and therefore a finite number of refinements. In other words, $\Delta$ and all values of $D$ are assumed to be in $\delta N$, where $\delta \in R$ is a positive unit of time chosen according to the system's time constraints (for example, one second or one hour).

Clearly, the two parameters can be combined and a general under-approximation of $\chi$ is defined as $\chi' = CP(L, D', T, O')$ with $D' \le D$, $O' \subseteq O$, at least one of the inequalities being strict. And a general refinement (over-approximation) of $\chi'$ that remains an under-approximation of $\chi$ is defined as $\chi'' = CP(L, D'', T, O'')$ with $D' \le D'' \le D$, $O' \subseteq O'' \subseteq O$, with at least one of the inequalities between the parameters of $\chi'$ and $\chi''$ being strict. The

<caption>**Fig. 5** Under-approximation refinement process</caption>

$$ \phi \xrightarrow{\text{under-approximation}} \check{\phi} \supseteq \text{refine}^1(\check{\phi}) \supseteq \text{refine}^2(\check{\phi}) \supseteq \dots \supseteq \text{refine}^n(\check{\phi}) = \phi $$
number of refinements (from $\chi'$ to $\chi$ if necessary) is therefore finite, as bounded above by $\lfloor(D - D')/\delta\rfloor + (|O| - |O'|)$. Note that we do not use the parameter $L$ to define an under-approximation by increasing it, as the problem turns out to be even more complex to solve (we will see that the length bound actually seems to be the key factor in complexity). As for parameter $T$, it cannot be increased as its initial value encompasses all the transitions in the system. Finally, parameter $O$ is the only one that can be used to define both over- and under-approximations.

We will also use another under-approximation, obtained by weakening the condition of equivalence of timed observations between faulty and normal trajectories of a timed critical pair (condition 3 of Definition 4) into a condition of semi-equivalence.

**Definition 5** (Semi-Equivalence of Observations) Given a TAA and the fault under consideration $F$, two timed trajectories $\rho_F, \rho$, with $\rho_F$ containing $F$ and $\rho$ not containing $F$, are observationally semi-equivalent, if $P(\rho_F) \subseteq P(\rho)$.

Clearly, semi-equivalence is weaker than equivalence, since only the inclusion of timed observations is required instead of identity, the inclusion of timed trajectories being defined as follows: $\rho \subseteq \rho'$ means that $\rho$ is obtained from $\rho'$ by deleting certain events and summing the periods between successive events in the resulting sequence, i.e., all events in $\rho$ appear in $\rho'$ with the same time of occurrence. It should be noted that it would be pointless to define semi-equivalence in the other way, i.e., by including the observations of the normal trajectory into those of the faulty trajectory, as this requirement is trivially satisfied by taking as the normal trajectory any prefix of the faulty trajectory prior to the first occurrence of the fault (e.g., the empty trajectory).

Now, an under-approximation of the formula $\chi = CP(L, D, T, O)$, representing a parameterized critical pair that is being sought, is obtained by replacing the equivalence condition with a semi-equivalence in its verification (denoted $CP_\subseteq$, with the order relation $CP_\subseteq \prec CP$). A special case is obtained by choosing $D' = 0$ and $O' = O$, which boils down to finding a pair of faulty and normal timed trajectories such that the observations of the faulty trajectory are included in the observations of the normal trajectory. But semi-equivalence can also be used in conjunction with changes in the values of the $D$ and $O$ parameters. A general under-approximation of $\chi$ is then defined as $\chi' = CP'(L, D', T, O')$ with $CP' \subseteq CP$ (i.e., $CP' \in \{CP, CP_\subseteq\})$, $D' \le D, O' \subseteq O$ and a general refinement of $\chi'$ that remains an under-approximation of $\chi$ is defined as $\chi'' = CP''(L, D'', T, O'')$ with $CP' \subseteq CP'' \subseteq CP, D' \le D'' \le D, O' \subseteq O'' \subseteq O$. We see that the number of refinements is increased by at most one unit using the semi-equivalence condition.

The above analysis can be summed up as follows:

**Lemma 3** (Diagnosability checking with under-approximations)

1. (Under-approximation) Given a positive real number $\delta$ (unit of time), a current formula $\chi = CP(L, D, T, O)$ representing a parameterized $D-CP$, $D \in \delta\mathbb{N}$, with a length of at most $L$ constructed from a set of transitions $T \subseteq \delta^X$ and a set of observable events $O \subseteq \Sigma_o$, the formula $\tilde{\chi} = CP^0(L, D^0, T, O^0)$ with $CP^0 \preceq CP$ (i.e.,
$CP^0 \in \{CP, CP_\subseteq\}$, either identity or only inclusion of the observed faulty trajectory in the observed normal trajectory), $D^0 \in \delta\mathbb{N}$, $D^0 \le D$, $O_\subseteq^0 \subseteq O$ (at least one of the inequalities being strict) defines an under-approximation of $\chi$.

2. (Refinement process) Any sequence of formulas $\chi^n = CP^n(L, D^n, T, O_\subseteq^n)$, $n > 0$, with $CP^0 \le CP^n \le CP^{n+1} \le CP$, $D^n \in \delta\mathbb{N}$, $D^0 \le D^n \le D^{n+1} \le D$, $O_\subseteq^0 \subseteq O_\subseteq^n \subseteq O_\subseteq^{n+1} \subseteq O$ (at least one of the inequalities between the parameters of $\chi^n$ and $\chi^{n+1}$ being strict) defines a general refinement process of $\tilde{\chi}$, $\chi^n = refine^n(\tilde{\chi})$, i.e., every $\chi^n$ is an over-approximation of $\tilde{\chi}$ which remains an under-approximation of $\chi$, and $\chi^{n+1}$ is an over-approximation of $\chi^n$.

3. (Finiteness) This process is necessarily finite, bounded above by $\lfloor \frac{D}{\delta} \rfloor + |\Sigma_o| + 1$, reaching at worst formula $\chi$, and constitutes a sound and complete satisfiability checking procedure for $\chi$, regardless of the choice strategy of $CP^n, D^n, O_\subseteq^n$.

## 4.1 Counterexample analysis

Instead of the blind refinement process given in Lemma 3, we can, in the spirit of the CEGAR procedure, analyze the counterexample provided as a solution to $\chi^n$ in the case of satisfiability, in order to guide the next choice of formula $\chi^{n+1}$, if necessary. For this, the critical pair $(\rho_F, \rho)$ returned as a solution, with its three refinement parameters $CP^n, D^n, O_\subseteq^n$, is checked to see if there is evidence it is not a real solution of the original formula $\chi$, i.e., not a critical pair for the parameters $CP, D, O$. If this is the case, the analysis provides a way to refine these parameters in order to avoid an analog counterexample at the next refinement step. For reasons of efficiency, in this analysis we retain only the structure of the critical pair as two ordered sequences of transitions, and not the time valuations found for the correspondence of observations in the two trajectories. And we want both the checking of the solution and the definition of the refinement to be done without calling the SMT solver. We choose to examine parameters $CP^n, O_\subseteq^n$, and $D^n$ one by one in this order and to modify one single parameter in the next refinement, if any.

First, if semi-equivalence of observations is used in the current under-approximation, i.e., if $CP^n = CP_\subseteq$, we check whether the solution still holds using the identity of the ordered sequences of observations, i.e., the original parameter $CP$. If it does not hold, this proves that the solution found to $\chi^n$ is not a solution to the original problem and we refine $\chi^n$ using the identity of observations instead of semi-equivalence, i.e., $CP$ instead of $CP_\subseteq$. If it holds, we turn to the parameter $O_\subseteq^n$ and check whether the solution still holds using the original set $O$ of observable events instead of $O_\subseteq^n$. If the solution no longer holds, we select the first (in the ordered sequence) observable event from $O$ present in $\rho_F$ and not in $\rho$ and add it to $O_\subseteq^n$ to define the observable events for the next refinement. If the solution still holds, we repeat the same process using observation identity instead of semi-equivalence. We obviously start directly with this step if the identity (and not the semi-equivalence) of the observations was used in the current under-approximation. If the current solution has passed all these tests, this means that the sequences of all the original observable events from $O$ are identical in $\rho_F$ and $\rho$. We then turn to the third parameter, i.e., the time after fault occurrence. Considering
the invariant in the last state of the trajectory $\rho_F$ (and similarly for the trajectory $\rho$), we check whether this current time $D^n$ can be extended to the original time $D$ by simply staying longer in these last two states (remember that the time is extended by integer multiples of $\delta$). If this is not the case, the current solution is not a true solution of the original problem and we refine it by extending the value of $D^n$ to the minimal value that is not achievable by staying longer in the last two states while satisfying their invariants (i.e., the maximal achievable time incremented by $\delta$). If this is the case, it means that the current solution to $\chi^n$ is in fact a solution for the original problem $\chi$ (i.e., with parameters $CP, D$ and $O$), except that the identity of the observable events from $O$ in $\rho_F$ and $\rho$ does not take into account the time valuations in the two trajectories of these events that are not in $O^n$. In order to check whether the identity of the time valuations of these events is possible (i.e., whether the current under-approximated solution is a true solution of the original problem, i.e., whether the model is not $D$-diagnosable), we define the next and last refinement as the original formula $\chi$. Finally, the whole analysis can be written as follows:

If $CP^n = CP_\subseteq$, we check whether the ordered sequences of events from $O^\subseteq$ in faulty and normal trajectories are identical.

If not, the refinement $\chi^{n+1}$ is defined as $CP^{n+1} = CP, D^{n+1} = D^n, O^\subseteq = O^\subseteq$.

If so (resp., if $CP^n = CP$), we check whether the ordered sequence of events from $O$ in the faulty trajectory is included in (resp., is identical to) that in the normal trajectory.

If it is not conclusive, a minimal subset $O'$ of events, with $O^\subseteq \subset O' \subseteq O$, is chosen such that the ordered sequence of events from $O'$ in the faulty trajectory is not included in (resp., not identical to) that in the normal trajectory (in practice, we choose $O' = O^\subseteq \cup \{o\}$, where $o$ is the first (or one of the first two in the two trajectories) event from $O \setminus O^\subseteq$ which is at odds between the two ordered sequences), and the refinement $\chi^{n+1}$ is defined as $CP^{n+1} = CP^n, D^{n+1} = D^n, O^\subseteq = O'$.

If it is conclusive, and if $CP^n = CP_\subseteq$, we check whether the ordered sequences of events from $O$ in the faulty and normal trajectories are identical.

If this is not the case, the refinement $\chi^{n+1}$ is defined as $CP^{n+1} = CP, D^{n+1} = D^n, O^\subseteq = O'$.

If this is the case or if $CP^n = CP$, we check, by considering the invariant for the last state of each trajectory, whether the critical pair can satisfy, by staying longer in these two last states, an increase in the time ($D$ instead of $D^n$) after the fault appears in the faulty trajectory.

If this is the case, then the solution found satisfies all properties of a critical pair for the original problem, except that the identity of the time valuations of the events from $O \setminus O^\subseteq$ in the two trajectories has not been checked. This checking is done by defining the refinement $\chi^{n+1}$ as $CP^{n+1} = CP, D^{n+1} = D, O^\subseteq = O'$.

If not, a minimal $D' \in \delta\mathbb{N}$, with $D^n < D' \le D$, is determined in such a way that the current critical pair cannot reach the time $D'$ after fault by staying longer in the last two states and the refinement $\chi^{n+1}$ is defined as $CP^{n+1} = CP, D^{n+1} = D', O^\subseteq = O'$.

Algorithm 2 provides the pseudo-code for this analysis.
<caption>**Algorithm 2** Counterexample analysis and refinement in under-approximation</caption>

**input** : problem *CP*(*L*, *D*, *T*, *O*) solved by under-approximation
*χ*<sup>*n*</sup> formula coding *n*<sup>*th*</sup> refinement *CP*<sup>*n*</sup>(*L*, *D*<sup>*n*</sup>, *T*, *O*<sup>*n*</sup>)
counterexample returned *Check*(*χ*<sup>*n*</sup>) = (*ρ*<sub>*F*</sub>, *ρ*)
**output**: Refine(*χ*<sup>*n*</sup>)
**if** *CP*<sup>*n*</sup> = *CP*<sub>⊆</sub> **then**
  *result* ← *Check*(*ρ*<sub>*F*|*O*<sub>⊆</sub></sub> = *ρ*<sub>|*O*<sub>⊆</sub></sub>)
  **if not result then**
    **return** Refine(*χ*<sup>*n*</sup>) = *CP*(*L*, *D*<sup>*n*</sup>, *T*, *O*<sup>*n*</sup>)
  **else**
    *result* ← *Check*(*ρ*<sub>*F*|*O*</sub> ⊆ *ρ*<sub>|*O*</sub>)
    **if not result then**
      *o* ← FirstDisagreement(*ρ*<sub>*F*|*O*</sub> ⊆ *ρ*<sub>|*O*</sub>)
      **return** Refine(*χ*<sup>*n*</sup>) = *CP*<sub>⊆</sub>(*L*, *D*<sup>*n*</sup>, *T*, *O*<sup>*n*</sup> ∪ {*o*})
    **end**
  **end**
**end**
*result* ← *Check*(*ρ*<sub>*F*|*O*</sub> = *ρ*<sub>|*O*</sub>)
**if not result then**
  *o* ← FirstDisagreement(*ρ*<sub>*F*|*O*</sub> = *ρ*<sub>|*O*</sub>)
  **return** Refine(*χ*<sup>*n*</sup>) = *CP*(*L*, *D*<sup>*n*</sup>, *T*, *O*<sup>*n*</sup> ∪ {*o*})
**else**
  *D* ← max{*kδ* | it is possible to stay in *LastState*(*ρ*<sub>*F*</sub>) up to *kδ* after *F* occurrence and in *LastState*(*ρ*) up to the same global time}
  **if** *D* < *D* then
    **return** Refine(*χ*<sup>*n*</sup>) = *CP*(*L*, *D* + *δ*, *T*, *O*)
  **else**
    **return** Refine(*χ*<sup>*n*</sup>) = *CP*(*L*, *D*, *T*, *O*)
  **end**
**end**

It should be noted that none of these verification tests require a call to the SMT solver: they simply involve comparisons of sequences of events and an invariant analysis for the last states in the two trajectories of the critical pair, which represents a negligible computational cost. Obviously, a different order in the choice of the three parameters can be adopted.

It should also be noted that the choice to process parametric formulas implies all formulas and counterexamples have the same form (they all represent a critical pair) with different parameter values. Thus, the problem to be solved is always the same, and incremental use of SMT can be made, retaining the benefit of past deductions obtained during refinements, and fine control over parameters can be performed, which would not have been the case with blind under-approximation techniques, such as the random deletion of certain clauses in the conjunctive normal form formula.

# 5 A RECAR-like approach for bounded diagnosability analysis of RTS

CEGAR-over is generally efficient for early detection, through an over-approximations refinement loop, of the satisfiability of an original formula that is satisfiable (i.e., in our case, when the system is non-Δ-diagnosable). CEGAR-under is generally efficient for early detection, through an under-approximations refinement loop, of the unsatisfiability of an original formula that is in fact unsatisfiable (i.e., in our case, when the system is bounded Δ-diagnosable). However, CEGAR-over is not conclusive for an unsatisfiable original for-
mula, as long as refinement has not reached it, and CEGAR-under is not conclusive for a satisfiable original formula, as long as refinement has not reached it. In order to effectively check the diagnosability of a TA, we propose, inspired by the RECAR algorithm, to alternate between CEGAR-over and CEGAR-under during the search for a solution, i.e., to change the approximation type (from over- to under- or vice versa) of CEGAR when it can be estimated that this might be more efficient than continuing to refine the same type of formula. We call this method RECAR-like, because RECAR adopts a different recursive framework.

Figure 6 shows how the techniques of over-approximation (cf. Fig. 2) and under-approximation (cf. Fig. 4) can be interwoven to solve the diagnosability problem using an SMT solver. The SF switching function is a Boolean function that determines whether an alternation should take place, reflecting an estimate of the relative efficiency of continuing the current refinement process or changing the approximation type. For example, SF can make its decision by comparing the execution time of the current control in relation to a current waiting time or the ratio between the execution times of the current control and the previous control in relation to a current multiplicative threshold (see Algorithm 3 for pseudo-code examples).

<caption>**Algorithm 3** Switching function SF($\psi^n$), SF($\chi^n$)</caption>

input : $\xi = \psi$ or $\chi$, TimeToCheck($\xi^n$)
output: Boolean
result $\leftarrow$ (TimeToCheck($\xi^n$) > Timeout)
if (result and $\xi = \chi$) then Timeout $\leftarrow$ Timeout + Timeincrement
return result
input : $\xi = \psi$ or $\chi$, TimeToCheck($\xi^n$), TimeToCheck($\xi^{n-1}$)
output: Boolean
result $\leftarrow$ (TimeToCheck($\xi^n$) / TimeToCheck($\xi^{n-1}$) > Threshold)
if (result and $\xi = \chi$) then Threshold $\leftarrow$ Threshold $\times$ Factor
return result

The idea of our RECAR-like approach is therefore to alternate the two types of approximation and use the SF switching function to decide whether to switch from CEGAR-over to CEGAR-under or vice versa, otherwise to continue refining the over- or under-approximation until we get the result. *Under\_called* is also a Boolean function that indicates whether

<figure><img src="image_7.png" /><figcaption>**Fig. 6** RECAR-like framework for diagnosability checking</figcaption></figure>
the under-approximation has already been called (its value is false only during the first switch from over-approximation to under-approximation in order to initialize the under-approximation). After each switch from over- to under-approximation (resp., from under- to over-approximation), refinement continues from the last under- (resp., over-) approximation that was processed, and each switch from under- to over-approximation resets the allocated delay or threshold used in SF, increasing it by a given amount.

Algorithm 4 gives the pseudo-code of our approach, corresponding to Fig. 6. On lines 1 and 2, the Boolean *Under\_called* is set to *False* and the process is initialized with an over-approximation $\psi$ of the original formula $\phi$ whose satisfiability is studied (we chose to start with an over-approximation because it proves to be more efficient than the under-approximation). Then, on line 3, we enter a global refinement loop (from line 3 to line 27), which will end (in the absence of a timeout) either when a checking of the current formula is conclusive (lines 5 or 18), thus achieving a shortcut in the proof, or at worst when $\phi$ is reached (lines 6 or 19). The current over-approximated formula $\psi$ is checked for satisfiability on line 4. If the test is conclusive (satisfiable) we can conclude that $\phi$ is satisfiable, i.e., that the model is not $\Delta$-diagnosable (line 5). Otherwise, and if $\psi$ is not equivalent to $\phi$ (in which case $\phi$ is unsatisfiable and therefore the model is $\Delta$-diagnosable within the bound *B*, line 6), the switching function *SF* of Algorithm 3 is called on $\psi$ (line 7). If the switch condition is not yet met, $\psi$ is refined (line 7) and the algorithm iterates back to line 4. This refinement loop of the current over-approximated formula (line 7) continues as long as the conditions of the tests in lines 5 and 6 and of the switching are not satisfied. When the switching condition is satisfied (line 8) we switch to the under-approximation process. On the first switch, the condition on line 9 is satisfied and the process is initialized with an under-approximation $\chi$ of $\phi$ (line 10) and the Boolean *Under\_called* is set to *True* (line 11), which prevents the *then* block on lines 10-11 from being considered in the rest of the algorithm. Next, we set a Boolean *Cond* to *True* (line 15), which is the condition for entering line 16 in the local refinement loop (from line 16 to line 25) of the current under-approximated formula, analogous to the over-approximation refinement loop. The current under-approximated formula $\chi$ is checked for satisfiability at line 17. If the test is conclusive (unsatisfiable) we can conclude that $\phi$ is unsatisfiable, i.e., the model is $\Delta$-diagnosable within *B* (line 18). Otherwise, and if $\chi$ is not equivalent to $\phi$ (in which case $\phi$ is satisfiable and therefore the model is not $\Delta$-diagnosable, line 19), the switching function *SF* is called on $\chi$ (line 20). If the switching condition is not yet satisfied, $\chi$ is refined on line 20 and the algorithm iterates on line 17. This refinement loop of the current under-approximated formula (line 20) continues as long as the conditions of the tests on lines 18 and 19 and of the switching are not satisfied. When the switching condition is satisfied (line 21) we switch to the over-approximation process: the current over-approximated formula $\psi$ is refined (line 22), we exit the under-approximation refinement loop by setting *Cond* to *False* (line 23) and continue the over-approximation process at line 4. ON the next switch to the under-approximation process (line 8), we now begin (line 12) by refining the current under-approximated formula $\chi$ (line 13) before entering the under-approximation refinement loop on line 16.
<caption>**Algorithm 4** RECAR-like algorithm for verifying bounded diagnosability</caption>

input : original formula $\phi$ coding logically a bounded $\Delta$-$CP$ for A
output : check whether $\phi$ is satisfiable, i.e., A non-$\Delta$-diagnosable
1 Under叫叫= False
2 $\psi \leftarrow$ OverApprox($\phi$)
3 while True do
4 $result \leftarrow$ Check($\psi$)
5 if result then return "the model is not $\Delta$-diagnosable"
6 if EquivCheck($\psi, \phi$) then return "the model is $\Delta$-diagnosable"
7 if not SF($\psi$) then $\psi \leftarrow$ Refine($\psi$)
8 else
9 | if not Under叫叫 then
10 | $\chi \leftarrow$ UnderApprox($\phi$)
11 | Under叫叫= True
12 else
13 | $\chi \leftarrow$ Refine($\chi$)
14 end
15 Cond= True
16 while Cond do
17 $result \leftarrow$ Check($\chi$)
18 if not result then return "the model is $\Delta$-diagnosable"
19 if EquivCheck($\chi, \phi$) then return "the model is not $\Delta$-diagnosable"
20 if not SF($\chi$) then $\chi \leftarrow$ Refine($\chi$)
21 else
22 | $\psi \leftarrow$ Refine($\psi$)
23 | Cond= False
24 end
25 end
26 end
27 end

From the definitions and properties of the refinements set out above, it is clear that this
RECAR-like method is sound, complete, and terminating, as long as the *checking* function
(in our case, the Z3 solver) is a sound and complete implementation of *isSAT* (and therefore
also of *isUNSAT*) that terminates. This is in fact a consequence of the following properties:

1. isSAT($\hat{\phi}$) implies isSAT(refine($\hat{\phi}$)).

2. isUNSAT($\hat{\phi}$) implies isUNSAT(refine($\check{\phi}$)).

3. There exists $n \in \mathbb{N}$ such that $refine^n(\hat{\phi}) = \phi$ and $refine^n(\check{\phi}) = \phi$.

4. isUNSAT($\check{\phi}$) implies isUNSAT($\phi$) and isSAT($\hat{\phi}$) implies isSAT($\phi$).

1. results from Lemma 2 (refine($\hat{\phi}$)) is an under-approximation of $\hat{\phi}$; 2. results from Lemma 3 (refine($\check{\phi}$)) is an over-approximation of $\check{\phi}$; 3. results from the two lemmas: both refinement processes end, because the parameter space defining the set of possible refined formulas for each process is finite; 4. is a consequence of the first three points.

In total, the RECAR-like refinement process is as follows:

$$
\begin{align*}
\check{\phi} &\subseteq \text{refine}^1(\hat{\phi}) \subseteq \dots \subseteq \text{refine}^{k1}(\hat{\phi}) \quad \text{SF}(\text{refine}^{k1}(\hat{\phi})) \\
\check{\phi} &\supseteq \text{refine}^1(\check{\phi}) \supseteq \dots \supseteq \text{refine}^{l1}(\check{\phi}) \quad \text{SF}(\text{refine}^{l1}(\check{\phi})) \\
\text{refine}^{k1+1}(\check{\phi}) &\subseteq \dots \subseteq \text{refine}^k(\check{\phi}) \quad \text{SF}(\text{refine}^k(\check{\phi})) \\
\text{refine}^{l1+1}(\check{\phi}) &\supseteq \dots \supseteq \text{refine}^{l2}(\check{\phi}) \quad \text{SF}(\text{refine}^{l2}(\check{\phi}))
\end{align*}
$$

$$
refine^{k+n+1}(\hat{\phi}) \subseteq \dots \subseteq refine^m(\hat{\phi}) = \phi \text{ or}
$$

$$
refine^{l+n+1}(\check{\phi}) \supseteq \dots \supseteq refine^m(\check{\phi}) = \phi,
$$
reaching at worst the initial formula $\phi$ in a finite number of steps.

The above analysis of the RECAR-like refinement process, together with the results of Lemma 2 concerning its over-approximation part and Lemma 3 concerning its under-approximation part can be summarized in the following main result which grounds our approach:

**Proposition 4 (Diagnosability checking with over- and under-approximations)**

1. (Over-and under-approximations) Given as input an original formula $\phi = CP(B, \Delta, \delta^X, \Sigma_o)$ representing a $\Delta$-CP of maximal length $B$ constructed from a set of transitions $\delta^X$ and a set of observable events $\Sigma_o$ of a TA A, and a positive real number $\delta$ (unit of time): the formula $\psi^0 = CP(L^0, \Delta, T^0, O_+^0)$ with $L^0 \le B, T^0 \le \delta^X, O_+^0 \supseteq \Sigma_o$ (at least one of the inequalities being strict) defines an over-approximation $\tilde{\phi}$ of $\phi$, the formula $\chi^0 = CP^0(B, D^0, \delta^X, O_-^0)$ with $CP^0 \in \{CP, CP_\subseteq\}, CP^0 \not\subseteq CP, D^0 \in \delta\mathbb{N}, D^0 \le \Delta, O_-^0 \subseteq \Sigma_o$ (at least one of the inequalities being strict) defines an under-approximation $\tilde{\phi}$ of $\phi$.

2. (Double-refinement process) Any sequence of formulas $\{\{\psi^n\}_{0\le n\le k_1}, \{\chi^n\}_{0\le n\le l_1}, \{\psi^n\}_{k_1+1\le n\le k_2}, \{\chi^n\}_{l_1+1\le n\le l_2}, \dots, \{\psi^n\}_{k_i+1\le n\le k_{i+1}}, \{\chi^n\}_{l_i+1\le n\le l_{i+1}}, \dots\}$ with: $\psi^n = CP(L^n, \Delta, T^n, O_+^n)$, $L^n \le O_+^n \le T^n \le B, T^0 \subseteq T^n \subseteq T^{n+1} \subseteq \delta^X, O_+^0 \supseteq O_-^n \supseteq O_+^{n+1} \supseteq \Sigma_o$ (at least one of the inequalities between the parameters of $\psi^n$ and $\psi^{n+1}$ being strict), $\chi^n = CP^n(B, D^n, \delta^X, O_-^n)$, with $CP^n \in \{CP, CP_\subseteq\} \subseteq CP^{n+1} \subseteq CP, D^n \in \delta\mathbb{N}, D^0 \le D^n \le D^{n+1} \le \Delta, O_0^0 \subseteq O_n^0 \subseteq O_-^{n+1} \subseteq \Sigma_o$ (at least one of the inequalities between the parameters of $\chi^n$ and $\chi^{n+1}$ being strict), defines a general (RECAR-like) double-refinement process: $\psi^n = refine^n(\tilde{\phi})$, i.e., each $\psi^n$ is an under-approximation of $\tilde{\phi}$ which remains an over-approximation of $\phi$, and $\psi^{n+1}$ is an under-approximation of $\psi^n$, $\chi^n = refine^n(\tilde{\phi})$, i.e., each $\chi^n$ is an over-approximation of $\tilde{\phi}$ which remains an under-approximation of $\phi$, and $\chi^{n+1}$ is an over-approximation of $\chi^n$.

3. (Finiteness) This process is necessarily finite, bounded above by $B + \lfloor \frac{\Delta}{\delta} \rfloor + |\delta^X| + |\Sigma \setminus \Sigma_f| + 1$, reaching at worst formula $\phi$, and constitutes a sound and complete satisfiability checking procedure for $\phi$, whatever the choice strategy of $CP^n, L^n, D^n, T^n, O_+^n, O_-^n$ and of the switching function between $\{\psi^n\}$ and $\{\chi^n\}$ subsequences.

# 6 Encoding RECAR-like approach

In this section, we show how to encode our RECAR-like approach (the Z3 SMT solver was used for formula verification and Python for the rest of the code). First, as mentioned above, we encode TA and a $\Delta$-CP as logical formulas, following the classical SAT implementation (Grastien et al. 2007; Rintanen and Grastien 2007) extended to SMT to handle time constraints (details are provided in He et al. (2018)). In particular, an additional global clock, i.e., that is never reset, is used in the code, enabling to easily handle multiple clocks within time constraints. As the CEGAR algorithm consists in an iteration process, we use selectors to choose the values of the modifiable parameters in SMT to support incremental processing of refinements. The code and experiments (see Section 7 below) are available on GitHub at the address https://github.com/ailxxxx/RECAR.
## 6.1 Pre-processing

Before the CEGAR and RECAR-like methods are encoded, the system data is pre-processed to improve efficiency.

1. Given a TA, an Index is defined and its value pre-computed for each transition, representing the shortest path length between the initial state and the source state of that transition. In this way, during the process of searching for a D-CP with a length bound L, Z3 is required to consider only admissible transitions, i.e., transitions whose index is not greater than L, thus reducing the search space.

2. System A's fault diagnoser and normal diagnoser for fault F are pre-computed and their transitions indexed as above so that Z3 searches for transitions for the faulty (resp., normal) trajectory of the D-CP only among the admissible transitions of the fault (resp., normal) diagnoser. Recall that A's diagnoser for F is obtained from A by labeling each state with its Faulty (resp., Normal) fault status according to whether F occurs (resp., does not occur) in any path from the initial state to the state in question (thus, if F occurs in at least one such path and does not occur in at least one other such path, the state is divided into two states, one with the Faulty label and the other with the Normal label). The normal (resp., fault) diagnoser is the sub-diagnoser whose states are all Normal states (resp., all Faulty states plus Normal states belonging to a path from the initial state to a Faulty state).

## 6.2 Encoding of modifiable parameters

In our RECAR-like approach using both over- and under-approximations, we have seen that we play with the parameters L, D, T, O (initialized to their respective values B, Δ, δ^X, Σ_o in the initial problem), whose values must be able to be modified in the various refinement loops. We show below how these values are chosen and how they are defined in the Z3 SMT solver using so-called selectors.

**Length bound L** Given {$n_i$} the possible integer values of L in the over-approximation of the initial problem and its successive refinements (corresponding to increasing $n_i$'s, at most B in number), we use a formula that associates a fresh variable $l_i$ (a selector) with each value $n_i$. In the over-approximation and its refinements, L is therefore set by Z3 to the given value $n_i$ by setting $l_i$ to True (the $l_j$'s, $j \neq i$, are then automatically set to False, since L has only one value). This is encoded as follows:

$$ \bigwedge_i ((L = n_i) \lor \neg l_i) \text{ with } n_i \in \mathbb{N}, 1 \le n_i \le B. $$

**Time after fault occurrence D** Given {$t_i$} the finite set of possible values of D that we selected in the under-approximation of the initial problem and its successive refinements (corresponding to increasing $t_i$'s, integer multiples of $\delta$, at most $\lfloor \frac{\Delta}{\delta} \rfloor$ in number), we use a formula that associates a fresh variable $d_i$ (a selector) with each value $t_i$. In the under-approximation and its refinements, D is set by Z3 to the given value $t_i$ by setting $d_i$ to True (and thus the $d_j$'s, $j \neq i$, to False). This is encoded as follows:
$$ \bigwedge_{i} ((D = t_i) \lor \neg d_i) \text{ with } t_i \in \delta\mathbb{N}, \delta \le t_i \le \Delta. $$

**Transition set T** We associate a fresh variable (selector) $tr_i$ with each transition, $trans_i \in \delta^X$, of the system. In the over-approximation of the initial problem and its successive refinements (corresponding to increasing $T$'s, at most equal in number to $|\{tr \in \delta^X | Index(tr) \le B\}|$), $T$ is set by Z3 to a given subset of $\delta^X$ by setting $tr_i$ to True for all $trans_i$ transitions that belong to this subset and $tr_j$ to False for all $trans_j$ transitions that do not belong to this subset. Bearing in mind that only transitions whose pre-computed index is not greater than the current value of the length bound $L$, must be taken into account, the formula is finally encoded as follows:

$$ \bigwedge_{trans_i \in \delta^X} ((trans_i \in T) \lor \neg (Index(trans_i) \le L) \lor \neg tr_i). $$

**Set of observable events O** To make observable events modifiable, we associate a fresh variable (selector) $o_i$ with each event $e_i \in \Sigma \setminus \Sigma_f$. $O$ is set by Z3 to a given subset of $\Sigma \setminus \Sigma_f$ (which contains $\Sigma_o$ in the case of an over-approximation $O_+$ and its successive refinements corresponding to decreasing $O_+$'s, in number at most equal to $|\Sigma_u|$, or is included in $\Sigma_o$ in the case of an under-approximation $O_-$ and its successive refinements corresponding to increasing $O_-$'s, in number at most equal to $|\Sigma_o|$) by setting $o_i$ to True for all events $e_i$ that belong to this subset (so, in particular for all $e_i \in \Sigma_o$ for over-approximations) and $o_j$ to False for all events $e_j$ that do not belong to this subset (so, in particular for all $e_i \in \Sigma_u$ for under-approximations). This is encoded as follows:

$$ \bigwedge_{e_i \in \Sigma \setminus \Sigma_f} ((e_i \in O) \lor \neg o_i). $$

## 6.3 Refinement strategies

Below, we explain the refinement strategies, linked to each parameter, that are used in the experiments, i.e., how the initial values of the parameters defining the first over- or under-approximation are chosen and how their changes are fixed in the successive refinements.

*   **Length bound $L$.** In CEGAR-over, $L$ is initialized to 1, i.e., $n_1 = 1$, then at each refinement step, the value of $L$ is increased by 1, i.e. $n_{i+1} = n_i + 1$, until the satisfiable conclusion is reached, or until $n_B = B$ (in which case, the verdict of satisfiability is the result returned by Z3). There are therefore at most $B-1$ refinements. In CEGAR-under, $L$ is fixed at $B$ ($L = B$) and there are no refinements.

*   **Time after fault occurrence $D$.** The unit of time is assumed to be given by $\delta$, i.e., $\delta = 1$ and all values of $D$ are therefore positive integers. In CEGAR-under, $D$ is initialized to (the integer part of) a tenth of the initial $\Delta$ (if $\Delta \ge 10$), i.e., $t_1 = \Delta \text{ div } 10$ and then, at each refinement step, the value of $D$ is increased by default by this quantity, i.e., $t_{i+1} = t_i + t_1 = (i+1)t_1$, until we obtain the unsatisfiable conclusion, or until reaching $t_{11} = t_{10} + \Delta \text{ mod } 10 = \Delta$ (in which case the verdict of satisfiability is the result
returned by Z3). If $\Delta < 10$, we choose by default $t_1 = 1$ and $t_{i+1} = t_i + t_1 = (i+1)$. In this way, we can guarantee that refinement occurs at most 10 times. If a counterexample analysis is performed, the updated value of $D$ at each refinement step is taken equal to the minimum integer such that the critical pair returned as a counterexample cannot reach a time $D$ after fault by simply remaining longer in its final states in both trajectories. In CEGAR-over, $D$ is fixed at $\Delta$ ($D = \Delta$) and there is no refinement.

*   *Transition set* $T$. In CEGAR-over, $T$ is initialized to a nonempty subset of size $k_1$ of these transitions in $\delta^X$ within $B$, i.e., whose index is not greater than $B$ (e.g., 10% of them, i.e., $k_1 = |T| \div 10$, chosen randomly), then at each refinement step, $k_1$ more (randomly chosen) of these transitions are added to $T$, until we reach the satisfiable conclusion, or until $T$ is equal to the set of transitions within $B$ (in which case the satisfiability verdict is the result returned by Z3). In this way, refinement occurs a maximum of 10 times. If the parameters $T$ and $L$ are mixed in the definition of the over-approximation and its refinements, $T$ is initialized to a nonempty subset of those transitions in $\delta^X$ within $n_1$ (the initial value of $L$), then at each refinement step, a nonempty subset of new transitions within $n_i$ (the current value of $L$ in this refinement) is added to $T$. In CEGAR-under, $T$ is fixed at the subset of $\delta^X$ within $B$ and there is no refinement.

*   *Set of observable events* $O$. In CEGAR-over, $O$ is initialized to $\Sigma \setminus \Sigma_f$, i.e., treating all unobservable normal events as observable events, then, at each refinement step, we remove an unobservable event (the first remaining in random order in $\Sigma_u$) from $O$, until we reach the satisfiable conclusion, or until $O = \Sigma_o$ (in which case the verdict of satisfiability is the result returned by Z3). There are therefore at most $|\Sigma_u|$ refinement steps. In CEGAR-under, $O$ is initialized to a single observable event (the first according to a random order in $\Sigma_o$), then at each refinement step, we add another observable event to $O$ (by default, the first remaining according to the previous order; if a counterexample analysis is performed, the first, or one of the first two, that differs in the ordered sequences of observable events from the faulty and normal trajectories of the critical pair returned as the counterexample), until we obtain the unsatisfiable result or until $O = \Sigma_o$ (in which case the satisfiability verdict is the result returned by Z3). There are therefore at most $|\Sigma_o| - 1$ refinement steps.

As usual, our bounded model checking approach can verify non-Δ-diagnosability (SAT case), since bounded non-Δ-diagnosability implies non-Δ-diagnosability. It should be noted, however, that bounded Δ-diagnosability (UNSAT case), does not imply Δ-diagnosability, as the problem could become SAT when we increase the given length bound $B$.

# 7 Experiments

We carried out all the experiments under the same experimental conditions: running the prototype implementation in Python and the Z3 SMT solver on a Mac OS laptop with an Intel Core i5 processor running at 2.7 GHz and 8 GB 1600 MHz DDR3 memory.

We present several versions of four benchmarks from the literature, which have been modified to obtain diagnosable and non-diagnosable versions. In addition, in order to demonstrate the scalability of the approach and given that these examples from the literature are normally quite small, we tested hand-crafted versions of these examples where the state
space was generated in a partially random way while keeping the diagnosability verdicts the same. The first group of examples *hvac*<sub>i</sub> is inspired by the HVAC system from Sampath et al. (1995), modeled as a finite automaton, to which we have added various time constraints and an arbitrary number of events so that the verdict remains the same with increasing TA size. *hvac*<sub>2</sub> is a version modified by the addition of a clock to constrain the *valve\_closing* event so that the corresponding delay is always different for a normal trajectory and for a faulty trajectory, thus ensuring system diagnosability. Then, by modifying this delay on faulty trajectories, the system becomes non-diagnosable, as shown in example *hvac*<sub>1</sub>. Similarly, the second group of examples, denoted by *jiang*<sub>i</sub>, is obtained by extending the finite automaton of Jiang et al. (2001) with time constraints. The third group of examples, *zbrz*<sub>i</sub>, is obtained from Zbrzezny and Półrola (2007) and the fourth group of examples *lee*<sub>i</sub> consists of models of traffic light controllers at a crosswalk, obtained from Lee and Seshia (2016). The original examples in these last two groups were already TA and we have only modified them into two versions, one non-diagnosable and the other diagnosable, and enlarged them to ensure scalability. Finally, the fifth and last group of examples, designated *ex*<sub>i</sub>, is designed entirely by hand for testing structurally complex systems, i.e., TA with many cycles.

Tables 1 and 2 show the effect of optimization due to pre-processing, mainly transition indexing (see Subsection 6.1). The experiments are carried out only on the first and fifth groups of examples but with six *hvac*<sub>i</sub> examples from the first group of increasing complexity. The 2nd column indicates the value chosen for the length bound *B* of the critical pair; the 3rd indicates the given value of the time Δ after the occurrence of the fault, a parameter of the critical pair; the 4th indicates the size of the logical formula encoding the existence of a Δ-critical pair expressed by its number of clauses; the 5th is the memory required in MB; the 6th gives, in Table 1, the total number of transitions in the system and, in Table 2, the

<table><caption>**Table 1** Experimental results before optimization</caption><thead><tr><th></th><th><em>B</em></th><th>Δ</th><th>|clauses|</th><th>memory</th><th>|transitions|</th><th>time</th><th>SAT?</th></tr></thead><tbody><tr><td><em>hvac</em><sub>1</sub></td><td>9</td><td>6</td><td>345756</td><td>33</td><td>15</td><td>26</td><td>Yes</td></tr><tr><td><em>hvac</em><sub>2</sub></td><td>5</td><td>3</td><td>496963</td><td>69</td><td>15</td><td>30</td><td>No</td></tr><tr><td><em>hvac</em><sub>3</sub></td><td>9</td><td>5</td><td>465393</td><td>52</td><td>15</td><td>21</td><td>Yes</td></tr><tr><td><em>hvac</em><sub>4</sub></td><td>6</td><td>3</td><td>737395</td><td>63</td><td>15</td><td>39</td><td>No</td></tr><tr><td><em>hvac</em><sub>5</sub></td><td>15</td><td>7</td><td>1353321</td><td>75</td><td>156</td><td>152</td><td>Yes</td></tr><tr><td><em>hvac</em><sub>6</sub></td><td>7</td><td>6</td><td>1709069</td><td>129</td><td>156</td><td>306</td><td>No</td></tr><tr><td><em>ex</em><sub>1</sub></td><td>21</td><td>15</td><td>246563</td><td>21</td><td>123</td><td>21</td><td>Yes</td></tr><tr><td><em>ex</em><sub>2</sub></td><td>9</td><td>6</td><td>903296</td><td>285</td><td>123</td><td>135</td><td>No</td></tr></tbody></table>

<table><caption>**Table 2** Experimental results after optimization</caption><thead><tr><th></th><th><em>B</em></th><th>Δ</th><th>|clauses|</th><th>memory</th><th>|transitions within <em>B</em>|</th><th>time</th><th>SAT?</th></tr></thead><tbody><tr><td><em>hvac</em><sub>1</sub></td><td>9</td><td>6</td><td>345756</td><td>33</td><td>15</td><td>26</td><td>Yes</td></tr><tr><td><em>hvac</em><sub>2</sub></td><td>5</td><td>3</td><td>172836</td><td>16</td><td>11</td><td>13</td><td>No</td></tr><tr><td><em>hvac</em><sub>3</sub></td><td>9</td><td>5</td><td>465393</td><td>52</td><td>15</td><td>21</td><td>Yes</td></tr><tr><td><em>hvac</em><sub>4</sub></td><td>6</td><td>3</td><td>362738</td><td>43</td><td>12</td><td>16</td><td>No</td></tr><tr><td><em>hvac</em><sub>5</sub></td><td>15</td><td>7</td><td>701523</td><td>39</td><td>30</td><td>69</td><td>Yes</td></tr><tr><td><em>hvac</em><sub>6</sub></td><td>7</td><td>6</td><td>253648</td><td>31</td><td>16</td><td>22</td><td>No</td></tr><tr><td><em>ex</em><sub>1</sub></td><td>21</td><td>15</td><td>174536</td><td>17</td><td>28</td><td>16</td><td>Yes</td></tr><tr><td><em>ex</em><sub>2</sub></td><td>9</td><td>6</td><td>146328</td><td>14</td><td>16</td><td>12</td><td>No</td></tr></tbody></table>
number of these transitions whose index is not greater than *B*; the 7th gives the execution time in seconds (including, in Table 2, the pre-processing time for computing the transitions whose index is not greater than *B*) and the 8th provides the satisfiability verdict (so, the Δ-diagnosability verdict is the opposite). Comparison of the two tables shows the advantage of our optimization, due to the pre-processing step, on reducing the search space (6th column), the formula size (4th column), and therefore the memory required (5th column) and finally the execution time (7th column). Note that the optimization effect becomes more obvious with larger state spaces. The experimental results demonstrate the feasibility and effectiveness of this optimization, which will be applied in all subsequent experiments.

Table 3 shows the effect of the counterexample analysis presented in Subsection 4.1. The number of refinements and execution time are given successively in the absence of counter-example analysis, with a fixed refinement strategy (columns 2 and 3), with counterexample analysis to choose the new observable event to add for the next refinement (columns 4 and 5), and with counterexample analysis with choice of the next observable event or extension of time *D* after the fault has occurred (columns 6 and 7). We observe a reduction in the number of refinements (and therefore execution time) for a single UNSAT example in the second case, but for another UNSAT example (which means a faster UNSAT shortcut) and all five SAT examples (which means that a counterexample is returned after some refinements, which turns out to be a true solution to the original problem, i.e., time after the fault occurrence can be extended to the original Δ on this example) in the third case.

Now, to demonstrate the feasibility of our algorithm, we compare our RECAR-like approach with a pure CEGAR-over approach and with a pure CEGAR-under approach with different refinement strategies, as well as with the direct method that uses no approximation (all with the above optimization). The results are presented in Tables 4 and 5. For case of comparison, the first five columns and the last three columns are identical. The first column shows the five groups of two examples (one diagnosable, the other not). The 2nd, 3rd, and 4th columns give the values of the length bound *B* and of the time Δ after fault occurrence as parameters of the initial problem and the total number of system transitions, respectively. The 5th column gives the execution time in seconds of the direct Δ-diagnosability check without using CEGAR. At the other end of the tables, the last four columns give the execution time of the Δ-diagnosability check using our RECAR-like approach (based on alternating *Over*<sub>all</sub> and *Under*<sub>all</sub>, see below), the corresponding number of switches (calls to

<table><caption>**Table 3** Experimental results for CEGAR-under without or with counterexample analysis</caption><thead><tr><th rowspan="2"></th><th colspan="2">No counterexample analysis</th><th colspan="2">Counterexample analysis<br>Increase O<sub>-</sub></th><th colspan="2">Counterexample analysis<br>Increase O<sub>-</sub> and D</th><th rowspan="2">SAT?</th></tr><tr><th>| refinements | Time</th><th></th><th>| refinements | Time</th><th></th><th>| refinements | Time</th><th></th></tr></thead><tbody><tr><td><i>hvac<sub>1</sub></i></td><td>9</td><td>22.31</td><td>9</td><td>22.31</td><td>3</td><td>15.32</td><td>Yes</td></tr><tr><td><i>hvac<sub>2</sub></i></td><td>3</td><td>6.55</td><td>2</td><td>4.32</td><td>2</td><td>4.31</td><td>No</td></tr><tr><td><i>jiang<sub>1</sub></i></td><td>9</td><td>24.21</td><td>9</td><td>24.20</td><td>3</td><td>14.33</td><td>Yes</td></tr><tr><td><i>jiang<sub>2</sub></i></td><td>2</td><td>5.33</td><td>2</td><td>5.33</td><td>2</td><td>5.33</td><td>No</td></tr><tr><td><i>zbrz<sub>1</sub></i></td><td>9</td><td>3.63</td><td>9</td><td>3.62</td><td>2</td><td>0.99</td><td>Yes</td></tr><tr><td><i>zbrz<sub>2</sub></i></td><td>2</td><td>3.22</td><td>2</td><td>3.23</td><td>2</td><td>3.22</td><td>No</td></tr><tr><td><i>lee<sub>1</sub></i></td><td>9</td><td>3.20</td><td>9</td><td>3.19</td><td>3</td><td>1.01</td><td>Yes</td></tr><tr><td><i>lee<sub>2</sub></i></td><td>3</td><td>142.17</td><td>3</td><td>129.33</td><td>3</td><td>133.32</td><td>No</td></tr><tr><td><i>ex<sub>1</sub></i></td><td>9</td><td>9.55</td><td>9</td><td>9.54</td><td>5</td><td>6.55</td><td>Yes</td></tr><tr><td><i>ex<sub>2</sub></i></td><td>7</td><td>200.36</td><td>7</td><td>193.22</td><td>4</td><td>74.08</td><td>No</td></tr></tbody></table>
<table><caption>**Table 5** Experimental results for CEGAR-under vs. RECAR-like</caption><thead><tr><th></th><th>B</th><th>Δ</th><th>|trans.|</th><th>Direct</th><th>UnderD</th><th>UnderO</th><th>Underail</th><th>|ref<sup>ts</sup>|</th><th>RECAR</th><th>|swies|</th><th>|ref<sup>ts</sup>|</th><th>SAT?</th></tr></thead><tbody><tr><td>hvac1</td><td>50</td><td>50</td><td>500</td><td>6.57</td><td>25.65</td><td>38.33</td><td>15.32</td><td>3</td><td>0.33</td><td>0</td><td>4</td><td>Yes</td></tr><tr><td>hvac2</td><td>50</td><td>50</td><td>500</td><td>4.4</td><td>7.94</td><td>7.45</td><td>4.31</td><td>2</td><td>2.50</td><td>0</td><td>50</td><td>No</td></tr><tr><td>jiang1</td><td>50</td><td>50</td><td>500</td><td>5.15</td><td>30.12</td><td>28.33</td><td>14.33</td><td>3</td><td>0.10</td><td>0</td><td>3</td><td>Yes</td></tr><tr><td>jiang2</td><td>50</td><td>50</td><td>500</td><td>1.77</td><td>2.01</td><td>3.13</td><td>5.33</td><td>2</td><td>2.11</td><td>0</td><td>50</td><td>No</td></tr><tr><td>zbrz1</td><td>30</td><td>30</td><td>500</td><td>1.55</td><td>4.04</td><td>6.15</td><td>0.99</td><td>2</td><td>0.03</td><td>0</td><td>2</td><td>Yes</td></tr><tr><td>zbrz2</td><td>30</td><td>30</td><td>500</td><td>1.56</td><td>3.50</td><td>3.33</td><td>3.22</td><td>2</td><td>0.66</td><td>0</td><td>30</td><td>No</td></tr><tr><td>lee1</td><td>23</td><td>23</td><td>450</td><td>1.08</td><td>3.20</td><td>4.32</td><td>1.01</td><td>3</td><td>0.04</td><td>0</td><td>3</td><td>Yes</td></tr><tr><td>lee2</td><td>23</td><td>23</td><td>450</td><td>141.12</td><td>45.77</td><td>&gt;500</td><td>133.32</td><td>3</td><td>144.31</td><td>5</td><td>14</td><td>No</td></tr><tr><td>ex1</td><td>20</td><td>16</td><td>34</td><td>3.85</td><td>15.56</td><td>9.78</td><td>6.55</td><td>5</td><td>0.46</td><td>0</td><td>10</td><td>Yes</td></tr><tr><td>ex2</td><td>20</td><td>16</td><td>34</td><td>217.97</td><td>344.32</td><td>202.17</td><td>74.08</td><td>4</td><td>187.73</td><td>5</td><td>9</td><td>No</td></tr></tbody></table>
$SF$) between over-approximation and under-approximation, or inverse, the total number of refinements and diagnosability verdict, respectively.

In its central part (6th to 10th columns), Table 4 shows some of our experimental results for CEGAR-over with different over-approximations. The 6th, 7th and 8th columns give the CEGAR-over execution time in seconds for approximations defined by the single parameter *Length bound L*, *Transition set T* and *Set of observable events O*, respectively; the 9th and 10th columns give the CEGAR-over execution time and number of refinements with a combination of these three parameters. The execution time of CEGAR-over techniques is obtained by adding the execution time of the first over-approximation chosen and those of each successive refinement of this approximation until the verdict is reached.

In the middle (6th to 9th columns), Table 5 shows some of our experimental results for CEGAR-under with different under-approximations. The 6th and 7th columns give the execution time of CEGAR-under for approximations defined by the single parameter *Time after fault occurrence D* and *Set of observable events O*, respectively; the 8th and 9th columns give the execution time and number of refinements of CEGAR-under with a combination of these two parameters (plus possibly the use of semi-equivalence of observations instead of equivalence) and analysis of the counterexample. The execution time of CEGAR-under techniques is obtained by adding the execution time of the first under-approximation chosen and those of each successive refinement of this approximation until the verdict is reached.

# 8 Results and discussion

The experimental results in Tables 4 and 5 show, as expected, that CEGAR-over techniques with over-approximations parameterized with the appropriate coefficients speed up the verification of satisfiable instances, while slowing down the verification of most unsatisfiable instances. Unfortunately, CEGAR-under techniques with under-approximations are inefficient not only (as expected) for satisfiable instances, but also (which was not expected) for unsatisfiable ones. This is the key factor in the ineffectiveness of RECAR-like approaches. We summarize and analyze these data in more detail below.

Firstly, CEGAR-over with the single parameter *Length bound L* performs as well as CEGAR-over with three mixed parameters *Length bound L*, *Transition set T* and *Observable event set O* on all benchmarks and better than the direct method (without using CEGAR) on satisfiable instances (with little refinement in this case), but worse than the direct method on most unsatisfiable instances, especially the larger ones (with a lot of refinement as over-approximations have to be refined back to the initial problem). However, CEGAR-over with the single parameter *Observable event set O* underperforms both the above over-approximations and the direct method on all benchmarks. This is also the case for CEGAR-over with the single parameter *Transition set T* on most benchmarks. Secondly, CEGAR-under does not perform well on all benchmarks, even on unsatisfiable instances. The performance of CEGAR-under with the *Time after fault occurrence* parameter, with the *Observable event set O* parameter, and with these two mixed parameters is comparable to and worse than that of the direct method. This is normal for satisfiable instances, as they require numerous under-approximations refinements until the initial problem is reached, but unexpected a priori for unsatisfiable instances where the number of refinements is low.
The key factor in complexity, and therefore non-efficiency, seems to be the *length bound* of the critical pair being sought, and therefore the size of the formula whose satisfiability is being checked. For over-approximations, this length bound *L* is a parameter that can be considerably reduced and can lead to a SAT shortcut for satisfiable instances (in fact the over-approximation based on *L* is by far the most efficient of the three over-approximations based on a single parameter). But for the under-approximations, this length must be maintained at the initial value *B* given for the length bound, which brings no improvement even for unsatisfiable instances (although there are few refinements, solving each of them with the same value *B* for *L* is too costly and the total time to solve all these refinements therefore exceeds the time needed to solve the initial problem directly). This probably explains why CEGAR-under remains ineffective for unsatisfiable instances.

Let's now look at the results of our RECAR-like approach. For satisfiable instances, the RECAR-like algorithm does not switch and continues to run in CEGAR-over mode, with the same performance as CEGAR-over (with over-approximations combining all three parameters), so better than the direct method, as expected. For unsatisfiable instances, either RECAR-like does not switch and continues to run in CEGAR-over mode (case of the first three instances), with performance like CEGAR-over and similar to or slightly better than that of the direct method or it switches several times between over-approximations and under-approximations (case of the last two instances) with performance similar to that of the direct method and of CEGAR-under in the first case and better than that of the direct method but unfortunately worse than that of CEGAR-under in the second case. As a result, our RECAR-like approach is more effective than the direct method in checking Δ-diagnosability for satisfiable instances, but shows no improvement for unsatisfiable instances.

The explanation for these results is as follows. With the RECAR-like approach, we start by using CEGAR-over and, if this is inconclusive, we have the option of switching to CEGAR-under when the *SF* switching function is triggered. Now, if the instance is satisfi-able, the *SF* switching function, which is evaluated on the basis of the ratio between the last verification time and the previous one, is unlikely to be triggered because over-approximations with the parameter length bound *L* (or with the three mixed parameters) always gives good results for satisfiable instances, even after several refinement loops, i.e., the last verification time is generally no longer than the previous, also due to the use of an incremental SMT solver. In this case, the RECAR-like approach continues to run CEGAR-over, which is obviously good for satisfiable instances, and the efficiency of the former comes from the efficiency of the latter. If the instance is now unsatisfiable, we get the following situations:

1. The *SF* switching function is not triggered, i.e., it is always the CEGAR-over algorithm that runs until successive refinements of the over-approximation reach the initial formula. CEGAR-over, based on *L* or the three parameters combined, is effective even on unsatisfiable instances, in fact similarly or even slightly more effective than direct problem solving (probably due to the incremental SMT), and the same applies to the RECAR-like approach.

2. *SF* is triggered, then the CEGAR-under algorithm is executed, and, possibly after several switches, we obtain the unsatisfiable conclusion either of CEGAR-over (if the number of switches is even) because the initial formula is finally reached by the succession of refinements of its over-approximation, or of CEGAR-under (if the number of switches is odd, which is the case of our two instances concerned) which returns
UNSAT. In the first case, the RECAR-like algorithm contains the entire CEGAR-over
process plus part of the additional CEGAR-under process, and in the second case, the
entire CEGAR-under process plus part of the additional CEGAR-over process. Both
cases therefore contain the full or partial CEGAR-under process. Since the latter is inef-
ficient, as pointed out above, the RECAR-like approach is also inefficient.

9 Related work

Since the introduction of the diagnosability definition for discrete event systems (Sampath et al. 1995), many works provided improvements or extensions (Sampath et al. 1998; Genc and Lafortune 2009) for the discrete framework.

Fewer studies have investigated this property for real-time systems, which are neverthe-
less more realistic applications. In 2002, Tripakis (2002) proposed for the first time the
definition of diagnosability of TAs, and then gave a sufficient and necessary condition by
adapting the twin plant method and proving the PSPACE completeness of this verifica-
tion process. However, this work lacks experimental results. Next, Bouyer et al. (2005)
proposed a method for synthesizing fault diagnosers in the form of deterministic timed
automata, which can be used as on-line fault detectors. Deterministic timed automata and
event-recording timed automata are studied in this work, for which the problem of diag-
noser synthesis is decidable (2EXPTIME-complete for the former and PSPACE-complete
for the latter) with limited resources. Subsequently, Bouyer et al. (2018, 2021) introduced
timed markings or timed sets as a new formalism for one-clock timed automata. The idea
is to keep track of reachable configurations that evolve over time in an efficient way. The
implementation of this approach has demonstrated superior performance to that presented
in Tripakis (2002).

Some works deal with general verification on TA using SMT techniques with fairly good
results. In Badban and Lange (2011), a new SMT-based approach is proposed to incremen-
tally analyze TA for certain special decidable problems, including universality for deter-
ministic timed automata and language inclusion of a nondeterministic automaton into a
deterministic automaton. This is done by adopting a bounded version for reasons of effi-
ciency. To verify the reachability of the TA, Kindermann et al. (2012) introduced a bounded
model check based on SMT to handle non-lasso-shaped infinite runs by integrating the
region abstraction.

On the other hand, some studies have adapted the CEGAR approach to the verification of
timed automata, where abstractions (i.e., under-approximations) consist of deleting clocks
and discrete variables and refinements involve adding clocks (Dierks et al. 2007; He et al.
2010). In the worst case, we end up adding all the clocks, which renders these methods
useless. Next, Roussanaly et al. (2019) studied the abstraction of predicates on clock vari-
ables by defining abstract state spaces with predicates. In particular, new predicates can be
generated during the refinement step. Two algorithms were implemented to demonstrate the
effectiveness of this approach compared with state-of-the-art tools: a zone-based algorithm
and a Binary Decision Diagram (BDD) based algorithm. All the verifications mentioned
above concern only a single trajectory in the TA and the systems concerned are not partially
observed. Consequently, the abstraction criteria are not suitable for verifying diagnosability,
which involves comparing the observations of two trajectories to search for critical pairs, making its verification more complicated.

More recently, attention has been focused on the verification of special failure models, called Failure Propagation Models (FPM), where the failure propagation information is abstracted from the original system model. The approach proposed in Bozzano et al. (2015) presents how to encode in SMT the diagnosability problem for a given timed FPM. It should be noted that TA are totally different from FPMs, the former being considered as original system models, on the basis of which FPMs can be abstracted. However, this transformation is by no means trivial, as demonstrated in Priesterjahn et al. (2013); Bittner et al. (2016a, 2016b). To the best of our knowledge, our present work is the first which verifies diagnosability directly on the TA using SMT techniques and offers an alternative to systems for which FPM abstraction is not practical.

Finally, in work Zaatiti et al. (2018) devoted to analyzing the diagnosability of hybrid dynamic cyber-physical systems, modeled by hybrid automata that generalize timed automata by adding a continuous framework to the discrete framework, a CEGAR-under process is used to approximate this undecidable problem (with refinement up to a given accuracy), where the abstraction of the continuous and temporal characteristics of the systems is provided by timed automata. The present work should improve the efficiency of the method by approximating the abstraction itself with RECAR to determine its diagnosability.

## 10 Conclusion

In this paper, we have proposed a new approach to improve the efficiency of diagnosability analysis of timed automata, using an alternating abstraction and refinement approach allowing optimizations such as early SAT or UNSAT termination. We defined several types of parameterized over- and under-approximations of the problem and various refinement strategies. Finally, we evaluated the effectiveness of our approach and its implementation with the Z3 SMT solver on literature benchmarks, extended to study scalability. Our RECAR-like approach, mixing SAT and UNSAT shortcuts, performs well for satisfiable (non-diagnosable) instances, thanks to the effectiveness of our over-approximations (in particular the one obtained by decreasing the length bound of the critical pair sought), but unfortunately performs poorly for unsatisfiable (diagnosable) instances, which seem to stem from the ineffectiveness of all our under-approximations. We concluded that the key complexity factor is the critical pair length bound, which remains equal to its initial value in all our under-approximations, explaining their inefficiency.

Future work will therefore be devoted to improving the efficiency of CEGAR-under. One solution is to define purely syntactic under-approximations by “forgetting” part of the diagnosability formula in conjunctive normal form, but preliminary experiments show that, in the UNSAT case, most of the sub-formulas we have tried are satisfiable and that an unsatisfiable sub-formula would probably be close to the global formula in terms of size. Furthermore, there is a significant advantage, for the interpretation of results, in working with semantic approximations as we have done, i.e., which define the same problem as the original one but with different parameter values. In this context, another possible approach is to play with the time constraints expressed in the guards and invariants, i.e., to tighten these constraints to define over-approximations and relax them to define under-approximations.
But here again, very preliminary experiments seem to show that for under-approximations, the Length bound parameter set at *B* remains the cause of inefficiency. Therefore, study of the relationship between *B* and, on the one hand, Δ and, on the other, the length of a path between the initial state and the occurrence of the fault can be fruitful.

**Author contributions** Lulu He contributed to this work during her Ph.D. thesis with a fellowship from Université Paris-Saclay.

**Funding** Open access funding provided by Université Paris-Saclay. No funding was received to assist with the preparation of this manuscript.

**Data availability** The data set (code, benchmarks and experiments) is available on GitHub at https://github.com/ailxxxx/RECAR.

## Declarations

**Competing interests** The authors have no competing interests to declare that are relevant to the content of this article.

**Open Access** This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

## References

Alur R, Dill DL (1994) A theory of timed automata. Theoretical Comput Sci 126(2):183–235

Badban B, Lange M (2011) Exact incremental analysis of timed automata with an smt-solver. In: Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’11). LNCS, vol. 6919. Springer, NY, USA

Bittner B, Bozzano M, Cimatti A (2016) Automated synthesis of timed failure propagation graphs. In: Proceedings of the 25th international joint conference on artificial intelligence (IJCAI’16), pp 972–978

Bittner B, Bozzano M, Cimatti A, Zampedri G (2016) Automated verification and tightening of failure propagation models. In: Proceedings of the 30th conference on artificial intelligence (AAAI’16), pp 907–913

Bouyer P, Henry L, Jaziri S, Jéron T, Markey N (2021) Diagnosing timed automata using timed markings. Int J Softw Tools Technol Transf 23(2):229–253. https://doi.org/10.1007/S10009-021-00606-2

Bouyer P, Chevalier F, D’Souza D (2005) Fault diagnosis using timed automata. In: Proceedings of international conference on foundations of software science and computation structures (FoSSaCS’05). Lecture Notes in Computer Science. Springer, NY, USA

Bouyer P, Jaziri S, Markey N (2018) Efficient timed diagnosis using automata with timed domains. In: Colombo C, Leucker M (eds.) Proceedings of the 18th International Conference on Runtime Verification (RV’18). LNCS, vol. 11237, pp 205–221. Springer, NY, USA. https://doi.org/10.1007/978-3-030-03769-7_12

Bozzano M, Cimatti A, Gario M, Micheli A (2015) Smt-based validation of timed failure propagation graphs. In: Proceedings of the 29th conference on artificial intelligence (AAAI’15), pp 3724–3730

Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification CAV 2000. Lecture Notes in Computer Science, vol. 1855, Springer, pp 154–169
Dierks H, Kupferschmid S, Larsen KG (2007) Automatic abstraction refinement for timed automata. In: Raskin J, Thiagarajan PS (eds.) Formal Modeling and Analysis of Timed Systems, Proceedings of the 5th International Conference, FORMATS 2007, Salzburg. LNCS, vol. 4763, pp. 114–129. Springer, NY, USA. https://doi.org/10.1007/978-3-540-75454-1_10

Genc S, Lafortune S (2009) Predictability of event occurrences in partially-observed discrete-event systems. Autom 45(2):301–311. https://doi.org/10.1016/j.AUTOMATICA.2008.06.022

Grastien A, Anbulagan A, Rintanen J, Kelareva E (2007) Diagnosis of discrete-event systems using satisfiability algorithms. In: Proceedings of the 22nd national conference on artificial intelligence AAAI’07, pp 305–310

He L, Ye L, Dague P (2018) SMT-based diagnosability analysis of real-time systems. In: Proceedings of the 10th Symposium on Fault Detection, Supervision and Safety for Technical Processes, IFAC SAFEPRO-CESS 2018

He F, Zhu H, Hung WNN, Song X, Gu M (2010) Compositional abstraction refinement for timed systems. In: Liu J, Peled DA, Wang B, Wang F (eds.) Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2010, pp 168–176. IEEE Computer Society, USA. https://doi.org/10.1109/TASE.2010.27

Jiang S, Huang Z, Chandra V, Kumar R (2001) A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Trans Autom Control 46(8):1318–1321

Kindermann R, Junttila T, Niemela I (2012) Beyond lassos: Complete smt-based bounded model checking for timed automata. In: Proceedings of Joint FMOODS 2012 and FORTE 2012. LNCS, vol. 7273. Springer, NY, USA

Lagniez J, Le Berre D, Lima T. Montmirail V (2017) A recursive shortcut for CEGAR: application to the modal logic K satisfiability problem. In: Proceedings of the Twenty-Sixth international joint conference on artificial intelligence IJCAI’17, pp 674–680

Lee EA, Seshia SA (2016) Introduction to Embedded Systems: A Cyber-Physical Systems Approach. MIT Press, Cambridge, MA, USA

Priesterjahn C, Heinzemann C, Schäfer W (2013) From timed automata to timed failure propagation graphs. In: Proceedings of the 16th IEEE International Symposium on Object/component/service-oriented Real-time distributed Computing (ISORC’13)

Rintanen J, Grastien A (2007) Diagnosability testing with satisfiability algorithms. In: Proceedings of the 20th international joint conference on artificial intelligence IJCAI’07, pp 532–537

Roussanaly V, Sankur O, Markey N (2019) Abstraction refinement algorithms for timed automata. In: Dillig I, Tasiran S (eds.) Computer Aided Verification. LNCS, vol. 11561, pp 22–40. Springer, NY, USA. https://doi.org/10.1007/978-3-030-25540-4_2

Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis D (1995) Diagnosability of discrete-event systems. IEEE Trans Autom Control 40(9):1555–1575

Sampath M, Lafortune S, Teneketzis D (1998) Active diagnosis of discrete-event systems. IEEE Trans Autom Control 43(7):908–929

Tripakis S (2002) Fault diagnosis for timed automata. In: Proceedings of the international symposium on formal techniques in real-time and fault-tolerant systems (FTRTFT’02). LNCS, Springer, NY, USA, pp 205–221

Zaatiti H, Ye L, Dague P, Gallois J-P, Travé-Massuyès L (2018) Abstractions refinement for hybrid systems diagnosability analysis. In: Sayed-Mouchaweh M (ed) Diagnosability, Security and Safety of Hybrid Dynamic and Cyber-Physical Systems, Chapter 11. Springer, NY, USA, pp 279–318

Zbrzezny A, Półtola A (2007) Sat-based reachability checking for timed automata with discrete data. Fundamenta Inf 79(3–4):579–593

**Publisher's Note** Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
<figure><img src="image_8.png" /></figure>

**Lulu He** received her PhD in Computer Science from the University Paris-Saclay in 2022. She is currently a lecturer at Hertsfordshire College, Changzhou Institute of Technology, and heads the Electrical and Electronic Engineering (EEE) program. Her research focuses on formal methods, model-based diagnosis, and medical image processing.

<figure><img src="image_9.png" /></figure>

**Philippe Dague** received his engineering degree from Ecole Centrale de Paris in 1972 and his doctorate in Theoretical Physics from the University Paris 6 in 1976. He was assistant professor of Mathematics at the University of Poitiers, then at the University Paris 6, from 1976 to 1983. From 1983 to 1992, he was a research engineer in Computer Science at the IBM Scientific Center in Paris. He obtained his Habilitation to Supervise Research in Computer Science in 1992 at the University of Paris 6. From 1992 to 2005, he was a full professor of Computer Science at the University Paris-Nord 13, where he founded the Artificial Learning, Diagnosis and Agents group of the Laboratoire d'Informatique de Paris-Nord (LIPN) in 1999 and headed it until 2005. From 2005 to 2019, he was a full professor of Computer Science at the University Paris-Sud and from 2010 to 2014 he headed the "Laboratoire de Recherche en Informatique" (LRI). His research activity from 1984 has focused on Artificial Intelligence techniques (Knowledge Representation and Reasoning) for Engineering, in particular qualitative, causal and temporal modeling and reasoning, model-based diagnosis and diagnosability analysis using formal methods. He has applied these techniques to a variety of fields, through partnerships with industrials and national and international projects: diagnosis of electronic, automotive and space systems, supervision of telecommunication networks, monitoring of Web services. He is also currently working in bioinformatics on the analysis of metabolic networks and the semantics of Boolean networks. He has been a member of the program committee of over 65 conferences and of the evaluation committee of several national programs. He is the author of over 100 articles in international and national conferences and journals, as well as several book chapters. He has been Professor Emeritus since 2019.

<figure><img src="image_10.png" /></figure>

**Lina Ye** received her PhD in Computer Science from the University Paris-Sud 11, France, in 2011. She held a post-doctoral position in the CONVECS team at Inria Rhône-Alpes from 2012 to 2014. She is currently an Associate Professor in Computer Science at CentraleSupélec and conducts her research in the LMF laboratory (Université Paris-Saclay, CNRS, ENS), France. Her main research interests focus on formal methods, model-based diagnosis, and the integration of formal methods with deep learning.