TBA
On monday, at 2pm - UPEC CMC - Room P2-131
December 4, 2023
Timed Automata Verification and Synthesis via Finite Automata Learning
We present algorithms for model checking and controller synthesis of timed automata, seeing a timed automaton model as a parallel composition of a large finite-state machine and a relatively smaller timed automaton, and using compositional reasoning on this composition. We use automata learning algorithms to learn finite automata approximations of the timed automaton component, in order to reduce the problem at hand to finite-state model checking or to finite-state controller synthesis. We present an experimental evaluation of our approach.
November 27, 2023
TBA
TBA
October 16, 2023
Inside and Beyond Decisiveness for Infinite Probabilistic Models
Decisiveness of infinite Markov chains is a key property that allows to compute reachability probabilities up to an arbitrary precision. However such a generic method suffers from two limitations: (1) decisiveness is somewhat related to recurrence of Markov chains and so does not cover transient models and (2) most of the applicable cases of decisiveness require that the transition weights are independent of the current state which forbids a relevant fraction of probabilistic modelings requiring dynamic weights (i.e., also depending on the current state). In this work, we extend this approach in two directions. First we introduce a new property called divergence that somehow complements decisiveness and also leads to a similar computation. Then we study the decidability of these two properties for dynamic probabilistic versions of counter machines, pushdown automata, and Petri nets. Finally, we exhibit some divergent or decisive subclasses of channel systems and Petri nets.
This presentation is based on two papers accepted by CONCUR’23 and by RP’23, and are joint work with Alain Finkel (LMF) and Serge Haddad (LMF).
October 9, 2023
TBA
TBA
October 2, 2023
Génération automatique de code parallèle isochrone
Depuis la stagnation de la fréquence d’horloge des processeurs, l’accroissement de la puissance de calcul a dépendu entièrement de l’accroissement du nombre d’unités de calcul.
Plus que la difficulté algorithmique impliquée par l’écriture de tout programme séquentiel, la programmation parallèle demande au programmeur de gérer de nombreuses unités de calcul, incluant leurs tâches et leurs interactions.
Pour alléger le fardeau du programmeur, cette présentation propose deux approches différentes de génération automatique de code parallèle.
Le modèle parallèle isochrone BSP possède des propriétés intéressantes telles que sa simplicité et son modèle de coût qui en font la cible de notre génération de code parallèle.
Les automates et expressions régulières sont souvent choisis pour modéliser les calculs séquentiels et leurs parallélisation devrait, à long terme, aboutir à de solide fondations pour la génération de code parallèle.
Pour notre approche principale, nous développons la théorie des automates BSP avec leur génération et déterminisation.
Cette théorie est utilisée dans une nouvelle méthode pour la recherche parallèle de motif à l’aide d’expressions régulières.
Notre autre approche propose un langage spécifique au domaine des réseaux de neurones où la composition fonctionnelle d’un petit nombre de primitives facilite le développement, la maintenance et la définition formelle du langage par rapport aux approches existantes.