TY - THES A1 - Chodak, Jacek T1 - Spike - a tool for reproducible simulation experiments T1 - Spike - ein Werkzeug für reproduzierbare Simulationsexperimente N2 - Reproducibility of simulation experiments is still a significant challenge and has attracted considerable attention in recent years. One cause of this situation is bad habits of the scientific community. Many results are published without data or source code, and only a textual description of the simulation set-up is provided. Other causes are: no complete simulation set-up, no proper output data analysis and inconsistency of published data, which makes it impossible to compare results. The progress of computational modelling, amount of data and complexity of models requires designing experiments in such a way that ensures reproducibility. A textual description does not provide all the needed details. A computer code is more reliable than a textual description. It is the precise specification that describes a simulation configuration, model, etc. When computer code, data, models and all parameters are provided, the simulation results become reproducible. The main goal of this thesis is to develop a tool that ensures reproducibility and efficient execution of simulation experiments, often involving many individual simulation runs. The tool should support a wide range of application scenarios, where the typical scenario is simulation of biochemical reaction networks, which are represented as (coloured) Petri nets interpreted in the stochastic, continuous or hybrid paradigm. The model to be simulated can be given in various formats, including SBML. The result is a command line tool called Spike, which can be used for various scenarios, including benchmarking, simulation of adaptive models and parameter optimization. It builds on a human-readable configuration script SPC, supporting the efficient specification of multiple model configurations as well as multiple simulator configurations in a single configuration file. N2 - Die Reproduzierbarkeit von Simulationsexperimenten ist nach wie vor eine große Herausforderung und hat in den letzten Jahren viel Aufmerksamkeit bekommen. Eine Ursache für diese Situation sind schlechte Gewohnheiten der wissenschaftlichen Gemeinschaft. Aus irgendwelchen Gründen werden viele Ergebnisse ohne Daten und Quellcode veröffentlicht und es wird nur eine textliche Beschreibung des Simulationsaufbaus gegeben. Andere Ursachen sind: kein ordnungsgemäßer Simulationsaufbau, keine ordnungsgemäße Analyse der Ausgabedaten und Inkonsistenz der veröffentlichten Daten (was einen Vergleich der Ergebnisse unmöglich macht). Der Fortschritt der computergestützten Modellierung, die Datenmenge und die Komplexität der Modelle erfordern es, Experimente so zu gestalten, dass die Reproduzierbarkeit gewährleistet ist. Eine textliche Beschreibung liefert nicht alle Details. Ein Computercode ist zuverlässiger als eine Textbeschreibung. Es bedarf einer genauen Spezifikation einer Simulationskonfiguration, eines Modells usw. Durch die Bereitstellung von Computercode, Daten, Modellen und allen Parametern werden die Ergebnisse einer Simulation reproduzierbar. Das Hauptziel dieser Arbeit ist es, ein Werkzeug zu entwickeln, das die Reproduzierbarkeit und effiziente Durchführung von Simulationsexperimenten, die oft viele einzelne Simulationsläufe umfassen, gewährleistet. Das Werkzeug soll vielfältige Anwendungsszenarien unterstützen, wobei das typische Szenario die Simulation biochemischer Reaktionsnetzwerke ist, die als (farbige) Petri Netze dargestellt werden, die im stochastischen, kontinuierlichen oder hybriden Paradigma interpretiert werden. Das zu simulierende Modell kann in verschiedenen Formaten, einschließlich SBML, vorliegen. Das Ergebnis ist ein Kommandozeilenwerkzeug namens Spike, das in verschiedenen Anwendungsfällen eingesetzt werden kann, darunter Benchmarking, Simulation adaptiver Modelle und Parameteroptimierung. Es basiert auf einem für Menschen lesbaren Konfigurationsskript SPC und unterstützt die effiziente Spezifikation mehrerer Modellkonfigurationen sowie mehrerer Simulator-Konfigurationen in einer einzigen Konfigurationsdatei. KW - Petri nets KW - Parallel simulation KW - Parameter scanning KW - Reproducibility KW - Simulation of adaptive models KW - Petri Netze KW - Parallelsimulation KW - Parameterscannen KW - Reproduzierbarkeit KW - Simulation von adaptiven Modellen KW - Gefärbtes Petri-Netz KW - Simulation KW - Reproduzierbarkeit Y1 - 2021 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus4-58509 ER - TY - THES A1 - Rohr, Christian T1 - Simulative analysis of coloured extended stochastic Petri nets T1 - Simulative Analyse von gefärbten erweiterten stochastischen Petri Netzen N2 - Stochastic modelling of biochemical reaction networks is getting more and more popular. Throughout the past decades typical biological models increased in their size and complexity, because of advances in systems and molecular biology, in particular through the high-throughput omic technologies. Here biochemical networks of different levels of detail are modelled, starting with simple chemical reactions and signal transduction networks, up to individual cells and entire organisms. This increases the demand for efficient analysis methods. A Petri net is a mathematical modelling language for the description of concurrent behaviour of distributed systems. Its advantage is the ease of scalability of the models, which relates to the network’s state space, as well as the structure of the network itself. In this work, we recall several stochastic simulation algorithms, e.g., exact as well as approximate methods. Furthermore, we introduce an approach to improve the efficiency of stochastic simulation for large and dense networks by a new approximate stochastic simulation algorithm called discrete-time leap method. We depict the wide range of simulative analyses of complex stochastic systems ranging from trace generation to the computation of transient solutions and steady state distributions. We set forth advanced analysis of stochastic models by means of simulative model checking. For the use of simulative model checking, we integrate the continuous stochastic (reward) logic (CS(R)L) and the probabilistic linear-time temporal logic with constraints (PLTLc). Simulative model checking has some limitations compared to the numerical methods, e.g., in principle it is possible to consider nested probabilistic formulas in CS(R)L, but not practical, since the calculation is not feasible in a reasonable period of time. In addition to the transient analysis, the steady state analysis is often of interest; therefore we have implemented two on-the-fly steady state detection methods. The first one is based on a “sample batch means” algorithm and is used in the linear-time temporal logic. The second approximates the steady state distribution and checks for convergence. We apply the aforementioned techniques to several case studies from systems biology and technical systems. The main contributions of this thesis to scientific knowledge are the development of the discrete-time leap method for the simulation of stochastic models, the approximations of transient solutions and steady state distributions by use of stochastic simulation for stochastic models and Markov reward models, the development of an infinite time horizon model checking algorithm exploiting the steady state property for PLTLc and CSL, and the first simulative model checking algorithm for CSRL incorporating state and impulse rewards. All presented algorithms and methods are implemented in the advanced analysis tool MARCIE. N2 - Stochastische Modellierung von biochemischen Reaktionsnetzwerken wird immer populärer. Im Laufe der letzten Jahrzehnte hat sich sowohl die Größe als auch die Komplexität typischer biologischer Modelle immer weiter erhöht. Hier werden biochemische Netzwerke unterschiedlicher Detailebenen modelliert, beginnend mit einfachen chemischen Reaktionen und Signaltransduktionsnetzwerken, bis zu einzelnen Zellen und ganzen Organismen. Dadurch erhöht sich die Nachfrage nach leistungsfähigen Analyseverfahren. Ein Petri-Netz ist eine mathematische Modellierungssprache für die Beschreibung des nebenläufigen Verhaltens von verteilten Systemen. Ein Vorteil ist die einfache Skalierbarkeit der Modelle sowohl in Bezug auf die Struktur des Netzes als auch auf ihren Zustandsraum. In dieser Arbeit stellen wir verschiedene stochastische Simulationsalgorithmen vor, sowohl exakte wie auch approximative Verfahren. Darüber hinaus stellen wir einen Ansatz vor, um die Effizienz der stochastischen Simulation für große und dichte Netzwerke durch einen neuen approximativen stochastischen Simulation Algorithmus, genannt discrete-time leap method, zu verbessern. Wir zeigen das breite Spektrum der simulativen Analysen komplexer stochastischer Systeme von der Pfaderzeugung bis zur Berechnung von transienten Lösungen und stationärer Verteilungen. Wir legen erweiterte Analysen von stochastischen Modellen mit Hilfe von simulativer Modellprüfung dar. Wir integrieren die Continuous Stochastic (Reward) Logic (CS(R)L) und die Probabilistic Linear-time Temporal Logic with contraints (PLTLc) für die simulative Modellprüfung. Neben der Transientenanalyse ist oftmals die Analyse der stationären Verteilung von Interesse, deshalb haben wir zwei Methoden zur Erkennung des stationären Zustandes implementiert. Die erste basiert auf einem “sample batch means” Algorithmus und wird in der linearen temporalen Logik verwendet. Die zweite approximiert die stationäre Verteilung und prüft auf Konvergenz. Wir wenden die oben genannten Techniken auf mehrere Fallstudien aus Systembiologie und technischen Systemen an. Der größte Beitrag dieser Arbeit zum aktuellen Stand von Wissenschaft und Technik liegt in der Entwicklung der discrete-time leap method zur Simulation stochastischer Modelle, der Approximationen transienter Lösungen und stationärer Verteilungen mittels stochastischer Simulation für stochastische Modelle und Markov-Rewardmodelle, der Entwicklung eines nicht zeitbeschränkten Algorithmus zur simulativen Modellprüfung, der die stationäre Eigenschaft für PLTLc und CSL ausnutzt, und des ersten Algorithmus zur simulativen Modellprüfung für CSRL, der Zustands- und Impulsrewards enthält. Alle vorgestellten Algorithmen und Methoden sind in dem Analyse-Tool MARCIE implementiert. KW - Coloured extended Stochastic Petri Nets KW - Stochastic simulation KW - Delta-leaping KW - Simulative model checking KW - Gefärbte erweiterte stochastische Petri Netze KW - Stochastische Simulation KW - Delta-leaping KW - Simulatives Modelchecking KW - Stochastisches Modell KW - Gefärbtes Petri-Netz KW - Model Checking Y1 - 2016 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus4-41476 ER -