This page contains additional information on our article “Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT”. More precisely, we describe our implementation and our experiments.
Implementation
Our implementation in our new version of KoAT can be executed via web interfaces, via a Docker image, and via a provided static binary. See our documentation for a list of external tools and libraries used by KoAT. A direct link to the source code of new prob-CFR-release of KoAT, as well as to the static binary and the Docker image can be found here. A direct link to the web interface of KoAT’s prob-CFR-release for probabilistic integer programs is here.
Concerning the input format, for integer programs we use the corresponding input format from the Termination and Complexity Competition as described here. Note that a disjunction is modeled by two parallel transitions with the same update, and negations are modeled by flipping every comparator (i.e., ¬(x<y) is equivalent to x≥y). Additionally, we also allow for costs in transitions as described here.
Details on the input format of probabilistic integer programs are described here.
Our implementation of the control-flow refinement algorithm can also be used as a black box for other tools.
To this end, KoAT can be executed by the subcommand cfr.
The input file must be specified by the flag -i whereas the output flag -o is optional.
If the output flag is omitted, then the resulting program is written to the standard output.
For probabilistic programs, either the flag --probabilistic or -pmust be used.
Furthermore, --refinement-locations can be used to specify a list of comma-separated locations.
Then, CFR is only applied modularly to transitions which have both start and target location in the given list.
For example, the command ./koat2_static cfr --refinement-locations l1,l2 -p -i cfr02.koat -o result.koat uses our static binary and applies CFR to the leading example of our paper (see here) locally to all transitions between locations l1 and l2 and stores the result in the file result.koat.
Experiments
To evaluate the power and performance of our approach, we tested it on the 75 benchmarks from here.
Moreover, we added 15 new benchmarks including our leading example and problems from the Termination Problem Data Base (see here), e.g., a probabilistic version of McCarthy’s 91 function, which demonstrate the benefits of (probabilistic) CFR. In particular, our benchmarks also contain more involved examples where CFR is useful even if it cannot separate probabilistic from non-probabilistic program parts as in our leading example.
See here for a detailed description of our new benchmarks. Moreover, we provide a zip file containing all our 90 benchmarks and their translation into the format of Absynth and eco-imp. Since Absynth and eco-imp do not allow temporary variables, we model them with (cost-free) loops which initialize a corresponding variable non-deterministically.
We compare the runtime bounds computed by the tools asymptotically as functions which depend on the largest initial absolute value n of all program variables. KoAT and eco-imp were run inside an Ubuntu Docker container. All tools were evaluated on a machine with an AMD Ryzen 7 3700X octa-core CPU and 48 GB of RAM. The benchmarks were evaluated in parallel such that at most 8 containers were running at once, each limited to 1.9 CPU cores. In particular, the runtimes of the tools include the times to set-up the environment (e.g., start the docker container). We give both the average runtime of each tool on all runs and the average runtime on successful runs, i.e., where the tool inferred a finite runtime bound before reaching the timeout. A timeout of 5 minutes was enforced for every tool and program.
We compare the results of our tool KoAT in different configurations to the results of the tools Abysnth and eco-imp. Please click on the tool names to obtain a detailed list of all results or to download the output of the corresponding configuration. Note that for all configurations of KoAT, the integer programs in the output have been rendered as graphs using Graphviz.
| Tool | O(1) | O(n) | O(n²) | O(nᵏ), k>2 | O(EXP) | < ∞ | Avg. Runtime on Successful Runs | Avg. Runtime on All Runs |
|---|---|---|---|---|---|---|---|---|
| KoAT + CFR | 11 (2) | 56 (12) | 14 | 2 | 1 | 84 (14) | 11.68 s | 11.34 s |
| KoAT | 9 | 41 (1) | 16 (1) | 2 | 1 | 69 (2) | 2.71 s | 2.41 s |
| Abysnth | 7 | 35 | 9 | 0 | 0 | 51 | 2.86 s | 37.48 s |
| eco-imp | 8 | 35 | 6 | 0 | 0 | 49 | 0.34 s | 68.02 s |