Analysis and Design of Biological Systems Using Finite State Abstractions

This project is concerned with the study of finite state abstractions for biological systems. The goal is to represent a complex biological system through a finite state machine, without losing the underlying dynamics of the system. Such simplifications are very important in the biological context; synthetic biology for example aims to modify or mimic biological systems, a task that requires numerous simulations before performing expensive and time consuming real-life experiments in vitro or in vivo. To assist this task, we try to exploit the intrinsic structure of biological systems, and more specifically the notion of monotonicity or mixed monotonicity, which is a natural property of biological systems. An algorithm to produce a finite abstraction of a mixed monotone system is explored and applied to two different casestudies: a discrete time dynamical system representing the dynamics of the Tribolium castaneum flour beetle, and a continuous time dynamical system representing the metabolism of lactose in E. Coli. We verify that our abstracted models satisfy certain behaviours of the original systems, which we express as properties defined in linear temporal logic (LTL).