On-the-fly verification and optimization of DTA-properties for large Markov chains

We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies.