Adaptive formal approximations of Markov chains

• https://www.sciencedirect.com/science/article/pii/S0166531621000249

Markov models,  Probabilistic model checking,  Approximation techniques, 
Adaptive aggregation

We explore formal approximation techniques for Markov chains based on state-space
reduction that aim at improving the scalability of the analysis, while providing
formal bounds on the approximation error. We first present a comprehensive survey
of existing state-reduction techniques based on clustering or truncation. Then,
we extend existing frameworks for aggregation-based analysis of Markov chains by
allowing them to handle chains with an arbitrary structure of the underlying
state space - including continuous-time models - and improve upon existing bounds
on the approximation error. Finally, we introduce a new hybrid scheme that
utilises both aggregation and truncation of the state space and provides the best
available approach for approximating continuous-time models. We conclude with
a broad and detailed comparative evaluation of existing and new approximation
techniques and investigate how different methods handle various Markov models.
The results also show that the introduced hybrid scheme significantly outperforms
existing approaches and provides a speedup of the analysis up to a factor of 30
with the corresponding approximation error bounded within 0.1%.