Process Refinement and Asynchronous Composition with Modalities

Dorsaf El~hog-Benzina 1 Serge Haddad 1 Rolf Hennicker
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 propose a framework for the specification of infinite state systems based on Petri nets with distinguished may- and must-transitions (called modalities) which specify the allowed and the required behavior of refinements and hence of implementations. Formally, refinements are defined by relating the modal language specifications generated by two modal Petri nets according to the refinement relation for modal language specifications. We show that this refinement relation is decidable if the underlying modal Petri nets are weakly deterministic. We also show that the membership problem for the class of weakly deterministic modal Petri nets is decidable. As an important application of our approach we consider I/O-Petri nets which are obtained by asynchronous composition and thus exhibit inherently an infinite behavior.
Type de document :
Communication dans un congrès
Sidorova, Natalia and Serebrenik, Alexander. Proceedings of the 2nd International Workshop on Abstractions for Petri Nets and Other Models of Concurrency (APNOC'10), 2010, Braga, Portugal. 2010
Liste complète des métadonnées

https://hal.inria.fr/hal-00779893
Contributeur : Stefan Haar <>
Soumis le : mardi 22 janvier 2013 - 16:49:46
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

  • HAL Id : hal-00779893, version 1

Collections

Citation

Dorsaf El~hog-Benzina, Serge Haddad, Rolf Hennicker. Process Refinement and Asynchronous Composition with Modalities. Sidorova, Natalia and Serebrenik, Alexander. Proceedings of the 2nd International Workshop on Abstractions for Petri Nets and Other Models of Concurrency (APNOC'10), 2010, Braga, Portugal. 2010. 〈hal-00779893〉

Partager

Métriques

Consultations de la notice

191