7th International Conference on Performance Evaluation Methodologies and Tools

Research Article

Contextual Lumpability

  • @INPROCEEDINGS{10.4108/icst.valuetools.2013.254408,
        author={Jane Hillston and Andrea Marin and Sabina Rossi and Carla Piazza},
        title={Contextual Lumpability},
        proceedings={7th International Conference on Performance Evaluation Methodologies and Tools},
        keywords={lumpability markovian process algebra bisimilarity markov processes pepa},
  • Jane Hillston
    Andrea Marin
    Sabina Rossi
    Carla Piazza
    Year: 2014
    Contextual Lumpability
    DOI: 10.4108/icst.valuetools.2013.254408
Jane Hillston1, Andrea Marin2, Sabina Rossi2,*, Carla Piazza3
  • 1: University of Edinburgh
  • 2: Università Ca' Foscari Venezia
  • 3: Universita di Udine
*Contact email: srossi@dais.unive.it


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 automata that carry out actions. Nevertheless, as with all state-based modelling techniques, Markovian process algebras suffer from the well-known state space explosion problem. State aggregation, specifically lumping, is one of the possible methods for tackling this problem. In this paper we revisit the notion of Markovian bisimulaton which has previously been shown to induce a lumpable relation in the underlying Markov process. Here we consider a coarser relation of contextual lumpability, and taking the specific example of strong equivalence in PEPA, we propose a slightly relaxed definition of Markovian bisimulation, named lumpable bisimularity, and prove that this is a characterisation of the notion of contextual lumpability for PEPA components. Moreover, we show that lumpable bisimularity induces the largest contextual lumping over the Markov process underlying any PEPA component. We provide an algorithm for lumpable bisimilarity and study both its time and space complexity.