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

    Baier, C., Baeten, J. C. M. (Ed.), Mauw, S. (Ed.), Katoen, J. P., & Hermanns, H. (1999). Approximate symbolic model checking of continous-time Markov chains. 146-162. Paper presented at 10th International Conference on Concurrency Theory, CONCUR 1999, Eindhoven, Netherlands. https://doi.org/10.1007/3-540-48320-9
    Baier, Christel ; Baeten, J.C.M. (Editor) ; Mauw, S. (Editor) ; Katoen, Joost P. ; Hermanns, H. / Approximate symbolic model checking of continous-time Markov chains. Paper presented at 10th International Conference on Concurrency Theory, CONCUR 1999, Eindhoven, Netherlands.17 p.
    @conference{04a978a7b0454547a600df91e6b8d85b,
    title = "Approximate symbolic model checking of continous-time Markov chains",
    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.",
    keywords = "FMT-MC: MODEL CHECKING, FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, IR-63300, FMT-BDD: BINARY DECISION DIAGRAMS, EWI-6483",
    author = "Christel Baier and J.C.M. Baeten and S. Mauw and Katoen, {Joost P.} and H. Hermanns",
    year = "1999",
    doi = "10.1007/3-540-48320-9",
    language = "Undefined",
    pages = "146--162",
    note = "null ; Conference date: 24-08-1999 Through 27-08-1999",

    }

    Baier, C, Baeten, JCM (ed.), Mauw, S (ed.), Katoen, JP & Hermanns, H 1999, 'Approximate symbolic model checking of continous-time Markov chains' Paper presented at 10th International Conference on Concurrency Theory, CONCUR 1999, Eindhoven, Netherlands, 24/08/99 - 27/08/99, pp. 146-162. https://doi.org/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.

    1999. 146-162 Paper presented at 10th International Conference on Concurrency Theory, CONCUR 1999, Eindhoven, Netherlands.

    Research output: Contribution to conferencePaper

    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 -

    Baier C, Baeten JCM, (ed.), Mauw S, (ed.), Katoen JP, Hermanns H. Approximate symbolic model checking of continous-time Markov chains. 1999. Paper presented at 10th International Conference on Concurrency Theory, CONCUR 1999, Eindhoven, Netherlands. https://doi.org/10.1007/3-540-48320-9