LACL, salle P2-131 (Univ. Créteil): comment y aller
Abstract : Monte Carlo model checking introduced by Smolka and Grosu is an approach to analyse non-probabilistic models using sampling and draw conclusions with a given condence interval by applying statistical inference. Though not exhaustive, the method enables verication of complex models, even in cases where the underlying problem is undecidable. I will present a recent work where we develop Monte Carlo model checking techniques to evaluate quantitative properties of timed languages. Our approach is based on uniform random sampling of behaviours, as opposed to isotropic sampling that chooses the next step uniformly at random. The uniformity is defined with respect to volume measure of timed languages previously studied by Asarin, Degorre and I. We improve over this work by employing a zone graph abstraction instead of the region graph abstraction and incorporating uniform sampling within a zone-based Monte Carlo model checking framework. We implement our algorithms using tools PRISM, SageMath and COSMOS, and demonstrate their usefulness on statistical language inclusion measurement in terms of volume.
Abstract : We study the synthesis problem of reactive systems in distributed architectures. The question is to synthesize strategies for some components that we control such that the interaction with the other processes satisfy some specifications. Each process in the distributed system may have partial observation on the global state of the system and has to take decisions based on the local observation. Also, the processes that are not controlled may be hostile or may have their own objectives and play rational. We study the different problems that arise from different combinations of the above possible settings and propose algorithms that avoid complicated constructions as Safra’s construction. For the case of antagonist environment, we provide an efficiently implemented Safraless procedure for specifications given as formulas in the positive fragment of KLTL. Then, for the case of rational environment, we provide tight complexities for different $\omega$-regular objectives under the assumption of perfect information and provide decidability results for the more general setting of imperfect information.