Spiking neural networks modelled as timed automata: with parameter learning

In this paper we address the issue of automatically learning parameters of spiking neural networks. Biological neurons are formalized as timed automata and synaptical connections are represented as shared channels among these automata. Such a formalism allows us to take into account several time-related aspects, such as the influence of past inputs in the computation of the potential value of each neuron, or the presence of the refractory period, a lapse of time immediately following the spike emission in which the neuron cannot emit. The proposed model is then formally validated: more precisely, we ensure that some relevant properties expressed as temporal logical formulae hold in the model. Once the validation step is accomplished, we take advantage of the proposed model to write an algorithm for learning synaptical weight values such that an expected behavior can be displayed. The technique we present takes inspiration from supervised learning ones: we compare the effective output of the network to the expected one and backpropagate proper corrective actions in the network. We develop several case studies including a mutual inhibition network.