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 -