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

Elisabetta De Maria is an associate professor at Université Côte d’Azur, France. From 2011 to 2013, she was the coordinator of the International Research Master Program “Computational Biology and Biomedicine” (CBB) of University of Nice, France. Her expertise in bioinformatics led her to be the program chair of the conferences BIOINFORMATICS 2019 and 2020 (10th and 11th International Conference on Bioinformatics Models, Methods and Algorithms), and CSBio 2019 (10th International Conference on Computational Systems-Biology and Bioinformatics). Her research aims at substantiating the claim that formal methods of computer science can provide effective solutions to solve biological and medical problems

Abdorrahim Bahrami is a PhD candidate in computer science at University of Ottawa since 2016, working under the supervision of Dr. Amy Felty (University of Ottawa, Canada) and Dr. Elisabetta De Maria (University of Nice, France). His thesis, entitled “Verified Model of Neurons, Basic Structures, and Neuronal Archetypes of Human Neural Networks: A Formal Methods Approach”, involves analytical studies, implementation, and modelling of biological neural networks using formal verification. In 2009, he was awarded a bronze medal in SAT competition for the best program in crafted data category. He received another bronze medal and the best student solver award in SAT race 2010

Thibaud L’Yvonnet started his studies in biology at Université Côte d'Azur, France. He is currently a PhD student at INRIA Sophia Antipolis Méditerranée. His PhD research is supervised by Sabine Moisan (INRIA, Université Côte d’Azur) and Elisabetta De Maria (I3S, Université Côte d’Azur). Funded by Région Provence Alpe Côte d’Azur, his PhD thesis aims at analyzing cognitive impairment patient’s behavior in situation of medical serious games using formal methods of computer science

Amy Felty is a professor of computer science at the University of Ottawa, Canada. She is an expert in formal methods and has over 25 years of experience in applying them in various domains. She is widely known for her work on logical frameworks and their application in domains such as programming languages, systems biology, privacy and security, and access control policy analysis. She is on the editorial board of several journals, including Springer Nature’s Journal of Automated Reasoning. She has served as a Steering Committe Member, Program Chair or Co-Chair, and Program Committee Member of over 60 conferences and workshops in logic and formal methods. She is currently Treasurer of the ACM Special Interest Group on Logic and Computation

Daniel Gaffé received the PhD degree in electrical engineering in 1996 from the University of Nice-Sophia Antipolis, France. In 1997, he was recruited as an associate professor at the Université Nice Sophia-Antipolis, actual Université Côte d'Azur. He is doing his research at the LEAT (Laboratoire d’Electronique, Antennes et Telecommunications) since 2007. His studies concerns synchronous languages. In this framework, he develops the Light Esterel language with INRIA Institue. He applies the synchronous languages to the neural networks modelling too

Annie Ressouche received her PhD degree in mathematics from the University of Paris 7 in 1978. Since 1979 she was a researcher at Inria, in Sophia Antipolis research center, France. First she contributed to the development of the Esterel language and the synchronous model of time and she studied model checking techniques for this model. In 2002, she joined the Stars team where she applies the synchronous modeling to the generation of safe activity recognition systems. In collaboration with the Côte d’Azur University she studied the safe composition of components in component-based adaptive reactive middleware and she develops the Light Esterel synchronous language. She applies the synchronous approach to neural networks modeling

Franck Grammont is an assistant professor in neurophysiology, theoretical neuroscience and cognitive sciences at the Dieudonné Laboratory of the Côte d’Azur University, France. His main interests concern the theory of neuronal archetypes, the theory of neuronal assemblies, the analysis of neuronal activity and the study of sensorimotor systems

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

Acknowledgements

This work was supported by the French government through the UCA-Jedi project managed by the National Research Agency (ANR-15- IDEX-01) and, in particular, by the interdisciplinary Institute for Modeling in Neuroscience and Cognition (NeuroMod) of the Université Côte d’Azur. It was also supported by the Natural Sciences and Engineering Research Council of Canada. We thank Alexandre Muzy for fruitful discussions on neuron modeling.

RIGHTS & PERMISSIONS

2022 Higher Education Press