Quantitative analysis of computer systems is often based on Markovian models. Among the formalisms that are used in practice, Markovian process algebras have found many applications, also thanks to their compositional nature that allows one to specify systems as interacting individual au- tomata that carry out actions. Nevertheless, as with all state-based modelling techniques, Markovian process alge- bras suer from the well-known state space explosion prob- lem. State aggregation, specically lumping, is one of the possible methods for tackling this problem. In this paper we revisit the notion ofMarkovian bisimulation which has previ- ously been shown to induce a lumpable relation in the under- lying Markov process. Here we consider the coarser relation of contextual lumpability, and taking the specic example of strong equivalence in PEPA, we propose a slightly relaxed denition of Markovian bisimulation, named lumpable bisim- ilarity, and prove that this is a characterisation of the notion of contextual lumpability for PEPA components. Moreover, we show that lumpable bisimilarity induces the largest con- textual lumping over the Markov process underlying any PEPA component. We provide an algorithm for lumpable bisimilarity and study both its time and space complexity.

Contextual Lumpability

MARIN, Andrea;ROSSI, Sabina
2013-01-01

Abstract

Quantitative analysis of computer systems is often based on Markovian models. Among the formalisms that are used in practice, Markovian process algebras have found many applications, also thanks to their compositional nature that allows one to specify systems as interacting individual au- tomata that carry out actions. Nevertheless, as with all state-based modelling techniques, Markovian process alge- bras suer from the well-known state space explosion prob- lem. State aggregation, specically lumping, is one of the possible methods for tackling this problem. In this paper we revisit the notion ofMarkovian bisimulation which has previ- ously been shown to induce a lumpable relation in the under- lying Markov process. Here we consider the coarser relation of contextual lumpability, and taking the specic example of strong equivalence in PEPA, we propose a slightly relaxed denition of Markovian bisimulation, named lumpable bisim- ilarity, and prove that this is a characterisation of the notion of contextual lumpability for PEPA components. Moreover, we show that lumpable bisimilarity induces the largest con- textual lumping over the Markov process underlying any PEPA component. We provide an algorithm for lumpable bisimilarity and study both its time and space complexity.
2013
Proceedings of Valuetools 2013
File in questo prodotto:
File Dimensione Formato  
vt13-lump.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 358.14 kB
Formato Adobe PDF
358.14 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA 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/10278/39247
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 26
  • ???jsp.display-item.citation.isi??? ND
social impact