We study the verification of a finite continuous-time Markov chain (CTMC) Cagainst a linear real-time specification given as a deterministic timedautomaton (DTA) A with finite or Muller acceptance conditions. The centralquestion that we address is: what is the probability of the set of paths of Cthat are accepted by A, i.e., the likelihood that C satisfies A? It is shownthat under finite acceptance criteria this equals the reachability probabilityin a finite piecewise deterministic Markov process (PDP), whereas for Mulleracceptance criteria it coincides with the reachability probability of terminalstrongly connected components in such a PDP. Qualitative verification is shownto amount to a graph analysis of the PDP. Reachability probabilities in ourPDPs are then characterized as the least solution of a system of Volterraintegral equations of the second type and are shown to be approximated by thesolution of a system of partial differential equations. For single-clock DTA,this integral equation system can be transformed into a system of linearequations where the coefficients are solutions of ordinary differentialequations. As the coefficients are in fact transient probabilities in CTMCs,this result implies that standard algorithms for CTMC analysis suffice toverify single-clock DTA specifications.
展开▼
