Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT

TL;DR

The paper addresses automated complexity analysis for probabilistic programs by extending control-flow refinement (CFR) to the probabilistic setting and embedding it natively into KoAT. It presents a novel CFR algorithm for probabilistic integer programs that uses abstract labeling of locations and a finite abstraction layer to ensure termination, preserving the original program's expected runtime upper bound. The method is implemented inside KoAT and evaluated against probabilistic benchmarks, showing substantially improved bound power, including a finite expected-runtime bound on 84 of 90 examples and linear $O(n)$ bounds on 56 of those. While CFR can increase analysis time due to larger translated programs, the results demonstrate that CFR significantly enhances automated complexity analysis for probabilistic programs and can be adopted by other tools as a black-box technique.

Abstract

Recently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, in this paper we extend CFR to probabilistic programs and show its soundness for complexity analysis. To demonstrate its benefits, we implemented our new CFR technique in our complexity analysis tool KoAT.