title: Temporal logic patterns for querying dynamic models of cellular interaction networks.
abstract: BACKGROUND
  Models of the dynamics of cellular interaction networks have become increasingly larger in recent years. Formal verification based on model checking provides a powerful technology to keep up with this increase in scale and complexity. The application of modelchecking approaches is hampered, however, by the difficulty for nonexpert users to formulate appropriate questions in temporal logic.
  
  
  RESULTS
  In order to deal with this problem, we propose the use of patterns, that is, high-level query templates that capture recurring biological questions and can be automatically translated into temporal logic. The applicability of the developed set of patterns has been investigated by the analysis of an extended model of the network of global regulators controlling the carbon starvation response in Escherichia coli.
  
  
  BACKGROUND
  GNA and the model of the carbon starvation response network are available at http://www-helix.inrialpes.fr/gna.
authors.affiliation: INRIA Grenoble, Rhône-Alpes, 655 Av de l'Europe, Montbonnot, 38334 St Ismier Cedex, France.
authors.forename: Pedro T
authors.initials: PT
authors.lastname: Monteiro
authors.forename: Delphine
authors.initials: D
authors.lastname: Ropers
authors.forename: Radu
authors.initials: R
authors.lastname: Mateescu
authors.forename: Ana T
authors.initials: AT
authors.lastname: Freitas
authors.forename: Hidde
authors.initials: H
authors.lastname: de Jong
mesh_terms: D000465:Algorithms; D003198:Computer Simulation; D016015:Logistic Models; D008954:Models, Biological; D025941:Protein Interaction Mapping / Q000379:methods*; D020543:Proteome / Q000378:metabolism*; D015398:Signal Transduction / Q000502:physiology*; D012984:Software; D012986:Software Validation
chemical_list: D020543:Proteome