Formal Computational Modelling of Bone Physiology and Disease Processes

This thesis addresses the definition and the application of formal techniques in the field of Computational Systems Biology, with particular focus on bone remodelling (BR), the cellular process of bone renewal, and on the analysis and control of disease processes. Firstly, we study the multiscale and spatial mechanisms that connects disruptions at the molecular signalling level, to osteoporosis and other diseases characterized by low bone mass and structural weakening at the tissue level. We define a modelling framework based on a formal specification language which extends the Shape Calculus, a process algebra with spatial and geometrical primitives. The executable side is obtained by encoding the specification into an agent-based model, where agents are enriched with stochastic actions and perception. This framework is used to define a novel spatial and individual-based model of bone remodelling, parametrized in order to reproduce both healthy and osteoporotic conditions, and to analyse how the disposition of bone cells affects bone microstructure at the tissue level. Secondly, we propose a methodological study aiming at evaluating and comparing different models of bone remodelling and different techniques for the analysis of bone diseases and of stabilization and homeostasis-related properties. We consider a non-linear ODE model, over which we perform simulation and sensitivity analysis; a stochastic model on which we employ probabilistic model checking; and a hybrid piecewise-multiaffine approximation of the ODEs, supporting model checking and LTL-based parameter synthesis. We extend the model in order to describe osteoporosis and osteomyelitis (a bone infection) and we show how quantitative verification methods could provide clinically meaningful diagnostic estimators. Thirdly, we investigate the use of formal languages and hybrid techniques in the modelling of disease processes and in the synthesis of treatment strategies. In particular, hybrid models allow us to describe the disease dynamics in a continuous fashion, while the scheduling of multiple drugs discretely. We define a process-algebraic language for specifying general disease processes and treatments, called D-CGF (an extension to the CGF process algebra), from which multiple semantics can be derived: stochastic hybrid automata and hybrid dynamical systems. Then, hybrid non-linear control is employed to compute the optimal scheduling of multiple therapies. The approach is applied to an epidemic model of the H1N1 influenza, where we derive the optimal combination of vaccination and antiviral treatments.