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

Abstract

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.

Graphical abstract

Keywords

neuronal networks / leaky integrate and fire modeling / synchronous languages / model checking / theorem proving / Lustre / Coq / formal methods

References

[1] Sporns O . The human connectome: origins and challenges. NeuroImage, 2013, 80 : 53– 61

[2] Sporns O . Structure and function of complex brain networks. Dialogues in Clinical Neuroscience, 2013, 15 : 247– 262

[3] Sporns O . Graph theory methods: applications in brain networks. Dialogues in Clinical Neuroscience, 2018, 20 : 111– 121

[4] Fornito A , Zalesky A , Breakspear M . Graph analysis of the human connectome: Promise, progress, and pitfalls. NeuroImage, 2013, 80 : 426– 444

[5] Matsuoka K . Mechanisms of frequency and pattern control in the neural rhythm generators. Biological Cybernetics, 1987, 56( 5-6): 345– 353

[6] Lambert R C , Tuleau-Malot C , Bessaih T , Rivoirard V , Bouret Y , Leresche N , Reynaud-Bouret P . Reconstructing the functional connectivity of multiple spike trains using Hawkes models. Journal of Neuroscience Methods, 2018, 297 : 9– 21

[7] Marconi E , Nieus T , Maccione A , Valente P , Simi A . 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] McCulloch W S , Pitts W . 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] Gilbert D R , Heiner M . Advances in computational methods in systems biology. Theoretical Computer Science, 2015, 599 : 2– 3

[15] Fages F , Soliman S , Chabrier-rivier N . 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] De Maria E , Fages F , Rizk A , Soliman S . 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] Jeannet B . 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] Franzén A . 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] Burch J R , Clarke E M , Long D E , McMillan K L , Dill D L . Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994, 13( 4): 401– 424

[32] Clarke E M , Grumberg O , Long D E . 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] Hodgkin A L , Huxley A F . 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] Thomas R , Thieffry D , Kaufman M . 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] Regev A , Panina E M , Silverman W , Cardelli L , Shapiro E . Bioambients: an abstraction for biological compartments. Theoretical Camputer Science, 2004, 325( 1): 141– 167

[50] Chabrier-Rivier N , Chiaverini M , Danos V , Fages F , Schächter V . Modeling and querying biomolecular interaction networks. Theoretical Computer Science, 2004, 325( 1): 25– 44

[51] Hofestädt R , Thelen S . 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] Danos V , Laneve C . 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] Rashid A , Hasan O , Siddique U , Tahar S . 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] Maas W . 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] Cybenko G . Approximation by superpositions of a sigmoidal function. Mathematics of Control, Signals and Systems, 1989, 2( 4): 303– 314

[64] Izhikevich E M . Which model to use for cortical spiking neurons?. IEEE Transactions on Neural Networks, 2004, 15( 5): 1063– 1070

[65] Lapicque L . Recherches quantitatives sur l’excitation electrique des nerfs traitee comme une polarization. J Physiol Pathol Gen, 1907, 9 : 620– 635

[66] Aman B , Ciobanu G . 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] Coquand T , Huet G P . 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] Hebb D O . Organization of behavior. The Journal of Physiology, 1949, 6( 307): 335–

[75] Grammont F , Riehle A . 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

RIGHTS & PERMISSIONS

Higher Education Press