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

HAL
open science

# Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks

Jonathan Behaegel, Jean-Paul Comet, Maxime Folschette

► To cite this version:

Jonathan Behaegel, Jean-Paul Comet, Maxime Folschette. Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks. 24th International Symposium on Temporal Representation and Reasoning (TIME 2017), Oct 2017, Mons, Belgium. 10.4230/LIPIcs.TIME.2017.5 . hal-01655310

HAL Id: hal-01655310

https://hal.science/hal-01655310

Submitted on 4 Dec 2017

**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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks*

Jonathan Behaegel¹, Jean-Paul Comet², and Maxime Folschette³

1 Université Côte d'Azur, CNRS, I3S, Sophia Antipolis, France

2 Université Côte d'Azur, CNRS, I3S, Sophia Antipolis, France

3 Université de Nantes, LS2N, Nantes, France

## Abstract

We present a new hybrid Hoare logic dedicated for a class of linear hybrid automata well suited to model gene regulatory networks. These automata rely on Thomas' discrete framework in which qualitative parameters have been replaced by continuous parameters called celerities. The identification of these parameters remains one of the keypoints of the modelling process, and is difficult especially because the modelling framework is based on a continuous time. We introduce Hoare triples which handle biological traces and pre/post-conditions. Observed chronometrical biological traces play the role of an imperative program for classical Hoare logic and our hybrid Hoare logic, defined by inference rules, is proved to be sound. Furthermore, we present a weakest precondition calculus (a la Dijkstra) which leads to constraints on dynamical parameters. Finally, we illustrate our "constraints generator" with a simplified circadian clock model describing the rhythmicity of cells in mammals on a 24-hour period.

**1998 ACM Subject Classification** I.6.4 Model Validation and Analysis

**Keywords and phrases** Hoare logic, weakest precondition, linear hybrid automata, constraint synthesis, gene networks

**Digital Object Identifier** 10.4230/LIPIcs.TIME.2017.5

## 1 Introduction

Formal methods from computer science have been largely applied to model and analyse biological systems [5, 17]. In particular, verification tools like model-checking have been used to verify dynamical properties of discrete models [3, 7] in which the temporal aspects are only present through the succession of events: the delay between two successive events is not taken into account. Unfortunately, continuous time turns out to be important in most biological systems, in particular for gene regulatory networks.

Gene regulatory networks are models representing influences between genes leading to the modification of the synthesis of associated proteins. Because proteins can regulate their target genes, positive or negative feedback loops emerge making possible a large variety of behaviours. These gene regulatory networks are designed to apprehend and predict effects of a component on the system but such models are also useful to confront hypotheses with the up-to-date collected knowledge on the gene interactions.

Several modelling framework have been devoted to gene networks. These frameworks differ by the aspects they highlight. Stochastic models emphasize non-determinism, differential models represent a system with a lot of details (transcription, traduction, transports ...) [14]

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

<footnote>* This work is partially supported by the French National Agency for Research (ANR-14-CE09-0011).</footnote>
and give precise trajectories in terms of concentrations; qualitative models [16, 15] focus on the major features that explain the observations (only main causalities are taken into account); and hybrid models link qualitative aspects with continuous variables such as time.

Whatever the modelling framework, the main difficulty of building such networks is the identification of parameters governing the dynamics of the system. The determination of these parameters is crucial to observe a behaviour consistent with biological knowledge. We already showed [3] that formal methods can help in this parameter identification step in the René Thomas' discrete modelling framework [16]. Unfortunately, this framework abstracts temporal information, often necessary for tuning the models. This discrete approach is based on the splitting of homogeneous concentration areas which have the same effects on other components. In order to refine this complete discrete framework, we associated with each such area a celerity describing the evolution speed of each component. These parameters lead to a class of linear hybrid automata. We also showed how the known experimental traces can be used to establish constraints on dynamical parameters (celerities) and to restrain the set of admissible parameters [1].

Numerous works already focus on the study of hybrid automata [9]. Especially, several tools already exist to tackle the model checking of linear hybrid automata, either with classical exhaustive approaches [10] or using abstract interpretation [8]. Communicating sequential processes (CSP), a process algebra for describing patterns of interaction in concurrent systems, has also been extended to hybrid systems and hybrid Hoare logic has been proved to be useful in such context [18]. These methods among others propose parameter synthesis in some ways. Nevertheless, these tools are tailored for a general purpose and will not take into account the specificities coming from biological contexts.

We divert Hoare logic (whose aim is to rigorously reason about the correctness of imperative programs) in order to determine constraints on celerities in such models. This approach was already developed, for the discrete framework [2, 4] and we extend it in the present paper for hybrid automata. Hoare logic has already been extended to real time systems [11] in which continuous evolutions are not taken into account whereas they are important in our biological context. Hoare logic relies on triples of the form {$Pre$} $p$ {$Post$} where Pre and Post are conditions on states of the system and $p$ is a path of the system. A Hoare triple is considered true if, whenever the system is reset at a state satisfying the Pre condition, the path $p$ is possible and leads the system into a state which satisfies the condition Post. Following E. Dijkstra [6], the aim of the game is then to determine, for each path $p$ and postcondition Post, the weakest precondition Pre, thus covering the largest set of states, making the Hoare triple true. In our temporal approach, the time spent in each state becomes crucial to determine the constraints on parameters.

We illustrate our formalism with a biological process named circadian clock which synchronises all cells in mammals at a 24-hour rhythmicity. We design a hybrid automaton modelling this biological cycle and, from the observed trace of this process, we build constraints for each celerity of this hybrid automaton using the aforementioned hybrid Hoare logic. We finally show that simulations, run parameters values satisfying the constraints, exhibit curves which are similar to experimental data.

The paper is organised as follows. We first define in Section 2 the formalism of the hybrid modelling framework. Then Section 3 focuses on the syntax and the semantics of the modified Hoare logic, and the weakest precondition calculus, whereas Section 4 is devoted to the soundness of our hybrid Hoare logic. We illustrate in Section 5 the use of this Hoare logic for identifying the constraints on parameters of the simplified circadian clock model. Finally in Section 6, we discuss the limits of this approach and we expose some possible extensions.
<figure><img src="image_4.png" /><figcaption>Figure 1 Simplified model of the circadian clock in mammals. L is a zeitgeber (see Section 5).</figcaption></figure>

## 2 Hybrid Modelling Framework of Gene Network

A gene network is visualised as a labelled directed graph (interaction graph) in which vertices are either variables (within circles) or multiplexes (within rectangles), see Fig. 1. Variables abstract genes and their products, and multiplexes contain formulas that encode situations in which a variable or a group of variables (inputs of multiplexes, dashed arrows) influences the evolution of some other variables (output of multiplexes, plain arrows). A multiplex can encode the formation of molecular complexes, phosphorylation by a protein, competition of entities for the activation of a promoter, etc. Definition 1 gives the formal details of a gene network.

**► Definition 1 (Hybrid Gene Regulatory Network).** A hybrid gene regulatory network (GRN for short) is a tuple $R = (V, M, E, C)$ where:

- $V$ is a finite set whose elements are called *variables* of the network. With each variable $v \in V$ is associated a boundary $b_v \in \mathbb{N}^*$.

- $M$ is a finite set whose elements are called *multiplexes*. With each multiplex $m \in M$ is associated a formula $\varphi_m$ in the *multiplex language* formed of the atoms $“(v \ge n)”$, where $n \in [1, b_v]^{1}$, and the usual logical connectives $\neg, \wedge, \vee$ and $\Rightarrow$.

- $E$ is a set of edges of the form $(m \to v) \in M \times V$.

- $C = \{C_{v,\omega,n}\}$ is a family of real numbers indexed by a tuple $(v, \omega, n)$ where $v \in V$, $\omega$ is a subset of $R^-(v)$ where $R^-(v) = \{m \mid (m \to v) \in E\}$, that is, $\omega$ is a set of predecessors of $v$, and $n \in [0, b_v]$. $C_{v,\omega,n}$ is called the *celerity* of $v$ for $\omega$ at the level $n$ and these celerities have to satisfy the following constraints:

$$ \forall v \in V, \forall \omega \subset R^-(v), \forall n \in [0, b_v], \quad C_{v,\omega,n} = 0 \quad \Rightarrow \quad \begin{cases} \forall i \in [n+1, b_v] & C_{v,\omega,i} < 0 \\ \forall i \in [0, n-1] & C_{v,\omega,i} > 0 \end{cases} \\ \forall v \in V, \forall \omega \subset R^-(v), \forall k \in [0, b_v-1], \quad C_{v,\omega,k} \times C_{v,\omega,k+1} \ge 0. $$

Let us remark that the dashed arrows of Fig. 1 are not present in the previous definition. When representing a gene network, it is convenient to visualise the variables contributing to a particular multiplex, but from a formal point of view, this information is redundant with the formula of the considered multiplex.

Celerities (noted $C_{v,\omega,n}$) give the evolution of each variable $v$ when it is under the active regulation of the set $\omega$ of its predecessors and when it is in the qualitative state $n$. They code for the dynamics of the system and we aim at the identification of these celerities. The constraints on celerities given in the previous definition link the signs of celerities to the underlying dynamics and may need some explanations. The first one deals with the case where a celerity value is null for a given set of active predecessors $\omega$ of a variable $v$. This models an equilibrium state, thus the related constraint states that celerities around this equilibrium, for the same set of active predecessors $\omega$, must force $v$ to reach this equilibrium.

<footnote n="1">¹ $[a, b] = \{n \in \mathbb{N} | a \le n \le b\}$.</footnote>
## 5:4 Constraint Identification Using Modified Hoare Logic

As a consequence, there is a single null celerity at most for a given couple of $v$ and $\omega$. If, on the other hand, no celerity is null for these $v$ and $\omega$, a consequence of the second constraint is that they are all of the same sign. This models that $v$ either always decreases until full degradation or always increases up to saturation.

In the remainder of this section, we focus on the dynamics of a gene network. Definition 2 introduces the hybrid states whereas Def. 3 explains the crucial notion of resources of a variable in a particular state.

**Definition 2 (State of a GRN).** Let $R = (V, M, E, \mathcal{C})$ be a GRN. A hybrid state of $R$ is a tuple $h = (\eta, \pi)$ where

- $\eta$ is a function from $V$ to $\mathbb{N}$ such that for all $v \in V$, $0 \le \eta(v) \le b_v$;

- $\pi$ is a function from $V$ to the interval $[0, 1]$ of real numbers.

$\eta$ is called the *discrete state* or *qualitative state* of $h$ whereas $\pi$ is called its *fractional part*. For simplicity, we note in the sequel $\eta_v = \eta(v)$ and $\pi_v = \pi(v)$. We denote $S$ the set of hybrid states of $R$. When there is no ambiguity, we often use $\eta$ and $\pi$ without explicit mention of $h$.

Figure 2-Centre illustrates an example of hybrid state. The tuple of all fractional parts represents coordinates inside the current qualitative state.

**Definition 3 (Resources).** Let $R = (V, M, E, \mathcal{C})$ be a GRN and let $v \in V$. The satisfaction relation $h \models \varphi$, where $h = (\eta, \pi)$ is a hybrid state of $R$ and $\varphi$ is a formula of the multiplex language, is inductively defined as follows:

- If $\varphi$ is the atom $(v \ge n)$ with $n \in [1, b_v]$, then $h \models \varphi$ iff $\eta_v \ge n$;

- The usual meaning of the logical connectives is used.

The set of resources of a variable $v$ at a state $h$ is defined by: $\rho(h, v) = \{m \in R^-(v) | h \models \varphi_m\}$, that is, the multiplexes that are predecessors of $v$ and whose formula is satisfied.

We note that the set $\rho(h, v)$ only depends on the discrete state of $h$: all hybrid states having the same discrete part thus have the same resources. Indeed, inside a discrete state $\eta$, the dynamics of $v$ is controlled in the same manner, thus the celerity is the same for all states $h = (\eta, \pi)$, that is: $C_{v,\rho(h,v),\eta_v}$. By abuse of language, we also use the notation $\rho(\eta, v)$. From this celerity, and given a particular hybrid state, one can compute the touch delay (Def. 4) of each variable, which measures the time necessary for the variable to reach a border of the discrete state.

**Definition 4 (Touch Delay).** Let $R = (V, M, E, \mathcal{C})$ be a GRN, $v$ be a variable of $V$ and $h = (\eta, \pi)$ be a hybrid state. We note $\delta_h(v)$ the *touch delay* of $v$ in $h$ for reaching the border of the discrete state. More precisely, $\delta_h$ is the function from $V$ to $\mathbb{R}^+ \cup \{+\infty\}$ defined by:

- If $C_{v,\rho(h,v),\eta_v} = 0$ then $\delta_h(v) = +\infty$;

- If $C_{v,\rho(h,v),\eta_v} > 0$ (resp. $< 0$) then $\delta_h(v) = \frac{1-\pi_v}{C_{v,\rho(h,v),\eta_v}}$ (resp. $\frac{-\pi_v}{C_{v,\rho(h,v),\eta_v}}$).

Nevertheless, reaching the border of a discrete state is not sufficient to go beyond the frontier: there may be no other qualitative level beyond the border (we call such a border an external wall) or the celerity in the neighbour state may be of the opposite sign (internal wall), as given in Def. 5.

**Definition 5 (External and Internal Walls).** Let $R = (V, M, E, \mathcal{C})$ be a GRN, let $v \in V$ be a variable and $h = (\eta, \pi)$ a hybrid state.

1. $v$ is said to *face an external wall* at state $h$ if:

$$((C_{v,\rho(h,v),\eta_v} < 0) \land (\eta_v = 0)) \lor ((C_{v,\rho(h,v),\eta_v} > 0) \land (\eta_v = b_v)).$$
<figure><img src="image_5.png" /><figcaption>**Figure 2 Continuous transitions.** Inside each state, a continuous transition $(h_0 \to h'_0)$ goes from the initial point $h_0$ to the unique point $h'_0$ from which a discrete transition takes place $(h'_0 \to h_1)$. **Left:** The celerity vector allows, without sliding mode, the trajectory to directly reach a border which is crossed. **Center:** From $h'_0$ two possible discrete transitions can occur: $h'_0 \to h_1$ or $h'_0 \to h_2$. Moreover $(\pi_g, \pi_{pc})$ corresponds to the fractional coordinates of a hybrid state $h$ along the path. **Right:** The grey zone depicts an external or internal wall. The only possible discrete transition is $h'_0 \to h_1$.</figcaption></figure>

2. Let $h' = (\eta', \pi')$ be another hybrid state s.t. $\eta'_v = \eta_v + \text{sgn}(C_{v,\rho(h,v),\eta_v})$ and $\eta'_u = \eta_u$ for all $u \neq v$. Variable $v$ is said to face an internal wall at state $h$ if $\text{sgn}(C_{v,\rho(h,v),\eta_v}) \times \text{sgn}(C_{v,\rho(h',v),\eta'_v}) = -1$, where sgn is the classical sign function.

We note $sv(h)$ the set of sliding variables, that is, variables that face an internal or external wall in the qualitative state of $h$.

We note that a sliding variable $v \in sv(h)$ may not be actually sliding if it has not reached its border yet. However, if in addition $\delta_h(v) = 0$, then $v$ is located on an internal wall or external wall. In this case, its fractional part cannot evolve anymore in the current qualitative state (see Fig. 2-Right where variable $g$ reaches an external wall). We introduce the notion of first changing variables in Def. 6 which are the first variables able to change their discrete levels.

**Definition 6 (First Changing Variables).** Let $R = (V, M, E, C)$ be a GRN and $h = (\eta, \pi)$ be a hybrid state. The set of first changing variables is defined by:

$$ \text{first}(h) = \{v \in V \setminus sv(h) \mid \delta_h(v) \neq +\infty \wedge \forall u \in V \setminus sv(h), \delta_h(u) \geq \delta_h(v)\}. $$

Moreover, $\delta_h^{first}$ denotes the time spent in the qualitative state of $h$ when starting from $h$ for any $v \in \text{first}(h)$, $\delta_h^{first} = \delta_h(v)$, or $\delta_h^{first} = +\infty$ if $\text{first}(h) = \emptyset$.

The set first($h$) represents the set of variables whose qualitative coordinates can change first. If a variable is on an external or internal wall, it cannot evolve as long as other variables do not change, thus: first($h$) $\cap$ sv($h$) = $\emptyset$. Similarly, if the celerity of $v$ in the current state is null, its qualitative value cannot change because of an infinite touch delay.

Figure 2 illustrates several evolutions of a gene network. From a particular hybrid state $h_0$, the dynamics alternates continuous transitions (within the discrete state) and discrete transitions (when changing the discrete state). When the trajectory reaches an external or internal wall (see Fig. 2-Right), the variable slides along the wall only if the celerity of some other variable can drive the trajectory in such a direction. This description leads to the following definition.

**Definition 7 (Hybrid State Space).** Let $R = (V, M, E, C)$ be a GRN. We note $\mathcal{R} = (S, cT, dT)$ the hybrid state space of $R$ where $S$ is the set of hybrid states, and $cT$ (resp. $dT$) is the set of continuous (resp. discrete) transitions:
5:6 Constraint Identification Using Modified Hoare Logic

1. There exists a continuous transition in cT from state h = (η, π) to state h' = (η', π') iff:

a. Either first(h) ≠ ∅ and there exists a variable v ∈ first(h) such that:

i. δh(v) ≠ 0, where δh(v) is called the *duration* of the (continuous) transition,

ii. η' = η and π'_{u} = 
    \{ 0 if C_{u,ρ(h,u),η_u} < 0 
    1 if C_{u,ρ(h,u),η_u} > 0 
\} for all u ∈ (first(h) ∪ σ)

where σ = {x ∈ sv(h) | δh(x) ≤ δ'_{first}},

iii. ∀z ∈ V \ (first(h) ∪ σ), then π'_z = π_z + δ_h(v) × C_{z,ρ(h,z),η_z}.

b. Or first(h) = ∅ (meaning that each variable v either reaches an equilibrium state: C<sub>v,ρ(h,v),η<sub>v</sub></sub> = 0; or faces a wall: v ∈ sv(h)) and:

i. ∀v ∈ sv(h), π'_v = 
    \{ 0 if C<sub>v,ρ(h,v),η<sub>v</sub></sub> < 0 
    1 if C<sub>v,ρ(h,v),η<sub>v</sub></sub> > 0 
\

ii. ∀u ∉ sv(h), π'_{u} = π_{u} (since in this case C_{u,ρ(h,u),η_u} = 0).

2. There exists a discrete transition in dT from state h' = (η', π') to state h'' = (η'', π'') iff there exists a variable v ∈ first(h') such that:

a. δh''(v) = 0, where δh''(v) is called the *duration* of the (discrete) transition,

b. η''_v = η'_v + sgn(C<sub>v,ρ(h',v),η'_v</sub>) and π''_v = 
    \{ 0 if C<sub>v,ρ(h',v),η'_v</sub> > 0 
    1 if C<sub>v,ρ(h',v),η'_v</sub> < 0 
\} ,

c. ∀u ∈ V \ {v}, η''_u = η'_u and π''_u = π'_u.

The states from which there do not exist any transitions (discrete or continuous) are called **steady states**.

The continuous transitions lead to the last hybrid state inside the current discrete state, at which point a qualitative change can happen. The *instantaneous* discrete transitions make the system evolve, as soon as the system can (that is, when $\delta_{h'}(v) = 0$), into the next qualitative state by going through a border. These two different kinds of transitions can be observed on Fig. 3 where the discrete transitions are in dotted lines and the continuous transitions are in plain lines. Let us remark that there is a unique continuous transition starting at a given hybrid state. Indeed, assuming that there exist two continuous transitions $h \to h_1$ and $h \to h_2$ from the same hybrid state $h$, the item 1 of the previous definition leads to the equality $h_1 = h_2$ regarding the ends of the continuous transitions (whatever the value of the set first($h$)).

Let us notice that the defined linear hybrid automata leads to an undeterministic behaviour: when the celerity vector allows the trajectory to reach more than one border at the same time, several discrete transitions can be considered (see Fig. 2-Center). Some of these discrete transitions can be forbidden in case of internal wall.

3 Hybrid Hoare Logic

This section is dedicated to the presentation of the Hoare logic adapted to our hybrid
formalism. Hoare logic is based on Hoare triples noted {Pre} p {Post} meaning that if a
program p is executed from a state satisfying a precondition Pre, then after execution, the
postcondition Post is true. In our case, the program p is replaced by a biological trace
characterising biological knowledge on the chronometrical qualitative behaviour of the system.

For this, we define the property language used for pre- and postconditions in Subsec. 3.1
and the path language used to describe observed traces in Subsec. 3.2. Then, Hoare logic
is defined using these languages and we give in Subsec. 3.3 an adaptation of the weakest
precondition calculus, that is, the computation of the weakest (the most general) precondition
that makes the trace possible and such that the postcondition *Post* is satisfied afterwards.
In the rest of this section, we denote by □ any of the usual comparison symbols on integers or real numbers: <, ≤, >, ≥, =, ≠.

## 3.1 Property Language

We first define the property language describing pre- and postconditions.

**► Definition 8 (Property Language $\mathcal{L}_C$).** The terms of the property language $\mathcal{L}_C$ are inductively defined as follows:

- A discrete term is a variable $\eta_u$ with $u \in V$, or a constant of $\mathbb{N}$;

- A continuous term is a variable $\pi_u$ or $\pi'_u$ with $u \in V$, or $C_{u,\omega,n}$ with $u \in V$, $\omega \subset R^-(u)$ and $n \in [0, b_u]$, or a constant of $\mathbb{R}$;

- The connectives $+$, $-$, $\times$ and $/$ create new terms by composition, the latter being only valid for continuous terms. We use their usual semantics.

Discrete atoms are of the form $n \sqcap n'$ where $n$ and $n'$ are discrete terms and continuous atoms are of the form $f \sqcap f'$ where $f$ and $f'$ are continuous terms.

The discrete conditions are defined by: $D ::= a_d | \neg D | D \land D | D \lor D$ where $a_d$ is a discrete atom.

The hybrid conditions are defined by: $H ::= a_d | a_c | \neg H | H \land H | H \lor H$ where $a_d$ and $a_c$ are respectively a discrete atom and a continuous one.

A property is a couple $(D, H)$ formed by a discrete and a hybrid condition. All such couples $(D, H)$ form the property language $\mathcal{L}_C$.

A hybrid state $h$ satisfies a property $\varphi = (D, H) \in \mathcal{L}_C$ iff both $D$ and $H$ hold in $h$, by using the usual meaning of the connectives; in this case, we note $h \models \varphi$.

## 3.2 Path Language

The path language given in Def. 12 takes the role of an imperative program in a Hoare triple by describing a biological behaviour. Such a path consists in explicit discrete transitions as given in Def. 9, but also in continuous transitions described by duration and some information, see Def. 10. The characterisation of continuous transitions is based on two kinds of atoms: $C_v \sqcap c$ constrains the value of the current celerity of $v$, and slide($v$) constrains $v$ to slide.

**► Definition 9 (Discrete Path Atom).** The (discrete) path atoms are defined by:
$dpa ::= v+ | v-$ where $v \in V$ is a variable name.

For any states $h = (\eta, \pi)$ and $h' = (\eta', \pi')$, the transition $h \xrightarrow{v+} h'$ (resp. $h \xrightarrow{v-} h'$) is satisfied iff there exists a discrete transition from $h$ to $h'$ so that $\eta'_v = \eta_v + 1$ (resp. $\eta'_v = \eta_v - 1$).

In the following, if $v \in V$ is a variable, $v \pm$ refers indistinctly to $v+$ or $v-$.

**► Definition 10 (Assertion Language $\mathcal{L}_A$).** The assertion language $\mathcal{L}_A$ is defined by the following grammar:

$$ a ::= \top | C_v \sqcap c | \text{slide}(v) | \text{slide}^{+}(v) | \text{slide}^{-}(v) | \neg a | a \land a | a \lor a $$

where $v \in V$ is a variable name and $c \in \mathbb{R}$ is a real number.

A couple $(\Delta t, a) \in \mathbb{R}^+ \times \mathcal{L}_A$ of a non-negative real number and an element of the assertion language is called an *assertion couple*.

The following definition gives the semantics of such assertion couples. From an informal point of view, for any states $h = (\eta, \pi)$ and $h' = (\eta', \pi')$ in the same qualitative state $\eta$, the continuous transition $h \rightarrow h'$ satisfies the assertion couple $(\Delta t, a)$ if the continuous transition exists and if it lasts $\Delta t$ units of time and it respects the assertion $a$: $\top$ is always true; $C_v \sqcap c$
## 5:8 Constraint Identification Using Modified Hoare Logic

is satisfied iff $C_{v,\rho(h,v),\eta_v} \square c$ where $C_{v,\rho(h,v),\eta_v}$ is the celerity of $v$ in the current qualitative state; $\text{slide}^+(v)$ (resp. $\text{slide}^-(v)$) is satisfied iff $v$ faces and reaches a wall at the top of the domain (resp. at the bottom); $\text{slide}(v)$ is a shorthand for $\text{slide}^+(v) \lor \text{slide}^-(v)$; and logical connectives have their usual meanings. We note indifferently $(h, h') \models (\Delta t, a)$ or $h \xrightarrow{(\Delta t, a)} h'$.

Regarding Def. 10, the special case where $\Delta t$ equals 0 characterises a situation where the system enters a qualitative state in a “corner” and no continuous transition is required between two successive discrete transitions.

**Definition 11 (Semantics of the Assertion Couple $(\Delta t, a)$).** Let us consider a hybrid state $h = (\eta, \pi)$ and the unique continuous transition starting from $h$ and ending in $h' = (\eta, \pi')$. The satisfaction relation between the continuous transition $h \rightarrow h'$ and an assertion couple $(\Delta t, a) \in \mathbb{R}^+ \times \mathcal{L}_A$ is noted $(h, h') \models (\Delta t, a)$, by overloading of notation, and is defined as follows:

- If $a \equiv \top$, $(h, h') \models (\Delta t, a)$ iff $\delta_h^{\text{first}} = \Delta t$.

- If $a$ is of the form $(C_u \square c)$, $(h, h') \models (\Delta t, a)$ iff $\delta_h^{\text{first}} = \Delta t$ and $(C_{u,\rho(h,u),\eta_u} \square c)$.

- If $a$ is of the form $\text{slide}(v)$, $(h, h') \models (\Delta t, a)$ iff $\delta_h^{\text{first}} = \Delta t$ and $\delta_h(v) < \delta_h^{\text{first}}$.

- If $a$ is of the form $\text{slide}^+(v)$ (resp. $\text{slide}^-(v)$), $(h, h') \models (\Delta t, a)$ iff $\delta_h^{\text{first}} = \Delta t$ and $\delta_h(v) < \delta_h^{\text{first}}$ and $C_{v,\rho(h,v),\eta_v} > 0$ (resp. $C_{v,\rho(h,v),\eta_v} < 0$).

- If $a$ is of the form $\neg a'$, $(h, h') \models (\Delta t, a)$ iff $\delta_h^{\text{first}} = \Delta t$ and $(h, h') \not\models (\Delta t, a')$.

- If $a$ is of the form $a' \wedge a''$ (resp. $a' \vee a''$), $(h, h') \models (\Delta t, a)$ iff $(h, h') \models (\Delta t, a')$ and (resp. or) $(h, h') \models (\Delta t, a'')$.

**Definition 12 (Path Language $\mathcal{L}_P$).** The (discrete) paths are defined by:

$$p ::= \varepsilon \mid (\Delta t, a, v \pm) \mid p; p$$

where $(\Delta t, a)$ is an assertion couple and $v \pm$ is a discrete path atom. The semantics of a path $p$ is given by the binary relation $\xrightarrow{p}$ between states defined by:

- If $p = \varepsilon$, then $h_1 \xrightarrow{p} h_2$ iff $h_1 = h_2$;

- If $p = (\Delta t, a, v \pm)$, then $h_1 \xrightarrow{p} h_2$ iff there exists a state $h'_1$ s.t. $h_1 \xrightarrow{(\Delta t, a)} h'_1$ and $h'_1 \xrightarrow{v \pm} h_2$;

- If $p \equiv p_1; p_2$, then $h_1 \xrightarrow{p_1} h_2$ iff there exists a state $h_3$ s.t. $h_1 \xrightarrow{p_2} h_3$ and $h_3 \xrightarrow{p_2} h_2$.

A path containing only $(\Delta t, a, v \pm)$ is called an *elementary path*.

The path language allows the modeller to express experimental biological traces as sequences of elementary paths. The next section shows how such information can be formally taken into account in order to help the identification of celerities compatible with such paths.

## 3.3 Hoare Triples and Weakest Precondition

We are now able to give the definition (Def. 13) of a Hoare triple in the scope of our hybrid formalism which is a natural extension of the classical definition. Figure 3 gives an example of a valid Hoare triple.

**Definition 13 (Hybrid Hoare Triples).** A Hoare triple for a given GRN is an expression of the form $\{\text{Pre}\} p \{\text{Post}\}$ where Pre and Post, called *precondition* and *postcondition* respectively, are properties of $\mathcal{L}_C$, and $p$ is a path from $\mathcal{L}_P$. A Hoare triple $\{\text{Pre}\} p \{\text{Post}\}$ is *satisfied* iff for all state $h_1 \models \text{Pre}$, there exists another state $h_2$ so that $h_1 \xrightarrow{p} h_2$ and $h_2 \models \text{Post}$.

Now that the semantics of this new Hoare logic is defined, we aim at adapting the weakest precondition calculus as proposed by Dijkstra [6] to our hybrid framework (Def. 14).
<figure><img src="image_6.png" /><figcaption>Figure 3 Hoare triple example: {$\mathit{PreC}$} ($\Delta_t^1$, $\top$, $g+$) {$\mathit{PostC}$}. Starting from the hybrid state $h_1 \models \mathit{PreC}$, and considering the path in bold line, it is possible to chain a continuous transition ($h_1 \rightarrow h'_1$) of duration $\Delta_t^1$ and a discrete transition ($h'_1 \rightarrow h_2$) leading to a $h_2 \models \mathit{PostC}$: this Hoare triple is therefore satisfied.</figcaption></figure>

Edsger Dijkstra introduced a *predicate transformer semantics*: the semantics of an imperative programming language is defined by assigning to each instruction in this language a corresponding predicate transformer. For each elementary instruction *EI* of the imperative programming language, the weakest precondition of *EI* is a function mapping any postcondition *Post* to a precondition *Pre*. Actually, this function returns the weakest precondition on the initial state ensuring that the execution of *EI* terminates in a final state satisfying *Post*. For each sequential imperative program *"P; EI"* whose last instruction is *EI*, and for each postcondition *Post*, the predicate transformer of *EI* allows us to first determine the weakest precondition just before the last instruction and by iterating the same process, it becomes possible to determine the weakest precondition of the whole imperative program (loops are treated in a particular way with the help of *invariants*).

In our setting, the same approach leads to build the minimal constraints on the celerities insuring that starting from a state satisfying the precondition *Pre*, the model exhibits the known path *p* (corresponding to a biological trace) leading to a state satisfying the postcondition *Post*. Each constraint depends on each elementary path which is defined by the time $\Delta t$ spent in the current qualitative state, the assertion *a* and the discrete path atom $v \pm$. Each elementary path takes the role of an elementary instruction.

**► Definition 14 (Weakest Precondition).** Let *p* be a path program and *Post* = (*D*, *H*<sub>*f*</sub>) be a post-condition parameterized by a final state index *f*. The *weakest precondition* attributed to *p* and *Post* is a property: $WP_f^i(p, Post) \equiv (D', H'_{i,f})$, parameterized by a fresh initial state index *i* and the same final state *f*, and whose value is recursively defined by:

- If $p = \varepsilon$ is the empty sequence program, then $D' \equiv D$ and $H'_{i,f} \equiv H_f$;

- If $p = (\Delta t, a, v+)$ is an atom, with $v \in V$:

- $D' \equiv D[\eta_v \setminus \eta_v + 1]$,

- $H'_{i,f} \equiv H_f[\eta_v \setminus \eta_v + 1] \wedge \Phi_v^+(\Delta t) \wedge \mathcal{F}(\Delta t) \wedge \neg W_v^+ \wedge \mathcal{A}(\Delta t, a) \wedge \mathcal{J}_v$;

- If $p = (\Delta t, a, v-)$ is an atom, with $v \in V$:

- $D' \equiv D[\eta_v \setminus \eta_v - 1]$,

- $H'_{i,f} \equiv H_f[\eta_v \setminus \eta_v - 1] \wedge \Phi_v^-(\Delta t) \wedge \mathcal{F}(\Delta t) \wedge \neg W_v^- \wedge \mathcal{A}(\Delta t, a) \wedge \mathcal{J}_v$;

- If $p = p_1; p_2$ is a concatenation of programs:

$$WP_f^i(p_1; p_2, Post) \equiv WP_m^i(p_1, WP_f^m(p_2, Post))$$

which is parameterized by a fresh intermediate state index *m*;
## 5:10 Constraint Identification Using Modified Hoare Logic

where $\Phi_v^+(\Delta t)$, $\Phi_v^-(\Delta t)$, $W_v^+$, $W_v^-$, $\mathcal{F}(\Delta t)$, $\mathcal{A}(\Delta t, a)$ and $\mathcal{J}_v$ are sub-properties detailed in Appendix A.

We note that in the cases corresponding to atoms $p = (\Delta t, a, v\pm)$, the formula $H'_{i,f}$ contains $H_f$ with substitutions, in conjunction with $\Phi_v^+(\Delta t), \neg W_v^+, \mathcal{F}(\Delta t), \mathcal{A}(\Delta t, a)$ and $\mathcal{J}_v$, which makes the weakest precondition of a sequence of instructions very big and difficult to compute or analyse by hand. Nevertheless, each of the previous subformulas corresponds to a condition which has to be met to allow the execution of an atomic instruction $(\Delta t, a, v\pm)$:

- The sign of the celerity of $v$ in the current state is given by $v\pm$;

- Traversing the qualitative state lasts $\Delta t$ units of time ($\Phi_v^+(\Delta t)$);

- There is no internal or external wall preventing $v$ to increase or decrease its qualitative state ($\neg W_v^+$);

- All components other than first changing variables must either reach their border after $v$, or face an internal or external wall ($\mathcal{F}(\Delta t)$).

- The assertion $a$ is verified along the continuous transition ($\mathcal{A}(\Delta t, a)$);

- The continuous transition inside a discrete state links the fractional parts of $v$, its celerity and time spent in the current discrete state. Similarly the discrete transition indicates that the fractional parts of states before and after a discrete transition are the same except for the variable $v$ changing its discrete level ($\mathcal{J}_v$).

Finally, the computation of the weakest precondition for a given Hoare triple $\{Pre\} p \{Post\}$ is automated using the classical backward proof strategy:

- If $p$ is of the form $(\Delta t, a, v\pm)$ or $\varepsilon$, then we compute the precondition.

- If $p = p_1; p_2$ with $p_2 = (\Delta t, a, v\pm)$, we compute the precondition before $p_2$ and we iterate for path $p_1$ (we never consider $p_2$ as $\varepsilon$).

These two items are mutually exclusive which means that the proof strategy generates a unique proof tree.

An implementation of this weakest precondition calculus has been realised<fnref n="2" />. Section 5 details its result on a model of the circadian clock and before that, next section gives the theorem of its soundness.

# 4 Soundness of the Hybrid Hoare Logic

## 4.1 Inference Rules and Axioms

The considered Hoare logic for hybrid gene regulatory networks is defined by the following inference rules:

$$ \text{Incrementation rule:} \qquad \left\{ \begin{array}{l} D[\eta_v \setminus \eta_v + 1] \\ H'_{i,f} \end{array} \right\} \begin{pmatrix} \Delta t \\ a \\ v+ \end{pmatrix} \left\{ \begin{array}{l} D \\ H_f \end{array} \right\} $$

$$ \text{Decrementation rule:} \qquad \left\{ \begin{array}{l} D[\eta_v \setminus \eta_v - 1] \\ H'_{i,f} \end{array} \right\} \begin{pmatrix} \Delta t \\ a \\ v- \end{pmatrix} \left\{ \begin{array}{l} D \\ H_f \end{array} \right\} $$

where $v$ is a variable, $\eta_v$ its expression level, $D$ (resp. $H$) the discrete (resp. hybrid) condition, $H'_{i,f} \equiv H_f[\eta_v \setminus \eta_v + 1] \land \Phi_v^+(\Delta t) \land \mathcal{F}(\Delta t) \land \neg W_v^+ \land \mathcal{A}(\Delta t, a) \land \mathcal{J}_v$ (Incrementation rule), or $H'_{i,f} \equiv H_f[\eta_v \setminus \eta_v - 1] \land \Phi_v^-(\Delta t) \land \mathcal{F}(\Delta t) \land \neg W_v^- \land \mathcal{A}(\Delta t, a) \land \mathcal{J}_v$ (Decrementation rule),

<footnote n="2">² Available at: http://www.i3s.unice.fr/~comet/DOCUMENTS/hybridisation.tar.gz.</footnote>
both detailed in Appendix A, Δt the time spent inside the current discrete state and a an
assertion. The last inference rule is the sequential composition rule:

$$
\text{Sequential composition rule: } \frac{\{Q_1\} p_1 \{Q_3\} \quad \{Q_3\} p_2 \{Q_2\}}{\{Q_1\} p_1; p_2 \{Q_2\}}
$$

where $Q_1, Q_2, Q_3$ are properties of the form $(D, H)$ having the role of pre- and postconditions,
and $p_1$ and $p_2$ are particular paths deduced from biological experiments.

The two following axioms, based on the semantics of the hybrid model, complement the
inference rules:

- $\eta_v \ge 0 \land \eta_v \le b_v$ (the expression level has to be in its definition domain),

- $C_{v,\omega,\eta_v} \times C_{v,\omega,\eta_v+1} \ge 0$ (for two neighbour qualitative states, if the variable $v$ is controlled by the same resources, then the celerities of $v$ cannot be of opposite signs).

## 4.2 Soundness of the Hoare logic

The following lemmas are useful for the proof of soundness. Lemma 15 states that the time spent in the current discrete state is equal to the time mandatory, for the variable which changes first, to reach its border. Lemma 16 expresses the fact that the truth value of a formula remains the same after a continuous transition.

**Lemma 15 (Time Spent in a Discrete State).** Let $h$ be a hybrid state. If $h \models (D_1, H_1)$ and $H_1 \Rightarrow \Phi_v^+(\Delta t) \wedge \mathcal{F}(\Delta t)$ (resp. $H_1 \Rightarrow \Phi_v^-(\Delta t) \wedge \mathcal{F}(\Delta t)$), then: $\delta_h^{\text{first}} = \delta_h(v) = \Delta t$.

**Proof.** Let us consider $H_1 \Rightarrow \Phi_v^+(\Delta t) \wedge \mathcal{F}(\Delta t)$ (resp. $H_1 \Rightarrow \Phi_v^-(\Delta t) \wedge \mathcal{F}(\Delta t)$). Let $h = (\eta, \pi)$ be a hybrid state such that $h \models (D_1, H_1)$.

From the definition of the sub-property $\Phi_v^+(\Delta t)$, see Appendix A.2, variable $v$ reaches its
upper border ($\pi_v' = 1$) and its celerity is positive ($C_{v,\omega,n} > 0$). Let $h' = (\eta, \pi')$ be the hybrid
state where $v$ first touches this border. The time spent in the current qualitative state $\eta$
corresponds to the time necessary to reach the border where $v$ changes its qualitative level.
Indeed, from $\Phi_v^+(\Delta t)$ we deduce:

$$
\pi_v^i = \pi_v^{i'} - C_{v,\omega,n} \cdot \Delta t = 1 - C_{v,\omega,n} \cdot \Delta t, \quad \text{that is,} \quad \Delta t = \frac{1 - \pi_v^i}{C_{v,\omega,n}}.
$$

From Def. 4, we have $\Delta t = \delta_h(v)$.

Finally, the sub-property $\mathcal{F}(\Delta t)$, see Appendix A.4, expresses the fact that if a variable $u$ different from $v$ reaches its border before $v$, $u$ faces an internal or external wall (see Appendix A.3). Thus, since $\delta_h(v) = \Delta t$ and according to Def. 6, we deduce $\delta_h^{\text{first}} = \delta_h(v) = \Delta t$. ◀

**Lemma 16 (Preservation of Formulas Evaluation Along a Continuous Transition).** Let us consider a Hoare triple $\{(D', H'_{i,f})\} p \{(D, H_f)\}$ obtained by the weakest precondition calculus, a hybrid state $h = (\eta, \pi^i)$, and finally the unique continuous transition $h \rightarrow h'$ starting from $h$. If $h \models (D', H'_{i,f})$, then $h' \models (D', H'_{i,f})$.

Proof.

- Since $h$ and $h'$ belong to the same discrete state, the expression levels of all variables are the same. The evaluation of $D'$ in $h'$ is then the evaluation of $D'$ in $h$.

- The atoms of $H'_{i,f}$ (see subformulas in Appendix A) concern either celerities or discrete or continuous coordinates of different points of the trajectory (entrance and arrival points in different discrete states). These points are either outside the current discrete state, or are the points $h$ or $h'$.
## 5:12 Constraint Identification Using Modified Hoare Logic

Moreover, the celerities are constants, the points of the trajectory which do not belong to the current discrete state as well as the points *h* and *h'* do not change.

The interpretation of ($D', H'_{i,f}$) is therefore the same in *h* and *h'*.

The soundness of the modified Hoare logic, adapted for the hybrid modelling framework, means that if a Hoare triple is built in agreement with the inference rules (Def. 14) then this Hoare triple is satisfied according to the semantics of Hoare triples (Def. 13).

► **Theorem 17.** *The hybrid Hoare logic is sound.*

The proof is detailed in Appendix B.

# 5 Example: Simplified Circadian Cycle

The circadian rhythm is a biological process regulating cells of an organism with a 24-hour period and controlling the electrical and metabolic processes.

## 5.1 Presentation of the Circadian Cycle

In mammals, the main circadian cycle is located in the suprachiasmatic nucleus and regulates the peripheral clocks. It is affected by light, acting like a synchronizer called *Zeitgeber*, which means “giver of time”.

The circadian rhythm is mainly controlled by two protein complexes which are PER/CRY and BMAL1/CLOCK. When light appears, the BMAL1/CLOCK complex activates the *per* and *cry* genes by binding the *E-box* response element in the promoter upstream these genes [12]. The PER and CRY proteins are synthesized and dimerised in the cytoplasm. During night, this complex is found inside the nucleus and inhibits BMAL1/CLOCK implying a negative feedback of PER/CRY on its genes. Finally, PER/CRY is degraded by proteasome. The circadian cycle completes and a new one begins with the transcription of genes *bmal1* and *clock*.

We decided to use an interaction graph which focuses on the *per* and *cry* components, as represented in Fig. 1. The Light/Day cycle (whose duration is 12h/12h) is represented by the node named *L*. (Let us notice that the node labelled *X* is a modelling artefact to get an oscillating feature for light.) This node enhances the *per* and *cry* genes (modelled with node *g*) when the light is activated, that is, when the qualitative value of *L* is at level 1. These genes synthesize their proteins which complex and spread inside the nucleus. When the complex is activated (which is modelled by an expression level of 1 for *pc*), those genes are inhibited, blocking the synthesis during night. Because genes are disabled, the protein complex will be degraded by proteasome and a new cycle begins with the reactivation of the genes. All four nodes of this model have two qualitative levels of expression named 0 (not active) and 1 (active).

## 5.2 Hoare Triple and Results

The steps of the circadian clock explained in Subsec. 5.1 are represented in the Hoare Triple below. The time spent in each qualitative state comes from biological information obtained during a light/day cycle of 12h/12h. The assertions slide$^+$(*g*) and slide$^+$(*pc*) (resp. slide$^-$(*L*)) characterize a saturation (resp. complete degradation) of *g* and *pc* (resp. of *L*, corresponding
<table><caption>Table 1 Constraints obtained by computation of the weakest precondition. Left: Constraints on celerities of *g* and *pc*. Right: Constraints on celerities of *L* and *X*.</caption><thead><tr><th colspan="2">Constraints on celerities of g and pc</th><th colspan="2">Constraints on celerities of L and X</th></tr></thead><tbody><tr><td>C<sub>g,Ø,0</sub> &lt; 0</td><td>0 &lt; C<sub>g,{pc,L}0</sub></td><td>-<sup>1</sup>&frasl;<sub>0.6</sub> &lt; C<sub>L,Ø,0</sub> &lt; 0</td><td>C<sub>X,Ø,0</sub> &lt; 0</td></tr><tr><td>C<sub>g,Ø,1</sub> &lt; 0</td><td>0 &lt; C<sub>g,{pc,L},1</sub> &lt; <sup>1</sup>&frasl;<sub>5.53</sub></td><td>C<sub>L,Ø,1</sub> &lt; 0</td><td>-<sup>1</sup>&frasl;<sub>6</sub> &le; C<sub>X,Ø,1</sub> &lt; 0</td></tr><tr><td>C<sub>g,{L},0</sub> &lt; 0</td><td>C<sub>pc,Ø,0</sub> &lt; 0</td><td>0 &lt; C<sub>L,{X},0</sub></td><td>0 &lt; C<sub>X,{L},0</sub> &lt; <sup>1</sup>&frasl;<sub>5.1</sub></td></tr><tr><td>C<sub>g,{L},1</sub> &lt; 0</td><td>C<sub>pc,Ø,1</sub> = -<sup>0.12</sup>&frasl;<sub>0.9</sub></td><td>0 &lt; C<sub>L,{X},1</sub></td><td>0 &lt; C<sub>X,{L},1</sub></td></tr><tr><td>C<sub>g,{pc},0</sub> &gt; 0</td><td>0 &lt; C<sub>pc,{g},0</sub> &lt; <sup>1</sup>&frasl;<sub>6.13</sub></td><td></td><td></td></tr><tr><td>C<sub>g,{pc},1</sub> &gt; 0</td><td>0 &lt; C<sub>pc,{g},1</sub> &lt; <sup>1</sup>&frasl;<sub>5.4</sub></td><td></td><td></td></tr></tbody></table>

to the beginning of the night). This information is summed up in the following Hoare triple:

$$ \{D_8\} \begin{array}{c} \begin{pmatrix} 0.9 \\ \top \\ pc- \end{pmatrix} \\ H_8 \end{array} ; \begin{array}{c} \begin{pmatrix} 4.5 \\ \top \\ g+ \end{pmatrix} \\ H_8 \end{array} ; \begin{array}{c} \begin{pmatrix} 0.6 \\ \top \\ X+ \end{pmatrix} \\ H_8 \end{array} ; \begin{array}{c} \begin{pmatrix} 5.53 \\ pc+ \end{pmatrix} \\ H_8 \end{array} ; \begin{array}{c} \begin{pmatrix} 0.47 \\ \top \\ L- \end{pmatrix} \\ H_8 \end{array} ; \begin{array}{c} \begin{pmatrix} 5.4 \\ g- \end{pmatrix} \\ H_8 \end{array} ; \begin{array}{c} \begin{pmatrix} 0.6 \\ X- \end{pmatrix} \\ H_8 \end{array} ; \begin{array}{c} \begin{pmatrix} 6 \\ \top \\ L+ \end{pmatrix} \\ H_8 \end{array} ; \{D_0\} $$

$$ \text{where} \quad \begin{cases} D_0 \equiv (\eta_g = 0) \land (\eta_{pc} = 1) \land (\eta_L = 1) \land (\eta_X = 0) \\ H_0 \equiv (\pi_g = 0.12) \land (\pi_{pc} = 0.12) \land (\pi_L = 0) \land (\pi_X = 0) \end{cases} $$

Using this Hoare triple, we compute *via* the backward strategy the weakest precondition iteratively by crossing the intermediate states of the path. In addition, because the behaviour is cyclic, we know that the starting hybrid state of this path is equal to the finishing one. The provided implementation allows us to identify and simplify the constraints of the celerities obtained through our weakest precondition calculus. After some automatic and manual simplifications, we finally obtain the constraints summed up in Table 1 which make the known cyclic behaviour possible.

In order to illustrate the validity of this process, we used the constraint solver IBEX<fnref n="3" /> to extract values satisfying the previous constraints. This constraint solver takes as input only conjunctions. Thus the obtained constraints are transformed in a disjunctive normal form (we obtained 3 terms in disjunction) and all terms of this disjunction are successively given to IBEX to extract possible values for variables. Amongst the values returned by IBEX, we arbitrarily chose one set of possible values to be injected in the model for simulation. Interestingly, the obtained constraints fully characterize one of the hybrid states along the limit cycle, which gives us an initial state for the simulation.

The simulated traces have then to be compared to biological experimental data. Because such data for the PER/CRY protein complex inside the nucleus are not published, the simulation (Fig. 4) is compared to experimental data of genes *per1*, *per2*, *cry1* and *cry2* as well as their respective proteins taken separately [13]. We noticed that the maximal activity of *per* genes of our simulation and experimental data occurs at the end of a day, and the curves of proteins are maximal during night at the same time slot for both curves. Thus our simplified circadian cycle model is consistent with biological experimental data although we arbitrarily used parameter values satisfying constraints. This simulation reinforces reliability of our formalism for determining constraints.

<footnote n="3">³ See http://www.ibex-lib.org/.</footnote>
5:14 Constraint Identification Using Modified Hoare Logic

<figure><img src="image_7.png" /><figcaption>Figure 4 Model simulation based on arbitrarily chosen celerities satisfying the deduced constraints. The plain (resp. dashed) line represents the PER/CRY complex (resp. gene) activity.</figcaption></figure>

6 Conclusion

In this paper, we have developed a suitable approach to determine constraints on the
parameters of a linear hybrid automaton. Our hybrid Hoare logic combined with experimental
biological traces including precise chronometrical information leads to constraints on celerities
which have to be satisfied to allow the model to represent the observed behaviour (HCSP [18]
is a formalism similar to ours but does not include chronometrical information along the
path). The obtained constraints *via* the weakest precondition calculus are analysed using
the solver IBEX which extracts all admissible intervals of celerities. Choosing celerity values
satisfying these constraints leads to a model which exhibits simulation traces similar to the
aforementioned experimental data, this approach has been tested on the simplified circadian
clock model.

The soundness of our hybrid Hoare logic is proved which means that simulations obtained
with parameters satisfying the computed precondition leads to simulated traces which are in
concordance with the path representing the experimental data.

This work opens many outlooks. Generally, it is useful to prove the completeness of
the weakest precondition calculus. Because of the continuous terms (real numbers), our
hybrid Hoare logic cannot be complete regarding all possible formulas. Nevertheless, we
think that our hybrid Hoare logic should be complete regarding closed propositional formulas
constructed from polynomial (in)equations and logical connectors. The decidability of the
theory of real closed fields implies that the precondition constraints can be analysed; it does
not mean that for each semantically correct Hoare triple, there exists a proof tree built on
our inference rules. Completeness of our framework would mean that if a Hoare triple is
semantically correct and if pre- and postconditions are expressions in the first order language
of real closed fields, then there exists a proof tree for this Hoare triple. Finally, because of
the combinatorial explosion of the size of the weakest precondition formula and despite some
on-the-fly simplifications, it could be interesting to investigate other ways to simplify the
result in some particular cases.

**Acknowledgements.** We are grateful to F. Delaunay for having shared his expertise on the circadian clock and to E. Cornillon and G. Bernot for fruitful discussions about the hybrid formalism.
References

1 J. Behaegel, J.-P. Comet, G. Bernot, E. Cornillon, and F. Delaunay. A hybrid model of cell cycle in mammals. *JBCB*, 14(1):1640001 [17 pp.], 2016.

2 G. Bernot, J.-P. Comet, Z. Khalis, A. Richard, and O. Roux. A genetically modified Hoare logic. *ArXiv: 1506.05887*, June 2015.

3 G. Bernot, J.-P. Comet, A. Richard, and J. Guespin. Application of formal methods to biological regulatory networks: extending thomas' asynchronous logical approach with temporal logic. *Journal of theoretical biology*, 229(3):339-347, 2004.

4 G. Bernot, J.-P. Comet, and O. Roux. A genetically modified Hoare logic that identifies the parameters of a gene networks. In O. Roux and J. Bourdon, editors, *CMSB'15*, volume 9308 of LNBI, pages 8-12, 2015.

5 F. Corblin, E. Fanchon, and L. Trilling. Applications of a formal approach to de-cipher discrete genetic networks. *BMC Bioinformatics*, 11:385, 2010. doi:10.1186/1471-2105-11-385.

6 E. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. *Commun. ACM*, 18:453-457, August 1975. doi:10.1145/360933.360975.

7 F. Fages. Temporal logic constraints in the biochemical abstract machine BIOCHAM. In *Logic Based Program Synthesis and Transformation, 15th International Symposium, LOP-STR 2005, London, UK, September 7-9, 2005, Revised Selected Papers*, pages 1-5, 2005. doi:10.1007/11680093_1.

8 N. Halbwachs, Y.-É. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In Baudouin Le Charlier, editor, *Proceedings of the First International Static Analysis Symposium (SAS'94)*, pages 223-237. Springer Berlin Heidelberg, 1994.

9 T. Henzinger. The theory of hybrid automata. In M. Kemal Inan and Robert P. Kurshan, editors, *Verification of Digital and Hybrid Systems*, pages 265-292. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000. doi:10.1007/978-3-642-59615-5_13.

10 T. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. In Orna Grumberg, editor, *Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97)*, pages 460-463. Springer Berlin Heidelberg, 1997.

11 J. Hooman. Extending Hoare logic to real-time. *Formal Aspects of Computing*, 6:801-825, 1994.

12 T. Hunt and P. Sassone-Corsi. Riding tandem: circadian clocks and the cell cycle. *Cell*, 129(3):461-464, 2007.

13 C. Lee, J.-P. Etchegaray, F. Cagampang, A. Loudon, and S. Reppert. Posttranslational mechanisms regulate the mammalian circadian clock. *Cell*, 107(7):855-867, 2001.

14 T. Liu, X. Zhang, and X. Gao. Stability analysis for continuous-time and discrete-time genetic regulatory networks with delays. *Applied mathematics and computation*, 274:628-643, 2016.

15 R. Thomas. Boolean formalization of genetic control circuits. *Journal of theoretical biology*, 42(3):563-585, 1973.

16 R. Thomas and M. Kaufman. Multistationarity, the basis of cell differentiation and memory. II. logical analysis of regulatory networks in terms of feedback circuits. *Chaos*, 11:180-195, 2001.

17 P. Traynard, A. Fauré, F. Fages, and D. Thieffry. Logical model specification aided by model-checking techniques: application to the mammalian cell cycle regulation. *Bioinformatics*, 32(17):772-780, 2016. doi:10.1093/bioinformatics/btw457.

18 N. Zhan, S. Wang, and H. Zhao. Formal modelling, analysis and verification of hybrid systems. In *Unifying Theories of Programming and Formal Engineering Methods*, pages 207-281. Springer, 2013.
## A Appendix: Sub-properties of the Weakest Precondition Calculus

In this appendix, we detail each subformula of the weakest precondition in Def. 14.

### A.1 Weakest Precondition

In order to fully compute the weakest precondition, it is required to label the fractional parts of the states mentioned in the properties. For this, we use labels called below $f$ (final), $i$ (initial) and $m$ (intermediate). Moreover, by convention, we use $\pi'$ (resp. $\pi$) to specify the fractional part of the exit from the current discrete state (resp. entrance into the current discrete state).

Let us notice that all the following properties depend on the indices $i$ and $f$ used in Def. 14, although for readability issues we did not mention them on the names of each sub-property. Furthermore, for a given index $i$, we call by convention $\pi_u^i$ (resp. $\pi_u^{i'}$) the fractional part of the entering (resp. exiting) state inside the discrete state $i$.

Finally, for all variable $u \in V$ and all $\omega \subset R^-(v)$ subset of predecessors of $u$, we define:

$$ \Phi_v^\omega \equiv \left( \bigwedge_{m \in \omega} \varphi_m \right) \wedge \left( \bigwedge_{m \in R^{-1}(v) \setminus \omega} \neg \varphi_m \right). $$

In other words, $\Phi_v^\omega$ is true in a state $h$ if and only if the resources of $u$ are exactly $\omega$, that is, $\rho(h, v) = \omega$.

### A.2 Discrete Transition to the Next Discrete State

For all component $v \in V$, $\Phi_v^+(\Delta t)$ (resp. $\Phi_v^-(\Delta t)$) describes the conditions in which $v$ increases (resp. decreases) its discrete expression level after $\Delta t$ units of time: its celerity in the current state must be positive (resp. negative) and its fractional part only depends on $\Delta t$ in the way given at the very end of Section 2.

$$ \Phi_v^+(\Delta t) \equiv (\pi_v^{i'} = 1) \wedge \bigwedge_{\substack{\omega \subset R^-(v) \\ n \in [0, b_v]}} \left( \left( \Phi_v^\omega \wedge (\eta_v = n) \right) \Rightarrow (C_{v,\omega,n} > 0) \wedge (\pi_v^i = \pi_v^{i'} - C_{v,\omega,n} \cdot \Delta t) \right), $$

$$ \Phi_v^-(\Delta t) \equiv (\pi_v^{i'} = 0) \wedge \bigwedge_{\substack{\omega \subset R^-(v) \\ n \in [0, b_v]}} \left( \left( \Phi_v^\omega \wedge (\eta_v = n) \right) \Rightarrow (C_{v,\omega,n} < 0) \wedge (\pi_v^i = \pi_v^{i'} - C_{v,\omega,n} \cdot \Delta t) \right). $$

### A.3 Internal and External Walls

For all component $u \in V$, $W_u^+$ (resp. $W_u^-$) states that there is a wall preventing $u$ to increase (resp. decrease) its qualitative state. This wall can either be an external wall $EW_u^+$ (resp. $EW_u^-$) or an internal wall $IW_u^+$ (resp. $IW_u^-$). Furthermore, $\Phi_{u+}^{\omega'}$ (resp. $\Phi_{u-}^{\omega'}$), which is required in these subformulas, is true if and only if the set of resources of $u$ is exactly $\omega'$ in the state where $u$ is increased (resp. decreased) by 1.

$$ W_u^+ \equiv IW_u^+ \vee EW_u^+ \quad \text{and} \quad W_u^- \equiv IW_u^- \vee EW_u^- $$

where:

$$ EW_u^+ \equiv (\eta_u = b_u) \wedge \bigwedge_{\substack{\omega \subset R^-(u) \\ \omega \in [0, b_u]}} (\Phi_u^\omega \Rightarrow C_{u,\omega,b_u} > 0) , $$

$$ EW_u^- \equiv (\eta_u = 0) \wedge \bigwedge_{\substack{\omega \subset R^-(u) \\ \omega \in [0, b_u]}} (\Phi_u^\omega \Rightarrow C_{u,\omega,0} < 0) , $$
$$ \mathrm{IW}_{u}^{+} \equiv (\eta_{u} < b_{u}) \wedge \bigwedge_{\substack{\omega, \omega' \subset R^{-}(u) \\ n \in [0, b_{u}]}} \left( \begin{array}{c} (\eta_{u} = n) \wedge \\ (m = n + 1) \wedge \\ \Phi_{u}^{\omega} \wedge \Phi_{u+}^{\omega'} \end{array} \right) \Rightarrow C_{u, \omega, n} > 0 \wedge C_{u, \omega', m} < 0) , $$

$$ \mathrm{IW}_{u}^{-} \equiv (\eta_{u} > 0) \wedge \bigwedge_{\substack{\omega, \omega' \subset R^{-}(u) \\ n \in [0, b_{u}]}} \left( \begin{array}{c} (\eta_{u} = n) \wedge \\ (m = n - 1) \wedge \\ \Phi_{u}^{\omega} \wedge \Phi_{u-}^{\omega'} \end{array} \right) \Rightarrow C_{u, \omega, n} < 0 \wedge C_{u, \omega', m} > 0) , $$

$$ \Phi_{u+}^{\omega'} \equiv (\eta_u < b_u) \wedge \bigwedge_{n \in [0, b_u]} ((\eta_u = n) \Rightarrow \Phi_u^{\omega'}[\eta_u \setminus \eta_u + 1]) , $$

$$ \Phi_{u-}^{\omega'} \equiv (\eta_u > 0) \wedge \bigwedge_{n \in [0, b_u]} ((\eta_u = n) \Rightarrow \Phi_u^{\omega'}[\eta_u \setminus \eta_u - 1]) . $$

## A.4 First Changing Variables

$\mathcal{F}(\Delta t)$ states that all components that are not first changing variables must either reach their border after the first changing variables, or face an internal or external wall.

$$ \mathcal{F}(\Delta t) \equiv \bigwedge_{u \in V \setminus \text{first}(h_i)} \left[ \left( \bigwedge_{\substack{\omega \subset R^{-}(u) \\ n \in [0, b_u]}} \left( \begin{array}{c} (\eta_u = n) \wedge \Phi_u^{\omega} \wedge \\ C_{u, \omega, n} > 0 \wedge \\ \pi_u^i > \pi_u^{i'} - C_{u, \omega, n} \cdot \Delta t \end{array} \right) \Rightarrow \mathcal{W}_u^+ \right) \wedge \right. \\ \left. \left( \bigwedge_{\substack{\omega \subset R^{-}(u) \\ n \in [0, b_u]}} \left( \begin{array}{c} (\eta_u = n) \wedge \Phi_u^{\omega} \wedge \\ C_{u, \omega, n} < 0 \wedge \\ \pi_u^i < \pi_u^{i'} - C_{u, \omega, n} \cdot \Delta t \end{array} \right) \Rightarrow \mathcal{W}_u^- \right) \right] . $$

## A.5 Hybrid Assertions

The sub-property $\mathcal{A}(\Delta t, a)$ allows one to translate all assertion symbols given about the continuous transition related to the instruction (celerities and slides) into a property:

$$ \mathcal{A}(\Delta t, a) \equiv \bigwedge_{\substack{k \in [1, n] \\ \omega_k \in R^{-}(v_k) \\ n_k \in [0, b_k]}} \left( \bigwedge_{l \in [1, n]} ((\eta_{vl} = n_l) \wedge \Phi_{vl}^{\omega_l}) \Rightarrow a \left[ \begin{array}{c} C_{vl} \setminus C_{vl, \omega_l, n_l} \\ \mathbf{slide}(v_l) \setminus S_{vl, \omega_l, n_l}(\Delta t) \\ \mathbf{slide}^{+}(v_l) \setminus S_{vl, \omega_l, n_l}^{+}(\Delta t) \\ \mathbf{slide}^{-}(v_l) \setminus S_{vl, \omega_l, n_l}^{-}(\Delta t) \end{array} \right] \right) $$

where $a$ is the assert part of the instruction $P = (\Delta t, a, v_{\pm})$, and, for all variable $u \in V$:

$$ S_{u, \omega, n}^{+}(\Delta t) \equiv (\pi_{u}^{i'} = 1) \wedge (\pi_{u}^{i} > \pi_{u}^{i'} - C_{u, \omega, n} \cdot \Delta t) , $$

$$ S_{u, \omega, n}^{-}(\Delta t) \equiv (\pi_{u}^{i'} = 0) \wedge (\pi_{u}^{i} < \pi_{u}^{i'} - C_{u, \omega, n} \cdot \Delta t) , $$

$$ S_{u, \omega, n}(\Delta t) \equiv S_{u, \omega, n}^{+}(\Delta t) \vee S_{u, \omega, n}^{-}(\Delta t) . $$

These sub-properties indicate that the exit position of the corresponding variable $u$ is located on a threshold. In addition, the constraints $\pi_u^i > \pi_u^{i'} - C_{u,\omega,n} \cdot \Delta t$ and $\pi_u^i < \pi_u^{i'} - C_{u,\omega,n} \cdot \Delta t$ mean that the duration before reaching the border is lower than the one spent inside the current state $(\Delta t)$. The sign of the celerity of the sliding variable $u$ is constrained by the sub-property $\mathcal{F}$ and the constraint $\pi_u^i > \pi_u^{i'} - C_{u,\omega,n} \cdot \Delta t$ (resp. $\pi_u^i < \pi_u^{i'} - C_{u,\omega,n} \cdot \Delta t$) of the sub-property $S_{u,\omega,n}^{+}(\Delta t)$ (resp. $S_{u,\omega,n}^{-}(\Delta t)$) or $S_{u,\omega,n}(\Delta t)$.
## A.6 Junctions

### A.6.1 Continuous Junctions Inside Discrete States

For all component $v \in V$, and for a continuous transition between two hybrid states $h = (\eta, \pi)$ and $h' = (\eta, \pi')$, $C\mathcal{J}_v$ establishes a relationship between the fractional parts and the celerity of the variable $v$. If the exit fractional part of $v$ is 0 or 1, the sign of the celerity can be deduced and the time mandatory to $v$ to reach the border is lower than the time spent in the current discrete state. If $v$ does not reach its border, the exact position of the entrance fractional part of $v$ can be deduced from the exit position, the time spent in the current discrete state and the celerity.

$$ C\mathcal{J}_v \equiv \begin{cases} (\pi'_v = 0) & \Rightarrow C_{v,\rho(h,v),\eta_v} < 0 \land (\pi_v \le \pi'_v - C_{v,\rho(h,v),\eta_v} \times \delta_h^{\text{first}}) \\ (\pi'_v = 1) & \Rightarrow C_{v,\rho(h,v),\eta_v} > 0 \land (\pi_v \ge \pi'_v - C_{v,\rho(h,v),\eta_v} \times \delta_h^{\text{first}}) \\ (0 < \pi'_v < 1) & \Rightarrow (\pi_v = \pi'_v - C_{v,\rho(h,v),\eta_v} \times \delta_h^{\text{first}}) \end{cases} $$

### A.6.2 Discrete Junctions Between Discrete States

For all component $v \in V$, and for a discrete transition happening on component $v$ between an initial and a final state corresponding to the indices $i$ and $f$, $D\mathcal{J}_v$ establishes a junction between the fractional parts of these states. This formula states that the fractional part of $v$ switches from 1 to 0 for an increase, or from 0 to 1 for a decrease, whereas all other fractional parts are unchanged:

$$ D\mathcal{J}_v \equiv (\pi_v^f = 1 - \pi_v^{i'}) \land \bigwedge_{u \in V \setminus \{v\}} (\pi_u^f = \pi_u^{i'}) $$

Finally, we define:

$$ \mathcal{J}_v \equiv D\mathcal{J}_v \land \bigwedge_{u \in V} C\mathcal{J}_u $$

These relationships can be easily observed on Fig. 3 on the discrete transition in the centre: all fractional parts are left the same, except for the variable performing the transition.

## B Soundness Proof

The soundness proof is made for each inference rule which depends on its corresponding assertion (Def. 11). Each of them is treated according to the assertion type. We focus here on the proof of the soundness of the incrementation rule since the proof of the soundness of the decrementation rule is similar, and that the one for the sequential composition rule is classical. In this subsection, we consider the Hoare triple associated with the incrementation rule, described in Subsection 4.1, and a hybrid state $h = (\eta, \pi)$ satisfying the precondition.

### B.1 First Case: $a = \top$

(α) Let us first prove the existence of the continuous transition. According to the sub-property $\Phi_v^+(\Delta t)$, $\pi'_v = 1$ (arrival at the top border of $v$), $C_{v,\omega,n} > 0$ and $\pi'_v = \pi_v + C_{v,\omega,n} \times \Delta t$ (the time spent in the current state is $\Delta t$) if $\Phi_v^\omega$ and $\eta_v = n$ are satisfied. Let us also consider the unique hybrid state $h' = (\eta, \pi')$ such that the continuous transition $h \to h'$ exists. Thus, according to Lemma 15 and Definition 11, $(h, h') \models (\Delta t, \top)$.
(β) Let us now prove the existence of the discrete transition. Let us simplify the subformula $\neg W_v^+ \equiv \neg EW_v^+ \wedge \neg IW_v^+$ satisfied at $h'$. We have:

$$ \neg EW_v^+ \equiv \neg \left[ \underbrace{\left( \eta_v = b_v \right)}_{\omega \subset R^{-}(v)} \wedge \bigwedge \left( \Phi_v^\omega \Rightarrow C_{v,\omega,b_v} > 0 \right) \right] \equiv \top $$

which is evaluated to true because $v$ increases its level ($v+$ is the discrete path atom) and thus is not already at its maximal discrete value. Thus, $\neg W_v^+ \equiv \neg IW_v^+$:

$$ \begin{align*} \neg W_v^+ &\equiv \neg \left[ \bigwedge_{\substack{n \in [0, b_v] \\ \omega, \omega' \subset R^{-}(v)}} \left( \left( \begin{array}{@{}l@{}} (\eta_v = n) \wedge \\ \Phi_v^\omega \wedge \Phi_{v+}^{\omega'} \end{array} \right) \Rightarrow \left( \begin{array}{@{}l@{}} C_{v,\omega,n} > 0 \\ \wedge \\ C_{v,\omega',m} < 0 \end{array} \right) \right) \right] \\ &\equiv \neg \underbrace{\left( \eta_v < b_v \right)}_{\substack{\perp \\ \text{since } \eta_v < b_v}} \vee \bigvee_{\substack{n \in [0, b_v] \\ \omega, \omega' \subset R^{-}(v)}} \neg \left( \left( \begin{array}{@{}l@{}} (\eta_v = n) \wedge \\ \Phi_v^\omega \wedge \Phi_{v+}^{\omega'} \end{array} \right) \Rightarrow \left( \begin{array}{@{}l@{}} C_{v,\omega,n} > 0 \\ \wedge \\ C_{v,\omega',m} < 0 \end{array} \right) \right) \end{align*} $$

Amongst all premises of the remaining disjunctions, only one is satisfied because the current qualitative state and the next state have a unique qualitative level ($\eta_v = n$ and $m = n + 1$) and a unique set of resources ($\Phi_v^\omega$ and $\Phi_{v+}^{\omega'}$). Replacing $\omega$ and $\omega'$ by the right resources of the corresponding states $\rho(\eta, v)$ and $\rho(\eta'', v)$ and naming $\eta''$ the next state, we deduce:

$$ \neg W_v^+ \equiv \neg \left( \neg \underbrace{\left[ \begin{array}{@{}l@{}} (\eta_v = n) \wedge \\ (m = n + 1) \wedge \\ \Phi_v^{\rho(\eta,v)} \wedge \Phi_{v+}^{\rho(\eta'',v)} \end{array} \right]}_{\perp} \vee \left( \begin{array}{@{}l@{}} C_{v,\rho(\eta,v),\eta_v} > 0 \\ \wedge \\ C_{v,\rho(\eta'',v),\eta_v''} < 0 \end{array} \right) \right) \equiv \left( \begin{array}{@{}l@{}} C_{v,\rho(\eta,v),\eta_v} \le 0 \\ \vee \\ C_{v,\rho(\eta'',v),\eta_v''} \ge 0 \end{array} \right) $$

However, since $\Phi_v^+(\Delta t)$ is true at $h'$, we have $C_{v,\rho(\eta,v),\eta_v} > 0$. Thus $\neg W_v^+$ is equivalent to $C_{v,\rho(\eta'',v),\eta_v''} \ge 0$ and the previous inequation is true since $\neg W_v^+$ is satisfied at $h'$. Thus the variable $v$ reaches its threshold in $\Delta t$ time ($\Phi_v^+(\Delta t)$) and crosses it ($\neg W_v^+$) allowing a discrete transition $h' \to h''$ which increases $v$ because the signs of the celerities of $v$ in $h'$ and in $h''$ are the same.

(γ) Let us finally prove that the postcondition is satisfied after the elementary path. We previously proved that there exists a unique continuous transition $h \to h'$ and a discrete one $h' \to h''$. Since $h \models (D[\eta_v \setminus \eta_v + 1], H'_{i,f})$, we deduce with Lemma 16: $h' \models (D[\eta_v \setminus \eta_v + 1], H'_{i,f})$. The discrete transition increases the variable $v$ ($\eta_v'' = \eta_v + 1$), we deduce that:

$$ h'' \models (D[\eta_v \setminus \eta_v + 1][\eta_v \setminus \eta_v - 1], H'_{i,f}[\eta_v \setminus \eta_v - 1]), \quad \text{that is,} \quad h'' \models (D, H'_{i,f}[\eta_v \setminus \eta_v - 1]) $$

The hybrid condition $H'' \equiv H'_{i,f}[\eta_v \setminus \eta_v - 1]$ is satisfied in $h''$:

$$ \begin{align*} H'' &\equiv (H_f[\eta_v \setminus \eta_v + 1] \wedge \Phi_v^+(\Delta t) \wedge \mathcal{F}(\Delta t) \wedge \neg W_v^+ \wedge \mathcal{A}(\Delta t, a) \wedge \mathcal{J}_v)[\eta_v \setminus \eta_v - 1] \\ &\equiv H_f \wedge (\Phi_v^+(\Delta t) \wedge \mathcal{F}(\Delta t) \wedge \neg W_v^+ \wedge \mathcal{A}(\Delta t, a) \wedge \mathcal{J}_v)[\eta_v \setminus \eta_v - 1] \end{align*} $$

So, the discrete and hybrid conditions $D$ and $H_f$ are satisfied at $h''$ and the postcondition is verified.
## B.2 Second Case: $a = \text{slide}^+(u)$

(α) Similarly to the first case, we consider the unique hybrid state $h' = (\eta, \pi')$ such that the continuous transition $h \to h'$ exists. The time spent in the current qualitative state is also $\Delta t$ (sub-property $\Phi_v^+(\Delta t)$). Since $a \neq \top$, the sub-property $\mathcal{A}$ plays a crucial rule:

$$ \mathcal{A}(\Delta t, a) \equiv \bigwedge_{\substack{k \in [1, n] \\ \omega_k \in R^-(v_k) \\ n_k \in [0, b_{v_k}]}} \left( \bigwedge_{l \in [1, n]} \left( (\eta_{v_l} = n_l) \wedge \Phi_{v_l}^{\omega_l} \right) \Rightarrow a \left[ \begin{array}{l} C_{v_l} \setminus C_{v_l, \omega_l, n_l} \\ \text{slide}^+(v_l) \setminus S_{v_l, \omega_l, n_l}(\Delta t) \\ \text{slide}^+(v_l) \setminus S_{v_l, \omega_l, n_l}^+(\Delta t) \\ \text{slide}^-(v_l) \setminus S_{v_l, \omega_l, n_l}^-(\Delta t) \end{array} \right] \right) $$

Amongst all premises of these conjunctions, only one is satisfied because the current qualitative state has a unique qualitative level for each variable $v_l$ ($\eta_{v_l} = n_l$) and a unique set of resources for each $v_l$ ($\Phi_{v_l}^{\omega_l}$). We can then replace $\text{slide}^+(u)$ by the sub-property $S^+$:

$$ S_{u,\omega,n}^{+}(\Delta t) \equiv (\pi_{u}^{i'} = 1) \wedge (\pi_{u}^{i} > \pi_{u}^{i'} - C_{u,\omega,n} \cdot \Delta t) $$

where $\omega$ is the resources of $u$ and $n$ its current qualitative level. This formula means that the exit position of the current qualitative state is on the top border ($\pi_u^{i'} = 1$). We then deduce:

$$ C_{u,\omega,n} \cdot \Delta t > 1 - \pi_u^i \\ \Delta t > \frac{1 - \pi_u^i}{C_{u,\omega,n}} = \delta_{h'}(u) \quad \text{because } 1 - \pi_u^i \ge 0, \Delta t \ge 0 \text{ and } C_{u,\omega,n} > 0 $$

According to Lemma 15, we have $\delta_{h'}(v) = \delta_{h'}^{\text{first}} = \Delta t$ and so $\delta_{h'}(v) > \delta_{h'}(u)$. In other words, $u$ reaches its top border before $v$ reaches its one. Thus, the continuous transition $h \to h'$ is such that $(h, h') \models (\Delta t, a)$, see Definition 11.

(β and γ) The proof of the discrete transition existence from $h'$ is similar to the first case. This transition leads to $h''$ which satisfies the postcondition $h'' \models (D, H)$ (see the stages β and γ of the first case).

## B.3 Third Case: $a = C_u \Box c$ with $c \in \mathbb{R}$

(α) The sub-property $\mathcal{A}(\Delta t, a)$ allows one to replace the celerity $C_u$ in the assertion $a$ by the celerity indexed by the relevant set of resources of the current qualitative state. So, we deduce $C_{u,\rho(\eta,u),\eta_u} \Box c$. From Definition 11, the unique continuous transition $h \to h'$ where $h' = (\eta, \pi')$ is such that $(h, h') \models (\Delta t, a)$.

(β and γ) The proof of the discrete transition existence from $h'$ is similar to the first case. This transition leads to $h''$ which satisfies the postcondition $h'' \models (D, H)$ (see the stages β and γ of the first case).

## B.4 Fourth Case: $a = a_1 \wedge a_2$

(α) From the previous cases, it is possible to construct two hybrid states $h_1$ and $h_2$ such that $(h, h_1) \models (\Delta t, a_1)$ and $(h, h_2) \models (\Delta t, a_2)$. Because the continuous transition starting at $h$ is unique, $h_1 = h_2$. Thus, $(h, h_1) \models (\Delta t, a_1 \wedge a_2)$.
(β and γ) The proof of the discrete transition existence from *h*' is similar to the first case. This transition leads to *h''* which satisfies the postcondition *h''* ⊑ (*D*, *H*) (see the stages β and γ of the first case).

This proof is generalisable for all logical connectives and recursively to all formulas.