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 of the system, 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 previous approach to enforce progress of time. More precisely, we define transient regions as subsets of the state space left in finite time by every solution trajectory, show how they can be used to rule out time-converging behaviors, and provide sufficient conditions for their identification in PMA systems. This approach is implemented in RoVerGeNe and applied to the analysis of a network built in the bacterium E. coli. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Batt, G., Belta, C., & Weiss, R. (2007). Model checking liveness properties of genetic regulatory networks. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4424 LNCS, pp. 323–338). Springer Verlag. https://doi.org/10.1007/978-3-540-71209-1_25
Mendeley helps you to discover research relevant for your work.