The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
We consider the model of Time Petri Nets where time is associated with
transitions. Two semantics for time elapsing can be considered: the strong
one, for which all transitions are urgent, and the weak one, for which time
can elapse arbitrarily. It is well known that many verification problems such
as the marking reachability are undecidable with the strong semantics. In this
talk, we focus on Time Petri Nets with weak semantics equipped with three
different memory policies for the firing of transitions. We prove that the
reachability problem is decidable for the most common memory policy
(intermediate) and becomes undecidable otherwise. Moreover, we study the
relative expressiveness of these memory policies and obtain partial and
surprising results.
This a joint work with Pierre-Alain Reynier (LIF-Université Aix-Marseille)