Talk: Parameter Synthesis in Probabilistic Model Checking

Wednesday, 29.11.2017, 11:00am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

 

Speaker: Sebastian Junges

 

Model checking is widely applied technique to verify the correctness of hardware and software systems. Among others, it can be used to verify that a system described by a model never gets into a bad state. However, many systems exhibit random failures that cannot be prevented, for example in wireless communication or in the wear of mechanical parts. Here, it might always be possible to get into a bad state, but the relevant question is how likely this is. Probabilistic model checking extends classical model checking to deal with these quantitative aspects. A critical assumption here is that the system model contains fixed probabilities.

In this talk, I briefly sketch the most essential facts about probabilistic model checking and then discuss whether we can assume that probabilities are indeed fixed, and if not, how model checking techniques for variable probabilities may look like.