This thesis is a contribution to the field of systems biology, which is concerned with mathematical and computational modelling of biological systems. The aim of the field is to understand biological processes via holistic computational methods. One of the standing problems in systems biology is how to derive model of a system, preferably one easily understandable by humans, from experimental data and observations. Understandably, the structure of the problem depends heavily on the system of interest and the available data, therefore it is worthwhile to create new methods that utilize particular features, as there can hardly be a universal solution. Here we present an approach for modelling and analysis of complex biological networks that uses a high-level, abstract modelling framework---the multi-valued logical networks. In this framework we employ an automated method originating in the theoretical computer science, called model checking, which allows for formal reasoning about dynamical systems. We can then create a multitude of candidate models and use model checking method to compare the behaviour of these to experimental data. Our approach however produces high volumes of data. To be able to work with the data we use basic statistical methods, which allow us to summarize the dataset into a few key values. In addition, these values can be subsequently compared between multiple datasets. For better understanding we couple these methods with an interactive visualization software. The whole framework is implemented in a tool called TREMPPI, which is available under an open-source license and distributed together with this thesis. We illustrate the functions of TREMPPI on three biological studies---two human signalling pathways, related to cancer, and a protection mechanism of the bacteria E. Coli.
Diese Dissertation ist ein Beitrag zur Systembiologie, welche sich mit der mathematischen Modellierung biologischer Prozesse beschäftigt. Das Ziel dieses Forschungsbereiches ist es biologische Vorgänge mit Hilfe von ganz\\-heit\\-lich\\-en, computergestützten Methoden zu verstehen. Eine aktuelle Herausforderung der Systembiologie ist die automatische Herleitung von Modellen anhand von Beobachtungsdaten und Ex\\-pe\\-ri\\-men\\-ten, bestenfalls eines Modells, dessen Aufbau dem Nutzer leicht zugänglich ist. Natürlich hängen die Schwierigkeiten dieses Problems von dem zu modellierenden System ab und da kaum zu erwarten ist, dass es eine universelle Lösung geben kann, lohnt es sich spezifische Methoden für spezielle Systeme zu entwickeln. Wir stellen hier einen Ansatz zur Modellierung and Analyse von komplexen biologischen Netzwerken vor, der auf einer hohen Abstraktion der Vorgänge basiert---den sogenannten Mehrwertigen logischen Netzwerken. In diesem Zusammenhang verwenden wir eine Methode aus der theoretischen Informatik, nämlich die automatische Modellprüfung, welche uns erlaubt formal begründete Aussagen zur Dynamik der modellierten Systeme zu treffen. Wir erzeugen eine Menge von Modellkandidaten und verwenden die Modellprüfung um ihre Dynamiken mit den Beobachtungsdaten zu vergleichen. Unser Ansatz erzeugt große Mengen an Daten. Wir verwenden statistische Methoden um wichtige Eigenschaften eines Datensatzes hervorzuheben. Zusätzlich können aufgrund dieser Eigenschaften Vergleiche zwischen unterschiedlichen Datensätzen aufgestellt werden. Zum einfacheren Verständnis sind diese Methoden teil einer interaktiven Visualisierungssoftware. Der gesamte Ansatz ist als Software implementiert, welche TREMPPI heißt und frei, unter einer Open-Source Lizenz, erhältlich ist. Wir veranschaulichen die Funktionen von TREMPPI an drei biologischen Fallstudien---zwei Signalwege in menschlichen Zellen, welche im Zusammenhang von Krebs untersucht werden, und ein Modell zum Schutzmechanismus von E. Coli.
