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.
. [J]. Frontiers of Computer Science, 2022, 16(3): 163404.
Elisabetta DE MARIA, Abdorrahim BAHRAMI, Thibaud L’YVONNET, Amy FELTY, Daniel GAFFÉ, Annie RESSOUCHE, Franck GRAMMONT. On the use of formal methods to model and verify neuronal archetypes. Front. Comput. Sci., 2022, 16(3): 163404.
Successful proofs help in proving other properties
+
Counter-example automatically provided
Prove properties at a high level of generality
?
Prove properties for some given parameter values
An expert is needed
Tab.1
1
O Sporns . The human connectome: origins and challenges. NeuroImage, 2013, 80 : 53– 61
2
O Sporns . Structure and function of complex brain networks. Dialogues in Clinical Neuroscience, 2013, 15 : 247– 262
3
O Sporns . Graph theory methods: applications in brain networks. Dialogues in Clinical Neuroscience, 2018, 20 : 111– 121
4
A Fornito , A Zalesky , M Breakspear . Graph analysis of the human connectome: Promise, progress, and pitfalls. NeuroImage, 2013, 80 : 426– 444
5
K Matsuoka . Mechanisms of frequency and pattern control in the neural rhythm generators. Biological Cybernetics, 1987, 56( 5-6): 345– 353
6
R C Lambert , C Tuleau-Malot , T Bessaih , V Rivoirard , Y Bouret , N Leresche , P Reynaud-Bouret . Reconstructing the functional connectivity of multiple spike trains using Hawkes models. Journal of Neuroscience Methods, 2018, 297 : 9– 21
7
E Marconi , T Nieus , A Maccione , P Valente , A Simi . Emergent Functional Properties of Neuronal Networks with Controlled Topology. PLoS One, 2012, 7( 4): e34648–
8
De Maria E, Muzy A, Gaffé D, Ressouche A, Grammont F. Verification of temporal properties of neuronal archetypes modeled as synchronous reactive systems. In: Proceedings of Hybrid Systems Biology–5th International Workshop. 2016, 97–112
9
De Maria E, L’Yvonnet T, Gaffé D, Ressouche A, Grammont F. Modelling and formal verification of neuronal archetypes coupling. In: Proceedings of the 8th International Conference on Computational Systems-Biology and Bioinformatics. 2017, 3–10
10
Bahrami A, De Maria E, Felty A. Modelling and verifying dynamic properties of biological neural networks in coq. In: Proceedings of the 9th International Conference on Computational Systems-Biology and Bioinformatics. 2018, 12: 1–11
11
Wulfram G, Werner K. Spiking Neuron Models: An Introduction. 1st ed. New York: Cambridge University Press, 2002
12
W S McCulloch , W Pitts . A logical calculus of the ideas immanent in nervous activity. The Bulletin of Mathematical Biophysics, 1943, 5( 4): 115– 133
13
Clarke E M, Grumberg O, Peled D A. Model Checking. 1st ed. Cambridge: MIT Press, 1999
14
D R Gilbert , M Heiner . Advances in computational methods in systems biology. Theoretical Computer Science, 2015, 599 : 2– 3
15
F Fages , S Soliman , N Chabrier-rivier . Modelling and querying interaction networks in the biochemical abstract machine biocham. Journal of Biological Physics and Chemistry, 2004, 4 : 64– 73
16
Richard A, Comet J, Bernot G. Graph-based modeling of biological regulatory networks: Introduction of singular states. In: Proceedings of International Conference on Computational Methods in Systems Biology. 2004, 58–72
17
E De Maria , F Fages , A Rizk , S Soliman . 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. Theoretical Computer Science, 2011, 412( 21): 2108– 2127
18
Talcott C L, Knapp M. Explaining response to drugs using pathway logic. In: Proceedings of the 15th International Conference on Computational Methods in Systems Biology, 2017, 249–264
19
Halbwachs N. Synchronous programming of reactive systems. In: Proceedings of the 10th International Coference on Computer Aided Verification. 1998, 1–16
20
Halbwachs N, Lagnier F, Raymond P. Synchronous observers and the verification of reactive systems. In: Proceedings of the 3rd International Conference on Algebraic Methodology and Software Technology. 1994, 83-96
21
Halbwachs N, Raymond P. Validation of synchronous reactive systems: from formal verification to automatic testing. In: Proceedings of Asian Computing Science Conference. 1999, 1-12
22
B Jeannet . Dynamic partitioning in linear relation analysis. application to the verification of reactive systems. Formal Methods in System Design, 2003, 23( 1): 5– 37
23
Luke webpage
24
A Franzén . Using satisfiability modulo theories for inductive verification of lustre programs. Theoretical Computer Science, 2006, 144( 1): 19– 33
25
Hagen G, Tinelli C. Scaling up the formal verification of lustre programs with smt-based techniques. In: Proceedings of 2008 Formal Methods in Computer-Aided Design. 2008, 1–9
26
Champion A, Mebsout A, Sticksel C, Tinelli C. The kind 2 model checker. In: Proceedings of the 28th International Conference on Computer Aided Verification. 2016, 510–517
27
Lowe G. Breaking and fixing the needham-schroeder public-key protocol using FDR. In: Proceedings of International workshop on Tools and Algorithms for the Construction and Analysis of Systems. 1996, 147–166
28
Abdelmoula M, Gaffé D, Auguin M. Automatic test set generator with numeric constraints abstraction for embedded reactive systems: Autseg v2. In: Proceedings of SIMOL2015: The 7th International Conference on advances in System Simulation. 2015
29
Wijbrans K, Buve F, Rijkers R, Geurts W. Software engineering with formal methods: Experiences with the development of a storm surge barrier control system. In: Proceedings of International Symposium on Formal Methods. 2008, 419–424
30
Nelson S D, Pecheur C. Formal verification for a next-generation space shuttle. In: Proceedings of Interrnational workshop on Formal Approaches to Agent-Based Systems. 2002, 53−67
31
J R Burch , E M Clarke , D E Long , K L McMillan , D L Dill . Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994, 13( 4): 401– 424
32
E M Clarke , O Grumberg , D E Long . Model checking and abstraction. ACM Transactions on Programming Language and Systems, 1994, 16( 5): 1512– 1542
33
Clarke E M, Long D E, Mcmillan K L. Compositional model checking. 1989
34
Fontaine P, In: Proceedings of the 27th International Conference on Automated Deduction. 2019, 11716
35
Harrison J T AO. J, In: Proceedings of the 10th International Conference on Interactive Theorem Proving. 2019, 141
36
Bertot Y, Castéran P. Interactive Theorem Proving and Program Development−Coq’Art: The Calculus of Inductive Constructions. 1st ed. New York: Springer, 2004
37
Constable R L, et al. Implementing Mathematics with the Nuprl Proof Development System. 1986
38
Owre S, Rajan S, Rushby J, Shankar N, Srivas M. PVS: combining specification, proof checking, and model checking. In: Proceeding of International Conference on Formal Methods in Computer-Aided Design.1996, 411−414
39
Nipkow T, Wenzel M, Paulson L C. Isabelle/HOL: A proof assistant for higher-order logic. 1st ed. Berlin, Heidelberg: Springer-Verlag, 2002
40
Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107-115.
41
Yang X, Chen Y, Eide E, Regehr J. Finding and understanding bugs in C compilers. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. 2011, 283–294
42
Klein G, Elphinstone K, Heiser G, et al. Sel4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. 2009, 207−220
43
Gonthier G, Asperti A, Avigad J, et al. A machine-checked proof of the odd order theorem. In: Proceedings of the 4th International Conference on Interactive Theorem Proving. 2013, 163–179
44
Hales T, Adams M, Bauer G, et al. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 2017, 5
45
A L Hodgkin , A F Huxley . A quantitative description of membrane current and its application to conduction and excitation in nerve. The Journal of Physiology, 1952, 117( 4): 500– 544
46
R Thomas , D Thieffry , M Kaufman . Dynamical behaviour of biological regulatory networks−I. biological role of feedback loops and practical use of the concept of the loop-characteristic state. Bulletin of Mathematical Biology, 1995, 57( 2): 247– 276
47
Reddy V N, Mavrovouniotis M L, Liebman M N. Petri net representations in metabolic pathways. In: Proceedings of the 1st International Conference on Intelligent Systems for Molecular Biology. 1993, 328–336
48
Regev A, Silverman W, Shapiro E. Representation and simulation of biochemical processes using the pi-calculus process algebra. In: Proceedings of the 6th Pacific Symposium on Biocomputing. 2001, 459–470
49
A Regev , E M Panina , W Silverman , L Cardelli , E Shapiro . Bioambients: an abstraction for biological compartments. Theoretical Camputer Science, 2004, 325( 1): 141– 167
50
N Chabrier-Rivier , M Chiaverini , V Danos , F Fages , V Schächter . Modeling and querying biomolecular interaction networks. Theoretical Computer Science, 2004, 325( 1): 25– 44
51
R Hofestädt , S Thelen . Quantitative modeling of biochemical networks. In Silico Biology, 1998, 1 : 39– 53
52
Alur R, Belta C, Ivancic F. Hybrid modeling and simulation of biomolecular networks. In: Proceedings of International Workshop on Hybrid Systems: Computation and Control. 2001, 19–32
53
Phillips A, Cardelli L. Efficient, correct simulation of biological processes in the stochastic pi-calculus. In: Proceeding of International Conference on Computational Methods in, 2007, 184–199
54
V Danos , C Laneve . Formal molecular biology. Theoretical Computer Science, 2004, 325( 1): 69– 110
55
Cimatti A, Clarke E M, Giunchiglia F, Roveri M. NUSMV: A new symbolic model verifier. In: Proceedings of International Conference on Computer Aided Verification. 1999, 495–499
56
Kwiatkowska M Z, Norman G, Parker D. PRISM 4.0: verification of probabilistic real-time systems. In: Proceedings of International Conference on Computer Aided Verification. 2011, 585–591
57
De Maria E, Despeyroux J, Felty A P. A logical framework for systems biology. In: Proceedings of International Conference on Formal Methods in Macro-Biology. 2014, 136–155
58
Dénès M, Lesage B, Bertot Y, Richard A. Formal proof of theorems on genetic regulatory networks. In: Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. 2009, 69–76
59
A Rashid , O Hasan , U Siddique , S Tahar . Formal reasoning about systems biology using theorem proving. PLOS ONE, 2017, 12( 7): 1– 27
60
Pinaud B, Andrei O, Fernández M, Kirchner H, Melançon G, Vallet J. PORGY: a visual analytics platform for system modelling and analysis based on graph rewriting. Extraction et Gestion des Connaissances. 2017, 473–476
61
W Maas . Networks of spiking neurons: The third generation of neural network models. Neural Networks, 1997, 10( 9): 1659– 1671
62
Paugam-Moisy H, Bohte S M. Computing with spiking neuron networks. Handbook of Natural Computing, 2012, 335–376
63
G Cybenko . Approximation by superpositions of a sigmoidal function. Mathematics of Control, Signals and Systems, 1989, 2( 4): 303– 314
64
E M Izhikevich . Which model to use for cortical spiking neurons?. IEEE Transactions on Neural Networks, 2004, 15( 5): 1063– 1070
65
L Lapicque . Recherches quantitatives sur l’excitation electrique des nerfs traitee comme une polarization. J Physiol Pathol Gen, 1907, 9 : 620– 635
66
B Aman , G Ciobanu . Modelling and verification of weighted spiking neural systems. Theoretical Computer Science, 2016, 623 : 92– 102
67
De Maria E, Di Giusto C. Parameter learning for spiking neural networks modelled as timed automata. In: Proceedings of the 11th International Joint Conference on Biomedical Engineering Systems and Technologies (BIOSTEC 2018). 2018, 17–28
68
Purves D, Augustine G J, Fitzpatrick D, Hall W C, LaMantia A, McNamara J O, Williams S M., Neuroscience. 3rd edition. Sunderland, MA: Sinauer Associates, Inc., 2006
69
Coq reference manual.
70
T Coquand , G P Huet . The calculus of constructions. Information and Computation, 1988, 76( 2/3): 95– 120
71
Miller D, Nadathur G. Programming with Higher-Order Logic. 1st ed. New York: Cambridge University Press, 2012
72
De Maria E, Muzy A, Gaffé D, Ressouche A, Grammont F. Verification of temporal properties of neuronal archetypes using synchronous models. See hal.inria.fr. 2016
73
D’Angelo E, Danese G, Florimbi G, Leporati F, Majani A, Masoli S, Solinas S, Torti E. The human brain project: high performance computing for brain cells hw/sw simulation and understanding. In: Proceedings of 2015 Euromicro Conference on Digital System Design. 2015, 740–747
74
D O Hebb . Organization of behavior. The Journal of Physiology, 1949, 6( 307): 335–
75
F Grammont , A Riehle . Spike synchronization and firing rate in a population of motor cortical neurons in relation to movement direction and reaction time. Biological Cybernetics, 2003, 88( 5): 360– 373
