Temporal logic patterns for querying qualitative models of genetic regulatory networks

Formal verification based on model checking provides a powerful technology to query qualitative models of dynamical systems. The application of model-checking approaches is hampered, however, by the difficulty for non-expert users to formulate appropriate questions in temporal logic. In order to deal with this problem, we propose the use of patterns, that is, high-level query templates capturing recurring questions which can be automatically translated to temporal logic. We develop a set of patterns for the analysis of qualitative models of genetic regulatory networks, which are sufficiently generic though to be useful in other application do-mains. The applicability of the patterns has been in-vestigated by the analysis of a model of the network of global regulators controlling the carbon starvation re-sponse in Escherichia coli