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 identificationin
PMA systems. This approach is implemented in RoVerGeNe and applied to
the analysis of a network built in the bacterium E. coli.