Jeudi 24 mai, 14h en salle Minquiers
Loig Jezequel (Univ. Nantes)
Pomsets and Unfolding of Reset Petri Nets
Reset Petri nets are a particular class of Petri nets where transition firings can remove all tokens from a place without checking if this place actually holds tokens or not. In this talk we will discuss partial order semantics of such nets. In particular, we will propose a pomset bisimulation for comparing their concurrent behaviours. Building on this pomset bisimulation we will then generalize the standard finite complete prefixes of unfolding to the class of safe reset Petri nets.
Exposés des semaines suivantes
Jeudi 31 mai, 14h en salle Aurigny
Timothée Haudebourg (Celtique)
Verifying Higher-Order Functions with Tree Automata
This work is a fully automatic technique for verifying safety properties of higher- order functional programs. Tree automata are used to represent sets of reachable states and functional programs are modeled using term rewriting systems. From a tree automaton representing the initial state, a completion algorithm iteratively computes an automaton which over-approximates the output set of the program to verify. We identify a subclass of higher-order functional programs for which the completion is guaranteed to terminate. Precision and termination are obtained conjointly by a careful choice of equations between terms. The verification objective can be used to generate sets of equations automatically. Our experiments show that tree automata are sufficiently expressive to prove intricate safety properties and sufficiently simple for the verification result to be certified in Coq. These results extend state-of-the-art model-checking approaches for higher-order functional programs
Lundi 4 juin, 14h en salle Minquiers
Anne Bouillard (ENS/Nokia)
A data structure for analyzing spatio-temporal correlations of alarms
In this talk, I will present a data structure for the analysis of correlations of alarms, for root-cause analysis or prediction purposes. This is a joint work with Marc-Olivier Buob and Maxime Raynal (intern). A sequence of alarms is modeled by a directed acyclic graph. The nodes of the graph are the alarms, that are represented by a symbol and an interval of time. An arc of the graph is interpreted as a potential causality between two alarms. I will first show how to build a "compact" structure storing all the potential causal sequences of alarms and then how to weight this structure so that the actual correlations can be detected. The efficiency of the approach will be demonstrated on toy examples.