LTL Model Checking of Time-Inhomogeneous Markov Chains


Taolue Chen


10 December 09






We investigate the problem of verifying linear-time properties against inhomogeneous continuous-time Markov chains (ICTMCs). A fundamental question we address is how to compute reachability probabilities. We consider two variants: time-bounded and unbounded reachability. It turns out that both can be characterized as the least solution of a system of integral equations. We show that for the time-bounded case, the obtained integral equations can be transformed into a system of ordinary differential equations; for the time-unbounded case, we identify two sufficient conditions, namely the eventually periodic assumption and the eventually uniform assumption, under which the problem can be reduced to solving a time-bounded reachability problem for the ICTMCs and a reachability problem for a DTMC. These results provide the basis for a model checking algorithm for LTL. Under the eventually stable assumption, we show how to compute the probability of a set of ICTMC paths which satisfy a given LTL formula. By an automata-based approach, we reduce this problem to the previous established results for reachability problems.