HyperPCTL Model Checking by Probabilistic Decomposition

Probabilistic hyperproperties describe system properties involving probability measures over multiple runs and have numerous applications in information-flow security. However, the poor scalability of existing model checking algorithms for probabilistic hyperproperties limits their use to small models. In this paper, we propose a model checking algorithm to verify discrete-time Markov chains (DTMC) against HyperPCTL formulas by integrating numerical solution techniques. Our algorithm is based on a probabilistic decomposition of the self-composed DTMC into variants of the underlying DTMC. Experimentally, we show that our algorithm significantly outperforms both a symbolic approach and the original approach based on brute-force self-composition.