Abstract:
As a recently proposed biologically inspired computing model, cP systems can solve computationally hard problems in polynomial - often linear or sublinear - time. Similar to other membrane computing models, cP systems work in an ideal way, having unlimited space and computing power. This thesis discusses the formal verification of cP systems.
cP systems support labelled multiset-based terms and generic rewriting rules. To apply a rule, variable terms in its lhs (left-hand-side) and promoters need to be unified against system terms. Although several first-order unification algorithms were proposed in previous work, none of them can be readily applied to cP systems due to the use of labelled and nested multisets. In order to solve the issue, we formally defined the unification problem for labelled multisets and proposed a corresponding algorithm, namely LNMU. This can solve well-formed labelled multiset unification problems in linear time.
To verify cP systems, both model checking and interactive theorem proving are considered in this thesis. By using formal tools including PAT3, ProB, and Coq, several cP systems were verified including two NPC solutions proposed in this study. These are: ΠSSP - a cP system that solves the subset sum problem in linear time, and Π Sudoku - a cP system that solves Sudoku (m * m) in sublinear time. In order to automate the verification process, we proposed several mapping guidelines, which can be used to transform cP system notation into modelling languages including CSP#, B, and Gallina automatically.
Using existing general purpose formal tools to verify cP systems often requires human intervention. Furthermore, it is extremely hard to completely model cP systems with complex generic rules in third-party verifiers. In order to overcome these limitations, we designed and implemented a domain-specific formal framework for cP system simulation and verification, namely cPV. By implementing LNMU in an optimised way, cPV can efficiently simulate and verify cP systems. System properties including deadlockfreeness, confluence, termination, determinism, and goal reachability can be automatically verified in cPV.
We also presented a new research direction: using cP systems as a theorem proving tool. A cP system that can efficiently perform equational deduction was proposed. Using certain cP system friendly encodings and the power of maximal parallelism, the cP system can be exponentially faster than traditional rewrite systems when proving equational theories.