| Summary: | The study and development of tools for computational systems is an area where we can easily find diverse works and, nowadays, it is one of the dominant topics when we think about the research on computer science. As consequence, the field of computation has access to a solid theoretical basis, as well as to a wide collection of algorithms and tools (such as model checkers). The focus of this thesis is to look at a biological system under a computational perspective, where cells and gens replace the role of transistors as the fundamental elements of a computational system. Indeed, the notion of computation is often compared to the functioning of a brain in an animal. Taking into account this point of view, the goal of this work is to revisit basic concepts present on the study of intracelular dynamics, which are fundamentally the same for all living organisms, under a computer science perpective. Thus, we intend to understand how we can apply concepts, algorithms and computational tools, which are used the field of Computer Science, to the mentioned biological systems. In particular, we start by describing some kinds of models used to model the intracellular dynamics of living organisms – Piecewise linear models and Boolean networks. Hence, we propose a new perspective over Piecewise linear model, considering these models as reconfigurable. This allows one to use computational tools like KeYmaera and dReach to reason about these models. Afterward, discretizing this kind of model but maintaining the notion of reconfigurability, we obtain the concept of reactive Boolean network, based on the switch graph formalism, and propose a logical language to express and formally check properties of these systems along with a notion of bisimulation. In what relates to Boolean networks, we provide a new point of view over the notion of “terminal”, by relating it to the notion of bisimulation, which is widely known in the area of Computater Science. Then, we focus in the asymptotic graph method and, after a fundamental study, we propose a generalized and intermediate method that is less efficient in a computational perspective but more suitable to the intended context. Finally, we consider a new kind of stochastic model which is obtaining embeding weights in edges of switch graphs. We also develop an extension of PRISM model checker – rPrism – to ease the study of this specific class of stochastic models.
|
|---|