Approximate symbolic model checking of continous-time Markov chains

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

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
StatePublished - 1999
Event10th International Conference on Concurrency Theory, CONCUR 1999 - Eindhoven, Netherlands

Conference

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

Fingerprint

Logic
Operator
Symbolic model checking
Time operator
Continuous-time Markov chain
Decision diagrams
Volterra integral equations
Quadrature formula
Bounded operator
System of linear equations
Numerical integration
Model checking
Express

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.DOI: 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.

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

Research output: Scientific - peer-reviewPaper

@misc{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",
pages = "146--162",

}

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. DOI: 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: Scientific - peer-reviewPaper

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. Available from, DOI: 10.1007/3-540-48320-9