This website contains additional information on our article “Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes”:

- We provide the examples used for our experimental evaluation (in the formats of KoAT and of Absynth and eco-imp, which we used in our experiments).
- We make our tool KoAT available as a Docker image, as a static binary, as a link to the source code,
and via a
**web interface**. - We describe the input format of our tool KoAT.
- In the table at the bottom of this page, we give the detailed results of our experimental evaluation, including the detailed output of the tools KoAT, Absynth, and eco-imp on all examples.

## Abstract

We present a novel modular approach to infer upper bounds on the expected runtime of probabilistic integer programs automatically. To this end, it computes bounds on the runtime of program parts and on the sizes of their variables in an alternating way. To evaluate its power, we implemented our approach in a new version of our open-source tool KoAT.

## References

The full version of our paper can be found on arXiv. The paper itself will appear at TACAS 2021.

## Examples

The examples can be downloaded here. The provided zip file contains all inputs for KoAT, Absynth, and eco-imp as well as plots of the corresponding transition systems automatically generated by our tool KoAT and Graphviz.

## Artifact

An artifact including the examples from the paper and a static binary can be downloaded here. The provided zip-file contains a documentation on how to reproduce our experimental evaluation.

The version of the artifact which was accepted at the TACAS 21 Artifact Evaluation can be found here. This version contains five examples less. Additionally, in this version we did not compare with eco-imp since it was not yet published.

Both versions of “artifact.zip” can be used with the TACAS VM.

## Executing the Implementation

### Docker

A Docker image containing our implementation can be downloaded here.
The image can be loaded into Docker (provided Docker is installed, see here for installation instructions) by changing to the directory where you stored `koat_docker.tar`

and executing:

```
docker load --input=koat_docker.tar
```

The Docker image already contains all provided examples.
For instance, KoAT can be executed on the example `leading.koat`

by running:

```
docker run --rm -t koat:probabilistic -i leading.koat
```

Recall that while we over-approximated the maximum of expressions by their bounds to simplify the presentation in our paper, KoAT also constructs expressions with “max”, which may lead to slightly more precise bounds.

If you want to save KoATs output in a file, this can be achieved by
the usual command line instruction, e.g., `docker run --rm -t koat:probabilistic -i leading.koat > output.txt`

.

Moreover, when executing the Docker image with `run-all`

instead of `-i leading.koat`

, i.e.,
`docker run --rm -t koat:probabilistic run-all`

, KoAT analyzes all provided examples.

Additional examples can be added by mounting a directory.
Assume that the directory `/home/user/examples`

contains an example named `myExample.koat`

.
Then

```
docker run --rm -v '/home/user/examples:/home/koat2/examples:ro' -t koat:probabilistic -i myExample.koat
```

first mounts the directory in the Docker container and then executes KoAT on `myExample.koat`

.

### Static Binary

A static ELF binary, containing all necessary dependencies, can be downloaded here.
Please make sure that the binary is executable by running `chmod +x koat-static`

.
KoAT can then be run on an example by executing

```
/PATH/TO/KOAT/koat-static analyse -i /PATH/TO/EXAMPLES/example.koat
```

#### Additional Flags

Both the Docker image and the static binary can be invoked with additional flags, e.g., for choosing only certain preprocessors, for choosing a different output format, for getting information on the computation process, and many more. To see a detailed description of these flags run

```
docker run koat:probabilistic --help
```

when using the Docker image or

```
/PATH/TO/KOAT/koat-static analyse --help
```

when using the static binary.

For instance, to obtain the automatically generated proof of KoAT instead of just the result of the analysis,
one has to add the flag
`-r all`

at the end of the command (and to get an output in the format of the
Termination and Complexity Competition, one has to add the flag `-r termcomp`

).

### Source Code

The most current version of KoAT is available on GitHub. The source code of our official release version is here.

### Web Interface

Our implementation can also be tested via a web interface using the input format described below. (This web interface is provided via a special version of the web site of our tool AProVE).

- The window “Load Example” shows the PIP that is currently analyzed. The user can modify the PIP or replace it by a new one.
- Moreover, via the “Load Example” button, you can directly choose any of the examples from the collection used in our evaluation, and run KoAT on it.
- In addition, one can also “Upload a File” of a PIP to analyze.
- By choosing “Detailed Format”, one can obtain the automatically generated proof of KoAT instead of just the result of the analysis.
- After viewing the result of KoAT, “Return to program input” takes you back to the web page with the input PIP.

## Input Format

We use an adapted version of the format for *Integer Transition Systems* (see for example here or here) from the Termination and Complexity Competition for our *PIPs*. The leading example from our paper is represented by the following code, where the first and the third transition have the cost 0.

```
(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f))
(VAR x y)
(RULES
f(x,y) -{0}> g(x,y)
g(x,y) -> 0.5:g(x-1,y+x) :+: 0.5:g(x,y+x) :|: x>0
g(x,y) -{0}> h(x,y)
h(x,y) -> h(x,y-1) :|: y>0
)
```

- The first line
`(GOAL EXPECTEDCOMPLEXITY)`

indicates that we would like to compute upper bounds on the**expected runtime**of the given PIP. - The second line
`(STARTTERM (FUNCTIONSYMBOLS f))`

specifies that`f`

is the start location of the PIP. - The third line
`(VAR x y)`

specifies that the variables used in the system are`x`

and`y`

. - The fourth line
`(RULES ...`

indicates that we now state the general transitions of our system. It is ended by a closing parenthesis`)`

in the last line of the example code above. - The remaining lines contain the general transitions of the program in the form
`LHS -{COST}> RHS (:|: GUARD)`

or`LHS -> RHS (:|: GUARD)`

.`LHS`

is the start location of the general transition including the variables to be updated here, e.g.,`f(x,y)`

. Locations are arbitrary alpha-numerical strings.`COST`

is a non-negative integer constant that bounds the cost of the general transition. This is optional. If omitted, the cost defaults to`1`

.`RHS`

specifies the distribution over transitions in the general transition.- Elements of the transition are given by
`p:target(up1,...,upn)`

and are separated by`:+:`

. This means that the variable`x1`

is updated to`up1`

,…, the variable`xn`

is updated to`upn`

, and the system transitions to location`target`

with probability`p`

. - Probabilities are rational numbers strictly greater than 0 which must
*add up to 1*. - In case of a singleton general transition, the probability can be omitted and then defaults to 1, e.g.,
`f(x,y) -{0}> g(x,y)`

. - Updates are
**polynomial**expressions. If the updates contain variables which are not given on the left-hand side, they are treated as non-deterministic (those variables can be restricted in the guard).- For example,
`g(x,y) -> 0.5:g(x-1,y+x) :+: 0.5:g(x,y+x)`

means that from the start location`g`

, with probability 0.5`x`

is set to`x-1`

and`y`

is set to`y+x`

, and with the remaining probability 0.5`x`

is set to`x`

and`y`

is set to`y+x`

. - For example,
`g(x,y) -> 1:g(z,y)`

means that from the start location`g`

, the PIP chooses the transition to location`g`

where the first variable`x`

is updated non-deterministically and the second variable`y`

stays the same.

- For example,
- Updates can also be
**distribution functions**. In our semantics, the value drawn from this distribution is*added*to the current value of the variable.- For example,
`g(x,y) -> g(x,GEOMETRIC(0.5))`

means that in the transition from the location`g`

, the variable`x`

stays the same whereas`y`

is*increased*by a value drawn from a geometric distribution with parameter`0.5`

. - At the moment, we support the following
*discrete distributions*. Here,*parameters*are*integer polynomial expressions*, i.e., they may depend on variables, whereas*constants*are*non-negative integers*or*non-negative*rationals. The user has to ensure that their values meet the stated constraints:- Bernoulli distribution with rational constant
`0 < p < 1`

via`BERNOULLI(p)`

. - Binomial distribution with rational constant
`0 < p < 1`

and a non-negative integer parameter`n`

via`BINOMIAL(n,p)`

. - Geometric distribution with rational constant
`0 < p < 1`

via`GEOMETRIC(p)`

. - Hypergeometric distribution with non-negative integer constant
`N`

and non-negative integer parameters`k,n`

via`HYPERGEOMETRIC(N,k,n)`

. - Uniform distribution with integer parameters
`a < b`

via`UNIFORM(a,b)`

.

- Bernoulli distribution with rational constant

- For example,

- Elements of the transition are given by
`GUARD`

is a conjunction (using the connective`&&`

) of linear (in)equalities representing the guard of the transition, e.g.,`x > 0`

or`x > 0 && 2 * x + 3 * y = 0`

. This is optional. If omitted, GUARD defaults to*true*, e.g.,`g(x,y) -{0}> h(x,y)`

.

## Results

The tables below contain the results of our experiments with our tool KoAT
and the tools Absynth, and
eco-imp.
The output of **KoAT** always has the form `WORST_CASE(a,b)`

where `a`

is a lower bound and `b`

is an upper bound on the expected (worst-case) runtime. Depending on the output format chosen, **KoAT** only depicts asymptotic bounds or both concrete and asymptotic bounds. Currently, KoAT can only infer upper bounds (i.e., the lower bound is always constant).

By clicking on a result in the table, the corresponding output of the tool is shown.
Here, the result of **KoAT** also contains a visualization of the corresponding PIP as a graph. We refer to Sect. 6 in our paper and Sect. A.2 in our technical report for a description of the experiments.