The aim of this work is to propose a logical‐based approach for deriving the critical scenarii from a differential predicate transition Petri nets model and proof tree, to evaluate diagnosis and safety of hybrid systems.
The new approach integrates the Petri net model and linear logic. The design process is twofold: first, it considers the specific translation from Petri net to linear logic, and, second, it studies the relationship between the order of the rule application in the sequent proof and the processes associated with the same reachability problem.
With linear logic and Petri net it is proved that, from a canonical proof tree, a partial order can be derived (based on causality point of view) of transition firing and focusing the search of the parts of the model that are interesting for safety analysis. Each scenario is given by a partial order between the events necessary for the occurrence of the feared event.
This paper deals with safety in design of hybrid systems. For this purpose, it is important to characterize feared behaviours (which are critical) in the early design stage.
