Guest Talk: Learning-Based Techniques for the Verification of Partially-Specified MDPs

Thursday, 24.05.2018, 10:15am

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

 

Speaker: Guillermo A. Pérez

 

I will present two learning-based algorithms to solve common verification-related problems in unknown MDPs. That is, in MDPs whose probabilistic transition function and reward function are unknown.
First, I will describe the simplest offline-learning algorithm for aquantitative reachability objective that yields PAC-like guarantees. Then, I will present some of my work on the „never-worse relation“: an optimization that allows to make the previously-described algorithm more efficient in its learning. Second, I will consider more advanced objectives, namely mean-payoff and parity objectives. I will present recent work on a new online-learning algorithm for combinations of the latter objectives. In particular, we will see an online-learning algorithm for mean-payoff objectives whose correctness proof is arguably more accessible to the verification community than that of more classical alternatives.