Signaling P Systems and Verification Problems

We introduce a new model of membrane computing system (or P system), called signaling P system. It turns out that signaling systems are a form of P systems with promoters that have been studied earlier in the literature. However, unlike non-cooperative P systems with promoters, which are known to be universal, non-cooperative signaling systems have decidable reachability properties. Our focus in this paper is on verification problems of signaling systems; i.e., algorithmic solutions to a verification query on whether a given signaling system satisfies some desired behavioral property. Such solutions not only help us understand the power of “maximal parallelism” in P systems but also would provide a way to validate a (signaling) P system in vitro through digital computers when the P system is intended to simulate living cells. We present decidable and undecidable properties of the model of non-cooperative signaling systems using proof techniques that we believe are new in the P system area. For the positive results, we use a form of “upper-closed sets” to serve as a symbolic representation for configuration sets of the system, and prove decidable symbolic model-checking properties about them using backward reachability analysis. For the negative results, we use a reduction via the undecidability of Hilbert’s Tenth Problem. This is in contrast to previous proofs of universality in P systems where almost always the reduction is via matrix grammar with appearance checking or through Minsky’s two-counter machines. Here, we employ a new tool using Diophantine equations, which facilitates elegant proofs of the undecidable results. With multiplication being easily implemented under maximal parallelism, we feel that our new technique is of interest in its own right and might find additional applications in P systems.