ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 15:00 - 15:30 at SUN I - Hybrid and Stochastic Systems Chair(s): Kim Larsen

This paper considers large families of Markov chains (MCs) that are defined over a set of parameters with finite discrete domains. Such families occur in software product lines, planning under partial observability, and sketching of probabilistic programs. Simple questions, like `does at least one family member satisfy a property?’, are NP-hard. We tackle two problems: distinguish family members that satisfy a given quantitative property from those that do not, and determine the family member that satisfies the property optimally, i.e., with the highest probability or reward. We show that combining two well-known techniques, MDP model checking and abstraction refinement, mitigates the computational complexity. Experiments on a broad set of benchmarks show that in many situations, our approach is able to handle families of millions of MCs, providing superior scalability compared to existing solutions.

Wed 10 Apr

tacas-2019-papers
14:00 - 16:00: TACAS 2019 - Hybrid and Stochastic Systems at SUN I
Chair(s): Kim LarsenAalborg University
tacas-2019-papers14:00 - 14:30
Talk
Satoshi Kura, Natsuki Urabe, Ichiro HasuoNational Institute of Informatics
Link to publication
tacas-2019-papers14:30 - 15:00
Talk
Link to publication
tacas-2019-papers15:00 - 15:30
Talk
Milan CeskaBrno University of Technology , Nils JansenRWTH Aachen University, Sebastian JungesRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University
Link to publication
tacas-2019-papers15:30 - 16:00
Talk
Link to publication