@phdthesis{Chodak2021, author = {Chodak, Jacek}, title = {Spike - a tool for reproducible simulation experiments}, doi = {10.26127/BTUOpen-5850}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-58509}, school = {BTU Cottbus - Senftenberg}, year = {2021}, abstract = {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.}, subject = {Petri nets; Parallel simulation; Parameter scanning; Reproducibility; Simulation of adaptive models; Petri Netze; Parallelsimulation; Parameterscannen; Reproduzierbarkeit; Simulation von adaptiven Modellen; Gef{\"a}rbtes Petri-Netz; Simulation; Reproduzierbarkeit}, language = {en} } @phdthesis{Schwarick2013, author = {Schwarick, Martin}, title = {Symbolic on-the-fly analysis of stochastic Petri nets}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-30560}, school = {BTU Cottbus - Senftenberg}, year = {2013}, abstract = {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.}, subject = {Stochastic Petri nets; Continuous-time Markov Chains; Model Checking; Interval Decision Diagrams; Continuous Stochastic Reward Logic; Stochastische Petrinetze; Zeit-kontinuierliche Markovketten; Intervalentscheidungsdiagramme; Modelchecking; Kontinuierliche Stochastiche Reward Logik; Stochstisches Petri-Netz; Markov-Kette; Programmverifikation}, language = {en} } @phdthesis{Tovchigrechko2009, author = {Tovchigrechko, Alexey}, title = {Efficient symbolic analysis of bounded Petri nets using Interval decision diagrams}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-10294}, school = {BTU Cottbus - Senftenberg}, year = {2009}, abstract = {Der Schwerpunkt dieser Arbeit liegt bei verschiedenen Techniken, die Effizienz der symbolischen Petrinetzanalyse steigern k{\"o}nnen. Reduced ordered interval decision diagrams (ROIDDs) werden eingesetzt um Zustandsmengen von k-beschr{\"a}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{\"a}sentieren einen neuen Saturation-Ansatz, der Strukturen von ROIDDs und k-beschr{\"a}nkten P/T-Netzen ausnutzt. Der Ansatz erlaubt Diagrammgr{\"o}ßen kleiner zu halten und kann Effizienz der symbolischen Analyse drastisch steigern. Saturation-basierte Techniken werden bei den Aufz{\"a}hlungen von stark zusammenh{\"a}ngenden Komponenten und Modelchecking eingesetzt. Implementierung von symbolischen Modelcheckers f{\"u}r k-beschr{\"a}nkte P/T-Netzte wird beschrieben. Wir betrachten CTL- und einen neuartigen LTL-Modelchecker. Eine Reihe von Techniken zur Effizienzsteigerung der Implementierung wird betrachtet.}, subject = {Petri-Netz; Model Checking; Petrinetze; Symbolische Analyse; Entscheidungsdiagramme; Model Checking; Petri nets; Symbolic analysis; Decision diagrams; Model checking}, language = {en} } @phdthesis{Deussen2001, author = {Deussen, Peter H.}, title = {Analyse verteilter Systeme mit Hilfe von Prozeßautomaten}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-000000275}, school = {BTU Cottbus - Senftenberg}, year = {2001}, abstract = {Diese Arbeit behandelt einen Ansatz zur Verifikation verteilter Systeme. Zur Beschreibung des Verhaltens solcher Systeme verwenden wir die sog. Semiw{\"o}rter, die eine spezielle Form von pomsets darstellen, sowie Mazurkiewiczspuren. Wir weisen nach, daß jedes nebenl{\"a}ufige System (d. h. ein System, f{\"u}r dessen Aktionen eine Unabh{\"a}ngigkeitsrelation angegeben werden kann) als verteiltes System aufgefaßt werden kann. Wir beschreiben eine endliche Repr{\"a}sentation des Verhaltens nebenl{\"a}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{\"u}r diese Logik, der auf Prozeßautomaten operiert, schließt die Arbeit ab.}, subject = {Verteiltes System; Verifikation; Transitionssystem; Nebenl{\"a}ufigkeit; Halbordnung; Spurtheorie; Verteiltes System; Prozeßautomat; Modellchecking; Verifikation; Petri-Netz}, language = {de} } @phdthesis{Herajy2013, author = {Herajy, Mostafa}, title = {Computational steering of multi-scale biochemical networks}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-27255}, school = {BTU Cottbus - Senftenberg}, year = {2013}, abstract = {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{\"o}glichen, unterschiedliche Ausf{\"u}hrungen w{\"a}hrend der Berechung zu testen. Durch die rasant fortschreitende Entwicklung der rechnergest{\"u}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{\"a}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{\"a}rke hinsichtlich Modellierung und Simulation. Die Zuordnung der Transitionen zu kontinuierlichen oder stochastischen (Paritionierung) kann dabei sowohl statisch als auch dynamisch w{\"a}hrend der Simulation vorgenommen werden. Dar{\"u}ber hinaus wird ein neues Framework vorgestellt, das Petrinetze und Computational Steering zum Zweck der Darstellung und interaktiven Simulation biochemischer Netzwerke zusammenf{\"a}hrt. Die wesentlichen Besonderheiten sind: die enge Kopplung zwischen Simulation und Visualisierung, die verteilte; kooperative; und die interaktive Simulation und die intuitive Repr{\"a}sentation biochemischer Netze. Zusammen stellen verallgemeinerte hybride Petrinetze und Computational Steering f{\"u}r Systembiologen ein n{\"u}tzliches Werkzeug dar, das helfen kann, komplexe Zusammenh{\"a}nge auf Systemebene zu verstehen. GHPNbio k{\"o}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.}, subject = {Biochemie; Systemmodell; Hybrides System; Petri-Netz; Systembiologie; Computational Steering; Interaktive Simulation; Verallgemeinerte hybride Petrinetze; Hybride Modelle biochemischer Netze; Systems biology; Computational Steering; Interactive simulation; Generalised Hybrid Petri Nets; Hybrid modelling of biochemical networks}, language = {en} } @phdthesis{Spranger2001, author = {Spranger, Jochen}, title = {Symbolische LTL-Verifikation von Petrinetzen}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-000000179}, school = {BTU Cottbus - Senftenberg}, year = {2001}, abstract = {Diese Arbeit widmet sich der Verifikation nebenl{\"a}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{\"a}re Entscheidungsgraphen zur Repr{\"a}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{\"a}sentierung der Zust{\"a}nde mit einem on-the-fly Verifikationsverfahren verbindet und dabei eine zeitliche Komplexit{\"a}t der klassischen LTL-Modelcheckingverfahren erreicht.}, subject = {Komplexes System ; Nebenl{\"a}ufigkeit; Petri-Netz; Spezifikationssprache; Model checking; Temporale Logik; Nebenl{\"a}ufiges System; Verifikation; Modelchecking; Petrinetz; Stelle/Transitionsnetz}, language = {de} } @phdthesis{Assaf2021, author = {Assaf, George}, title = {Fuzzy coloured Petri nets for modelling biological systems with uncertain kinetic parameters}, doi = {10.26127/BTUOpen-5851}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-58516}, school = {BTU Cottbus - Senftenberg}, year = {2021}, abstract = {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.}, subject = {Uncertain biological systems; Petri nets; Fuzzy logic; Colouring fuzziness; Software harmonisation; Unbestimmte Systembiologie; Modellierung; Petri-Netze; Software Hamonisierung; Simulation; Gef{\"a}rbtes Petri-Netz; Systembiologie; Fuzzy-Logik}, language = {en} } @phdthesis{Liu2012, author = {Liu, Fei}, title = {Colored Petri Nets for systems biology}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-23656}, school = {BTU Cottbus - Senftenberg}, year = {2012}, abstract = {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.}, subject = {Petri-Netz; Datenstruktur; Systembiologie; Gef{\"a}rbte Petri-Netze; Stochastische Petri-Netze; Kontinuierliche Petri-Netze; Analyse-Techniken; Systems Biology; Colored Petri Nets; Stochastic Petri Nets; Continuous Petri Nets; Analysis techniques}, language = {en} } @phdthesis{Rohr2016, author = {Rohr, Christian}, title = {Simulative analysis of coloured extended stochastic Petri nets}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus4-41476}, school = {BTU Cottbus - Senftenberg}, year = {2016}, abstract = {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.}, subject = {Coloured extended Stochastic Petri Nets; Stochastic simulation; Delta-leaping; Simulative model checking; Gef{\"a}rbte erweiterte stochastische Petri Netze; Stochastische Simulation; Delta-leaping; Simulatives Modelchecking; Stochastisches Modell; Gef{\"a}rbtes Petri-Netz; Model Checking}, language = {en} }