Developing a Compositional Framework for the Construction and Analysis of Boolean Networks

Abstract

Boolean networks are a widely used qualitative approach for modelling and analysing biological systems. However, their application is restricted by the well–known state space explosion problem, which means that modelling large-scale, realistic biological systems is challenging. Composition is a well–known formal approach for allowing complex models to be constructed and analysed. In this thesis, we set out to develop a compositional framework for (synchronous) Boolean networks to facilitate the construction and analysis of large scale biological models. The novel compositional approach we present is based on composing Boolean networks by merging entities using a binary Boolean operator. We consider what it means to preserve the underlying behaviour of Boolean networks in a composed model and introduce the notion of compatibility to formalise this concept. It turns out that the compatibility property is difficult to verify as it references the behaviour of the composed model and so we develop the alignment property which is able to predict whether the composition of Boolean networks is compatible based only on their individual behaviour. We show formally that the alignment property is sufficient to ensure compatibility when the underlying Boolean operator being used is idempotent and illustrate its application by presenting results concerning the compatibility of composing duplicate copies of a Boolean network. While the alignment property is interesting, it turns out that is not a necessary property for compatibility and so does not completely characterise behaviour preservation. Therefore, we investigate extending the alignment property by considering the behavioural interference that can occur when two Boolean networks are composed.We formalise this interference using a labelled state graph approach and introduce an interference state graph, which turns up a significant structure that can capture the complete behaviour that a BN can have under the composition. Using the interference state graph, we can extend the alignment by adding interference and define weak alignment property. We show formally that weak alignment completely characterises compatibility when the underlying Boolean operator being used is idempotent and therefore provides an important scalable means of checking behaviour preservation in composed models. We investigate extending the theoretical framework definitions and results to make the compositional framework more practical by allowing multiple entities and multiple components of Boolean networks. We explain formally that all the key results conducted for a single entity case also hold when composing numerous entities from each Boolean model. Nevertheless, composing several components of Boolean networks turns out to be complicated approach; however, various initial results have been discussed. Algorithms developed for key results are providing a foundation for tool support. With a corporation with us, a prototype tool support has been developed which can automate our compositional framework and its associated analysis.