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