CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks (Q548484): Difference between revisions

The paper promotes the idea to use formal methods, in particular model checking, in order to analyse the behaviour of biological systems. To this end, it introduces a variant of the well-known branching-time temporal logic CTL, extended with regular expressions and fairness operators and shows ({i}) how formulas of this logic can be model checked and ({ii}) how this helps in the analysis of biological systems. The first aspect is covered in too much length. There are several extensions of CTL with regular expressions by now -- often introduced in articles by the first author -- and the extension with fairness operators has been known for a long time. A large amount of space in the paper is devoted to the translation of this new logic into the specification formalisms used internally by some model checker. The purpose does not justify the effort. The new logic is said to be designed specifically for the requirements occurring in the specification of biological systems. Thus, it would have been nicer to learn more about its use there as well as see it thoroughly compared to other extensions of CTL. The translation into modal equation systems -- a notational variant of the modal \(\mu\)-calculus -- is of little interest to people wanting to analyse biological systems. Thus, it would have sufficed to give a clean translation into the standard representation of the modal \(\mu\)-calculus with the hint that there are model checkers for this logic. Also, it seems like using \textit{J. A. Brzozowski}'s derivatives [J. ACM 11, 481--494 (1964; Zbl 0225.94044)] would have eliminated the need for some ad-hoc determinisation procedure, the correctness of which is not immediate to see.