The observer coverability graph for the analysis of observability properties of Place/Transition nets

In this paper we discuss the problem of estimating the marking of a Place/Transition net based on event observation, assuming that the net structure is known while the initial marking is not known. We consider different observability properties, some of which are new and some of which have already been defined by the authors in previous works, where a characterization based on the net language was also given to prove that they are decidable. Checking for language inclusion is difficult, thus in this paper we introduce a useful analysis tool, called observer coverability graph, that represents both the set of reachable markings of a net system and the corresponding estimate error. We also show that the graph provides either semi-decision or decision conditions for the considered properties.