Model Checking Liveness Properties of Genetic Regulatory Networks

Abstract. Recent studies have demonstrated the possibility to build genetic regulatory networks that confer a desired behavior to a living organism. However, the design of these networks is difficult, notably because of uncertainties on parameter values. In previous work, we proposed an approach to analyze genetic regulatory networks with parameter uncertainties. In this approach, the models are based on piecewise-multiaffine (PMA) differential equations, the specifications are expressed in temporal logic, and uncertain parameters are given by intervals. Abstractions are used to obtain finite discrete representations of the dynamics ystem, amenable to model checking. However, the abstraction process creates spurious behaviors along which time does not progress, called time-converging behaviors. Consequently, the verification of liveness properties, expressing that something will eventually happen, and implicitly assuming progress of time, often fails. In this work, we extend our pr...

• Type: Conference
• Year: 2007
• Where: TACAS
• Authors: Grégory Batt, Calin Belta, Ron Weiss
• Keywords: Algorithms, Genetic Regulatory Networks, Parameter Uncertainties, Parameters, TACAS 2007