Time-Bounded Verification Of Ctmcs Against Real-Time Specifications

In this paper we study time-bounded verification of a finite continuous-time Markov chain (CTMC) C against a real-time specification, provided either as a metric temporal logic (MTL) property phi, or as a timed automaton (TA) A. The key question is: what is the probability of the set of timed paths of C that satisfy phi (or are accepted by A) over a time interval of fixed, bounded length? We provide approximation algorithms to solve these problems. We first derive a bound N such that timed paths of C with at most N discrete jumps are sufficient to approximate the desired probability up to epsilon. Then, for each discrete (untimed) path sigma of length at most N, we generate timed constraints over variables determining the residence time of each state along sigma, depending on the real-time specification under consideration. The probability of the set of timed paths, determined by the discrete path and the associated timed constraints, can thus be formulated as a multidimensional integral. Summing up all such probabilities yields the result. For MTL, we consider both the continuous and the pointwise semantics. The approximation algorithms differ mainly in constraints generation for the two types of specifications.