A software tool for verification of Spiking Neural P Systems

A software tool for verification of Spiking Neural P Systems Miguel A. Gutie ´rrez-Naranjo Æ Mario J. Pe ´rez-Jime´nez Æ Daniel Ramı ´rez-Martı ´nez Abstract The formal verification of a Spiking Neural P System (SN P Systems, for short) designed for solving a given problem is usually a hard task. Basically, the verification process consists of the search of invariant formulae such that, once proved their validity, show the right answer to the problem. Even though there does not exist a general methodology for verifying SN P Systems, in (Pa ˘un et al., Int J Found Comput Sci 17(4):975– 1002, 2006) a new tool based on the transition diagram of the P system has been developed for helping the researcher in the search of invariant formulae. In this paper we show a software tool which allows to generate the transition diagram of an SN P System in an automatic way, so it can be considered as an assistant for the formal verification of such computational devices. Keywords Membrane computing  Spiking Neural P systems  Transition diagram 1 Introduction Natural Computing studies new computational paradigms inspired from various well known natural phenomena in physics, chemistry and biology. It abstracts the way in which nature computes, conceiving new computing models. There are several fields in Natural Computing that are now well established. Among them, Genetic algorithms introduced by Holland (1975) is inspired by natural evolution and selection in order to find a good solution in a large set of feasible candidate solutions; Neural Networks introduced by M. A. Gutie ´rrez-Naranjo (&)M. J. Pe ´rez-Jime ´nez D. Ramı ´rez-Martı ´nez Research Group on Natural Computing, Department of Computer Science and Artificial Intelligence, University of Sevilla, Sevilla, Spain e-mail: [email protected] M. J. Pe ´rez-Jime ´nez e-mail: [email protected] D. Ramı ´rez-Martı ´nez e-mail: [email protected] McCulloch and Pitts (1943) which is based on the interconnections of neurons in the brain; DNA-based molecular computing, that was born when Adleman (1994) published a solution to an instance of the Hamiltonian path problem by manipulating DNA strands in a lab. In the framework of Natural Computing, Pa ˘un introduced Membrane Computing in Pa ˘un (2000) under the assumption that the processes taking place in the compartmental structure of a living cell can be interpreted as computations. 1 Since then, a large number of variants have been considered, concerning both the syntax and the semantics of the model. The devices of this model are generically called P systems. The basic idea is to consider a distributed and parallel computing device, structured like a cell, by means of a hierarchical arrangement of membranes which delimit compartments where various chemicals (we call them objects) evolve according to local reaction rules. The objects can be described by symbols or by strings of symbols from a given alphabet. These objects can also pass through membranes, under the control of specific rules. Because the chemicals from the compartments of a cell are swimming in an aqueous solution, the data structure we consider is that of a multiset—a set with multiplicities associated with its elements. Also, in close analogy with what happens in a cell, the reaction rules are applied in a parallel manner. This means that in each computational step a maximal (multi)set of non-deterministically chosen rules is applied. The notions of membrane investigated in this new paradigm of computation are abstract entities which try to mimic some features of the functioning of membranes in living cells. The basic function of biological membranes is to define compartments and to relate compartments to their environment, including neighbouring compartments. The currently accepted model of the membrane structure is the so-called fluid-mosaic model, proposed in 1972 by S. Singer and G. Nicholson. According to this model, a membrane is a phospholipid bilayer in which protein molecules (as well as other molecules) are totally or partially embedded. Spiking Neural P Systems (SN P Systems, for short) were introduced in Ionescu et al. (2006) with the aim of incorporating in membrane computing ideas specific to spike-based neuron models. The intuitive goal was to have a directed graph where the nodes represent the neurons and the edges represent the synaptic connections among the neurons. The flow of information is carried on the action potentials, which are encoded by objects of the same type, the spikes, which are placed inside the neurons and can be sent from presynaptic to postsynaptic neurons according to specific rules and making use of the time as a support of information. The biological motivation for these new SN P Systems is based on recent discoveries on neural coding. Since all spikes of a given neuron look alike, the form of the action potential does not carry any information. Rather, it is the number and the timing of spikes which matter. Traditionally, it has been thought that most, if not all, of the relevant information was contained in the mean firing rate of the neuron. The concept of mean firing rates has been successfully applied during the last 80 years (see, e.g., Mountcastle 1957 or Hubel and Wiesel 1959) from the pioneering work of Adrian (1926a,b). Nonetheless, more and more experimental evidence has been accumulated during recent years which suggests that a straightforward firing rate concept based on temporal averaging may be too simplistic to describe brain activity. One of the main arguments is that reaction times in behavioural experiment are often too short to allow long temporal averages. For instance, recognition 1 A comprehensive presentation can be found in Pa ˘un (2002) and further updated bibliography in http://ppage.psystems.eu/. A presentation of applications can be found in Ciobanu et al. (2006). and reaction involve several processing steps from the retinal input to the finger movement at the output. If at each processing steps, neurons had to wait and perform a temporal average in order to read the message of the presynaptic neurons, the reaction time would be much longer. Many other studies show the evidence of precise temporal correlations between pulses of different neurons and stimulus-dependent synchronisation of the activity in populations of neurons (see, for example, Eckhorn et al. 1988 or Gray and Singer 1989). Most of these data are inconsistent with a concept of coding by mean firing rates where the exact timing of spikes should play no role. Instead of considering mean firing rates, spiking-based models consider the realistic situation in which a neuron abruptly receives an input at a given instant and for each neuron the timing of the first spike after the reference signal contains all the information about the new stimulus. The paper is organised as follows: in Sect. 2we recall some definitions related to SN P Systems (further information can be found in the literature, see http://ppage.psystems.eu/). Section 3is devoted to general aspects of simulation software in the framework of P systems, presenting the most relevant works until now. Next the simulator is presented and some features of its implementation are given. Section 5provides an example of how the simulator works and finally, in the last section some remarks and future work lines are presented. 2 Spiking Neural P Systems An SN P System consists of a set of neurons placed in the nodes of a directed graph and sending signals (called spikes) along the arcs of the graph (providing the synapses between neurons). The objects evolve according to a set of rules (called spiking rules). The idea is that a neuron containing a certain amount of spikes can consume some of them and produce other ones. These produced spikes are sent (maybe with a delay of some steps) to all neurons to which a synapse exists outgoing from the neuron where the rule was applied. There also are forgetting rules. By application of these rules no spikes are sent, simply some spikes are removed from the neuron where the rule was applied. A global clock is assumed and in each time unit each neuron which can use a rule should do it, but only (at most) one rule is used in each neuron. One of the neurons is considered to be the output neuron, and its spikes are also sent to the environment. Definition 1 An SN P System of degree mC1, is a construct of the form P¼ðO;r1;...;rm;syn;outÞ where –O={a} is the singleton alphabet (the object ais called spike); –r 1 ,…,r m are neurons, of the form r i =(n i ,R i ) with i[{1,…,m} where: •n i C0 is the initial number of spikes contained by the neuron r i ; •R i is a finite set of rules of the form E=ac!ap;d where Eis a regular expression over a,cC1 and p,dC0, with cCp;if p =0, then d=0 too. –syn f1;2;...;mgf1;2;...;mgwith ði;iÞ 62 syn for i[{1,…,m} (synapses); –out [{1, 2,…,m} is the output neuron. For the sake of simplicity, if p=d=0, the rule is written as E=ac!kinstead of E=ac!a0;0:This type of rules is called forgetting rules.IfL(E)={a c } then the rules are written in the simplified form ac!ap;dand ac!k: With respect to the application of the rules, if the neuron r i contains kspikes, a k [L(E) and kCc, then the rule E/a c ?a p ;d[R i (with pC1) can be applied; applying it means that cspikes are consumed, thus only k-cremain in the neuron r i ; the neuron r i is fired and it produces pspikes after dtime units. If d= 0, then the spikes are emitted immediately, otherwise the spikes are emitted after dsteps. In the case dC1, if the rule is used in step t, then in steps t,t+1, t+2,…,t+d-1 the neuron is closed, and it cannot receive new spikes (if a neuron has a synapse to a closed neuron and sends spikes along it, then the spikes are lost). In the step t+d, the neuron spikes and becomes again open, hence it can receive spikes. The pspikes emitted by a neuron r i are replicated and they go to all neurons r j such that (i,j)[syn (each r j receives pspikes). If the rule is a forgetting one then no spike is emitted and the neuron cannot be closed. In each time unit, in each neuron which can use a rule, a rule must be used, nondeterministically chosen if several rules are applicable. Note that each neuron processes sequentially its spikes, using only one rule in each time unit. During the computation, a configuration is described by both the number of spikes present in each neuron and by the number of steps to count down until it becomes open (this number is zero if the neuron is open, for example, in the initial configuration). Any sequence of transitions starting in the initial configuration is called a computation. A computation halts if it reaches a configuration where all neurons are open and no rule can be used. Let Pbe an SN P System and let C¼C0)C1)C2)be a computation in P: The spike train of computation C;denoted by stðCÞ;is the sequence of emitting steps, and we write it in the form stðCÞ ¼ ht1;t2;...i;with 1 t1\t2\:The set of all spike trains (over the set COMðPÞof all computations) of Pis denoted by STðPÞ:We also denote by NðCÞ ¼ fnjn¼titi1;for 2 ik;stðCÞ ¼ ht1;t2;...ig: One can associate a set of numbers with STðPÞin several ways. Then, like in Ionescu et al. (2006), we can consider the intervals between consecutive spikes as numbers computed by a computation, with several alternatives: – Taking into account only the first kC2 spikes: NkðPÞ¼fnjn¼titi1;for 2 ik;C2COMðPÞ; stðCÞ ¼ ht1;t2;...i;and Chas at least kspikesg: – Taking into account all spikes of computations with infinite spike trains: NxðPÞ¼fnjn¼titi1;for i2;C2COMðPÞ with stðcÞ¼ht1;t2;...iinfiniteg: – Taking into account all intervals of all computations: NallðPÞ¼[ k2 NkðPÞ[NxðPÞ: Definition 2 A system Pis said to be weakly x-coherent if there is a computation Cin P such that NðCÞ ¼ NallðPÞ(that is, there is a computation which provides all numbers which all other computations can provide). The graphical representation of an SN P System is rather intuitive: the neurons are represented by membranes, placed in the nodes of a directed graph whose arrows represent the synapses. Figure 1shows an example of the graphical representation of an SN P System taken from Pa ˘un et al. (2006). The transition diagram of an SN P System is also a directed graph where the nodes are configurations and an arc is drawn between two nodes/configurations if a direct transition is possible between them. This transition diagram is an interesting tool that allows obtaining invariant formulae to make easier the formal verification of a designed SN P System. 3 Software Since Pa ˘un initiated Membrane Computing (Pa ˘un 2000) as a new branch of Natural Computing, a large number of variants have been considered, both concerning the syntax and the semantics of the model. Let us recall here three of the main variants of P systems: Cell-like P systems, Tissuelike P Systems and Spiking Neural P Systems. In the cell-like model of P systems, membranes are hierarchically arranged in a tree-like structure (see Pa ˘un 2000). The biological inspiration for it is the morphology of cell, where small vesicles are surrounded by larger ones. This biological structure can be abstracted into a tree-like graph, where the root of the graph represents the skin of the cell (the outermost membrane), the leaves represent membranes that do not contain other ones (elementary membranes) and two nodes in the graph are connected if they represent two membranes such that one of them contains the other one. In the tissue P systems (Martı ´n Fig. 1 An SN P system computing frþni ji1g;for nC3 Vide et al. 2002,2003) we consider a general graph instead of a tree-like membrane structure, where the nodes can be considered as processors and the edges as connections among them in order to share information. This model has two biological inspirations: intercellular communication and cooperation between neurons. The common mathematical model of these two mechanisms is a network of processors dealing with symbols and communicating these symbols along channels specified in advance. Irrespectively of the selected approach, it is usually a complex task to predict or to guess how a P system will behave when we are designing a cellular solution to a problem. Moreover, as there do not exist, up to now, implementations in laboratories (neither in vitro nor in vivo nor in any electronical medium), it seems natural to look for software tools that can be used as assistants that are able to simulate computations of P systems. 3.1 Design Generically speaking, the design and development processes for a P system simulator can be structured as follows (see Gutie ´rrez-Naranjo et al. 2006 for details): –Formal definition of the model. First of all, one has to choose which variant of membrane systems is going to be simulated, stating precisely the syntax and semantics of the model to avoid ambiguous interpretations. –Choice of a programming language. Each programming language has its own advantages and disadvantages and, up to now, there is no objective criterion to decide which is the more suitable one for simulating the evolution of a membrane system. Indeed, a large number of different languages as Haskell, Prolog, Java, C, Lisp, Scheme, Visual C++, CLIPS, etc. have been chosen by authors in the literature. –A good way to represent the knowledge. The choice of a suitable data structure is a key problem in all fields of Computer Science (in particular, when dealing with the simulation of P systems). This decision is of course related with the programming language that is used, as specific techniques related with it have to be applied. A good representation allows a quick transition between configurations and therefore speeds up the simulation. –Design of an inference engine to carry out the computation. There exists two basic difficulties intrinsic to the simulation of a P system in a conventional computer: their massive parallelism and the non determinism. Both features must be beared in mind for designing simulators because sequential conventional computers have only one processor. 3.2 Existing Software The first simulators appeared in 2000, only 2 years after Pa ˘un’s foundational paper (Pa ˘un 2000) was presented. It was written by Malit¸a (2000) in LPA-Prolog and, since then, many other software simulators have been presented (see Gutie ´rrez-Naranjo et al. 2006 and references therein for a presentation of the first generation of simulators). The common purpose of this first generation was the better understanding of the computational process of P systems, for pedagogical purposes as well as assistant for researchers. Among these simulators, we can find simulators for P systems where the membrane structure does no change along the computation (as Malit¸a’s one) or simulators able to deal with P Systems where the membranes can divide (as Ciobanu and Paraschiv’s simulator (2002)). Some of them explore new architectures looking for increasing the speed of the computation, as Ciobanu and Wenyuan’s simulator (2004) based on parallel architecture. Others put the stress on a simulation closer to biological laws, as the simulator by the Group for Models of Natural Computing (http://www.di.univr.it) in Verona, based on the implementation of the metabolic algorithm introduced in Bianco et al. (2006). After the first wave, a new generation of software simulators has arisen. They have left the pedagogical purposes and focus their goals on realistic simulations of physical processes via membrane computing techniques. Among them, we can find Nishida’s simulator for the Membrane Approximation Algorithm, the two simulators from D. Pescini and P. Cazzaniga related to Vibrio Fischeri and Dynamical Probabilistic P Systems, Cyto-Sim (Sedwards and Mazza 2007) a processes simulator designed at the Microsoft Research— University of Trento Centre for Computational and Systems Biology, the stochastic simulator based on a generalisation of the Gillespie algorithm designed by Romero-Campero and Pe ´rez-Jime ´nez (2008) and the simulators for biological processes from the University of Sheffield group and Seville team (all of them available from http://ppage.psystems.eu/). 4 A simulator for SN P Systems In Ramı ´rez-Martı ´nez and Gutie ´rrez-Naranjo (2007), a simulator for SN P Systems was presented. It receives the description of an SN P System and outputs its transition diagram with an user friendly interface. Until now, no other software tool has been presented for dealing with SN P Systems. It shares the common purpose of the first simulators of other P system models: the understanding of the computational process of the systems and becoming an assistant for researchers. As pointed out above, the graphical representation of an SN P System is rather intuitive: the neurons are represented by membranes, placed in the nodes of a directed graph whose arrows represent the synapses. In the graphical representation of this software tool, the environment is also represented by a membrane and an arrow exits from the output neuron, pointing to this membrane; in each neuron we specify the rules and the spikes present in the initial configuration. Figure 2shows a screen snapshot of the designer module of the software by showing the graphical representation of an SN P System. 4.1 Technical features The software tool 2 for simulating the evolution of an SN P System is composed by the integration of three modules: – A Graphical User Interface (GUI) which allows an easy interface to users, decoupling experimentation and simulation from programming. This module is written in XBase++ (http://www.alaska-software.com), which is an object oriented language to program database oriented graphic applications. – A second module, written in SWI-Prolog (http://www.swi-prolog.org) which is the inference engine. It takes the initial configuration, the synapses and the rules and produces the transition diagram in text mode. – A graphical designer tool, which allows the user to draw neurons, synapses and to associate spikes and rules with them by using a friendly interface. 2 The simulator is available at (http://ppage.psystems.eu/). The basic way of providing the data to the simulator is by a plain text file with the information stored in an appropriate way. Figure 3shows the input file of the example represented 3 in Fig. 1. The syntax is quite intuitive. The file consists on a set of literals with the predicate symbols rule;synapses and initial: – Rules are of the form ruleðNX;LatexÞ;where Nis the label of the neuron, Xis the ordinal of the rule and Latex is the rule written in Latex mode. In the current version, we accept seven syntactically different types of rules: (1) a^s=a^cnto a^p; d meaning as=ac!ap;d (2) a^s=a^cnto a; d meaning as=ac!a;d (3) a^cnto a^p; d meaning ac!ap;d (4) a^cnto nlamda meaning ac!k Fig. 2 Screen snapshot of the designer interface Fig. 3 Input file 3 for the values r = 3, n = 5 and the labels d 1 = 6, d 2 = 7, d 3 = 8, out = 7, env = 10 and 0 = 11. 2 (5) anto a; d meaning a!a;d (6) a^cnto a; d meaning ac!a;d (7) anto nlamda meaning a!k –synapses has as argument a list of pairs of neurons Start End: –initial stores the initial configuration. A configuration is a list of pairs A=Bwhere the i-th pair A=Bdenotes the number of spikes ðAÞand the number of steps to became open ðBÞthe neuron with label i. The simulator also provides a graphical interface which allows the user to design an SN P System, to store it and build its transition diagram. The SN P System can also be exported from the graphical representation to a file with a text mode representation as described above. 5 An example Next, we illustrate how important it is to know the transition diagram associated with an SN P System by means of an example. Let us consider the SN P System, P, described by Fig. 1. For each configuration Cwe denote by C d (with d=0,1) the configuration obtained from Capplying in neuron 0 the rule a?a;d. Then, the transition diagram of Passociated with the SN P System Pcan be depicted by Fig. 4. Firstly, we note that there are no halting computations in P:We denote by rthe path C2!!Crþ2and by sthe path Crþ2!Crþn1!C0 rþn!C0 rþnþ1:Then, Length(r)=rand Length (s)=n-1. Fig. 4 Transition diagram of the SN P system in Fig. 1