206
2 mars 2017 - 15h30
Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement
par Nicolas Basset de Université Libre de Bruxelles
Abstract: (joint work with B. Barbot, B. Beunardeau and M. Kwiatkowska)
In this talk, I will present Monte Carlo model checking techniques to evaluate quantitative properties of timed languages. Our approach is based on uniform random sampling of behaviours, the uniformity being defined with respect to volume measure of timed languages previously studied by Asarin, Degorre and me. We implement our algorithms using tools PRISM, SageMath and COSMOS, and demonstrate their usefulness on statistical timed language inclusion measurement in terms of volume.
