Spiking neural P systems (in short, SN P systems) are models of computation inspired by biological spiking neurons. SN P systems have neurons as spike processors which are placed on the nodes of a directed and static graph (the edges in the graph are the synapses). In this work, we introduce a variant called SN P systems with scheduled synapses (in short, SSN P systems). SSN P systems are inspired and motivated by the structural dynamism of biological synapses, while incorporating ideas from nonstatic (i.e. dynamic) graphs and networks. In particular, synapses in SSN P systems are available only at specific durations according to their schedules. The SSN P systems model is a response to the problem of introducing durations to synapses of SN P systems. Since SN P systems are in essence static graphs, it is natural to consider them for dynamic graphs also. We introduce local and global schedule types, also taking inspiration from the above mentioned sources. We prove that SSN P systems are computationally universal as number generators and acceptors for both schedule types, under a normal form (i.e. a simplifying set of restrictions). The introduction of synapse schedules for either schedule type proves useful in programming the system, despite restrictions in the normal form.

Structural and behavioural properties of models are very important in development of complex systems and applications. In this paper, we investigate such properties for some classes of SN P systems. First, a class of SN P systems associated to a set of routing problems are investigated through their matrix representation. This allows to make certain connections amongst some of these problems. Secondly, the behavioural properties of these SN P systems are formally verified through a natural and direct mapping of these models into kP systems which are equipped with adequate formal verification methods and tools. Some examples are used to prove the effectiveness of the verification approach.