### Abstract

Original language | English |
---|---|

Pages | 358-372 |

Number of pages | 15 |

DOIs | |

Publication status | Published - 2000 |

Event | 12th International Conference on Computer Aided Verification, CAV 2000 - Chicago, United States Duration: 15 Jul 2000 → 19 Jul 2000 Conference number: 12 |

### Conference

Conference | 12th International Conference on Computer Aided Verification, CAV 2000 |
---|---|

Abbreviated title | CAV |

Country | United States |

City | Chicago |

Period | 15/07/00 → 19/07/00 |

### Fingerprint

### Keywords

- EWI-6442
- FMT-MC: MODEL CHECKING
- FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
- FMT-PM: PROBABILISTIC METHODS
- IR-63277

### Cite this

*Model Checking Continuous-Time Markov Chains by Transient Analysis*. 358-372. Paper presented at 12th International Conference on Computer Aided Verification, CAV 2000, Chicago, United States. https://doi.org/10.1007/10722167_28

}

**Model Checking Continuous-Time Markov Chains by Transient Analysis.** / Baier, Christel; Haverkort, Boudewijn; Hermanns, Holger; Katoen, Joost Pieter.

Research output: Contribution to conference › Paper › Academic › peer-review

TY - CONF

T1 - Model Checking Continuous-Time Markov Chains by Transient Analysis

AU - Baier, Christel

AU - Haverkort, Boudewijn

AU - Hermanns, Holger

AU - Katoen, Joost Pieter

PY - 2000

Y1 - 2000

N2 - The verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [3,6], a stochastic branching time temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties of the form Pp(Φ1 UI Φ2), for state formulas Φ1 and Φ2, comparison operator , probability p, and real interval I. The main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas.

AB - The verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [3,6], a stochastic branching time temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties of the form Pp(Φ1 UI Φ2), for state formulas Φ1 and Φ2, comparison operator , probability p, and real interval I. The main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas.

KW - EWI-6442

KW - FMT-MC: MODEL CHECKING

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-PM: PROBABILISTIC METHODS

KW - IR-63277

U2 - 10.1007/10722167_28

DO - 10.1007/10722167_28

M3 - Paper

SP - 358

EP - 372

ER -