Efficient CTMC Model Checking of Linear Real-Time Objectives

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

    Research output: Contribution to conferencePaperpeer-review

    32 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
    Event17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011 - Saarbrücken, Germany
    Duration: 26 Mar 20113 Apr 2011

    Conference

    Conference17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011
    Period26/03/113/04/11
    Other26 March - 3 April 2011

    Keywords

    • IR-79389
    • EWI-21247

    Cite this