Modelling and Formal Verification of Neuronal Archetypes Coupling

Abstract : In the literature, neuronal networks are often represented as graphs where each node symbolizes a neuron and each arc stands for a synaptic connection. Some specific neuronal graphs have biologically relevant structures and behaviors and we call them archetypes. Six of them have already been characterized and validated using formal methods. In this work, we tackle the next logical step and proceed to the study of the properties of their couplings. For this purpose, we rely on Leaky Integrate and Fire neuron modeling and we use the synchronous programming language Lustre to implement the neuronal archetypes and to formalize their expected properties. Then, we exploit an associated model checker called kind2 to automatically validate these behaviors. We show that, when the archetypes are coupled, either these behaviors are slightly modulated or they give way to a brand new behavior. We can also observe that different archetype couplings can give rise to strictly identical behaviors. Our results show that time coding modeling is more suited than rate coding modeling for this kind of studies.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [16 references]  Display  Hide  Download
Contributor : Annie Ressouche <>
Submitted on : Thursday, December 7, 2017 - 11:17:58 AM
Last modification on : Tuesday, April 2, 2019 - 9:54:05 PM


Files produced by the author(s)



Elisabetta de Maria, Thibaud L 'Yvonnet, Daniel Gaffé, Annie Ressouche, Franck Grammont. Modelling and Formal Verification of Neuronal Archetypes Coupling . CSBio 2017 - 8th International Conference on Computational Systems-Biology and Bioinformatics, Dec 2017, Nha Trang, Vietnam. pp.3-10, ⟨10.1145/3156346.3156348⟩. ⟨hal-01643862⟩



Record views


Files downloads