J.-M. Couvreur, D. Poitrenaud Model Checking based on Occurrence Net Graph La construction du graphe d'accessibilités est la méthode la plus utilisée pour la vérification des propriétés d'un système. Son inconvénient principal est l'explosion du nombre d'états. Deux approches différentes sont généralement employées pour lut­ ter contre ce problème: définir de nouvelles representations con­ cises du graphe pour lesquelles les méthodes de vérification sont adaptées; réduire le graphe tout en préservant les propriétés à vérifier. Nous proposons une nouvelle représentation des graphes d'accessibilités dans laquelle chaque noeud est un réseau de Petri particulier, un réseau d'occurrences, caractérisant une partie des états accessibles. La vérification de propriétés in­ variantes peut être réalisée par l'utilisation d'algorithmes ef­ ficaces dédiés aux réseaux d'occurrences. De plus, notre représentation peut être utilisée de façon à obtenir un graphe respectant l'équivalence begayante à partir duquel les formules de logique temporelle à temps linéaire (privée de l'opérateur Next) peuvent être vérifiées. The computation of a reachability graph is one of the most used method to check system properties. Its main drawback is the state explosion. Two different approaches are generally used to tackle this problem: to define new concise graph representations for which verification methods are adapted; to reduce graphs while preserving observed properties. We propose a new representation of a reachability graph where nodes are particular Petri nets, occurrence nets, characterizing state space parts. Checking in­ variant properties can be done using efficient algorithms for oc­ currence nets. Moreover, our representation can be used to obtain a stuttering equivalent graph on which nexttime-less linear tem­ poral formulas are verified.