Séminaires
Séminaire du 11 mars 2011
Lieu
IBISC, salle de séminaire au 1er étage: comment y aller
Programme
14h00-15h00: S. Evangelista, Université Paris 13, "Parallel Nested Depth-First Searches for LTL Model Checking"
Abstract:
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: 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.