Afin de munir le formalisme des MSG de compteurs, de timers et d'autres aspects, nous introduisons le modèle des réseaux de Petri avec états et une sémantique de processus non-branchants. Ce modèle est non seulement plus expressif que les MSG, mais il permet également des spécifications plus concises. Nous nous intéressons à trois problèmes de vérification classiques sur l'ensemble des marquages accessibles par les préfixes des processus : le caractère borné, la couverture et l'accessibilité. Nous montrons comment réduire ces problèmes au cas particulier des réseaux de Petri de telle sorte que tous les résultats de complexité et de décidabilité s'étendent des réseaux de Petri aux réseaux avec états sous la sémantique des processus. Nous introduisons aussi la notion de borne semi-structurelle afin de considérer des systèmes paramétrés. Cela consiste à fixer le marquage initial d'un sous-ensemble approprié de places, puis à vérifier que le système est borné quel que soit les valeurs des paramètres. Nous montrons comment un dépliage conduit à un problème plus simple à vérifier à l'aide de la Programmation Linéaire.