Computing the Reveals Relation in Occurrence Nets - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Theoretical Computer Science Année : 2013

Computing the Reveals Relation in Occurrence Nets

Résumé

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 behaviors 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 vertical bar P vertical bar and show that the new bounds are optimal for the method presented. 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

Dates et versions

hal-00925742 , version 1 (08-01-2014)

Identifiants

Citer

Stefan Haar, Christian Kern, Stefan Schwoon. Computing the Reveals Relation in Occurrence Nets. Theoretical Computer Science, 2013, 493, pp.66-79. ⟨10.1016/j.tcs.2013.04.028⟩. ⟨hal-00925742⟩
75 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More