CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
type: Item
instance of: scholarly article
title: CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
zbMATH Open document ID: 1231.68163
author: Radu Mateescu
author: P. T. Monteiro
author: Estelle Dumas
author: Hidde de Jong
published in: Theoretical Computer Science
publication date: 2011-06-28T00:00:00Z
full work available at URL: Mateescu-Monteiro-Dumas-deJong-11.pdf
review text: 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.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 92C42
zbMATH DE Number: 5914351
zbMATH Keywords: temporal logic
zbMATH Keywords: model checking
zbMATH Keywords: regular expressions
zbMATH Keywords: systems biology
zbMATH Keywords: genetic regulatory networks
Wikidata QID: Q59843858
describes a project that uses: SPIN
describes a project that uses: DiVinE
describes a project that uses: NuSMV
describes a project that uses: CADP
describes a project that uses: Exp.Open
describes a project that uses: CAESAR_SOLVE
MaRDI profile type: Publication
OpenAlex ID: W1966021826
cites work: Counterexample-guided predicate abstraction of hybrid systems
cites work: Q4472249
cites work: Parallel model checking large-scale genetic regulatory networks with DiVinE
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: Model Checking Software
cites work: Symbolic reachability analysis of genetic regulatory networks using discrete abstractions
cites work: Q4551164
cites work: Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic
cites work: Q3430687
cites work: Derivatives of Regular Expressions
cites work: Modeling and querying biomolecular interaction networks
cites work: Verification of infinite-state dynamic systems using approximate quotient transition systems
cites work: NuSMV: A new symbolic model checker
cites work: A linear-time model-checking algorithm for the alternation-free modal mu- calculus
cites work: CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
cites work: LSCs: Breathing life into message sequence charts
cites work: Qualitative simulation of the initiation of sporulation in \textit{Bacillus subtilis}
cites work: Qualitative simulation of genetic regulatory networks using piecewise-linear models
cites work: “Sometimes” and “not never” revisited
cites work: Modalities for model checking: Branching time logic strikes back
cites work: Propositional dynamic logic of regular programs
cites work: Biology and control theory: Current challenges
cites work: Q4037390
cites work: Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
cites work: Q5812175
cites work: Results on the propositional \(\mu\)-calculus
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Q3792217
cites work: Compiling communicating processes into delay-insensitive VLSI circuits
cites work: Computation Tree Regular Logic for Genetic Regulatory Networks
cites work: Efficient on-the-fly model-checking for regular alternation-free \(\mu\)-calculus
cites work: Modeling the onset of virulence in a pectinolytic bacterium
cites work: Propositional dynamic logic of looping and converse is elementarily decidable
cites work: A lattice-theoretical fixpoint theorem and its applications
cites work: Multistationarity, the basis of cell differentiation and memory. I: Structural conditions of multistationarity and other nontrivial behavior
cites work: Dynamical behaviour of biological regulatory networks. I: Biological role of feedback loops and practical use of the concept of the loop- characteristic state
cites work: Q4733423
cites work: Q4736610
cites work: Efficient local correctness checking for single and alternating boolean equation systems
cites work: Temporal logic can be more expressive
DOI: 10.1016/J.TCS.2010.05.009
Recommended article: Model Checking Software
Recommended article: Computation Tree Regular Logic for Genetic Regulatory Networks
Recommended article: Model Checking Genetic Regulatory Networks with Parameter Uncertainty
Recommended article: Model Checking Gene Regulatory Networks
Recommended article: Controllability of Conjunctive Boolean Networks With Application to Gene Regulation
Recommended article: Symbolic reachability analysis of genetic regulatory networks using discrete abstractions
Recommended article: On algorithmic analysis of transcriptional regulation by LTL model checking
Recommended article: Parallel model checking large-scale genetic regulatory networks with DiVinE
Recommended article: The formulation of the control of an expression pattern in a gene network by propositional calculus

CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks (Recommended article)
Recommended article: Model Checking Liveness Properties of Genetic Regulatory Networks
Similarity Score: 0.81882745
Recommender Run: Recommender Run 3