Abstract

Mohamed BOUALI, Pavol BARGER, Walter SCHÖN

Abstract : This paper presents the Backward reachability which is a structural analysis method applicable to Colored Petri Nets. This method avoids the fastidious computation of simulation and, at the same time, the combinatorial explosion of the reachable state space. The backward reachability provides the information about different ways of reaching a particular marking. This evaluation considers an evolution of markings participating in each sequence and leading to the desired state. The analysis is performed on an Inverse Colored Petri Net which is obtained through a transformation of the original model according to given transformation rules. This work develops the rules allowing the definition of the inverse model and some complementary mechanisms allowing the backward analysis. The main advantage of this method is that it allows to determine the sequence leading from any initial state to a given final marking without investigating all possible sequences starting with all possible initial states. The method is illustrated on an example inspired by a guided urban system: a tramway braking system.

Keywords : Petri Nets ; Backward Reachability ; Model Analysis ; Structural Transformations

Year : 2012
Issue : 2
Volume : 4

Available