Séminaire du 11 juin 2021


LIP6, salle 24-25/405. Instructions pour venir ici.

et en distancielle sur zoom.


14h00-14h40: Pierre Bouvier (Grenoble); Trois problèmes d'accessibilité dans les réseaux de Petri saufs

Abstract : Decision Diagrams (DD) have been successfully used to store the state space of large discrete event dynamic systems (DEDS), typically described in terms of discrete variables and events. The availability of well-established libraries, as well as more recent ones, makes the use of DD in this context very straightforward. On the other side it is well known that the effectiveness of a DD representation of a state space is strongly dependent on the specific assignment of the DEDS variable to the DD levels, an NP-complete problem. Given that a brute force approach is not feasible, many heuristics have been defined. This talk concentrate on heuristics for variable orders, their definition and their evaluation. In particular I will concentrate on heuristics that make use of structural information of the system (like p-semiflows for Petri net), on metrics to evaluate such heuristics and on the use of metrics as meta-heuristics for the selection of "good" orders.

14h40-15h30 : Yann Thierry-Mieg (LIP6);Symbolic and Structural Model-checking

Abstract : Brute-force model-checking consists in exhaustive exploration of the state-space of aPetri net, and meets the dreaded state-space explosion problem.In contrast, this paper shows how to solve model-checking problems using a combination oftechniques that stay in complexity proportional to the sizeof the net structure rather than to thestate-space size. We combine an SMT based over-approximation to prove that some behaviors are unfeasible, an under-approximation using memory-less sampling of runs to find witness traces or counter-examples, and a set of structural reduction rules that can simplify both the system and the property. This approach was able to win by a clear margin the model-checking contest 2020 for reachability queries as well as deadlock detection, thus demonstrating the practical effectiveness and general applicability of the system of rules presented in this paper

15h30-16h00: pause café

16h00-16h30: vie du groupe