We present a theory for the design and analysis of concurrent/distributed systems with real-time and stochastic time aspects. We start by presenting the model of Interactive Generalized Semi-Markov Processes (IGSMP): a compositional model for representing the class of stochastic processes known as Generalised Semi-Markov Processes (GSMPs), i.e. probabilistic timed systems where durations of delays are expressed by random variables with a general probability distribution. Technically, IGSMPs extend GSMPs with action transitions representing the ability of a process to interact with another process. Then, we introduce the calculus of Interactive Generalized Semi-Markov Processes, a stochastic process algebra which produces IGSMPs as semantic models of its terms. This is obtained by expressing the concurrent execution of delays through a simple probabilistic extension of Van Glabbeek and Vaandrageer's ST semantics based on dynamic names. We also present observational equivalence over IGSMPs, we observe that it is a congruence for all the operators of the calculus and we produce an axiomatization for this equivalence which is complete over finite-state strongly guarded processes. Finally, we present a case study on queuing systems G/G/1/q.

M. Bravetti (2004). Real Time and Stochastic Time. BERLIN : Springer [10.1007/978-3-540-30080-9_5].

Real Time and Stochastic Time

BRAVETTI, MARIO
2004

Abstract

We present a theory for the design and analysis of concurrent/distributed systems with real-time and stochastic time aspects. We start by presenting the model of Interactive Generalized Semi-Markov Processes (IGSMP): a compositional model for representing the class of stochastic processes known as Generalised Semi-Markov Processes (GSMPs), i.e. probabilistic timed systems where durations of delays are expressed by random variables with a general probability distribution. Technically, IGSMPs extend GSMPs with action transitions representing the ability of a process to interact with another process. Then, we introduce the calculus of Interactive Generalized Semi-Markov Processes, a stochastic process algebra which produces IGSMPs as semantic models of its terms. This is obtained by expressing the concurrent execution of delays through a simple probabilistic extension of Van Glabbeek and Vaandrageer's ST semantics based on dynamic names. We also present observational equivalence over IGSMPs, we observe that it is a congruence for all the operators of the calculus and we produce an axiomatization for this equivalence which is complete over finite-state strongly guarded processes. Finally, we present a case study on queuing systems G/G/1/q.
2004
Formal Methods for the Design of Real-Time Systems, Revised Lectures
132
180
M. Bravetti (2004). Real Time and Stochastic Time. BERLIN : Springer [10.1007/978-3-540-30080-9_5].
M. Bravetti
File in questo prodotto:
Eventuali allegati, non sono esposti

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/11585/10127
 Attenzione

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

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