### Abstract

Original language | Undefined |
---|---|

Title of host publication | Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation |

Editors | Ivana Černá, Gerald Lüttgen |

Place of Publication | Amsterdam |

Publisher | Elsevier |

Pages | 35-50 |

Number of pages | 16 |

DOIs | |

Publication status | Published - 3 Dec 2008 |

Event | 7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008 - Budapest, Hungary Duration: 29 Mar 2008 → 29 Mar 2008 Conference number: 7 http://anna.fi.muni.cz/PDMC/PDMC08/cfp.shtml |

### Publication series

Name | Electronic Notes in Theoretical Computer Science |
---|---|

Publisher | Elsevier |

Number | 2 |

Volume | 220 |

ISSN (Print) | 1571-0661 |

ISSN (Electronic) | 1571-0661 |

### Workshop

Workshop | 7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008 |
---|---|

Abbreviated title | PDMC |

Country | Hungary |

City | Budapest |

Period | 29/03/08 → 29/03/08 |

Internet address |

### Keywords

- FMT-TOOLS
- FMT-MC: MODEL CHECKING
- METIS-254871
- EC Grant Agreement nr.: FP6/043235
- EWI-12290
- IR-62249

### Cite this

*Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation*(pp. 35-50). [10.1016/j.entcs.2008.11.012] (Electronic Notes in Theoretical Computer Science; Vol. 220, No. 2). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2008.11.012

}

*Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation.*, 10.1016/j.entcs.2008.11.012, Electronic Notes in Theoretical Computer Science, no. 2, vol. 220, Elsevier, Amsterdam, pp. 35-50, 7th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2008, Budapest, Hungary, 29/03/08. https://doi.org/10.1016/j.entcs.2008.11.012

**Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking.** / Blom, Stefan; Haverkort, Boudewijn R.H.M.; Kuntz, G.W.M.; van de Pol, Jan Cornelis.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking

AU - Blom, Stefan

AU - Haverkort, Boudewijn R.H.M.

AU - Kuntz, G.W.M.

AU - van de Pol, Jan Cornelis

N1 - Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008)

PY - 2008/12/3

Y1 - 2008/12/3

N2 - The verification of quantitative aspects like performance and dependability by means of model checking has become an important and vivid area of research over the past decade. An important result of that research is the logic CSL (continuous stochastic logic) and its corresponding model checking algorithms. The evaluation of properties expressed in CSL makes it necessary to solve large systems of linear (differential) equations, usually by means of numerical analysis. Both the inherent time and space complexity of the numerical algorithms make it practically infeasible to model check systems with more than 100 million states, whereas realistic system models may have billions of states. To overcome this severe restriction, it is important to be able to replace the original state space with a probabilistically equivalent, but smaller one. The most prominent equivalence relation is bisimulation, for which also a stochastic variant exists (Markovian bisimulation). In many cases, this bisimulation allows for a substantial reduction of the state space size. But, these savings in space come at the cost of an increased time complexity. Therefore in this paper a new distributed signature-based algorithm for the computation of the bisimulation quotient of a given state space is introduced. To demonstrate the feasibility of our approach in both a sequential, and more important, in a distributed setting, we have performed a number of case studies.

AB - The verification of quantitative aspects like performance and dependability by means of model checking has become an important and vivid area of research over the past decade. An important result of that research is the logic CSL (continuous stochastic logic) and its corresponding model checking algorithms. The evaluation of properties expressed in CSL makes it necessary to solve large systems of linear (differential) equations, usually by means of numerical analysis. Both the inherent time and space complexity of the numerical algorithms make it practically infeasible to model check systems with more than 100 million states, whereas realistic system models may have billions of states. To overcome this severe restriction, it is important to be able to replace the original state space with a probabilistically equivalent, but smaller one. The most prominent equivalence relation is bisimulation, for which also a stochastic variant exists (Markovian bisimulation). In many cases, this bisimulation allows for a substantial reduction of the state space size. But, these savings in space come at the cost of an increased time complexity. Therefore in this paper a new distributed signature-based algorithm for the computation of the bisimulation quotient of a given state space is introduced. To demonstrate the feasibility of our approach in both a sequential, and more important, in a distributed setting, we have performed a number of case studies.

KW - FMT-TOOLS

KW - FMT-MC: MODEL CHECKING

KW - METIS-254871

KW - EC Grant Agreement nr.: FP6/043235

KW - EWI-12290

KW - IR-62249

U2 - 10.1016/j.entcs.2008.11.012

DO - 10.1016/j.entcs.2008.11.012

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 35

EP - 50

BT - Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation

A2 - Černá, Ivana

A2 - Lüttgen, Gerald

PB - Elsevier

CY - Amsterdam

ER -