Modelling and verification of weighted spiking neural systems

This paper presents spiking neural P systems with weighted synapses, a class of distributed parallel neural-like computing models, abstracted from the way in which the complex system of neurons processes information and communicates to ensure a proper functioning of the brain. Neurons communicate with each other through synapses endowed with an integer weight denoting the number of synapses for each pair of connected neurons. We translate the spiking neural P systems with weighted synapses into a class of timed safety automata, proving that such a translation is formally correct. This relationship allows the verification of several kinds of properties, both qualitative and quantitative, using tools and techniques developed for timed automata.