Minimality of Critical Scenarios in Petri Net Models

The aim of this paper is to define the concept of minimality of scenarios, considering that in our approach a scenario is defined as a partial order between events. For deriving feared scenario (ie: scenario that leads the system to critical situation) Petri nets are used for the modelling of systems. To avoid space state explosion, Petri net reachability is translated into provability of linear logic sequent. It is possible to determine a partial order of transition firings and extract feared scenarios which are represented by sequents. By analogy with the concept of minimal cutsets for the fault trees, we define in this paper the concept of minimal scenario.