LIPN, CNRS UMR 7030, Université Paris 13, Institut Galilée. B107 Plan du campus L'accès au LIPN depuis les transports se fait par l'entrée nord et est contrôlé. Lorsque vous arrivez, il faut prendre l'escalier en dessous du pont et prendre le premier bâtiment de la passerelle puis traverser la terrasse et la salle de séminaire est en B107 (Bâtiment B, Premier étage).
Abstract : Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches for concurrent systems have recently emerged. This talk presents a new framework allowing to take a significant step beyond available results and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. The approach automatically refines the global alphabet into component alphabets while learning the component models. It is based on the development of a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets. This allows to characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. Based on this theory, a compositional learning algorithm implementing these ideas is presented, where learning counterexamples precisely correspond to distribution counterexamples under well-defined conditions. Finally, some experiments are presented, showing that in more than 630 subject systems, the implementation of this new algorithm delivers orders of magnitude improvements (up to five orders) in membership queries and in systems with significant concurrency, it also achieves better scalability in the number of equivalence queries.
Abstract : In this talk, we will tackle the problem of computing guaranteed controllers for switched dynamical systems. We have designed a control procedure inspired by model predictive control. However, instead of relying on a cost function evaluated by simulating the original system, we first build a formal discrete probabilistic approximation of the original system, and the cost function is evaluated using this approximation. This approximate model takes the form of a Markov chain, which we represent compactly as a dynamic Bayesian network (DBN). The inference algorithms available for DBNs enable us to efficiently evaluate and minimize the approximate cost function. We compute guaranteed controllers thanks to the use of set-based reachability analysis for computing the transition probabilities of the approximate model. Moreover, the search space of the optimization procedure is reduced to the control modes that are guaranteed safe.