Submitted: April 2016
Abstract
Over the years there were always new algorithms that tried to solve the time bounded reachability problem for continuous-time Markov chains (CTMCs) / continuous time Markov decision processes (CTMDPs). CTMCs are labelled transition systems that take transitions according to some exponential distribution while CTMDPs represent an extension of those in regard to non-determinism. This non-determinism is taken care of by so called schedulers. One of the main topics that has been targeted is the “time bounded reachability” which is the maximum probability to reach a set of goal states within a certain time bound given a class of schedulers. An algorithm called Unif+ has been recently developed to compute this time bounded reachability of CTMDPs. While the correctness of this algorithm up to a certain error has already been proven the termination still needs to be shown. In this Bachelor thesis of mine I will prove that the algorithm Unif+ does indeed terminate.
We will first start off by going through the necessary preliminaries. Here we will discuss the definition of CTMDPs along with all necessary sub-definitions which are based on CTMDPs. In order to properly define CTMDPs we will also have a quick overview into probability theory, i.e. probability measures and then finally we are going to have a look at the algorithm Unif+ itself.
After concluding these preliminaries we can then move forward to the main part of this thesis which is the proof of termination for this algorithm. Since this proof uses several Lemmas where in some cases proofs are still needed we will first be listing all these Lemmas and give the proofs. When all of this footwork is established we will then move on to the main part of the proof where the termination will be proven.