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

Abstract

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.

@article{mikeevOnTheFlyVerificationAndOptimization2013,
 author = {Linar Mikeev and Martin R. Neuhäußer and David Spieler and Verena Wolf},
 doi = {10.1007/s10703-012-0165-1},
 editor = {Nicht bekannt},
 journal = {Formal Methods in System Design},
 month = {10},
 number = {2},
 pages = {313-337},
 publisher = {Springer US, USA},
 title = {On-the-fly verification and optimization of DTA-properties for large Markov chains},
 volume = {43},
 year = {2013}
}