Refine
Document Type
- Doctoral thesis (2)
Has Fulltext
- yes (2)
Is part of the Bibliography
- no (2)
Language
- English (2)
Keywords
- Markov-Kette (2) (remove)
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.
This work focusses on applications of classical probability theory, especially point process theory, to quantum stochastics. We consider a class of quantum Markov chains in the sense of ACCARDI on the basis of beam splitters and generalized splitting procedures. Time evolutions of boson systems described by these procedures are constructed. Furthermore, the following questions are discussed: Which initial states allow an explicit description of later states, especially of the corresponding position distribution? Which states are invariant under the considered dynamics? For which initial states one obtains convergence to an invariant state? The considered boson systems are described using a representation of the symmetric Fock space as £2-space with a not necessarily atomless measure. So, the case of bosons on a lattice is also included.