### Abstract

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

Title of host publication | Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 |

Editors | S. Gilmore, L. de Alfaro |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 23-38 |

Number of pages | 16 |

ISBN (Print) | 3-540-42556-X |

DOIs | |

Publication status | Published - 2001 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 2165 |

ISSN (Print) | 0302-9743 |

### Keywords

- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
- FMT-BDD: BINARY DECISION DIAGRAMS
- FMT-PM: PROBABILISTIC METHODS
- FMT-MC: MODEL CHECKING
- FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
- FMT-TOOLS
- EWI-6449
- IR-63281
- METIS-203851

### Cite this

*Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001*(pp. 23-38). (Lecture Notes in Computer Science; Vol. 2165). Berlin: Springer. https://doi.org/10.1007/3-540-44804-7_2

}

*Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001.*Lecture Notes in Computer Science, vol. 2165, Springer, Berlin, pp. 23-38. https://doi.org/10.1007/3-540-44804-7_2

**Faster and symbolic CTMC model checking.** / Katoen, Joost P.; Kwiatkowska, Marta; Norman, Gethin; Parker, David.

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

TY - GEN

T1 - Faster and symbolic CTMC model checking

AU - Katoen, Joost P.

AU - Kwiatkowska, Marta

AU - Norman, Gethin

AU - Parker, David

PY - 2001

Y1 - 2001

N2 - This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) [7] which includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N)]]> in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.

AB - This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) [7] which includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N)]]> in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - FMT-BDD: BINARY DECISION DIAGRAMS

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-MC: MODEL CHECKING

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-TOOLS

KW - EWI-6449

KW - IR-63281

KW - METIS-203851

U2 - 10.1007/3-540-44804-7_2

DO - 10.1007/3-540-44804-7_2

M3 - Conference contribution

SN - 3-540-42556-X

T3 - Lecture Notes in Computer Science

SP - 23

EP - 38

BT - Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001

A2 - Gilmore, S.

A2 - de Alfaro, L.

PB - Springer

CY - Berlin

ER -