@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{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} }