Types of Asynchronous Diagnosability and the Reveals-Relation in Occurrence Nets

Stefan Haar 1, 2, *
* Auteur correspondant
1 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 : We consider asynchronous diagnosis in (safe) Petri net models of distributed systems, using the partial order semantics of occurrence net unfoldings. Unlike the classical case, observability and diagnosability will appear in two different forms each: a strong form associated to interleaving semantics, and a weak form characteristic of nonsequential processes, and requiring an asynchronous progress assumption on those processes. We give algebraic characterizations for both types, and give verification methods. Sufficient conditions for strong diagnosability are derived from linear semiflows. The study of weak diagnosability leads us to the analysis of a relation in occurrence nets, first presented in \cite{CDC07}: given the occurrence of some event $a$ that \emph{reveals} $b$, the occurrence of $b$ is inevitable; here $b$ may be concurrent to, or even in the future of $a$. We show that the \emph{reveals-}relation can be effectively computed on a suitable bounded prefix of the unfolding, and show its use in asynchronous diagnosis. Based on this relation, a decomposition of the Petri net unfolding into \emph{facets} is defined, yielding an abstraction technique that preserves and reflects maximal partially ordered runs.
Type de document :
Rapport
[Research Report] RR-6902, INRIA. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00379540
Contributeur : Stefan Haar <>
Soumis le : mercredi 13 mai 2009 - 15:39:29
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37
Document(s) archivé(s) le : jeudi 10 juin 2010 - 22:13:15

Fichiers

RR-6902.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00379540, version 1

Collections

Citation

Stefan Haar. Types of Asynchronous Diagnosability and the Reveals-Relation in Occurrence Nets. [Research Report] RR-6902, INRIA. 2009. 〈inria-00379540〉

Partager

Métriques

Consultations de la notice

186

Téléchargements de fichiers

106