Séminaire du 11 mars 2011


IBISC, salle de séminaire au 1er étage: comment y aller


14h00-15h00: S. Evangelista, Université Paris 13, "Parallel Nested Depth-First Searches for LTL Model Checking"

Abstract:transparents This talk introduces a parallel version of the nested-depth first search algorithm for LTL model checking. Our algorithm is adapted to shared memory, multi-core architectures. It exhibits good speed-ups as supported by a series of experiments.

15h00-15h30 : C. Rodriguez, ENS de Cachan, "Efficient contextual unfolding"

Abstract:transparents A contextual net is a Petri net extended with read arcs, that is, special arcs allowing a transition to check for the presence of tokens in a place without consuming them. The unfolding of a contextual net is another safe, acyclic contextual net that completely expresses its behaviour. Paolo Baldan et al. presented in 2008 an abstract procedure to construct a complete prefix of the unfolding for a (safe) contextual net. In this talk, we present this abstract procedure, with focus on the work done to obtain a first real (moderately efficient) implementation of it.

15h30-16h00: pause café

16h00: vie du groupe