Les lundis, à partir de 14h - UPEC CMC - Salle P2-131

15 janvier 2024

Model-checking appuyé par des sur et sous-approximations

Yann Thierry-Mieg (LIP6)

L’exposé sera centré sur du model-checking (accessibilité et LTL), avec des stratégies qui mixent des sur-approximations (basées sur SMT) des sous approximations (comme des explorations aléatoires ou dirigée) et des abstractions précises vis à vis de la propriété (comme des réductions structurelles). L’implantation de ces stratégies concrètement pour la vérification de réseaux de Petri permettent à l’outil ITS-Tools de remporter la compétition de model-checking MCC.

8 janvier 2024

Formal verification for quantum programs, challenges and the Qbricks solution

Christophe Chareton (CEA LIST)

While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. We review the induced challenges for an efficient use of formal methods in quantum computing and introduce our solution, Qbricks, and ongoing efforts.

18 décembre 2023

Paramétrisation et analyse de systèmes naturels à l’aide de vérification statistique

Benoît Delahaye (LS2N)

Dans cet exposé, je reviendrai sur un ensemble de travaux récents dont l’objet est la modélisation et l’analyse de systèmes naturels complexes à l’aide (en partie) de model-checking statistique. La particularité des systèmes considérés est qu’ils sont constitués, au moins en partie, de processus continus modélisés par des équations différentielles. Dans un premier temps, je présenterai des résultats permettant de donner des garanties probabilistes sur la vérification statistique de ces systèmes malgré les erreurs introduites lors de l’intégration numérique des équations différentielles, et je présenterai des applications à la paramétrisation de ces modèles et à l’analyse de leur stabilité. Dans un deuxième temps, je présenterai une abstraction de ces systèmes permettant de les combiner avec des processus discrets de contrôle. Finalement, je présenterai brièvement deux cas d’études concrets de paramétrisation de tels modèles : la croissance de la méduse Pelagia Noctiluca en méditerranée et la repousse de parcelles de forêt amazonienne lorsqu’elle sont soumises à des évènements extrêmes.

11 décembre 2023

Computational Content of Set Theory

Richard Matthews (LACL)

The method of realizability was first developed by Kleene and is seen as a way to extract computational content from mathematical proofs via the Curry-Howard Correspondence. The Curry-Howard Correspondence is a way to associate with each mathematical proof a computer program. Then, from a theorem one can extract computational content by analysing the programs associated to the proof of the statement. Traditionally, this method was restricted to producing models which satisfied intuitionistic logic; however it was later extended by Krivine to produce models which satisfy full classical logic and even Zermelo-Fraenkel set theory with choice. In this talk we will discuss Krivine’s method to construct realizability models of ZF and what this reveals about the computational content of set theory with respect to the Curry-Howard Correspondence. We will then present recent results concerning ordinals and cardinals in these realizability models. This is joint work with Laura Fontanella and Guillaume Geoffroy.

4 décembre 2023

Timed Automata Verification and Synthesis via Finite Automata Learning

Ocan Sankur (Irisa)

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.

27 novembre 2023

Learning the Structure of Bayesian Networks using Constraint Programming

George Katsirelos (MIA Paris-Saclay, INRAE)

Bayesian networks are probabilistic graphical models with a wide range of application areas including gene regulatory network inference, risk analysis and image processing. Learning the structure of a Bayesian network (BNSL) from discrete data is known to be an NP-hard task with a superexponential search space of directed acyclic graphs.

In this talk, I will present recent work on solving the BNSL using constraint programming. Building on previous work on solving BNSL with CP and with ILP, we propose new algorithms for handling the difficult acyclicity constraint and the so-called cluster cuts that can be generated from it. We give a new polynomial time algorithm for discovering a subset of all possible cluster cuts, a greedy algorithm for approximately solving the resulting linear program, and a generalised arc consistency algorithm for the acyclicity constraint. These improve performance by orders of magnitude compared to previous CP-based approaches, but scalability is still limited by the fact that the basic decision variables used in this model have domain size Omega(n^log n). We propose a novel representation of domains using decision trees and show that relatively simple operations are sufficient to implement all propagation and bounding algorithms. The combination of the algorithmic techniques and the new representation result in a solver which compares favourably with all competing state-of-the-art approaches.

20 novembre 2023

Stochastic Modeling and Optimization For Power and Performance Control In DVFS Systems

Youssef Ait El Mahjoub (EFREI)

This work addresses the problem of performance-energy trade-off in DVFS (Dynamic Voltage Frequency Scaling) systems. We propose a stochastic hybrid model between hysteresis models and server block models. We provide a closed form for the steady-state distribution probability and we establish a “st” type order to compare the performance measures.

The fast computation of power and performance measures leads to a multi-objective optimization analysis in two forms: a scalarization method and a Pareto based method. For the two approaches, we propose fast and efficient approximate algorithms that construct progressively an optimal solution. To discuss results, the model is used to simulate a physical server hosting several VMs (Virtual Machines) where we investigate optimal thresholds for the performance-energy trade-off.

13 novembre 2023

Automates communicants et communications quasi-synchrones

Loïc Germerie Guizouarn (LACL)

Les systèmes distribués sont le plus souvent basés sur l’échange asynchrone de messages entre des agents. Les automates communicants sont un formalisme permettant de modéliser les communications de ces systèmes, afin de détecter automatiquement des erreurs comme des pertes de messages ou des inter-blocages. Ces problèmes sont indécidables en général pour des systèmes à partir de deux machines, et plusieurs hypothèses restrictives ont été étudiées pour les rendre décidables. Dans cette présentation, nous étudierons une de ces approches, basée sur l’étude des systèmes dont les exécutions sont réalisables avec des communications synchrones (Realisable with Synchronous Communication, ou RSC). Les comportements de ces systèmes approximent des comportements synchrones, où les messages sont envoyés et reçus simultanément.

16 octobre 2023

Inside and Beyond Decisiveness for Infinite Probabilistic Models

Lina Ye (LMF)

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).

9 octobre 2023

Queens of the Hill

Sergiu Ivanov (IBISC, Université d'Évry)

Inspired by the programming game Core Wars, we propose in this work a framework and the organisation of king of the hill-style tournaments between P systems.  We call these tournaments Queens of the Hill and the individual contestants valkyries.  The goal of each valkyrie is to dissolve as many membranes of as many other valkyries as possible, while at the same time resisting the attacks. Valkyries are transition P systems with cooperative rules, target indication, and rudimentary matter–anti-matter annihilation rules. These ingredients are sufficient for computational completeness, but the context of Queens of the Hill reduces the relevance of this statement.  We give some tentative examples of strategies and discuss their advantages and drawbacks. Finally, we describe how Queens of the Hill can be used as a teaching exercise, and also a tool to federate the students’ creativity to push the frontiers of membrane computing.