Olav Bunte: Quantitative model checking on probabilistic systems using plmu*+

Event Details

Although most model checking logics focus on proving qualitative properties, with the logic plmu*+ introduced in Mio’s PhD thesis one can check the probability that some behaviour happens. In this work we try to bring this logic to practice. We attempt to find intuitive meaning for plmu*+-formulas with the aim to create guidelines to create meaningful formulas. Also, we give an alternative representation of a plmu*+ model checking problem in form of an equations system and we give an algorithm to extract the solution from this representation, based on the work of Mader. This algorithm will be compared to an approximation algorithm by applying both on a number of use cases.