CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
From MaRDI portal
Publication:548484
DOI10.1016/j.tcs.2010.05.009zbMath1231.68163OpenAlexW1966021826WikidataQ59843858 ScholiaQ59843858MaRDI QIDQ548484
Estelle Dumas, Pedro T. Monteiro, Hidde de Jong, Radu Mateescu
Publication date: 28 June 2011
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00610831/file/Mateescu-Monteiro-Dumas-deJong-11.pdf
Specification and verification (program logics, model checking, etc.) (68Q60) Systems biology, networks (92C42)
Related Items (5)
Model Checking of Biological Systems ⋮ On the Model Checking Problem for Some Extension of CTL* ⋮ Model checking interval temporal logics with regular expressions ⋮ STL*: extending signal temporal logic with signal-value freezing operator ⋮ GR(1)*: GR(1) specifications extended with existential guarantees
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Qualitative simulation of the initiation of sporulation in \textit{Bacillus subtilis}
- Qualitative simulation of genetic regulatory networks using piecewise-linear models
- Results on the propositional \(\mu\)-calculus
- Compiling communicating processes into delay-insensitive VLSI circuits
- Propositional dynamic logic of regular programs
- CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
- Dynamical behaviour of biological regulatory networks. I: Biological role of feedback loops and practical use of the concept of the loop- characteristic state
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- Modalities for model checking: Branching time logic strikes back
- NuSMV: A new symbolic model checker
- Efficient on-the-fly model-checking for regular alternation-free \(\mu\)-calculus
- Modeling and querying biomolecular interaction networks
- Application of formal methods to biological regulatory networks: extending Thomas' asynchronous logical approach with temporal logic
- Modeling the onset of virulence in a pectinolytic bacterium
- Counterexample-guided predicate abstraction of hybrid systems
- Biology and control theory: Current challenges
- Symbolic reachability analysis of genetic regulatory networks using discrete abstractions
- A lattice-theoretical fixpoint theorem and its applications
- Multistationarity, the basis of cell differentiation and memory. I. Structural conditions of multistationarity and other nontrivial behavior
- Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE
- Temporal logic can be more expressive
- Computation Tree Regular Logic for Genetic Regulatory Networks
- Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
- Propositional dynamic logic of looping and converse is elementarily decidable
- “Sometimes” and “not never” revisited
- Verification of infinite-state dynamic systems using approximate quotient transition systems
- Efficient local correctness checking for single and alternating boolean equation systems
- Model Checking Software
- Derivatives of Regular Expressions
- Tools and Algorithms for the Construction and Analysis of Systems
- Model Checking Software
- Verification, Model Checking, and Abstract Interpretation
- LSCs: Breathing life into message sequence charts
This page was built for publication: CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
