1 Modelling and Decidability Results

The years 80s witnessed a growing interest in timed systems that combine discrete models with metric time, in order to specify behaviours of reactive systems not only qualitatively but also quantitatively. This interest, which remains vibrant today, led to the development of a variety of formal models and logics. Timed automata [5], introduced together with a verification algorithm in the early 90s by Rajeev Alur and David Dill, have been undoubtedly the most popular formalism. They are used in many successful tools, such as UPPAAL [34], for specifying and verifying real-time systems. In the 80s, Oded was a PhD student at Weizmann Institute of Science, working on his thesis titled “Finite Automata: Infinite Behavior, Learnability and Decomposition”, under the supervision of Amir Pnueli. His advisor, winner of the Turing award in 1996 for his work on temporal logics, was part of the timed systems movement. He proposed a model, called timed transition system, and versions of real-time temporal logics [49]. This activity of his advisor certainly had a lot of impact on Oded who was already interested in the physical world outside computers and programs. He discovered a paper by R. Brooks from MIT AI lab which proposed a “behaviour-based” approach to robotic systems integrating control programs, sensors, actuators and timers. This prompted him to think how one can verify that such systems behave correctly in a given environment. Together with Amir Pnueli, he wrote a proposal titled “Systematic Development of Robots”. This idea perhaps sounded too avant-garde at that time, partly because of the inter-cultural gap between computer scientists and control theorists. In addition, the verification research did not yet reach its successes in industrial applications. The proposal did not pass and Oded moved to France to do his postdoc at IRISA (Rennes). During his post-doc, together with Amir Pnueli and Zohar Manna, he wrote the paper “From timed to hybrid systems” [59] which proposed a model called phase transition systems, the first formal hybrid model coming from the verification community. This model, which combines discrete transitions (that take no time) and continuous dynamics specified by differential equations, can be thought of as a precursor of the model of hybrid automata proposed a little later in a seminal paper [3]. In parallel, various models were proposed by the control community. These models, designed to include specific discrete phenomena arising in computer control systems (such as autonomous or controlled switchings and jumps), are suitable for the purpose of extending the existing analytic control methods to hybrid systems. Many studies were devoted to the topology and computational capabilities of such models. The reader is referred to the PhD thesis of Michael S. Branicky at MIT in 1995 [26] for a thorough survey of the hybrid models proposed in the beginning of the hybrid systems research history, including a technical comparison and classification of these models. Many of these models (such as, hybrid automata and switched systems) are now widely used for verification and control purposes. These models were however too complex for the verification algorithms developed by computer scientists, who still considered differential equations outside the traditional scope of their domain. Motivated by the success of decidability results and model-checking algorithms for timed automata, the verification community was then more interested in extending these results to hybrid automata with simple continuous dynamics, such as with clocks that can be stopped, or with continuous variables having constant or piece-wise constant derivatives [4, 48]. Oded was by that time an CNRS researcher in the laboratory VERIMAG, headed by Joseph Sifakis whose group contributed to the development of the hybrid automaton model [3]. In this new movement, Oded’s contributions were the decidability and undecidability results for piecewise constant derivative systems (PCD). Such a system consists of a polyhedral partition of the state space and in each region of the partition the continuous variables evolve with constant derivatives. He first proved decidability of such systems with 2 continuous variables (planar PCD) [61], based on the observation that a trajectory cannot intersect itself (Jordan curve theorem), unlike the trajectory depicted in Fig. 1. Additionally, for every trajectory, the sequence of edges it crosses is ultimately-periodic. Therefore, one can define a finite abstract alphabet to describe qualitative behaviours as sequences of regions or edges. Then, Oded and his colleague Eugene Asarin proved the undecidability of PCD in 3 and higher dimensions [12, 14]. They also proved, using Zeno paradox, how all the arithmetical hierarchy can be realized by PCD [15]. These results and directions have a number of important technical follow-ups, among which we can mention: a generalisation to planar differential inclusions [17], stability of polyhedral switched systems [68], and in particular models of computation [24]. Despite the recognition these theoretical results received, Oded was disappointed because these negative decidability results seemed to imply that if the verification problem for such simple systems is undecidable, there would be no hope that one can verify real-life hybrid systems. This disappointment reflected his ambition to export the verification methodology to practical application domains. It also made him question the appropriateness of the exact formulation of verification problems in the context of hybrid systems. While pondering upon this methodological issue, Oded continued to work actively on timed systems. Indeed he never stopped working on this theme and his contributions in timed systems were abundant and impactful, covering a large number of problems: controller synthesis for timed automata [16, 62], scheduling using timed automata (with optimality and under stochastic uncertainty) [1, 52], compositional timing analysis [69], control with bounded computational resources [58], multi-criteria optimisation [30], embedded multicore [71], timed regular expressions [13], real-time temporal logic, monitoring, timed pattern matching [20]. It is important to emphasise that his results on Signal Temporal Logic [60] not only successfully gained industrial acceptance but also opened new research directions in cyber-physical systems monitoring and testing (see for example [21]).

Fig. 1.
figure 1

Illustration of an impossible situation: the depicted trajectory exits a region at a boundary point \(x_1\) and then exits this region again at a boundary point \(x_2\), thus it cannot intersect the boundary part between \(x_1\) and \(x_2\).

Full size image

2 Reachability Analysis

While negative decidability results hindered a direct application of the algorithmic verification methodology to hybrid systems with non-trivial dynamics, they also incited the verification community with a new motivation. In a continuous world, it is meaningful to seek approximate answers for non-trivial systems, rather than insisting on exact answers which are possible only for trivial systems. Oded set out to tackle the first obstacle: continuous systems described by differential equations. While restricting to the problem of approximating reachable sets for this type of dynamics, he aimed at a solution that could be extended to hybrid systems and could be used further for problems beyond verification, in particular for controller synthesis. Although the type of dynamics was restricted, the goal turned out to be very ambitious because the considered class is general, including non-linear dynamics. With his student, he developed a method for tracking the evolution of a (general) polyhedron under continuous dynamics. Essentially, due to continuity of trajectories, it suffices to track the evolution of the faces of the polyhedron. A face is pushed outward if there is a point on the face at which the projection of the vector field on the normal of the face points outward, and the pushing amount depends on the time step size and the maximum projection magnitude over all the points on the face. This results in a new polyhedron for which the same procedure is applied in the next time step. This method can be seen as a set-valued Euler integration scheme. To ensure accurate results, the faces with a large derivative variation need to be subdivided, which generates non-convex polyhedra. The development of this method was much inspired by the work of Greenstreet [44] in 1996 where this idea was proposed for two dimensional systems and reachable sets are thus polygons. Non-convex polygons benefit from well-developed plane geometric manipulation algorithms, unlike general dimensional non-convex polyhedra. Treating high dimensional systems was never seen as ambitious, since real-life models are rarely limited to a few variables. It was thus necessary to choose a set representation on which the specific operations (such as pushing, splitting) as well as the Boolean set-theoretic operations (intersection and union, for handling discrete transitions) can be efficiently computed. To this end, orthogonal polyhedra (which are union of hyper-rectangles) were used [25]. The method, called “face-lifting” (see Fig. 2), was published in the proceedings of the conference HSCC (Hybrid Systems: Computation and Control) 1998 [32]. Although disappointment ensued again when it became clear that the face-lifting technique was very computationally expensive, this paper turned out to be well received by the hybrid systems community and obtained a test-of-time award at the conference HSCC 2019, to the surprise of the (living) co-author (and, plausibly, of the other co-author too). The reason was perhaps that this paper, by stating a reachability analysis problem and describing the ingredients necessary for designing an effective algorithm to solve it, opened a new concrete direction for hybrid systems verification. Indeed, as attested by the publications at the HSCC conferences, reachability analysis itself has become a central problem.

Fig. 2.
figure 2

Illustration of the face-lifting technique.

Full size image

The experience with non-linear systems made Oded and his student more aware of the importance of exploiting the structure of the system. Together with Eugene Asarin, they focused on linear systems, for which the reachable set can be constructed from a finite number of trajectories via the convex hull operations. This allowed them to obtain a second-order approximation scheme that uses convex polyhedra to represent reachable sets [7, 8]. The method was then extended to linear systems with uncertain input using the Maximum Principle from optimal control. These results were implemented in the tool d/dt [11]. The extension to uncertain input was inspired by the ellipsoidal technique of Kurzhanski [54] and the polyhedral technique of Varaiya [74], developed in the context of uncertain systems (although these techniques worked only for discrete-time reachable sets). Another related work was that by Chutinan and Krogh [28], who proposed a similar polyhedral approximation for systems with constant input. Besides the direct ordinary differential equation (ODE) formulation, the reachability problem was tackled using the partial differential equation (PDE) formulation [63, 64, 73] and level sets were used to represent reachable sets. While computer scientists tried to handle differential equations, control theorists became interested in the decidability question and contributed fundamental results for hybrid systems with linear continuous dynamics [4, 6, 57].

In the quest for efficient set representations to make reachability algorithms more scalable, Greenstreet and Mitchell extended their method to polygonal projections [42, 43]. Antoine Girard proposed zonotopes, for which computing linear transformation and Minkowski sum can be done in an algebraic manner, and this allows tracking the evolution of zonotopes under linear dynamics efficiently, without resorting to expensive geometric computations (in particular the convex hull operations) [39]. The algebraic manipulation was later adapted to general convex sets represented by support functions, in the thesis work of Colas Le Guernic, supervised by Oded and Antoine [40, 41, 45, 46]. This thesis work culminated in a method that could compute reachable sets for systems of hundreds of dimensions. Special attention also put on performing numerical schemes intelligently to avoid error accumulation. The representations by zonotopes and support functions were implemented in the tool SpaceEx [38], developed by Oded’s group under the direction of Goran Frehse. The tool quickly became one of the most advanced tools for hybrid systems verification. The influence of the work on zonotope-based reachability computation was attested by the HSCC 2018 test-of-time award given to Antoine’s first paper on this topic [39].

It is fair to say that using these set representations the reachability problem for linear continuous systems is solved; however computing intersection of their unions remains (until now) a big challenge. This is a reason why the state-of-the-art reachability analysis techniques can handle purely continuous systems of up to billions of dimensions [19] but are still limited when handling hybrid systems (especially with a large number of discrete transitions).

3 Non-linear Systems and Hybrid Systems Biology

The research directions in systems biology that Oded pursued involved building and analysing dynamical system models of biological phenomena. For engineering systems, this approach is termed model-based, in the sense that a model is developed and used to debug, since correcting a model is cheaper than fixing a real system. Similarly, testing and exploring biological models in silico is preferred over expensive experiments. A network of interacting genes and proteins is thinkable as an information processing system that evolves in space and time according to fundamental laws of physics, and can thus be formally described in mathematical terms. Therefore, intuitively speaking, the biological modelling activity consists of discovering a dynamical model that can explain the relation between a diagram of biological interactions and experimental data obtained by measuring some entities in the diagram.

Whereas hybrid systems became a mathematical model widely accepted for reasoning about interactions between discrete and analog parts of embedded and cyber-physical systems, they also drew a lot of attention of researchers in systems biology since they can capture phenomena of hybrid nature in molecular biology. Oded was one of the founders of the workshop Hybrid Systems Biology. The term “hybrid systems biology” can be understood (literatim) as a branch of systems biology which relies on the techniques developed in the domain of hybrid systems. In a more allegorical manner, this term expresses a view of thinking and reasoning about biological mechanisms and processes in the spirit of the mathematical and computational methods for specifying and analysing behaviours of heterogenous systems with mixed discrete-continuous dynamics. It is important to emphasise before continuing that this note focuses only on the synergy between Oded’s reachability analysis research and his interest in systems biology. He also approached systems biology via his research on real-time temporal logics for specifying and testing biological hypotheses, such as [35, 66, 70].

Oded created collaborations with some biologists (having a reciprocal interest) in Grenoble, in an effort to apply hybrid systems verification technology to biological systems, in particular the techniques that can be used to analyse in a systematic manner quantitative models admitting uncertainty whose nature is set-theoretic. Parameter uncertainty in biological models is uncertainty of this type. These collaborations led to the following observation. Hybrid systems can be used not only as a model but also to approximate complex systems by simpler ones (which can be analysed by more efficient techniques). In addition, they can naturally capture stiffness in continuous dynamics arising in many biological systems, which often causes instability in traditional numerical methods. However, their use does not come for free. Indeed, even when continuous dynamics can be efficiently handled (such as linear dynamics), discrete dynamics (which in principle can be handled using well-developed techniques for discrete systems) may lead to significant computation effort, as costly as that for overcoming numerical instability. Indeed, while numerical instability can be addressed by reducing the time step in order to adapt to fast changes of some variables, switching continuous dynamics via discrete transitions in a hybrid system may deteriorate “nice” geometric structures of continuous reachable sets. As an example, trajectories starting from points in a convex polyhedron can reach a transition guard at very different times, and the accumulation of starting points for the next continuous dynamics may form a “curved” non-convex set with complex geometry.

Taking both the drawbacks and advantages of the hybrid systems methodology into account, Oded’s group revisited the hybridization approach developed in [9, 10]. The main idea of this approach is to decompose a non-linear vector field into different segments corresponding to disjoint regions of the state space. Each segment is then approximated with a simpler (such as linear) vector field. This approach is very general and in principle can be applied to a large class of non-linear systems. However, in practice, the price for having artificial discrete transitions is often high, since the simpler approximate dynamics are used, the larger number of segments is needed in order to assure a desired precision. One way to avoid intersections with the boundary of two adjacent regions is to “smoothen” the transitions without compromising the approximation quality. Furthermore, geometric properties of the dynamics should be exploited to determine approximation domains that are as large as possible. This work shows an interplay between ideas from geometric modelling and set-based numerical integration, which is sketched in the following.

Given a non-linear system \(\dot{x}(t) = f(x(t)), ~x \in {\mathcal {X}} \subset {\mathbb {R}}^n\) where the function f is Lipschitz. One can approximate this original system with a system: \(\dot{x}(t)=g(x(t)) + u(t), ~x \in {\mathcal {X}} \). The input \(u(\cdot )\) such that \(||u(\cdot )||\le \mu \) where \(\mu \) is the bound of \(||g-f||\), is added in the approximate system in order to conservatively account for the dynamics approximation error. The construction of such an approximate system consists of two main steps. Inside a zone of interest that contains the current reachable set, an approximation domain and its associated approximate vector field are computed. When the system leaves the current approximation domain, a new domain is created. This technique was implemented using linear interpolation over simplicial domains and multi-affine interpolation over hyper-rectangles (the interpolants in both cases can be uniquely determined). Note that the error in the reachable set approximation depends on the dynamics error bound \(\mu \). It is thus important to derive tight error bounds. For systems satisfying some smooth conditions, [33] proved for each simplex an error bound that depends on the maximal curvature of f in the simplex and on the radius of the smallest ball that contains the simplex. This error bound is tighter than the error bound used in [10] which depends on the maximal simplex edge length. In addition, one can obtain a larger simplex by stretching an equilateral simplex along a direction in which the curvature is small. This can be done by mapping the simplices to an “isotropic” space where the curvature bounds are isotropic. An illustration of this transformation is depicted in Fig. 3, where the application of the mapping to an ellipsoid produces a circle. When applying the mapping to the triangle inscribed the ellipsoid shown on the left, the result is a more regular triangle shown on the right. This mapping can be used further to define optimal shape and orientation of the simplicial domains. This dynamic hybridization based on dynamics curvature allowed treating a number of biological systems with up to 12 continuous variables [31]. This constituted a considerable progress since the original hybridization approach was limited to systems with only 3, 4 continuous variables. On the other hand, most of the existing state-of-the-art techniques for non-linear systems worked efficiently only for low-dimensional systems.

Fig. 3.
figure 3

Illustration of the transformation to the isotropic space.

Full size image

In the following, we illustrate the results obtained by this approach for a model describing the loosening of the extra-cellular matrix [51]. This is a crucial process in angiogenesis, the sprouting of new blood vessels as a reaction to signals that indicate the need for additional oxygen in certain tissues [51, 75]. Interfering with angiogenesis is considered a promising direction for fighting cancer tumors by cutting their blood supply. The soluble and membrane-associated matrix metalloproteinases are among the enzymes responsible for the proteolytic processes that occur in the extra-cellular matrix. In [51], a network of reactions involving the entities of interest was established, and then, from this network, a system of ordinary differential equations was derived using mass action kinetics. This differential equation system of 12 variables, used in our reachability analysis case study (see Table 3 of [31]), can be used to describe the proteolysis of collagen I by matrix metalloproteinases 2 (MMP2) and membrane type 1 matrix metalloproteinases (MT1-MMP) in the presence of the tissue inhibitor of metalloproteinases 2 (TIMP2). The model focuses on the degradation of collagen type 1 (represented by the variable c1) by two enzymes MT1-MMP and MMP2 (the concentrations of which are represented by the variables mt1 and m2). The latter has to be activated from its passive form M2P obtained by a chain of reactions involving TIMP2 (the concentration of which is represented by the variable t2) which also plays the role of an inhibitor for MT1-MMP, which leads to an overall complex system of interactions. The study in [51] experimentally observed a convergence of the variables, stating from a single initial state of concentrations, towards a nearly steady state (see Fig. 2-A in [51]). We computed reachable sets to verify this observation for a set of initial concentrations. Figure 4 shows the projection of the reachable set evolution on the three variables mt1, m2, and t2. The initial set is a small set around the origin (corresponding to the cube in the figure). We observe that the variables converge towards the dense part of the reachable set (drawn in cyan colour). This confirmed the observation of convergence in [51].

Fig. 4.
figure 4

Projection of the reachable set on the first three variables mt1, m2 and t2. The cube in this figure is the set of initial concentrations. We can observe that the variables converge towards the dense part of the reachable set (drawn in cyan colour), which confirmed the experimental observation of convergence in [51] (Color figure online).

Full size image

Oded once said humorously, “our computational methods are not fast enough [to fight cancer]”, referring to his ongoing Plan Cancer project (MoDyLAM - Dynamic modelling of iron-linked redox perturbations in Acute Myeloid Leukemia). His adventure in hybrid systems biology was not long, but he already paved a research path for us to follow.

4 Conclusion

This note was written in memoriam Oded Maler, who made groundbreaking contributions in the hybrid systems research. His creativity, courage, sharp mind and passion made him a role model to many of his colleagues. To celebrate Oded’s scientific legacy, nothing would be more cheerful than a listFootnote 1 of major hybrid verification tools which have been developed over the last two decades: Coho [43], CheckMate [28], HyperTech [47], MPT [56], HJB toolbox [64], ET Toolbox [55], KeYmaera [65], SpaceEx [38], Adriane [29], HySon [23], NLToolbox [72], Flow\(^{*}\) [27], CORA [2], dReach [53], C2E2 [37], AVERIST [67], HyReach [50], Sapo [36], HyLaa [18], and JuliaReach [22].