Reliable Software Systems Software Engineering Seminar (WS 2015)

Interval-valued discrete time Markov chains analysis Description Probabilistic model checking is a widely used technique supporting the verification of properties over quantitative measures of a system, including reliability, response time, energy consumption, or operational costs. The use of probabilistic model checking requires to abstract the behavior of a system by means of suitable formal models. Discrete time Markov chains (DTMCs) are essentially finite state automata enhanced with transitions probabilities, i.e. given the current state, the next state is decided according to a probability distribution. Several analysis algorithms have been defined to analyze such models. However, most of these algorithms assume the probability of moving from one state to another to be defined as a numeric value. Nonetheless, due to uncertainties in both the design process and the system execution, it is sometimes hard to characterize the transition probability between two stated by a single numeric value. An viable alternative is to assign to each transition a range of values, instead of a single one. For example, a transition may have a probability of being selected belonging to the interval [.3,.5]. DTMCs whose transition probability are defined only through intervals are called interval-valued DTMCs. Despite their increased expressiveness, the analysis of interval-valued DTMCs is still under study. The goal of this seminar is to assess the state of the art on model checking for interval-values DTMCs and to implement and evaluate novel techniques currently under development at the RSS group. This seminar may optionally be extended to a MS thesis. Prerequisites A basic knowledge of automata, linear algebra, and probability is recommended