Spiking Neural Networks as Timed Automata

In this paper we show how Spiking Neural Networks can be formalised using Timed Automata Networks. Neurons are modelled as timed automata waiting for inputs on a number of different channels (synapses), for a given amount of time (the accumulation period). When this period is over, the current potential value is computed taking into account the current sum of weighted inputs, and the previous decayed potential value. If the current potential overcomes a given threshold, the automaton emits a broadcast signal over its output channel, otherwise it restarts another accumulation period. After each emission, the automaton is constrained to remain inactive for a fixed refractory period after which the potential is reset. Spiking Neural Networks can be formalised as sets of automata, one for each neuron, running in parallel and sharing channels according to the structure of the network. The inputs needed to feed networks are defined through timed automata as well: we provide a language (and its encoding into timed automata) to model patterns of spikes and pauses and a way of generating unpredictable sequences.