cPV – Simulation and Verification for Membrane Computing

As a newly proposed computational paradigm of membrane computing, cP systems are used to solve several NP-complete and PSPACE-complete problems in linear or sub-linear time theoretically. Most cP systems proposed in previous studies lack of automated verification support. In this paper, we present cPV, the first software implementation for cP system simulation and verification. cPV offers multiple features, which include modelling, simulation, automated verification of properties such as absence of deadlock, confluence, termination, determinism, and goal reachability. As an extensible framework, modules in cPV are loosely coupled, where new verification algorithms, reduction techniques, and property specifications can be easily extended. To evaluate cPV, we constructed two benchmark datasets that cover several important aspects of cP systems. The experimental results demonstrated effective automatic verification support to the membrane computing problem domain.