Filtern
Dokumenttyp
- Buch (1)
- Dissertation (1)
Volltext vorhanden
- ja (2)
Gehört zur Bibliographie
- nein (2)
Erscheinungsjahr
- 2013 (2) (entfernen)
Schlagworte
In diesem Band sammeln wir Beiträge, die zum Anlass einer Tagung am 19.10.2013 an der BTU Cottbus – Senftenberg gehalten und für diese Veröffentlichung von den Referenten ausformuliert wurden. Im Zentrum der Tagung stand die internationale Konvention der ILO 169, welche Rechte indigener Völker definiert, und die Frage, inwieweit diese Konvention und andere Ansätze der (Selbst-)Organisation von Verfügungsrechten an Natur Anregungen für die Ausgestaltung der Selbstverwaltungsrechte der Minderheit der Sorben/Wenden bieten.
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.