%0 Generic %D 2011 %T Formal Veri cation of P Systems with Active Membranes through Model Checking %A Florentin Ipate %A Raluca Lefticaru %A Ignacio Pérez-Hurtado %A Mario J. Pérez-Jiménez %A Cristina Tudose %C Fontainebleau, France %P 241-252 %S Proceedings of the 12th International Conference on Membrane Computing (CMC12) %U http://cmc12.lacl.fr/cmc12proceedings.pdf %X 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. %8 08/2011