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