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 - Schwarick, Martin T1 - Symbolic on-the-fly analysis of stochastic Petri nets T1 - Symbolische "On-the-fly"-Analyse stochastischer Petrinetze N2 - This thesis investigates the efficient analysis, especially the model checking, of bounded stochastic Petri nets (SPNs) which can be augmented with reward structures. An SPN induces a continuous-time Markov chain (CTMC). A reward structure associates a reward to each state of the CTMC and defines a Markov reward model (MRM). The Continuous Stochastic Reward Logic (CSRL) permits to define sophisticated properties of CTMCs and MRMs which can be automatically verified by a model checker. CSRL model checking can be realized on top of established numerical analysis techniques for CTMCs which are based on the multiplication of a matrix and a vector. However, as these techniques consider a matrix and a vector at least in the size of the number of reachable states, it is still challenging to deal with the famous state space explosion problem. Several approaches, as for instance the use of Multi-terminal Decision Diagrams or Kronecker products to represent the matrix, have been investigated so far. They often enable the implementation of efficient CTMC analysis and are available in a couple of tools. As an alternative to these established techniques I enhance the idea of an on-the-fly computation of the matrix entries deploying a symbolic state space representation. The set of state transitions defining the matrix will be enumerated by the firing of the transitions of the given SPN for all reachable states. The reachable states are encoded by means of Interval Decision Diagrams (IDD). Further, I discuss crucial aspects for the implementation of the first multi-threaded symbolic CSRL model checker which is based on the developed technique and available in the tool MARCIE. An experimental comparison with the probabilistic model checker PRISM for a large number of experiments proves empirically the efficiency of the approach and its implementation, especially when investigating biological models. N2 - Die vorliegende Dissertation betrachtet die effiziente Analyse, im Besonderen Modelchecking, von beschränkten stochastischen Petrinetzen (SPN), die um Rewardstrukturen angereichert werden können. Ein SPN induziert eine Zeit-kontinuierliche Markov Kette (CTMC). Eine Rewardstruktur assoziiert zu jedem Zustand einen Reward und definiert ein Markov Reward Modell (MRM). Die Kontinuierliche Stochastische Reward Logik (CSRL) erlaubt es, sehr spezielle Eigenschaften für CTMCs und MRMs zu definieren, die von einem Modelchecker automatisch überprüft werden können. CSRL Modelchecking kann aufbauend auf etablierten numerischen Analysetechniken für CTMCs realisiert werden, die auf der Multiplikation einer Matrix mit einem Vektor basieren. Da diese Techniken eine Matrix und einen Vektor in der Größe der Menge der erreichbaren Zustände berücksichtigen, ist es jedoch schwierig mir dem Phänomen der Zustandsraumexplosion umzugehen. Verschiedene Ansätze, wie die Verwendung Multi-terminaler Entscheidungsdiagramme (MTDD) oder Kronecker-Produkten zur Darstellung der Matrix, wurden bereits untersucht. Oftmals erlauben diese die Implementierung effizienter CTMC Analyse und sind in einer Reihe von Werkzeugen verfügbar. Als eine Alternative zu diesen etablierten Techniken entwickle ich die Idee einer "on-the-fly" Berechnung der Matrixeinträge, unter Verwendung einer symbolischen Darstellung des Zustandsraums, weiter. Die Menge der Zustandsübergänge, die die Matrix definieren, wird durch das Feuern der Transitionen des Petrinetzes in allen erreichbaren Zuständen aufgezählt. Die Menge der erreichbaren Zustände wird mittels Intervall-Entscheidungsdiagrammen (IDD) kodiert. Weiter, diskutiere ich wesentliche Aspekte der Implementierung des ersten parallelisierten symbolischen CSRL Modelcheckers, der auf der entwickelten Technik basiert und Teil des Werkzeugs MARCIE ist. Ein experimenteller Vergleich mit dem probabilistischen Modelchecker PRISM für eine große Anzahl von Experimenten zeigt empirisch die Effizienz dieses Ansatzes und seiner Implementierung, insbesondere bei der Betrachtung biologischer Modelle. KW - Stochastic Petri nets KW - Continuous-time Markov Chains KW - Model Checking KW - Interval Decision Diagrams KW - Continuous Stochastic Reward Logic KW - Stochastische Petrinetze KW - Zeit-kontinuierliche Markovketten KW - Intervalentscheidungsdiagramme KW - Modelchecking KW - Kontinuierliche Stochastiche Reward Logik KW - Stochstisches Petri-Netz KW - Markov-Kette KW - Programmverifikation Y1 - 2013 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus4-30560 ER - TY - THES A1 - Tovchigrechko, Alexey T1 - Efficient symbolic analysis of bounded Petri nets using Interval decision diagrams T1 - Effiziente symbolische Analyse von beschränkten Petrinetzen mit Hilfe von Interval decision diagrams N2 - Der Schwerpunkt dieser Arbeit liegt bei verschiedenen Techniken, die Effizienz der symbolischen Petrinetzanalyse steigern können. Reduced ordered interval decision diagrams (ROIDDs) werden eingesetzt um Zustandsmengen von k-beschränkten Netzen zu codieren. Wir beschreiben Implementierung eines ROIDD-Packetes und spezielle ROIDD-Operationen, die in symbolischen Algorithmen verwendet werden. Wir untersuchen dann wie Effizienz der symbolischen Erreichbarkeitsanalyse verbessert werden kann und präsentieren einen neuen Saturation-Ansatz, der Strukturen von ROIDDs und k-beschränkten P/T-Netzen ausnutzt. Der Ansatz erlaubt Diagrammgrößen kleiner zu halten und kann Effizienz der symbolischen Analyse drastisch steigern. Saturation-basierte Techniken werden bei den Aufzählungen von stark zusammenhängenden Komponenten und Modelchecking eingesetzt. Implementierung von symbolischen Modelcheckers für k-beschränkte P/T-Netzte wird beschrieben. Wir betrachten CTL- und einen neuartigen LTL-Modelchecker. Eine Reihe von Techniken zur Effizienzsteigerung der Implementierung wird betrachtet. N2 - The research in this thesis focuses on different techniques which can improve efficiency of the symbolic analysis of Petri nets. Reduced ordered interval decision diagrams (ROIDDs) are employed to encode sets of states of k-bounded nets. We discuss implementation of an ROIDD package and special ROIDD operations needed in symbolic algorithms. We study then how to improve efficiency of the reachability analysis and propose a new saturation approach, which exploits the structure of ROIDDs and the structure of k-bounded P/T nets. It manages to keep sizes of intermediate diagrams smaller than other approaches and can drastically improve efficiency of the symbolic analysis. Saturation techniques are applied in the enumeration of strongly connected components and in model checking. Implementation of symbolic model checkers for k-bounded P/T nets are discussed. We consider CTL and a novel LTL model checker. A number of techniques to improve efficiency of the implementation are considered. KW - Petri-Netz KW - Model Checking KW - Petrinetze KW - Symbolische Analyse KW - Entscheidungsdiagramme KW - Model Checking KW - Petri nets KW - Symbolic analysis KW - Decision diagrams KW - Model checking Y1 - 2009 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus-10294 ER - TY - THES A1 - Deussen, Peter H. T1 - Analyse verteilter Systeme mit Hilfe von Prozeßautomaten N2 - Diese Arbeit behandelt einen Ansatz zur Verifikation verteilter Systeme. Zur Beschreibung des Verhaltens solcher Systeme verwenden wir die sog. Semiwörter, die eine spezielle Form von pomsets darstellen, sowie Mazurkiewiczspuren. Wir weisen nach, daß jedes nebenläufige System (d. h. ein System, für dessen Aktionen eine Unabhängigkeitsrelation angegeben werden kann) als verteiltes System aufgefaßt werden kann. Wir beschreiben eine endliche Repräsentation des Verhaltens nebenläufiger und verteilter Systeme, die auf dem Begriff des Prozeßautomaten beruht, und geben Algorithmen zur Konstruktion derartiger Prozeßautomaten an. Schließlich definieren wir die verteilte, agentenbasierte temporale Logik DCTL. Die Beschreibung eines Modelcheckers für diese Logik, der auf Prozeßautomaten operiert, schließt die Arbeit ab. N2 - This thesis addresses the verification of distributed systems. The description of the behaviour of distributed systems is done by so-called semi words. Semi words are a dedicated type of pomsets. Also, Mazurkiewicz traces are used as a behavioural description. We will prove that every concurrent system (i. e. a system for that an independence relation can be defined on system actions) can be considered as a distributed system. We describe a finite representation of the behaviour of concurrent and distributed systems based on the notion of process automata. We define algorithms for the construction of process automata. Finally, we describe the distributed, agent based temporal logic DCTL. A model checking algorithm for DCTL is given. This model checker operates on process automata. KW - Verteiltes System KW - Verifikation KW - Transitionssystem KW - Nebenläufigkeit KW - Halbordnung KW - Spurtheorie KW - Verteiltes System KW - Prozeßautomat KW - Modellchecking KW - Verifikation KW - Petri-Netz Y1 - 2001 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-000000275 ER - TY - THES A1 - Herajy, Mostafa T1 - Computational steering of multi-scale biochemical networks T1 - Computational Steering von biochemischen Netzwerken mit unterschiedlicher Skalierung N2 - Computational Steering ist eine interaktive Fernsteuerung von Applikationen mit langer Laufzeit. Der Nutzer kann sie einsetzen, um Paramater "on-the-fly" einzustellen. Die stochastische und hybride Simulation von biochemischem Netzwerk ist sehr rechenintensiv. Derart aufwendige Berechnungen erfordern interaktive Techniken, die es Nutzern ermöglichen, unterschiedliche Ausführungen während der Berechung zu testen. Durch die rasant fortschreitende Entwicklung der rechnergestützten Modellierung und Simulation biochemischer Netzwerke besteht zunehmender Bedarf, Modelle, in denen Substanzen und Reaktionen unterschiedlicher Skalierung (multi-scale models) auftreten, zu verwalten. Dabei sind Petrinetze von besonderer Bedeutung, da sie eine sehr intuitive visuelle Darstellung von Reaktionsnetzwerken erlauben. Die vorliegende Arbeit liefert folgenden Beitrag: Zunächst werden verallgemeinerte hybride Petrinetze (GHPNbio) und deren Simulation vorgestellt, um sogenannte "steife" (engl. stiff) biochemische Netzwerke zu modellieren und zu simulieren. Schnelle Reaktionen werden dabei kontinuierlich behandelt, langsame Reaktionen dagegen werden stochastisch behandelt. Durch die Kombination der Eigenschaft von kontinuierlichen Petrinetzen (CPN) und erweiterten stochastischen Petrinetzen (XSPN) bieten GHPNbio ein hohes Maß an Ausdruckstärke hinsichtlich Modellierung und Simulation. Die Zuordnung der Transitionen zu kontinuierlichen oder stochastischen (Paritionierung) kann dabei sowohl statisch als auch dynamisch während der Simulation vorgenommen werden. Darüber hinaus wird ein neues Framework vorgestellt, das Petrinetze und Computational Steering zum Zweck der Darstellung und interaktiven Simulation biochemischer Netzwerke zusammenfährt. Die wesentlichen Besonderheiten sind: die enge Kopplung zwischen Simulation und Visualisierung, die verteilte; kooperative; und die interaktive Simulation und die intuitive Repräsentation biochemischer Netze. Zusammen stellen verallgemeinerte hybride Petrinetze und Computational Steering für Systembiologen ein nützliches Werkzeug dar, das helfen kann, komplexe Zusammenhänge auf Systemebene zu verstehen. GHPNbio können dazu verwendet werden, die Simulation biochemischer Netze ohne Genauigkeitsverlust zu beschleunigen. Computational Steering erlaubt es Benutzern mit unterschiedlichem fachlichem Hintergrund biochemische Modelle gemeinsam zu bearbeiten und zu simulieren. Das vorgeschlagene Framework wurde in unserem Modellierungswerkzeug Snoopy implementiert. N2 - Computational steering is an interactive remote control of a long running application. The user can adopt it to adjust the simulation parameters on the fly. Correspondingly, simulation of large scale biochemical networks is computationally expensive, particularly stochastic and hybrid simulation. Such extremely intensive computations necessitate an interactive mechanism to permit users to try different paths and ask simultaneously "what-if" questions while the simulation is in progress. Furthermore, with the progress of computational modelling and the simulation of biochemical networks, there is a need to manage multi-scale models, which may contain species or reactions at different scales (called also stiff systems). In this context, Petri nets are of considerable importance in the modelling and analysis of biochemical networks, since they provide an intuitive visual representation of reaction networks. The contributions of this thesis are twofold: firstly, we introduce the definition and present simulation algorithms of Generalised Hybrid Petri Nets (GHPNbio) to represent and simulate stiff biochemical networks where fast reactions are represented and simulated continuously, while slow reactions are carried out stochastically. GHPNbio provide rich modelling and simulation functionalities by combining all features of Continuous Petri Nets (CPN) and Extended Stochastic Petri Nets (XSPN), including three types of deterministic transitions. Moreover, the partitioning of the reaction networks can either be done off-line before the simulation starts or on-line while the simulation is in progress. Secondly, we introduce a novel framework which combines Petri nets and computational steering for the representation and interactive simulation of biochemical networks. The main merits of the framework proposed in this thesis are: the tight coupling of simulation and visualisation, distributed; collaborative; and interactive simulation, and intuitive representation of biochemical networks by means of Petri nets. Generalised hybrid Petri nets and computational steering will together provide an invaluable tool for systems biologists to help them to obtain a deeper system level understanding. GHPNbio speed up the simulation and simultaneously preserve accuracy, while computational steering enables users of different background to share, collaborate and interactively simulate biochemical models. Finally, the implementation of the proposed framework is given as part of Snoopy - a tool to design and animate/simulate hierarchical graphs, among them qualitative, stochastic, continuous and hybrid Petri nets. KW - Biochemie KW - Systemmodell KW - Hybrides System KW - Petri-Netz KW - Systembiologie KW - Computational Steering KW - Interaktive Simulation KW - Verallgemeinerte hybride Petrinetze KW - Hybride Modelle biochemischer Netze KW - Systems biology KW - Computational Steering KW - Interactive simulation KW - Generalised Hybrid Petri Nets KW - Hybrid modelling of biochemical networks Y1 - 2013 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus-27255 ER - TY - THES A1 - Spranger, Jochen T1 - Symbolische LTL-Verifikation von Petrinetzen N2 - Diese Arbeit widmet sich der Verifikation nebenläufiger Systeme unter Verwendung von Modelcheckingverfahren. Es wurden Modelcheckingverfahren betrachtet und entwickelt, welche die drei Gebiete: Petrinetze als Modellierungssprache, linear-time temporale Logik zur Spezifikation von Systemeigenschaften und binäre Entscheidungsgraphen zur Repräsentation großer Zustandsmengen verbinden. Bei der Entwicklung von Modelcheckingverfahren wurde darauf geachtet, dass durch die Kombination der einzelnen Gebiete deren Vorteile erhalten bleiben und die sich zwischen den Gebieten ergebendnen Synergien ausgenutzt werden. Den wesentlichen innovativen Teil der Arbeit stellt die Entwicklung eines LTL-Modelcheckingverfahrens dar, welches eine symbolische Repräsentierung der Zustände mit einem on-the-fly Verifikationsverfahren verbindet und dabei eine zeitliche Komplexität der klassischen LTL-Modelcheckingverfahren erreicht. N2 - This thesis is devoted to studying the problem of verifying parallel systems using a model checking approach. We have looked at and developed model checking approaches, which combine the three topics: Petri nets as a modelling language, linear-time temporal logic to capture system properties, and binary decision diagrams to represent huge state spaces. During the development of the model checking approaches we especially have focused on keeping the advantages of the different areas and on achieving benefits by combining them.The major contribution of the thesis is the development of a LTL-based model checking approach, which combines the symbolic representation of reachable states with an on-the-fly model checking approach by having the same time complexity of the classical LTL-based model checking approaches. KW - Komplexes System ; Nebenläufigkeit KW - Petri-Netz KW - Spezifikationssprache KW - Model checking KW - Temporale Logik KW - Nebenläufiges System KW - Verifikation KW - Modelchecking KW - Petrinetz KW - Stelle/Transitionsnetz Y1 - 2001 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-000000179 ER - TY - THES A1 - Assaf, George T1 - Fuzzy coloured Petri nets for modelling biological systems with uncertain kinetic parameters T1 - Fuzzy-farbige Petri-Netze für die Modellierung biologischer Systeme mit unsicheren kinetischen Parametern N2 - Over the last twenty years, Petri nets have been increasingly adopted for modelling and simulating biological systems, as they offer an intuitive and graphical approach for this purpose. Their usability convenience comes from the fact that they offer many types of elements to describe systems in a qualitative and quantitative way. Coloured Petri nets are particularly useful to model systems with repeated components in a compact fashion. Our tool Snoopy for modelling and simulating Petri nets is one of the most well-known tools supporting a family of related Petri net classes comprising stochastic, continuous and hybrid Petri nets, and covering uncoloured and coloured Petri nets alike. However, kinetic information of a biological system, i.e. kinetic parameters may be uncertain, due to many reasons, e.g. environmental factors. Besides, coloured Petri nets as they were previously supported in Snoopy suffered from some inconsistencies. Due to these inconsistencies, exploring the model behaviour using different sizes (scaleability) was not feasible. Both challenges call for a new and more powerful approach integrating the modelling of uncertainties together with modelling features supporting repeated structures in a compact and scalable way. This thesis comprises two major contributions: Firstly, we introduce the definition and present the simulation algorithm for both uncoloured and coloured fuzzy Petri nets, by extending the existing quantitative uncoloured and coloured Petri nets in Snoopy. This includes discretising the uncertain kinetic parameters to crisp values by using sampling strategies. Secondly, we harmonise coloured Petri nets in Snoopy with their uncoloured counterparts and we extend the Snoopy’s coloured Petri nets by all the features, which are supported by the coloured abstract net description language - an exchange format of coloured Petri nets in our PetriNuts tool family. By performing fuzzy simulation, one can obtain two kinds of output: fuzzy bands of each output variable and their corresponding timed-membership functions. Each fuzzy band describes the uncertainties associated with the input, whereas membership functions give more accurate information about the associated uncertainties. The most important features that we obtain by harmonising coloured Petri nets are to develop scaleable models, by defining scaling factors as constants and unifying the usage of coloured Petri nets with the other tools in our PetriNuts tool family. N2 - In den letzten zwanzig Jahren wurden Petri-Netze zunehmend für die Modellierung und Simulation von biologischen Systemen eingesetzt. Sie bieten dafür sowohl eine qualitative als auch quantitative Modellierungsmethode an. Farbige Petri-Netze sind nützlich für die Modellierung von Systemen mit sich wiederholenden Komponenten. Snoopy ist eines der bekanntesten Werkzeuge, das eine Familie von Petri-Netzen unterstützt, darunter sowohl ungefärbte als auch gefärbte stochastische, kontinuierliche und hybride Petri-Netze. In dieser Dissertation werden zwei Themen behandelt. Einerseits können Biologische Systeme aus vielen Gründen unbestimmt sein, zum Beispiel aus Umweltgründen, anderereseits hatten farbige Petri-Netze in Snoopy Inkonsistenzen, die den Bau skalierbarer Modelle verhindern. Die Ergebnisse der Fuzzy-Simulation sind sowohl das Fuzzy-Band jeder interessierenden Variablen als auch zeitliche Zugehörigkeitsfunktionen für jede Variable, damit man die Unsicherheiten erforschen kann, die mit der Eingabe verbunden sind. Durch die Harmonisierung von farbigen Petri-Netzen können wir skalierbare Modelle konstruieren und dann das Verhalten des Modells mit verschiedenen Größen des vorliegenden Modells untersuchen. KW - Uncertain biological systems KW - Petri nets KW - Fuzzy logic KW - Colouring fuzziness KW - Software harmonisation KW - Unbestimmte Systembiologie KW - Modellierung KW - Petri-Netze KW - Software Hamonisierung KW - Simulation KW - Gefärbtes Petri-Netz KW - Systembiologie KW - Fuzzy-Logik Y1 - 2021 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus4-58516 ER - TY - THES A1 - Liu, Fei T1 - Colored Petri Nets for systems biology T1 - Gefärbte Petri-Netze für die Systembiologie N2 - Modeling plays a crucial role in Systems Biology in order to provide a system-level understanding of biological systems. With the rapid development of systems biology, modeling of biological systems has shifted from single scales to multiple scales. This introduces a series of challenges that should be addressed, e.g. repetition of components such as genes and cells, variation of components, or hierarchical organization of components. Traditional modeling approaches, e.g. Petri nets, cannot afford to cope with these challenges, which, however, can be tackled using colored Petri nets. This thesis aims to present a technology based on colored Petri nets and associated techniques to address challenges introduced by multiscale modeling in systems biology and to implement them in our modeling tool, Snoopy. To this aim, we present a colored Petri net framework for systems biology, which relates three modeling paradigms: colored qualitative Petri net (QPNC), colored stochastic Petri net (SPNC) and colored continuous Petri net (CPNC). Using this framework, we can model and analyze a biological system from three different perspectives: qualitative, stochastic and continuous by converting them into each other. We implement this framework in our modeling tool, Snoopy, and therefore in this thesis we explore three key problems concerning the implementation of colored Petri nets. For animating/simulating colored Petri nets, we present an efficient algorithm for the computation of enabled transition instances. In order to utilize the analysis techniques of Petri nets we present an efficient unfolding algorithm for large-scale colored Petri nets. In addition, we discuss three special cases for automatic folding (colorizing): colorizing T-invariants, master nets and twin nets in order to reduce the amount of work for folding Petri nets. Petri nets offer a large variety of analysis techniques ranging from informal techniques, e.g. animation/simulation to formal techniques, e.g. model checking. We summarize those analysis techniques that can be used for colored Petri nets, e.g. structural analysis, numerical and simulative model checking from the application point of view. We discuss some scenarios to illustrate the potential capability of colored Petri nets to cope with challenges in systems biology. Moreover, we apply our colored Petri net technology and techniques to three case studies, C. elegans vulval development, coupled Ca2+ channels and membrane systems. These case studies not only demonstrate how to use the colored Petri net framework and related analysis techniques for modeling and analyzing biological systems, but also show how to address the challenges of systems biology. N2 - Die Modellierung ist für die Systembiologie von zentraler Bedeutung, um biologische Systeme ganzheitlich auf einer Systemebene zu verstehen. Mit der rasanten Entwicklung der Systembiologie hat sich die Modellierung biologischer Systeme von single-skalen zu multi-skalen Systemen verschoben. Dies führt zu einer Reihe von Herausforderungen, die bewältigt werden müssen, unter anderem die Modellierung der Vervielfältigung, Variation und hierarchischen Organisation von Komponenten, z. B. Gene und Zellen. Traditionelle Modellierungsansätze, wie z. B. Petri-Netze, sind diesen Herausforderungen nicht gewachsen; sie können jedoch mit gefärbten Petri-Netzen in Angriff genommen werden. Das Ziel dieser Arbeit besteht in der Einführung einer Technologie, die auf gefärbten Petri-Netzen und zugehörigen Techniken beruht, um den Herausforderungen in der Systembiologie durch Multiskale-Modellierung zu begegnen, und deren Implementierung in unserem Modellierungswerkzeug Snoopy. Für diesen Zweck präsentieren wir für die Systembiologie ein Framework, das auf gefärbten Petri-Netzen beruht und drei Modellierungsparadigmen umfasst: gefärbte qualitative Petri-Netze (QPNC), gefärbte stochastische Petri-Netze (SPNC) und gefärbte kontinuierliche Petri-Netze (CPNC). Mit diesem Framework können wir ein biologisches System aus drei Perspektiven modellieren und analysieren: qualitativ, stochastisch und kontinuierlich, unterstützt durch deren Umwandelbarkeit untereinander. Wir implementieren dieses Framework in unserem Modellierungswerkzeug Snoopy und untersuchen dazu in der vorliegenden Arbeit drei wesentliche Probleme bei der Umsetzung der gefärbten Petri-Netze. Zur Animation/Simulation gefärbter Petri-Netze stellen wir einen effizienten Algorithmus zur Berechnung von schaltfähigen Transitionsinstanzen vor. Um die Analyse-Techniken von Petri-Netzen zu nutzen, stellen wir einen effizienten Algorithmus zur Entfaltung sehr großer gefärbter Petri-Netze vor. Um den Aufwand für die Färbung von Petri-Netzen zu reduzieren, diskutieren wir außerdem drei Sonderfälle für die automatische Faltung (Färbung): Färbung von T-Invarianten, von Master-Netzen sowie von Twin-Netzen. Petri-Netze bieten eine große Vielfalt von Analysetechniken an, die von der informellen Analyse, z. B. Animation/Simulation, bis zu formalen Techniken, z. B. Modelchecking, reichen. Wir geben aus Anwendersicht einen Überblick über die Analysetechniken, die für gefärbte Petri-Netze verwendet werden können, z. B. Strukturanalyse sowie analytisches und simulatives Modelchecking. Wir diskutieren einige Szenarien, in denen gefärbte Petri-Netze weiterhelfen, um ihr Potential bei der Bewältigung der Herausforderungen in der Systembiologie zu illustrieren. Um die Anwendbarkeit unseres Ansatzes zu demonstrieren, wenden wir unsere Methode der gefärbten Petri-Netze auf drei Fallstudien an, C. Elegans, gekoppelte Ca2+-Kanäle und Membran-Systeme. Diese Fallstudien zeigen nicht nur, wie das Framework der gefärbten Petri-Netze und der zugehörigen Analyse-Techniken für die Modellierung und Analyse praktischer biologischer Systeme genutzt werden kann, sondern zeigen auch, wie man den Herausforderungen der Systembiologie begegnen kann. KW - Petri-Netz KW - Datenstruktur KW - Systembiologie KW - Gefärbte Petri-Netze KW - Stochastische Petri-Netze KW - Kontinuierliche Petri-Netze KW - Analyse-Techniken KW - Systems Biology KW - Colored Petri Nets KW - Stochastic Petri Nets KW - Continuous Petri Nets KW - Analysis techniques Y1 - 2012 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus-23656 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 -