On The Model Checking Of SN P Systems Based On Rewriting Logic

With the interactions between computer science and other disciplines, many computational models have been presented, based on different theories. Membrane Computing (also called P Systems) is a novel computational model which is inspired by the structure and function of biological cells. SN P Systems (Spiking Neural P Systems) is an extension of Neural-like P Systems. The notion of time was introduced to the system, which makes it different from other kinds of P Systems distinctly. The computational power of SN P Systems has been proved to be equal to Turing complete.However, with the increase of complexity of SN P Systems, it becomes difficult to verify the correctness of the model manually. Therefore, it becomes an urgent problem that how to use computer verify a SN P System automatically. Model checking is introduced as an effective way to solve such a problem. There are many model checking tools like SPIN, Maude. Maude is also regarded as a powerful specification language, which can be executed by Maude interpreter. Maude is often used for model checking and logic induction.In this dissertation, a formal method is proposed to specify SN P Systems with Maude language. Operational semantics of SN P Systems are defined through applying the object-oriented programming in Maude. The specification is executable, which allows us to analyze the result of a computation and to monitor the states of the system during the computation. And then, we provide an example to illustrate the specification mechanism of SN P Systems provided in this thesis. It reveals how to implement the model checking of SN P systems.The main contribution of this thesis is that we apply the model checking techniques to SN P Systems. Based on rewriting logic, the function of Maude is extended to support the executable specification of SN P Systems. This allows us to verify the correctness of SN P Systems models aided by computers. It also enables us to study properties of the computation model more deeply.