Computation Tree Regular Logic for Genetic Regulatory Networks

Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for the genetic regulatory networks (

Grn

s) that govern the functioning of living cells. The applications of model checking in systems biology have revealed that temporal logics should be able to capture both branching-time and fairness properties. At the same time, they should have a user-friendly syntax easy to employ by non-experts. In this paper, we define

Ctrl

(Computation Tree Regular Logic), an extension of

Ctl

with regular expressions and fairness operators that attempts to match these criteria.

Ctrl

subsumes both

Ctl

and

Ltl

, and has a reduced set of temporal operators indexed by regular expressions, inspired from the modalities of

Pdl

(Propositional Dynamic Logic). We also develop a translation of

Ctrl

into

HmlR

(Hennessy-Milner Logic with Recursion), an equational variant of the modal

μ

-calculus. This has allowed us to obtain an on-the-fly model checker with diagnostic for

Ctrl

by directly reusing the verification technology available in the

Cadp

toolbox. We illustrate the application of the

Ctrl

model checker by analyzing the

Grn

controlling the carbon starvation response of

Escherichia coli

.