BERNOT , Gilles

The main contribution of this work is a mathematical theorem which establishes a necessary and sufficient condition to preserve the behaviour of a genetic regulatory network when it is embedded into a larger network. We adopt the modelling approach of René Thomas, which provides a discrete representation of biological regulatory networks. This...

International audience

International audience

The main difficulty when modelling gene networks is the identification of the parameters that govern the dynamics. Here we present a new approach based on Hoare logic and weakest preconditions (a la Dijkstra) that generates constraints on the parameter values: Once proper specifications are extracted from biological traces, they play a role...

No description

The formalism of hybrid functional petri nets (HFPN) has proved its convenience for simulating biological systems. The drawback of the noticeable expressiveness of HFPN is the difficulty to perform formal verifications of dynamical properties. In this article, we propose a model-checking procedure for timed hybrid petri nets (THPN), a sub-class...

Ce chapitre démontre que la modélisation des réseaux de régulation biologiques est grandement facilitée par des méthodes symboliques de vérification formelle comme le model-checking et les preuves en logique de Hoare. Il présente une méthodologie complète de modélisation formelle où les approches logiques classiques du génie logiciel s'adaptent...

The formalism of hybrid functional petri nets (HFPN) has proved its convenience for simulating biological systems. The drawback of the noticeable expressiveness of HFPN is the difficulty to perform formal verifications of dynamical properties. In this article, we propose a model-checking procedure for timed hybrid petri nets (THPN), a sub-class...

International audience

On ne compte plus le nombre de fois où les chercheurs en méthodes formelles pour le génie logiciel ont entendu cette plaisanterie : « Les méthodesformelles ont toujours été l'avenir de l'informatique... et le resteront toujours ! ». Dans ce chapitre nous montrons que les méthodes formelles sont le présent de l'analyse des réseaux de régulation...

No description

The Hybrid Functional Petri Nets (HFPN) formalism has shown its convenience for modelling biological systems. This class of models has been fruitfully applied in biology but the remarkable expressiveness of HFPN often leads to incomplete validations. In this paper, we propose a logical framework for Timed Hybrid Petri Nets (THPN), a sub-class...

The formalism of Hybrid Functional Petri Nets (HFPN) has proved its convenience for simulating biological systems. The drawback of the noticeable expressiveness of HFPN is the difficulty to perform formal verifications of dynamical properties. In this article, we propose a model-checking procedure for Timed Hybrid Petri Nets (THPN), a sub-class...

International audience

International audience

International audience

International audience

International audience

When designing a biological regulatory network, new information or wet experiments can require adding variables or interactions, inside a previously validated model. They can result in complete reconsiderations of established behaviours. Fortunately, formal methods allow for fully automated verification of properties, and TotemBioNet is an...

International audience

In this article we present a modelling framework that links the well known modelling framework of gene network introduced by R. Thomas and Markov chains. In a first development we introduce a Markov chain having as state space the set of all possible states of the R. Thomas models: we generate the transition probabilities by examining all the...

This article is threefold: (i) we define the first formal framework able to model dendritic integration within biological neurons, (ii) we show how we can turn continuous time into discrete time consistently and (iii) we show how a Lustre model checker can automatically perform proofs about neuron input/output behavioursowing to our...

We firstly define an improved version of the spiking neuron model with dendrites introduced in [8] and we focus here on the fundamental mathematical properties of the framework. Our main result is that, under few simplifications with respect to biology, dendrites can be simply abstracted by delays. Technically, we define a method allowing to...

International audience