Seminaire
Séminaire Analyse et Contrôle des Systèmes
> 28/03/2019 à 14h00

Seminaire
Séminaire Analyse et Contrôle des Systèmes
> 21/03/2019 à 14h00

Seminaire
[1ère demi-journée Pole Calcul LIS] “Logique et Méthodes formels”
> 21/03/2019 à 09h30

Dans le cadre du deuxième cycle des demi-journées du Pole Calcul du LIS, la prochaine sera autour du thème “Logique et Méthodes formels”, organisée le jour *21 Mars 9h30 à 12h30 (Luminy) dans l’Amphi 12 de Luminy.

Les demi-journées seront aussi enregistrés et on les rendra publique les vidéos sur une page dédiée ou sur une chaine youtube (lien à venir).

Les trois intervenants confirmés sont Damien Busatto-Gaston (LIS), Belaid Benhamou (LIS), Jean-Francois Raskin (ULB)

—————————————————————————————

Première demi-journée (Logique et Méthodes formelles) 21 Mars

(45min each + 10 mins questions + 15 min coffe break)

9h30 -> 10h15 — Damien Busatto-Gaston (PhD) , LIS

Titre : Synthesizing robust controllers for Büchi conditions in timed systems.

Abstract :

We solve the robust controller synthesis problem in timed automata with Büchi acceptance conditions. The goal of the controller is to play according to an accepting lasso of the automaton, while resisting to timing perturbations chosen by a competing environment. The talk will introduce classical notions for studying timed automata (regions, zones, constraint graphs) and explain how these can be extended to compute strategies that are resilient to arbitrarily small perturbations. We will also introduce a way to compute the largest perturbation allowed by a given controller. Our techniques are illustrated by the regulation of a train network.

10h25 -> 11h10 — Belaid Benhamou (MCF), LIS

Titre : Programmation logique au sens ASP (Answer Set Programming) : une nouvelle sémantique capturant et étendant celle des modèles stables.

Abstract :

Plusieurs travaux ont été faits pour définir des sémantiques pour les programmes logiques normaux. La plupart de ces sémantiques sont en fait des sémantiques de points fixes. L’idée principale est le calcul de modèles canoniques du programme logique considéré, appelés modèles stables (Gelfond et al. 1988). Dans cette exposé, nous décrivons une nouvelle sémantique pour les programmes logiques normaux. Cette dernière est basée sur une notion d’extensions de formules propositionnelles classiques. Un programme logique est alors codé par un ensemble de clauses de Horn propositionnelles. On prouve que chaque formule consistante (ou programme logique) admet au moins une extension et que, pour chaque modèle stable d’un programme logique, il existe une extension de son codage logique qui l’implique. Certaines extensions (extra-extensions) ne correspondent pas à des modèles stables du programme logique, mais sont intéressantes car elles représentent ici, une extension pour la sémantique des modèles stables. Nous donnons une condition discriminante simple qui permet de reconnaître les extensions « normales » et les distinguer des extra-extensions. Basé sur cette sémantique, nous proposons une nouvelle méthode de recherche de modèles stables pour les programmes logiques. Elle a l'avantage d'utiliser un ensemble de clauses de Horn et travaille à espace constant. Elle évite ainsi, la lourdeur induite par la gestion des boucles, dont souffrent la plupart des solveurs ASP utilisant la complétion de Clark et qui ont des complexités spatiales exponentielles dans le pire des cas. De plus, l'énumération est effectuée sur un ensemble restreint de variables du programme logique. Ce qui réduit en général, la complexité temporelle de l'algorithme. En plus de la recherche de modèles stables, cette méthode pourrait générer une sorte d'extra-modèles stables exprimant ainsi l'extension portée à la sémantique des modèles stables.

11h20 -> 11h35 Coffee break

11h35 -> 12h20 — Raskin Jean-Francois, ULB

Titre : Assume Admissible Synthesis.

Abstract :

In this talk, I will show how the notion of admissibility can be used to provide an elegant solution to the synthesis problem for reactive system where the environment is not completely adversarial or when the system is composed of several components. In particular, I will introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. Contrary to previous proposals in the literature, the rule « assume admissible » defines sets of solutions which are rectangular. This property leads to solutions which are robust and resilient, and allows one to synthesize strategies separately for each component.

End: 12h30

Conference
Big Data à la Russe
> 07/03/2019 à 00h00