Séminaires
Séminaire du 11 Février 2011
Lieu
CNAM, salle 35.2.25: comment y aller
Programme
14h00-15h00: J. Desel, KU Eicjstätt, "Partial Orders fit for work"
Abstract:
I will present two topics which fit to the above title: First, I show how occurrence nets, representing the partial order behavior of Petri nets, allow for nicer proofs in Petri net structure theory, compared to sequential semantics. Second, I show how the VIPtool based on occurrence nets can be used for industrial applications.
15h00-16h00 : C. lakos, Univ. Adelaïde, "Modular State Spaces for Prioritised Petri Nets"
Abstract: Verification of complex systems specification often encounters the so-called state space explosion problem, which prevents exhaustive model-checking in many practical cases. Many techniques have been developed to counter this problem by reducing the state space, either by retaining a smaller number of relevant states, or by using a smart representation. Among the latter, modular state spaces have turned out to be an efficient analysis technique in many cases. When the system uses a priority mechanism (e.g. timed system), there is increased coupling between the modules - preemption between modules can occur, thus disabling local events
Here, we show that the approach is still applicable even when considering dynamic priorities, i.e. priorities depending both on the transition and the current marking.