Building Tight Occurrence Nets from Reveals Relations.

Sandie Balaguer 1 Thomas Chatain 1, 2 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 : Occurrence nets are a well known partial order model for the concurrent behavior of Petri nets. The causality and conflict relations between events, which are explicitly represented in occurrence nets, induce logical dependencies between event occurrences: the occurrence of an event e in a run implies that all its causal predecessors also occur, and that no event in conflict with e occurs. But these structural relations do not express all the logical dependencies between event occurrences in maximal runs: in particular, the occurrence of e in any maximal run may imply the occurrence of another event that is not a causal predecessor of e, in that run. The reveals relation has been introduced in [Haar, IEEE TAC 55(10):2310-2320, 2010] to express this dependency between two events. Here we generalize the reveals relation to express more general dependencies, involving more than two events, and we introduce ERL logic to express them as boolean formulas. Finally we answer the synthesis problem that arises: given an ERL formula φ, is there an occurrence net N such that φ describes exactly the dependencies between the events of N?
keyword : occurrence nets
Type de document :
Communication dans un congrès
Caillaud, Benoit and Carmona, Josep. ACSD 2011, Jun 2011, Newcastle, United Kingdom. IEEE Computer Society Press, pp.44-53, 2011, 〈10.1109/ACSD.2011.16〉
Liste complète des métadonnées

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

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

Fichier

BCH-acsd11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Sandie Balaguer, Thomas Chatain, Stefan Haar. Building Tight Occurrence Nets from Reveals Relations.. Caillaud, Benoit and Carmona, Josep. ACSD 2011, Jun 2011, Newcastle, United Kingdom. IEEE Computer Society Press, pp.44-53, 2011, 〈10.1109/ACSD.2011.16〉. 〈inria-00638232〉

Partager

Métriques

Consultations de la notice

189

Téléchargements de fichiers

97