IBISC, salle de séminaire au 1er étage: comment y aller
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.
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.