Approximate symbolic model checking of continous-time Markov chains

Christel Baier, J.C.M. Baeten (Editor), S. Mauw (Editor), Joost P. Katoen, H. Hermanns

    Research output: Contribution to conferencePaper

    Abstract

    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.
    Original languageUndefined
    Pages146-162
    Number of pages17
    DOIs
    Publication statusPublished - 1999
    Event10th International Conference on Concurrency Theory, CONCUR 1999 - Eindhoven, Netherlands
    Duration: 24 Aug 199927 Aug 1999
    Conference number: 10

    Conference

    Conference10th International Conference on Concurrency Theory, CONCUR 1999
    Abbreviated titleCONCUR
    CountryNetherlands
    CityEindhoven
    Period24/08/9927/08/99

    Keywords

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

    Cite this