Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2011-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/697/pdf |
| _version_ | 1797268752157376512 |
|---|---|
| author | Taolue Chen Tingting Han Joost-Pieter Katoen Alexandru Mereacre |
| author_facet | Taolue Chen Tingting Han Joost-Pieter Katoen Alexandru Mereacre |
| author_sort | Taolue Chen |
| collection | DOAJ |
| description | We study the verification of a finite continuous-time Markov chain (CTMC) C
against a linear real-time specification given as a deterministic timed
automaton (DTA) A with finite or Muller acceptance conditions. The central
question that we address is: what is the probability of the set of paths of C
that are accepted by A, i.e., the likelihood that C satisfies A? It is shown
that under finite acceptance criteria this equals the reachability probability
in a finite piecewise deterministic Markov process (PDP), whereas for Muller
acceptance criteria it coincides with the reachability probability of terminal
strongly connected components in such a PDP. Qualitative verification is shown
to amount to a graph analysis of the PDP. Reachability probabilities in our
PDPs are then characterized as the least solution of a system of Volterra
integral equations of the second type and are shown to be approximated by the
solution of a system of partial differential equations. For single-clock DTA,
this integral equation system can be transformed into a system of linear
equations where the coefficients are solutions of ordinary differential
equations. As the coefficients are in fact transient probabilities in CTMCs,
this result implies that standard algorithms for CTMC analysis suffice to
verify single-clock DTA specifications. |
| first_indexed | 2024-04-25T01:37:28Z |
| format | Article |
| id | doaj.art-308863269a364332b2c4f17995430fce |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:28Z |
| publishDate | 2011-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-308863269a364332b2c4f17995430fce2024-03-08T09:14:52ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742011-03-01Volume 7, Issue 110.2168/LMCS-7(1:12)2011697Model Checking of Continuous-Time Markov Chains Against Timed Automata SpecificationsTaolue ChenTingting HanJoost-Pieter Katoenhttps://orcid.org/0000-0002-6143-1926Alexandru MereacreWe study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such a PDP. Qualitative verification is shown to amount to a graph analysis of the PDP. Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations. For single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations. As the coefficients are in fact transient probabilities in CTMCs, this result implies that standard algorithms for CTMC analysis suffice to verify single-clock DTA specifications.https://lmcs.episciences.org/697/pdfcomputer science - logic in computer scienced.2.4 |
| spellingShingle | Taolue Chen Tingting Han Joost-Pieter Katoen Alexandru Mereacre Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications Logical Methods in Computer Science computer science - logic in computer science d.2.4 |
| title | Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications |
| title_full | Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications |
| title_fullStr | Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications |
| title_full_unstemmed | Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications |
| title_short | Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications |
| title_sort | model checking of continuous time markov chains against timed automata specifications |
| topic | computer science - logic in computer science d.2.4 |
| url | https://lmcs.episciences.org/697/pdf |
| work_keys_str_mv | AT taoluechen modelcheckingofcontinuoustimemarkovchainsagainsttimedautomataspecifications AT tingtinghan modelcheckingofcontinuoustimemarkovchainsagainsttimedautomataspecifications AT joostpieterkatoen modelcheckingofcontinuoustimemarkovchainsagainsttimedautomataspecifications AT alexandrumereacre modelcheckingofcontinuoustimemarkovchainsagainsttimedautomataspecifications |