%0 Generic
%D 2012
%T Formal verification 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 Amsterdam, The Netherlands
%I Springer
%P 215-225
%R 10.1007/978-3-642-28024-5_15
%U http://www.springerlink.com/content/86113w5748425306/
%V 7184
%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.