Modelling and analysis of time-dependent concurrent/distributed systems is very challenging when such systems also exhibit a stochastic behavior. In this paper, the partially stochastic Time Petri Net formalism (psTPN) is introduced, which has the expressive power to model realistic complex systems. Each transition owns both a non-deterministic temporal interval and a stochastic duration established by a generally distributed (i.e., not necessarily Markovian) probabilistic function whose samples are constrained to occur in the associated time interval. A psTPN model admits two possible interpretations: the non-deterministic (which ignores stochastic aspects), useful for qualitative analysis (establishing that an event can possibly occur) and the stochastic one (which considers stochastic behavior), useful for quantitative analysis (estimating the probability for an event to actually occur). The paper focuses on the reduction of psTPN onto UPPAAL timed automata which permits non-deterministic analysis through the symbolic exhaustive model checker, and quantitative analysis through the statistical model checker (SMC) which rests on simulations and statistical inference. Although potentially less accurate of analysis techniques based on numerical methods and stochastic state space enumeration, this paper claims that statistical model checking can provide quantitative property assessment which is of practical engineering value. As an example, psTPN is exploited in the paper to model and evaluate a stochastic version of the Fisher timed-based mutual exclusion algorithm.

Modelling and Analysis of Partially Stochastic Time Petri Nets using Uppaal Model Checkers

Libero Nigro
Membro del Collaboration Group
;
Paolo F. Sciammarella
Membro del Collaboration Group
2019

Abstract

Modelling and analysis of time-dependent concurrent/distributed systems is very challenging when such systems also exhibit a stochastic behavior. In this paper, the partially stochastic Time Petri Net formalism (psTPN) is introduced, which has the expressive power to model realistic complex systems. Each transition owns both a non-deterministic temporal interval and a stochastic duration established by a generally distributed (i.e., not necessarily Markovian) probabilistic function whose samples are constrained to occur in the associated time interval. A psTPN model admits two possible interpretations: the non-deterministic (which ignores stochastic aspects), useful for qualitative analysis (establishing that an event can possibly occur) and the stochastic one (which considers stochastic behavior), useful for quantitative analysis (estimating the probability for an event to actually occur). The paper focuses on the reduction of psTPN onto UPPAAL timed automata which permits non-deterministic analysis through the symbolic exhaustive model checker, and quantitative analysis through the statistical model checker (SMC) which rests on simulations and statistical inference. Although potentially less accurate of analysis techniques based on numerical methods and stochastic state space enumeration, this paper claims that statistical model checking can provide quantitative property assessment which is of practical engineering value. As an example, psTPN is exploited in the paper to model and evaluate a stochastic version of the Fisher timed-based mutual exclusion algorithm.
Time Petri Nets, stochastic behavior, timing constraints, Fisher’s mutual exclusion, model checking, statistical model checking, UPPAAL
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/289303
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact