Document Open Access Logo

Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks

Authors Jonathan Behaegel, Jean-Paul Comet, Maxime Folschette

PDF
Thumbnail PDF

File

LIPIcs.TIME.2017.5.pdf
  • Filesize: 0.68 MB
  • 21 pages

Document Identifiers

Author Details

Jonathan Behaegel
Jean-Paul Comet
Maxime Folschette

Cite AsGet BibTex

Jonathan Behaegel, Jean-Paul Comet, and Maxime Folschette. Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.TIME.2017.5

Abstract

We present a new hybrid Hoare logic dedicated for a class of linear hybrid automata well suited to model gene regulatory networks. These automata rely on Thomas' discrete framework in which qualitative parameters have been replaced by continuous parameters called celerities. The identification of these parameters remains one of the keypoints of the modelling process, and is difficult especially because the modelling framework is based on a continuous time. We introduce Hoare triples which handle biological traces and pre/post-conditions. Observed chronometrical biological traces play the role of an imperative program for classical Hoare logic and our hybrid Hoare logic, defined by inference rules, is proved to be sound. Furthermore, we present a weakest precondition calculus (a la Dijkstra) which leads to constraints on dynamical parameters. Finally, we illustrate our "constraints generator" with a simplified circadian clock model describing the rhythmicity of cells in mammals on a 24-hour period.
Keywords
  • Hoare logic
  • weakest precondition
  • linear hybrid automata
  • constraint synthesis
  • gene networks

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. J. Behaegel, J.-P. Comet, G. Bernot, E. Cornillon, and F. Delaunay. A hybrid model of cell cycle in mammals. JBCB, 14(1):1640001 [17 pp.], 2016. Google Scholar
  2. G. Bernot, J.-P. Comet, Z. Khalis, A. Richard, and O. Roux. A genetically modified Hoare logic. ArXiv: 1506.05887, June 2015. Google Scholar
  3. G. Bernot, J.-P. Comet, A. Richard, and J. Guespin. Application of formal methods to biological regulatory networks: extending thomas’ asynchronous logical approach with temporal logic. Journal of theoretical biology, 229(3):339-347, 2004. Google Scholar
  4. G. Bernot, J.-P. Comet, and O. Roux. A genetically modified Hoare logic that identifies the parameters of a gene networks. In O. Roux and J. Bourdon, editors, CMSB'15, volume 9308 of LNBI, pages 8-12, 2015. Google Scholar
  5. F. Corblin, E. Fanchon, and L. Trilling. Applications of a formal approach to decipher discrete genetic networks. BMC Bioinformatics, 11:385, 2010. URL: http://dx.doi.org/10.1186/1471-2105-11-385.
  6. E. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18:453-457, August 1975. URL: http://dx.doi.org/10.1145/360933.360975.
  7. F. Fages. Temporal logic constraints in the biochemical abstract machine BIOCHAM. In Logic Based Program Synthesis and Transformation, 15th International Symposium, LOPSTR 2005, London, UK, September 7-9, 2005, Revised Selected Papers, pages 1-5, 2005. URL: http://dx.doi.org/10.1007/11680093_1.
  8. N. Halbwachs, Y.-É. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In Baudouin Le Charlier, editor, Proceedings of the First International Static Analysis Symposium (SAS'94), pages 223-237. Springer Berlin Heidelberg, 1994. Google Scholar
  9. T. Henzinger. The theory of hybrid automata. In M. Kemal Inan and Robert P. Kurshan, editors, Verification of Digital and Hybrid Systems, pages 265-292. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000. URL: http://dx.doi.org/10.1007/978-3-642-59615-5_13.
  10. T. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. In Orna Grumberg, editor, Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), pages 460-463. Springer Berlin Heidelberg, 1997. Google Scholar
  11. J. Hooman. Extending Hoare logic to real-time. Formal Aspects of Computing, 6:801-825, 1994. Google Scholar
  12. T. Hunt and P. Sassone-Corsi. Riding tandem: circadian clocks and the cell cycle. Cell, 129(3):461-464, 2007. Google Scholar
  13. C. Lee, J.-P. Etchegaray, F. Cagampang, A. Loudon, and S. Reppert. Posttranslational mechanisms regulate the mammalian circadian clock. Cell, 107(7):855-867, 2001. Google Scholar
  14. T. Liu, X. Zhang, and X. Gao. Stability analysis for continuous-time and discrete-time genetic regulatory networks with delays. Applied mathematics and computation, 274:628-643, 2016. Google Scholar
  15. R. Thomas. Boolean formalization of genetic control circuits. Journal of theoretical biology, 42(3):563-585, 1973. Google Scholar
  16. R. Thomas and M. Kaufman. Multistationarity, the basis of cell differentiation and memory. II. logical analysis of regulatory networks in terms of feedback circuits. Chaos, 11:180-195, 2001. Google Scholar
  17. P. Traynard, A. Fauré, F. Fages, and D. Thieffry. Logical model specification aided by model-checking techniques: application to the mammalian cell cycle regulation. Bioinformatics, 32(17):772-780, 2016. URL: http://dx.doi.org/10.1093/bioinformatics/btw457.
  18. N. Zhan, S. Wang, and H. Zhao. Formal modelling, analysis and verification of hybrid systems. In Unifying Theories of Programming and Formal Engineering Methods, pages 207-281. Springer, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact