Formulation of homeostasis by realisability on linear temporal logic

Abstract

Toward the system level understanding of the mechanisms contributing homeostasis in organisms, a computational framework to model a system and analyse its properties is indispensable. We propose a novel formalism to model and analyse homeostasis on gene networks. Since gene networks can be considered as reactive systems which respond to environmental input, we reduce the problem of analysing gene networks to that of verifying reactive system specifications. Based on this reduction, we formulate homeostasis as realisability of reactive system specifications. An advantage of this formulation is that we can consider any input sequence over time and any number of inputs, which are difficult to be captured by quantitative models. We demonstrate the usefulness and flexibility of our framework in analysing a number of small but tricky networks.