@article {788, title = {Formal Veri cation of P Systems with Active Membranes through Model Checking}, journal = {12th International Conference on Membrane Computing (CMC12)}, year = {2011}, month = {08/2011}, pages = {241-252}, address = {Fontainebleau, France}, abstract = {Formal verification of P systems using model checking has attracted a significant amount of research in recent years. However, up to now only P systems with static structure have been considered. This paper makes significant advances in this area by considering P systems with active membranes, in particular P systems with division rules. The paper presents a theoretical framework for addressing this problem and reports on a complex case study involving a well-known NP-complete problem solved using P systems with membrane division rules. This is implemented in Promela and non trivial properties are verified using Spin.}, url = {http://cmc12.lacl.fr/cmc12proceedings.pdf}, author = {Florentin Ipate and Raluca Lefticaru and Ignacio P{\'e}rez-Hurtado and Mario J. P{\'e}rez-Jim{\'e}nez and Cristina Tudose} }