On the use of formal methods to model and verify neuronal archetypes

被引:1
作者
De Maria, Elisabetta [1 ]
Bahrami, Abdorrahim [2 ]
L'Yvonnet, Thibaud [3 ]
Felty, Amy [2 ]
Gaffe, Daniel [4 ]
Ressouche, Annie [3 ]
Grammont, Franck [5 ]
机构
[1] Univ Cote Azur, CNRS, I3S, F-06903 Sophia Antipolis, France
[2] Univ Ottawa, Sch Elect Engn & Comp Sci, Ottawa, ON K1N 6N5, Canada
[3] Univ Cote Azur, INRIA SAM, F-06902 Sophia Antipolis, France
[4] Univ Cote Azur, CNRS, LEAT, F-06903 Sophia Antipolis, France
[5] Univ Cote Azur, LJAD, CNRS, F-06108 Nice 02, France
基金
加拿大自然科学与工程研究理事会;
关键词
neuronal networks; leaky integrate and fire modeling; synchronous languages; model checking; theorem proving; Lustre; Coq; formal methods; VERIFICATION; SYSTEMS; CHECKING; NETWORKS;
D O I
10.1007/s11704-020-0029-6
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Having a formal model of neural networks can greatly help in understanding and verifying their properties, behavior, and response to external factors such as disease and medicine. In this paper, we adopt a formal model to represent neurons, some neuronal graphs, and their composition. Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes. These archetypes are supposed to be the basis of typical instances of neuronal information processing. In this paper we study six fundamental archetypes (simple series, series with multiple outputs, parallel composition, negative loop, inhibition of a behavior, and contralateral inhibition), and we consider two ways to couple two archetypes: (i) connecting the output(s) of the first archetype to the input(s) of the second archetype and (ii) nesting the first archetype within the second one. We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings. The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings, and to express properties concerning their dynamic behavior. These properties are verified thanks to the use of model checkers. The second approach relies on a theorem prover, the Coq Proof Assistant, to prove dynamic properties of neurons and archetypes.
引用
收藏
页数:22
相关论文
共 74 条
  • [21] Modelling and Formal Verification of Neuronal Archetypes Coupling[J]. De Maria, Elisabetta;L'Yvonnet, Thibaud;Gaffe, Daniel;Ressouche, Annie;Grammont, Franck. PROCEEDINGS OF THE EIGHTH INTERNATIONAL CONFERENCE ON COMPUTATIONAL SYSTEMS-BIOLOGY AND BIOINFORMATICS (CSBIO 2017), 2017
  • [22] Verification of Temporal Properties of Neuronal Archetypes Modeled as Synchronous Reactive Systems[J]. De Maria, Elisabetta;Muzy, Alexandre;Gaffe, Daniel;Ressouche, Annie;Grammont, Franck. HYBRID SYSTEMS BIOLOGY, (HSB 2016), 2016
  • [23] de Maria E, 2014, LECT N BIOINFORMAT, V8738, P136, DOI 10.1007/978-3-319-10398-3_10
  • [24] Design, optimization and predictions of a coupled model of the cell cycle, circadian clock, DNA repair system, irinotecan metabolism and exposure control under temporal logic constraints[J]. De Maria, Elisabetta;Fages, Francois;Rizk, Aurelien;Soliman, Sylvain. THEORETICAL COMPUTER SCIENCE, 2011(21)
  • [25] Formal proof of theorems on genetic regulatory networks[J]. Denes, Maxime;Lesage, Benjamin;Bertot, Yves;Richard, Adrien. 11TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2009), 2009
  • [26] Fages Francois, 2004, Journal of Biological Physics and Chemistry, V4, P64, DOI 10.4024/2040402.jbpc.04.02
  • [27] Fontaine P., 2019, P 27 INT C AUT DED, P11716
  • [28] Graph analysis of the human connectome: Promise, progress, and pitfalls[J]. Fornito, Alex;Zalesky, Andrew;Breakspear, Michael. NEUROIMAGE, 2013
  • [29] Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs[J]. Franzen, Anders. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006(01)
  • [30] Advances in Computational Methods in Systems Biology Preface[J]. Gilbert, David;Heiner, Monika. THEORETICAL COMPUTER SCIENCE, 2015