Use of Büchi automata and randomness for the description of biological processes

摘要

The main topic of this study is the modelling and verification of biological systems using ω -automata. This work focuses on the protein folding problem and the infinite behaviour it features in many cases. Specifically, stochastic computational models with infinite input are used in this paper’s approach and indicative aspects of a biological problem are presented using both ω -automata and probabilistic Büchi automata (PBAs), making a novel attempt to establish their use in reasoning about biological processes. Necessary preliminary definitions and background towards this direction are provided. Finally, the pros and cons of each model are shown through examples. Overall, this work contributes by combining for the very first time PBAs with real biological mechanisms, with indicative examples, both with PBAs and NBAs (non-deterministic Büchi automata).