Modèles probabilistes et vérification de réseaux de neurones

National audienceResearch advances in the field of neurobiology imply that neural networks are becoming larger and more complex. However, this complexity increases the computation time of the model simulations and therefore the speed and the memory used by software. During this internship we choose to model neural networks as LI\&F models (Leaky Integrate and Fire) represented by Markov chains with PRISM, a probabilistic model checker. With this software, we have the possibility to include probability in spike emission in our models according to a sigmoid curve. After having implemented several network models containing different numbers of neurons, we test several properties encoded in PCTL (Probabilistic Computation Tree Logic). We established the pseudo-code of a reduction algorithm which takes as input a network and a property and gives as output a reduced network. This algorithm removes the "wall" neurons that block the transmission of the membrane potential and those whose suppression does not affect the output neurons or the topology of the network. The reduced networks obtained have a significantly lower complexity