R.: Computation tree regular logic for genetic regulatory networks

Abstract. Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for the genetic regulatory net-works (Grns) 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 opera-tors that attempts to match these criteria. Ctrl subsumes both Ctl and Ltl, and has a reduced set of temporal operators indexed by regular ex-pressions, 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 avail-able 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.