Formal verification of biologically inspired computing models
type: CreativeWork
description: 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 simul…
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 simul…
author: Liu, Yezhou
license: https://researchspace.auckland.ac.nz/docs/uoa-docs/rights.htm
date published: 2022
date modified: 2026-07-24T01:06:29Z
provider: University of Auckland
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: ResearchSpace@Auckland

PropertyValue
property ID: Handle
value: https://hdl.handle.net/2292/63353