Seminar 4 July 11:00, 2012
Quantitative Analysis of Markov Automata
Markov automata (MA) are stochastic models in which non-deterministic, probabilistic and timed events co-exists. Hence, they are a combination of interactive Markov chains (IMCs) and probabilistic automata (PAs). Since MAs were introduced recently, the analysis of them is mostly unexplored. In this thesis, we elaborate techniques which allows us to check the reliability and availability of components in MAs. Therefore, we provide on the one hand an algorithm to compute the expected time of reaching a set of goal states. On the other hand we provide an algorithm to compute the long-run average fraction of time spent in a set of goal states. Further, we prove the correctness of our results and show that a stationary deterministic scheduler will be sufficient to solve the non-determinism, with respect to obtain the minimum and maximum values. Moreover, we have a prototypical tool IMCA which supports these algorithms. Moreover, three case studies show the feasibility and scalability of the algorithms.
Markov automata (MA) are stochastic models in which non-deterministic, probabilistic and timed events co-exists. Hence, they are a combination of interactive Markov chains (IMCs) and probabilistic automata (PAs). Since MAs were introduced recently, the analysis of them is mostly unexplored. In this thesis, we elaborate techniques which allows us to check the reliability and availability of components in MAs. Therefore, we provide on the one hand an algorithm to compute the expected time of reaching a set of goal states. On the other hand we provide an algorithm to compute the long-run average fraction of time spent in a set of goal states. Further, we prove the correctness of our results and show that a stationary deterministic scheduler will be sufficient to solve the non-determinism, with respect to obtain the minimum and maximum values. Moreover, we have a prototypical tool IMCA which supports these algorithms. Moreover, three case studies show the feasibility and scalability of the algorithms.
