%0 Generic
%D 2011
%T Formal Verication 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