Efficient CTMC Model Checking of Linear Real-Time Objectives

Benoit Barbot, T. Chen, Tingting Han, Joost P. Katoen, Alexandru Mereacre

Research output: Contribution to conferencePaperAcademicpeer-review

31 Citations (Scopus)

Abstract

This paper makes verifying continuous-time Markov chains (CTMCs) against deterministic timed automata (DTA) objectives practical. We show that verifying 1-clock DTA can be done by analyzing subgraphs of the product of CTMC C and the region graph of DTA A. This improves upon earlier results and allows to only use standard analysis algorithms. Our graph decomposition approach naturally enables bisimulation minimization as well as parallelization. Experiments with various examples confirm that these optimizations lead to significant speed-ups. We also report on experiments with multiple-clock DTA objectives. The objectives and the size of the problem instances that can be checked with our prototypical tool go (far) beyond what could be checked so far.
Original languageUndefined
Pages128-142
Number of pages15
DOIs
Publication statusPublished - Mar 2011

Keywords

  • IR-79389
  • EWI-21247

Cite this

Barbot, Benoit ; Chen, T. ; Han, Tingting ; Katoen, Joost P. ; Mereacre, Alexandru. / Efficient CTMC Model Checking of Linear Real-Time Objectives. 15 p.
@conference{29a232e7315240bf9f312be85c797a08,
title = "Efficient CTMC Model Checking of Linear Real-Time Objectives",
abstract = "This paper makes verifying continuous-time Markov chains (CTMCs) against deterministic timed automata (DTA) objectives practical. We show that verifying 1-clock DTA can be done by analyzing subgraphs of the product of CTMC C and the region graph of DTA A. This improves upon earlier results and allows to only use standard analysis algorithms. Our graph decomposition approach naturally enables bisimulation minimization as well as parallelization. Experiments with various examples confirm that these optimizations lead to significant speed-ups. We also report on experiments with multiple-clock DTA objectives. The objectives and the size of the problem instances that can be checked with our prototypical tool go (far) beyond what could be checked so far.",
keywords = "IR-79389, EWI-21247",
author = "Benoit Barbot and T. Chen and Tingting Han and Katoen, {Joost P.} and Alexandru Mereacre",
year = "2011",
month = "3",
doi = "10.1007/978-3-642-19835-9_12",
language = "Undefined",
pages = "128--142",

}

Efficient CTMC Model Checking of Linear Real-Time Objectives. / Barbot, Benoit; Chen, T.; Han, Tingting; Katoen, Joost P.; Mereacre, Alexandru.

2011. 128-142.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

T1 - Efficient CTMC Model Checking of Linear Real-Time Objectives

AU - Barbot, Benoit

AU - Chen, T.

AU - Han, Tingting

AU - Katoen, Joost P.

AU - Mereacre, Alexandru

PY - 2011/3

Y1 - 2011/3

N2 - This paper makes verifying continuous-time Markov chains (CTMCs) against deterministic timed automata (DTA) objectives practical. We show that verifying 1-clock DTA can be done by analyzing subgraphs of the product of CTMC C and the region graph of DTA A. This improves upon earlier results and allows to only use standard analysis algorithms. Our graph decomposition approach naturally enables bisimulation minimization as well as parallelization. Experiments with various examples confirm that these optimizations lead to significant speed-ups. We also report on experiments with multiple-clock DTA objectives. The objectives and the size of the problem instances that can be checked with our prototypical tool go (far) beyond what could be checked so far.

AB - This paper makes verifying continuous-time Markov chains (CTMCs) against deterministic timed automata (DTA) objectives practical. We show that verifying 1-clock DTA can be done by analyzing subgraphs of the product of CTMC C and the region graph of DTA A. This improves upon earlier results and allows to only use standard analysis algorithms. Our graph decomposition approach naturally enables bisimulation minimization as well as parallelization. Experiments with various examples confirm that these optimizations lead to significant speed-ups. We also report on experiments with multiple-clock DTA objectives. The objectives and the size of the problem instances that can be checked with our prototypical tool go (far) beyond what could be checked so far.

KW - IR-79389

KW - EWI-21247

U2 - 10.1007/978-3-642-19835-9_12

DO - 10.1007/978-3-642-19835-9_12

M3 - Paper

SP - 128

EP - 142

ER -