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

Stefan Haar 1, 2
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 : We consider asynchronous diagnosis in (safe) Petri net models of distributed systems, using the partial order semantics of occurrence net unfoldings. Both the observability and diagnosability properties will appear in two different forms, depending on the semantics chosen: strong observability and diagnosability are the classical notions from the state machine model and correspond to interleaving semantics in Petri nets. By contrast, the weak form is linked to characteristics of nonsequential processes, and requires an asynchronous progress assumption on those processes. We give algebraic characterizations for both types, and give verification methods. The study of weak diagnosability leads us to the analysis of a relation in occurrence nets, first presented in [S. Haar (2007): Unfold and Cover: Qualitative Diagnosability for Petri Nets.]: given the occurrence of some event a that reveals b, the occurrence of b is inevitable. Then b may already have occurred, be concurrent to, or even in the future of a. We show that the reveals-relation can be effectively computed recursively--for each pair, a suitable finite prefix of bounded depth is sufficient--and show its use in asynchronous diagnosis. Based on this relation, a decomposition of the Petri net unfolding into facets is defined, yielding an abstraction technique that preserves and reflects maximal partially ordered runs.
Type de document :
Article dans une revue
IEEE Transactions on Automatic Control, Institute of Electrical and Electronics Engineers, 2010, 55 (10), pp.2310-2320. 〈10.1016/j.ic.2009.11.009〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00638209
Contributeur : Stefan Haar <>
Soumis le : vendredi 4 novembre 2011 - 11:56:40
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37
Document(s) archivé(s) le : dimanche 5 février 2012 - 02:22:15

Fichier

haar-tac10.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Stefan Haar. Types of Asynchronous Diagnosability and the Reveals-Relation in Occurrence Nets. IEEE Transactions on Automatic Control, Institute of Electrical and Electronics Engineers, 2010, 55 (10), pp.2310-2320. 〈10.1016/j.ic.2009.11.009〉. 〈inria-00638209〉

Partager

Métriques

Consultations de la notice

142

Téléchargements de fichiers

442