Statistical Model Checking of Interval Discrete-Time Markov Chain in Systems Biology

Formal analysis on model abstractions of biological processes constructed from experimental data is imprecise and incomplete. The uncertainty in the model is captured by probabilities. The fluctuations due to environmental conditions of the processes, causes imprecision in the probabilities of the processes. In this work, the biological processes are modeled using interval discrete-time Markov chain. The uncertainty in the probabilities is represented in the form of intervals in the interval discrete-time Markov chain. In this work, a tractable formalism for statistical model checking is created. The formalism is based on the approximations of interval discrete-time Markov chain into a set of discrete-time Markov chain. The output from the model checking of the set of discrete-time Markov chain is aggregated with statistical confidence scores. Statistical model checking is performed on a prototype of Galactose pathway as a case study of the formalism. The results elucidate the formalism and provide insights for improvements.