Formal verification of biologically inspired computing models

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.

Name thesis:degree_name

PhD

Level thesis:degree_level

Doctoral

Discipline thesis:degree_discipline

Computer Science

Grantor dc:publisher

ResearchSpace@Auckland

Year dc:date.issued

2022

Author dc:creator

• Liu, Yezhou

Advisors dc:contributor.advisor

• Sun, Jing
• Nicolescu, Radu

Statement dc:rights

• Items in ResearchSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Licence dc:rights.uri

• https://researchspace.auckland.ac.nz/docs/uoa-docs/rights.htm

Handle dc:identifier.uri

https://hdl.handle.net/2292/63353

OAI identifier oai:identifier

oai:researchspace.auckland.ac.nz:2292/63353