Academic Journal
On the Use of Formal Methods to Model and Verify Neuronal Archetypes
| العنوان: | On the Use of Formal Methods to Model and Verify Neuronal Archetypes |
|---|---|
| المؤلفون: | de Maria, Elisabetta, Bahrami, Abdorrahim, L’yvonnet, Thibaud, Felty, Amy, Gaffé, Daniel, Ressouche, Annie, Grammont, Franck |
| المساهمون: | Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UniCA), Université d'Ottawa Ontario (uOttawa), Laboratoire d'Electronique, Antennes et Télécommunications (LEAT), Université Nice Sophia Antipolis (1965 - 2019) (UNS)-Centre National de la Recherche Scientifique (CNRS), Spatio-Temporal Activity Recognition Systems (STARS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire Jean Alexandre Dieudonné (LJAD), ANR-15-IDEX-0001,UCA JEDI,Idex UCA JEDI(2015) |
| المصدر: | ISSN: 2095-2228. |
| بيانات النشر: | HAL CCSD Springer Verlag |
| سنة النشر: | 2021 |
| مصطلحات موضوعية: | Neuronal Networks, Leaky Integrate and Fire Modeling, Synchronous Languages, Model Checking, Theorem Proving, Lustre, Coq, Formal Methods, [INFO.INFO-NE]Computer Science [cs]/Neural and Evolutionary Computing [cs.NE], [INFO.INFO-BI]Computer Science [cs]/Bioinformatics [q-bio.QM], [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC] |
| الوصف: | International audience ; 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 |
| نوع الوثيقة: | article in journal/newspaper |
| اللغة: | English |
| DOI: | 10.1007/s11704-020-0029-6 |
| الاتاحة: | https://hal.science/hal-03053930 https://hal.science/hal-03053930v1/document https://hal.science/hal-03053930v1/file/archetypes-fcs-hal.pdf https://doi.org/10.1007/s11704-020-0029-6 |
| Rights: | info:eu-repo/semantics/OpenAccess |
| رقم الانضمام: | edsbas.CB5EDDB1 |
| قاعدة البيانات: | BASE |
| DOI: | 10.1007/s11704-020-0029-6 |
|---|