Reduction Methods for Probabilistic Model Checking

Marcus Größer
Reduction Methods for Probabilistic Model Checking
Phd thesis

KurzfassungAbstract
Model Checking is a fully automatic verification method that has undergone a vast development for almost 30 years now. In contrast to simulation and testing, model checking is a verification technique that explores all possible system states exhaustively and can therefore reveal errors that have not been discovered by testing or simulation. It thus is a prominent verification technique for safety-critical systems. However, exploring the entire state space makes model checking very sensitive to the size of the system to be verified. In this thesis, we address the issue of reduction techniques for probabilistic model checking. Taking probabilities into account in addition to nondeterministic behavior expands the possibilities of modeling certain aspects of the system under consideration. While nondeterministic systems are considered in connection to underspecification, interleaving of several processes and interaction with the specified system from the outside, the probabilities can be exploited to model a certain probability of error or other stochastic behavior both occurring in various real world applications, eg randomized algorithms or communication protocols over faulty media. In this thesis we restrict our investigations to models that are specified by Markov decision processes.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@phdthesis{G2025,
  author = {Marcus Gr{\"{o}}{\ss}er},
  title  = {Reduction Methods for Probabilistic Model Checking},
  year   = {2025}
}