典型文献
On the use of formal methods to model and verify neuronal archetypes
文献摘要：
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.
文献关键词：
中图分类号：
作者姓名：
Elisabetta DE MARIA;Abdorrahim BAHRAMI;Thibaud L'YVONNET;Amy FELTY;Daniel GAFFé;Annie RESSOUCHE;Franck GRAMMONT
作者机构：
Université C?te d'Azur,CNRS,I3S,06903 Sophia Antipolis Cedex,France;School of Electrical Engineering and Computer Science,University of Ottawa,Ontario,K1N 6N5,Canada;Université C?te d'Azur,INRIA SAM,06902 Sophia Antipolis Cedex,France;Université C?te d'Azur,CNRS,LEAT,06903 Sophia Antipolis Cedex,France;Université C?te d'Azur,CNRS,LJAD,06108 Nice Cedex 02,France
文献出处：
引用格式：
[1]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)[J].计算机科学前沿,2022(03):97-118
A类：
archetypes,checkers,prover,Coq
B类：
On,use,formal,methods,neuronal,Having,neural,networks,can,greatly,help,understanding,verifying,their,properties,response,external,factors,such,disease,medicine,In,this,paper,we,adopt,represent,neurons,some,graphs,composition,Some,specific,known,having,biologically,relevant,structures,behaviors,them,These,supposed,basis,typical,instances,information,processing,study,six,fundamental,simple,series,multiple,outputs,parallel,negative,loop,inhibition,contralateral,consider,ways,couple,connecting,first,input,second,ii,nesting,within,one,We,report,compare,key,approaches,modeling,verification,proposed,selected,couplings,exploits,synchronous,programming,language,Lustre,encode,express,concerning,dynamic,verified,thanks,relies,theorem,Proof,Assistant
AB值：
0.491147
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
