Preserving Partial Order Runs in Parametric Time Petri Nets

Étienne André 1 Thomas Chatain 2, 3 César Rodriguez 1
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 : Parameter synthesis for timed systems aims at deriving parameter valuations satisfying a given property. In this paper we target concurrent systems. We use partial-order semantics for parametric time Petri nets as a way to both 1) cope with the well-known state-space explosion due to concurrency, and 2) significantly enhance the result of an existing synthesis algorithm. Given a reference parameter valuation, our approach synthesizes other valuations preserving the partial-order executions of the reference parameter valuation. We show the applicability of our approach using a tool applied to asynchronous circuits.
Type de document :
Article dans une revue
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2016, 16, pp.25. 〈10.1145/3012283〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01425696
Contributeur : Thomas Chatain <>
Soumis le : mardi 3 janvier 2017 - 17:40:34
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37
Document(s) archivé(s) le : mardi 4 avril 2017 - 15:18:16

Fichier

IMPO-preprint.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Étienne André, Thomas Chatain, César Rodriguez. Preserving Partial Order Runs in Parametric Time Petri Nets. ACM Transactions on Embedded Computing Systems (TECS), ACM, 2016, 16, pp.25. 〈10.1145/3012283〉. 〈hal-01425696〉

Partager

Métriques

Consultations de la notice

243

Téléchargements de fichiers

56