The study of genetic regulatory networks has received a major impetus
from the recent development of high-throughput genomic techniques. This
experimental progress calls for the development of appropriate computer
tools supporting the analysis of genetic regulatory processes. We have
developed a modeling and simulation method, based on piecewise-linear
differential equations, that is well-adapted to the qualitative nature of
most available biological data. The method has been implemented in the
tool Genetic Network Analyzer (GNA), which produces a graph of qualitative
states and transitions between qualitative states. The graph provides a
discrete abstraction of the dynamics of the system. A bottleneck in the
application of the qualitative simulation method is the analysis of the
state transition graph, which is usually too large for visual inspection.
In this paper, we propose a model-checking approach to perform this task
in a systematic and efficient way. In particular, we will connect the
qualitative simulator GNA with the verification technologies provided by
the CADP toolbox. A dedicated translator has been developed, which
converts the state transition graph resulting from qualitative simulation
into a form suitable for automated verification. After instantaneous
states have been abstracted away by means of branching bisimulation,
various properties characterizing the evolution of protein concentrations
are checked by encoding them as regular alternation-free mu-calculus. The
diagnostics produced by the CADP model checker allow to establish a
correspondence between verification results and biological data, for
instance by characterizing evolutions leading to equilibrium states. We
illustrate the combined use of qualitative simulation and model checking
by means of a simple, biologically-inspired example.
