Computing the Reveals Relation in Occurrence Nets

Stefan Haar 1, 2 Christian Kern 3 Stefan Schwoon 1, 2, 4
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Petri net unfoldings are a useful tool to tackle state-space explosion in verification and related tasks. Moreover, their structure allows to access directly the relations of causal precedence, concurrency, and conflict between events. Here, we explore the data structure further, to determine the following relation: event a is said to reveal event b iff the occurrence of a implies that b inevitably occurs, too, be it before, after, or concurrently with a. Knowledge of reveals facilitates in particular the analysis of partially observable systems, in the context of diagnosis, testing, or verification; it can also be used to generate more concise representations of behaviours via abstractions. The reveals relation was previously introduced in the context of fault diagnosis, where it was shown that the reveals relation was decidable: for a given pair a,b in the unfolding U of a safe Petri net N, a finite prefix P of U is sufficient to decide whether or not a reveals b. In this paper, we first considerably improve the bound on |P|. We then show that there exists an efficient algorithm for computing the relation on a given prefix. We have implemented the algorithm and report on experiments.
Type de document :
Communication dans un congrès
D'Agostino, Giovanna and La Torre, Salvatore. Gandalf, Jun 2011, Minori, Italy. 54, pp.31-44, 2011, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.54.3〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00638262
Contributeur : Stefan Haar <>
Soumis le : vendredi 4 novembre 2011 - 14:23:25
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37
Document(s) archivé(s) le : jeudi 15 novembre 2012 - 11:10:59

Fichier

HKS-gandalf11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Stefan Haar, Christian Kern, Stefan Schwoon. Computing the Reveals Relation in Occurrence Nets. D'Agostino, Giovanna and La Torre, Salvatore. Gandalf, Jun 2011, Minori, Italy. 54, pp.31-44, 2011, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.54.3〉. 〈inria-00638262〉

Partager

Métriques

Consultations de la notice

255

Téléchargements de fichiers

193