Open Access

Martin Schwarick

• 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 ofThis 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.…
• 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 zurDie 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.…