Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics: (Extended Version)

Loïc Hélouët 1 Karim Kecir 1
1 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper considers realizability of expected schedules by production systems with concurrent tasks, bounded resources that have to be shared among tasks, and random behaviors and durations. Schedules are high level views of desired executions of systems represented as partial orders decorated with timing con- straints. Production systems (production cells,train networks. . . ) are modeled as stochastic time Petri nets STPNs with an elementary (1-bounded) semantics. We detail their interleaved operational semantics, and then propose a non-interleaved semantics through the notion of time processes. We then consider boolean re- alizability: a schedule S is realizable by a net N if S embeds in a time process of N that satisfies all its constraints. However, with continuous time domains, the probability of a time process with exact dates is null. We hence consider probabilistic realizability up to α time units, that holds if the probability that N realizes S with constraints enlarged by α is strictly positive. Upon a sensible restriction guaranteeing time progress, boolean and probabilistic realizability of a schedule can be checked on the finite set of symbolic prefixes extracted from a bounded unfolding of the net. We give a construction technique for these prefixes and show that they represent all time processes of a net occurring up to a given maximal date. We then show how to verify existence of an embedding and compute the probability of its realization.
Type de document :
Rapport
[Research Report] INRIA Rennes - Bretagne Atlantique. 2017
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01646920
Contributeur : Loic Helouet <>
Soumis le : lundi 27 novembre 2017 - 15:11:37
Dernière modification le : mercredi 16 mai 2018 - 11:24:13

Fichier

SCP-LHKK-Revision1.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01646920, version 2

Citation

Loïc Hélouët, Karim Kecir. Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics: (Extended Version). [Research Report] INRIA Rennes - Bretagne Atlantique. 2017. 〈hal-01646920v2〉

Partager

Métriques

Consultations de la notice

241

Téléchargements de fichiers

37