Modelling and optimisation of DNA stack nano-device using probabilistic model checking

DNA stack nano-device is a bio-computing system that can record and store molecular signals based on DNA-DNA hybridisation and strand displacement. In vitro implementation of the system faces a number of challenges regarding the performance of producing target stack. We apply probabilistic model checking, a formal verification technique for analysing the correctness of stochastic systems, to analyse and optimise the DNA stack system.

In this talk, I will describe the probabilistic model framework based on continuous-time Markov chain (CTMC) we used to describe the system behaviour. I will also show how we used the PRISM probabilistic model checker to answer two important questions: (1) what is the minimum required incubation time to record a signal, and (2) and how to maximise the yield of the target stack?