### Abstract

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

Pages | 146-162 |

Number of pages | 17 |

DOIs | |

State | Published - 1999 |

Event | 10th International Conference on Concurrency Theory, CONCUR 1999 - Eindhoven, Netherlands |

### Conference

Conference | 10th International Conference on Concurrency Theory, CONCUR 1999 |
---|---|

Abbreviated title | CONCUR |

Country | Netherlands |

City | Eindhoven |

Period | 24/08/99 → 27/08/99 |

### Fingerprint

### Keywords

- FMT-MC: MODEL CHECKING
- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
- IR-63300
- FMT-BDD: BINARY DECISION DIAGRAMS
- EWI-6483

### Cite this

*Approximate symbolic model checking of continous-time Markov chains*. 146-162. Paper presented at 10th International Conference on Concurrency Theory, CONCUR 1999, Eindhoven, Netherlands.DOI: 10.1007/3-540-48320-9

}

**Approximate symbolic model checking of continous-time Markov chains.** / Baier, Christel; Baeten, J.C.M. (Editor); Mauw, S. (Editor); Katoen, Joost P.; Hermanns, H.

Research output: Scientific - peer-review › Paper

TY - CONF

T1 - Approximate symbolic model checking of continous-time Markov chains

AU - Baier,Christel

AU - Katoen,Joost P.

AU - Hermanns,H.

A2 - Baeten,J.C.M.

A2 - Mauw,S.

PY - 1999

Y1 - 1999

N2 - This paper presents a symbolic model checking algorithm for continuous-time Markov chains for an extension of the continuous stochastic logic CSL of Aziz et al. [1] The considered logic contains a time-bounded until-operator and a novel operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady state-operator) and a Volterra integral equation system for time-bounded until. We propose a symbolic approximate method for solving the integrals using MTDDs (multi-terminal decision diagrams), a generalisation of MTBDDs. These new structures are suitable for numerical integration using quadrature formulas based on equally-spaced abscissas, like trapezoidal, Simpson and Romberg integration schemes.

AB - This paper presents a symbolic model checking algorithm for continuous-time Markov chains for an extension of the continuous stochastic logic CSL of Aziz et al. [1] The considered logic contains a time-bounded until-operator and a novel operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady state-operator) and a Volterra integral equation system for time-bounded until. We propose a symbolic approximate method for solving the integrals using MTDDs (multi-terminal decision diagrams), a generalisation of MTBDDs. These new structures are suitable for numerical integration using quadrature formulas based on equally-spaced abscissas, like trapezoidal, Simpson and Romberg integration schemes.

KW - FMT-MC: MODEL CHECKING

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

KW - IR-63300

KW - FMT-BDD: BINARY DECISION DIAGRAMS

KW - EWI-6483

U2 - 10.1007/3-540-48320-9

DO - 10.1007/3-540-48320-9

M3 - Paper

SP - 146

EP - 162

ER -