Efficient Reductions for LTL Formulae Verification

National audienceStructural model abstraction is a powerful technique for reducing the complexity of a state based enumeration analysis. We present in this paper new efficient ordinary Petri nets reductions. At first, we define ``behavioural'' reductions (i.e. based on conditions related to the language of the net) which preserve a fundamental property of a net (i.e. liveness) and any LTL formula that does not observe reduced transitions of the net. We substitute these conditions by structural or algebraical ones which lead to reductions which can be efficiently checked and applied whereas enlarging the application spectrum of the previous reductions. At last, we illustrate our method on significant and typical examples