Bibtex entries for publications

title = {Logical Modeling of Biological Systems},
author = {Lo\”{\i}c Paulev\'{e} and Courtney Chancellor and Maxime Folschette and Morgan Magnin and Olivier Roux},
chapter = {Analyzing Large Network Dynamics with Process Hitting},
editor = {Luis Fari{\~n}as del Cerro and Katsumi Inoue},
pages = {125 — 166},
publisher = {Wiley},
year = {2014},
class = {chapter},
file = {PCFMR14-chapterLMBS.pdf:PCFMR14-chapterLMBS.pdf:PDF},
owner = {roux},
pdf = {PCFMR14-chapterLMBS.pdf},
timestamp = {2014.06.16},
url = {}

title = “A genetically modified Hoare logic”,
journal = “Theoretical Computer Science”,
year = “2018”,
issn = “0304-3975”,
doi = “”,
url = “”,
author = “G. Bernot and J.-P. Comet and Z. Khalis and A. Richard and O. Roux”,
keywords = “Hoare logic, Gene regulatory networks, Thomas networks, Parameter identification, Soundness and completeness”,
abstract = “An important problem when modelling gene networks lies in the identification of parameters, even when using a discrete framework such as the one of René Thomas. We present in this article a new approach based on Hoare logic to generate constraints on parameter values. Specifications of observed behaviours play a role comparable to programs in the classical Hoare logic, and deduced weakest preconditions characterize the sets of all compatible parameterizations, expressed as constraints on parameters. Besides being natural and simple, our Hoare logic approach is remarkably powerful and, among others, it allows one to express external interventions of the biologist during experiments such as knockouts. In supplementary materials, we give a proof of soundness of our Hoare logic for gene networks as well as a proof of completeness and decidability based on the notion of the weakest precondition.”

AUTHOR={Bibi, Zurah and Ahmad, Jamil and Siddiqa, Amnah and Paracha, Rehan Z. and Saeed, Tariq and Ali, Amjad and Janjua, Hussnain Ahmed and Ullah, Shakir and Ben Abdallah, Emna and Roux, Olivier},
TITLE={Formal Modeling of mTOR Associated Biological Regulatory Network Reveals Novel Therapeutic Strategy for the Treatment of Cancer},
JOURNAL={Frontiers in Physiology},
ABSTRACT={Cellular homeostasis is a continuous phenomenon that if compromised can lead to several disorders including cancer. There is a need to understand the dynamics of cellular proliferation to get deeper insights into the prevalence of cancer. Mechanistic Target of Rapamycin (mTOR) is implicated as the central regulator of the metabolic pathway involved in growth whereas its two distinct complexes mTORC1 and mTORC2 perform particular functions in cellular propagation. To date, mTORC1 is a well defined therapeutic target to inhibit uncontrolled cell division, while the role of mTORC2 is not well characterized. Therefore, the current study is designed to understand the signaling dynamics of mTOR and its partner proteins such as PI3K, PTEN, mTORC2, PKB (Akt), mTORC1 and FOXO. For this purpose, a qualitative model of mTOR-associated Biological Regulatory Network (BRN) is constructed to predict its regulatory behaviors which may not be predictable otherwise. The depleted expression of PTEN and FOXO along with the overexpression of PI3K, mTORC2, mTORC1 and Akt is predicted as a stable steady state which is in accordance with their observed expression levels in the progression of various cancers. The qualitative model also predicts the homeostasis of all the entities in the form of qualitative cycles. The significant qualitative (discrete) cycle is identified by analyzing betweenness centralities of the qualitative (discrete) states. This cycle is further refined as a linear hybrid automaton model with the production (activation) and degradation (inhibition) time delays in order to analyze the real-time constraints for its existence. The analysis of the hybrid model provides a formal proof that during homeostasis the inhibition time delay of Akt is less than the inhibition time delay of mTORC2. In conclusion, our observations characterize that in homeostasis Akt is degraded with a faster rate than mTORC2 which suggests that the inhibition of Akt along with the activation of mTORC2 may be a better therapeutic strategy for the treatment of cancer.}

AUTHOR = {Chinesta, Francisco and Magnin, Morgan and Roux, Olivier and Ammar, Amine and Cueto, Elias},
TITLE = {Kinetic Theory Modeling and Efficient Numerical Simulation of Gene Regulatory Networks Based on Qualitative Descriptions},
JOURNAL = {Entropy},
VOLUME = {17},
YEAR = {2015},
NUMBER = {4},
PAGES = {1896--1915},
URL = {},
ISSN = {1099-4300},
DOI = {10.3390/e17041896}

title = "Identification of biological regulatory networks from Process Hitting models ",
journal = "Theoretical Computer Science ",
volume = "",
number = "0",
pages = " - ",
year = "2014",
note = "",
issn = "0304-3975",
doi = "",
url = "",
author = "Maxime Folschette and {L}o{\"i}c Paulev{\'e} and Katsumi Inoue and Morgan Magnin and Olivier Roux",
keywords = "Qualitative modeling",
keywords = "Model abstraction",
keywords = "Interaction Graph",
keywords = "Ren{\'e} Thomas' parameters",
keywords = "Answer Set Programming ",
abstract = "Abstract Qualitative formalisms offer a well-established alternative to the more traditionally used differential equation models of Biological Regulatory Networks (BRNs). These formalisms led to numerous theoretical works and practical tools to understand emerging behaviors. The analysis of the dynamics of very large models is however a rather hard problem, which led us to previously introduce the Process Hitting framework (PH), which is a particular class of nondeterministic asynchronous automata network (or safe Petri nets). Its major advantage lies in the efficiency of several static analyses recently designed to assess dynamical properties, making it possible to tackle very large models. In this paper, we address the formal identification of qualitative models of \{BRNs\} from \{PH\} models. First, the inference of the Interaction Graph from a \{PH\} model summarizes the signed influences between the components that are effective for the dynamics. Second, we provide the inference of all Ren{\'e} Thomas models of \{BRNs\} that are compatible with a given PH. As the \{PH\} allows the specification of nondeterministic interactions between components, our inference emphasizes the ability of \{PH\} to deal with large \{BRNs\} with incomplete knowledge on interactions, where Thomas' approach fails because of the combinatorics of parameters. The inference of corresponding Thomas models is implemented using Answer Set Programming, which allows in particular an efficient enumeration of (possibly numerous) compatible parameterizations. "

  author = {Paulev\'{e}, {L}o{\"i}c and Magnin, Morgan and Roux, Olivier},
  title = {Static Analysis of Biological Regulatory Networks Dynamics using Abstract Interpretation},
  journal = {Mathematical Structures in Computer Science},
  year = {2012},
  volume = {22},
  pages = {651-685},
  number = {04},
  class = {journal},
  doi = {10.1017/S0960129511000739},
  file = {PMR12-MSCS.pdf:PMR12-MSCS.pdf:PDF},
  owner = {pauleve},
  pdf = {PMR12-MSCS.pdf},
  timestamp = {2011.12.09}

  author = {{P}aulev{\'e}, {L}o{\"i}c and {M}agnin, {M}organ and {R}oux, {O}livier},
  title = {{T}uning {T}emporal {F}eatures within the {S}tochastic $\pi$-{C}alculus},
  journal = {IEEE Transactions on Software Engineering},
  year = {2011},
  volume = {37},
  pages = {858-871},
  number = {6},
  address = {Los Alamitos, CA, USA},
  class = {journal},
  doi = {10.1109/TSE.2010.95},
  file = {PMR10-TSE.pdf:PMR10-TSE.pdf:PDF},
  issn = {0098-5589},
  pdf = {PMR10-TSE.pdf},
  publisher = {IEEE Computer Society}

  author = {{P}aulev{\'e}, {L}o{\"i}c and {M}agnin, {M}organ and {R}oux, {O}livier},
  title = {Refining Dynamics of Gene Regulatory Networks in a Stochastic $\pi$-Calculus
  booktitle = {Transactions on Computational Systems Biology XIII},
  publisher = {Springer},
  year = {2011},
  volume = {6575},
  series = {Lecture Notes in Comp. Sci.},
  pages = {171-191},
  affiliation = {IRCCyN, UMR CNRS 6597, {\'E}cole Centrale de Nantes, France},
  class = {journal},
  doi = {10.1007/978-3-642-19748-2_8},
  file = {PMR10-TCSB.pdf:PMR10-TCSB.pdf:PDF},
  pdf = {PMR10-TCSB.pdf}

AUTHOR = {Fromentin, Jonathan and Eveillard, Damien and Roux, Olivier},
TITLE = {Hybrid modeling of biological networks: mixing temporal and qualitative biological properties},
JOURNAL = {BMC Systems Biology},
VOLUME = {4},
YEAR = {2010},
NUMBER = {1},
PAGES = {79},
URL = {},
DOI = {10.1186/1752-0509-4-79},
PubMedID = {20525331},
ISSN = {1752-0509}

title = "Invariance kernel of Biological Regulatory Networks",
journal = "International Journal of Data Mining and Bioinformatics (IJDBM) ",
volume = "4",
number = "5",
pages = "553 - 570",
year = "2010",
doi = "DOI: 10.1504/IJDMB.2010.035900",
url = "",
author = "Jamil Ahmad and Olivier Roux",

title = "Temporal constraints of a gene regulatory network: Refining a qualitative simulation",
journal = "Biosystems",
volume = "98",
number = "3",
pages = "149 - 159",
year = "2009",
note = "Evolving Gene Regulatory Networks",
issn = "0303-2647",
doi = "DOI: 10.1016/j.biosystems.2009.05.002",
url = "",
author = "Jamil Ahmad and J{\'e}r{\'e}mie Bourdon and Damien Eveillard and Jonathan Fromentin and Olivier Roux and Christine Sinoquet",
keywords = "Gene regulatory network",
keywords = "Delay parameter synthesis",
keywords = "Model-checking",
keywords = "Hybrid automaton",
keywords = "Escherichia coli"

    Author = {Jamil Ahmad and Olivier Roux and Gilles Bernot and Jean-Paul Comet and Adrien Richard},
    Journal = {International Journal of Bioinformatics Research and Applications  (IJBRA)},
    Publisher = {Inderscience Publisher},
    Title = {Analysing Formal Models of Genetic Regulatory Networks with Delays},
    Volume = {4},
    Number = {3},
    Pages = {240--262},
    Year = 2008 

    Author = {Jamil Ahmad and Gilles Bernot and Jean-Paul Comet and Didier Lime and Olivier Roux},
    Journal = {ComPlexUs},
    Publisher = {Karger Publisher},
    Title = {Hybrid Modelling and Dynamical Analysis of Gene Regulatory Networks with Delays},
    Volume = {3},
    Number = {4},
    Pages = {231--251},
    Year = 2007,
    month = oct 

  AUTHOR = {Gardey, Guillaume and Roux, Olivier (H.) and Roux, Olivier (F.)},
  TITLE = {State Space Computation and Analysis of Time {Petri} Nets},
  JOURNAL = {Theory and Practice of Logic Programming (TPLP). Special Issue on Specification Analysis and Verification of Reactive Systems},
  YEAR = 2006,
  PAGES = {301--320},
  VOLUME = {6},
  NUMBER = {3},
  PUBLISHER = {Cambridge University Press,},

  AUTHOR = {Cassez, Franck and Pagetti, Claire and Roux, Olivier},
  TITLE = {{A timed extension for \textsf{AltaRica}}},
  JOURNAL = {{Fundamenta Informatic\ae}},
  VOLUME = {62},
  NUMBER = {3--4},
  PAGES = {291--332},
  YEAR = {2004},

  AUTHOR = {Herbreteau, Fr{\'e}d{\'e}ric and Cassez, Franck and Roux, Olivier},
  TITLE = {{Application of Partial-Order Methods to Reactive Systems with Event Memorization}},
  JOURNAL = {Journal of Real-Time Systems},
  YEAR = 2001,
  VOLUME = {20},
  NUMBER = {3},
  NOTE = {Copyright \begin{rawhtml}Kluwer Academics\end{rawhtml}},
  PAGES = {287-316},
  PUBLISHER = {kluwer Academic Publishers},

  author    = {Olivier Roux and
               Vlad Rusu and
               Franck Cassez},
  title     = {Hybrid Verifications of Reactive Programs},
  journal   = {Formal Aspects of Computing},
  volume    = {11},
  number    = {4},
  year      = {1999},
  pages     = {448-471},
  ee        = {},
  bibsource = {DBLP,}

  AUTHOR = {Cassez, Franck and Roux, Olivier},
  TITLE = {{Compilation of the {Electre} Reactive Language into Finite Transition Systems}},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = {146},
  NUMBER = {1--2},
  YEAR = {1995},
  PAGES = {109--143},
  ABSTRACT = {We present in this paper an operational semantics for the
                  {\sf ELECTRE} reactive language (Roux et al.,
                  1992). This language is based on an asynchronous
                  approach to real-time systems. First basic concepts
                  and intuitive semantics are introduced. Then we give
                  rules to model dynamic semantics of {\sf ELECTRE}
                  programs: this constitutes an operational semantics
                  for the {\sf ELECTRE} language. This operational
                  semantics is used to define a model of execution for
                  {\sf ELECTRE} programs: transition system. In
                  addition, we prove, using structural induction on
                  the operational semantics, that this transition
                  system is a finite state transition
                  system. Eventually, we extend the previous
                  transition system so as to handle multiple-storage
                  events: it is important since the asynchronous {\sf
                  ELECTRE} language deals with multiple memorized
                  occurrences of the events. This result gives a means
                  of compiling the {\sf ELECTRE} language into a
                  finite-state machine. },
  URL = {},
  NOTE = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},

   Author = {Roux, O. and Rusu, V.},
   Title = {Translating from GRAFCET to the reactive language ELECTRE},
   Journal = {Automatique, Productique et Informatique Industrielle},
   Volume = {28},
   Number = {2},
   Pages = {131--158},
   Year = {1994}

 author = {Perraud, Jean and Roux, Olivier and Huou, Marc},
 title = {Operational semantics of a kernel of the language ELECTRE},
 journal = {Theor. Comput. Sci.},
 issue_date = {April 20, 1992},
 volume = {97},
 number = {1},
 month = apr,
 year = {1992},
 issn = {0304-3975},
 pages = {83--103},
 numpages = {21},
 url = {},
 doi = {10.1016/0304-3975(92)90388-V},
 acmid = {131852},
 publisher = {Elsevier Science Publishers Ltd.},
 address = {Essex, UK},



author = {Elloy, J. P. and Roux, O.}, 
title = {Electre: A Language for Control Structuring in Real time},
volume = {29}, 
number = {3}, 
pages = {229-234}, 
year = {1986}, 
doi = {10.1093/comjnl/29.3.229}, 
abstract ={This paper briefly reviews the general tools proposed to express the synchronisation conditions of real-time applications. We describe the evolution of these tools, and mention their shortcomings, which led us to propose a language enabling control structuring.First, an application is decomposed so as to deal with tasks featuring no breakpoint but software and hardware events. Then these elements are combined into sentences called control structures, designed so that occurring events rhythm the tasks. Finally, we provide a way to specify the synchronisation conditions very accurately, and examples are given to make clear the use of the language.}, 
URL = {}, 
eprint = {}, 
journal = {The Computer Journal}