Formalization of P Systems by Maude

Rewriting logic is a unified model of concurrency, which provides a formal common framework of wellknown models of concurrent systems. A new formal method of the specification and execution of P systems using rewriting logic was proposed. The powerful tool Maude 2. 0 is used to implement this specification. In order to present the general ideas in a concrete case study, a simple and classical example from the literature is adopted to present how to formally specify and execute a P system.