We introduce the class of *constant probability (CP)
programs*
and show that classical results from probability theory directly yield a
simple decision procedure for (positive) almost sure termination of programs in this class. Moreover, asymptotically tight bounds on their expected runtime can always be computed easily. Based on this, we present
an algorithm to infer the *exact*
expected runtime of any CP program.

Here is the full version of our paper Computing Expected Runtimes for Constant Probability Programs (including all proofs and a collection of examples to demonstrate the application of our algorithm).

We implemented our algorithm to determine the exact expected runtime of CP programs in our tool **KoAT**, which was already one of the leading tools
for complexity analysis of (non-probabilistic) integer programs, cf. our corresponding
ACM TOPLAS paper.
The implementation is
written in OCaml and
uses the open source Python libraries SymPy and MpMath as back-end for computing the
roots of the characteristic polynomial numerically, for solving linear equations,
and for the transformation of the complex roots to polar representation. Furthermore, the
full version of **KoAT** also
uses the SMT solver Z3
and the invariant
generator APRON. However, these tools are
not called when computing exact expected runtimes.

We provide our implementation (i.e., a special-purpose version of **KoAT**)
as a Docker container. To use it,
you first have to install Docker CE.
Docker is available for Windows, Mac, and Linux. After installing Docker CE, please proceed as follows:

- Start Docker
- Pull the latest Docker image of
**KoAT**. You have to download about 50 MB. The extracted image has about 150 MB. To this end, please use the following command:

`docker pull aprove/exact_runtime:latest`

If you are connected to a network with a firewall (e.g., networks of academic institutions) this might not work as the default DNS configuration of the Docker daemon is inadequate. Please see the Docker Network Configuration for details. - Alternatively, you can download the latest version of
the Docker image of
**KoAT**(~150 MB) here. The link directs to the file-sharing system Sciebo, a joint project by 26 German universities. After downloading the file`exact_runtime.zip`, please change to the directory where you stored the file and execute:`docker load --input=exact_runtime.zip`

If the Docker image was successfully imported (this may take a minute),`Loaded image: aprove/exact_runtime:latest`is prompted to your shell.

Our tool uses a special input format. The input is a file
with the ending `.koat`.
This file consists of 7 parts, which are described in the following:

- The first line specifies that we want to compute the
exact runtime of a CP
program. Therefore, the first line should be:
`(GOAL EXACTRUNTIME)` - In the second and third line, we specify the loop guard of
the simple program. For instance,
`(GUARDVEC (1,-1))`specifies the vectorfrom the paper, i.e., it means that we have two program variables*a**x1*and*x2*and the guard of the loop is*1*x1 +(-1)*x2 > b*where*b*will be specified in the next line. Note that`GUARDVEC`has to be a tuple. So it has to be enclosed by round brackets, even if it is one-dimensional. - As already mentioned, the third line specifies the
value
*b*in the loop guard, which is an arbitrary integer number. For instance, to set*b=2*, one has to write`(GUARDVAL 2)`. - The fourth line contains the updates of the program
variables in the loop body. The updates
are of the form
*p*:, where*c**p*is a rational probability andis the update tuple which is added to the variables with probability*c**p*. Asis a tuple, it has to be enclosed by round brackets, even if it is one-dimensional. The updates are separated by "*c**:+:*". For example`(UPDATES 1/5:(1,2) :+: 4/5:(-3,0))`means that in each loop iteration,*x1*is increased by*1*and*x2*is increased by*2*with probability*1/5*, whereas*x1*is decreased by*3*and*x2*stays unchanged with probability*4/5*. - The fifth line is optional and specifies the probability for
direct termination. It has the
form
*p'*:, where*d**p'*is a rational probability andare integer values which lead to direct termination. As*d*is a tuple, it has to be enclosed by round brackets, even if it is one-dimensional. If the program does not have direct termination, one can omit this line or just write*d*`(DIRECTTERMINATION 0:(0,0))`. Note that the probabilities of the updates in the fourth line and the probability*p'*must add up to 1. Otherwise, our implementation stops with an error message. Moreover, it also gives an error message if*p' > 0*andsatisfies the loop condition (i.e., if setting the program variables to*d*does not lead to direct termination).*d* - The next line is used for adjusting the precision. For
example,
`(PRECISION 10)`means that our algorithm performs floating point operations with a precision of 10 decimal places (i.e., in this way the user can select the precision used by MpMath for approximating the roots of the characteristic polynomial). This line is optional as well and the default precision is 100 decimal places. - The last line is used for giving an initial state in which we would like to evaluate the exact_runtime. For
example,
`(INITIAL (4,1))`specifies that we are interested in the expected runtime of the program when started in the initial state*x1=4*and*x2=1*. This line is optional. When it is provided, in addition to the general expected runtime the expected runtime evaluated in the initial state is computed.

Our tool generates an output prompted to the console. This output consists of up to 6 parts, which are described in the following:

- The first line begins with
`RESULT`and contains the expected runtime expressed in the program variables. Here, we only consider the expected runtime for inputs that satisfy the loop condition (for other inputs, the runtime is always 0). - If an initial state was specified which violates the loop guard, the second line is
`WARNING: For the given initial values the program is not executed at all.`If no initial state was specified or the entered initial state does not violate the loop guard, this line is of course omitted. - The third line contains the time needed for the
computation given in seconds. It starts
with
`TIME`. Note that the displayed time is the time SageMath needs to perform the steps of the algorithm presented in the paper. The times (one or two seconds) for starting the container and for starting SageMath are not taken into account. - If an initial state was specified, the next line contains the expected runtime evaluated in the given initial values. The line begins with
`EVALUATION`. - The next line contains the upper bound we gave in our paper for the given program, i.e., a constant if the program has direct termination (cf. Thm. 10) and an affine term if the program has no direct termination (cf. Thm. 21). The line starts with
`UPPER BOUND`. - If the program has no direct termination, the last line presents the linear lower bound (cf. Thm. 21) for the expected runtime, which is made clear by the keyword
`LOWER BOUND`.

Below are all examples from the paper, including the examples
in the appendix. They are provided in **KoAT**'s input format
that we
described above. Moreover, we also provide the resulting output of our
implementation for each of the examples
when running the tool on an Intel Core
i7-6500
with 8 GB memory. In fact, each example could be handled in
less than 1 second.

- Tortoise
and Hare in our Notation (
*P*, Ex. 1) Result_{race} - Tortoise
and Hare Program with Direct Termination
(
*P*, Ex. 11) Result_{direct} - Univariate Tortoise
and Hare Program (
*P*, Ex. 14) Result_{race}^{uni} - Example with Direct Termination and Non-Constant Exact Runtime (Ex. 35) Result
- Example with Complex Roots (Ex. 36) Result
- Example with Root of Higher Multiplicity (Ex. 37) Result
- Negative Binomial Loop (Ex. 38) Result
- Symmetric Random Walk (Ex. 39) Result
- Example with Irrational Runtime (Ex. 40) Result
- Asymmetric Random Walk (Ex. 41) Result
- Program which is not PAST (Ex. 68a) Result
- Program which is not AST (Ex. 68b) Result
- Input Format-Example Result

To run **KoAT**, please proceed as follows:

- Start Docker.
- If you are using Windows, please go to the settings of Docker, select "Shared
Drives", and enable sharing for the local drive where you store the example programs
that you want to analyze with
**KoAT**. - To run
**KoAT**on some example`example.koat`, please use a shell and change the current directory to the directory containing`example.koat`. - If you are
using a Unix-based operating system (e.g., Linux or Mac) or if you are using PowerShell
on Windows,
just execute the following command in your shell.

`docker run --mount type=bind,source="$(pwd)",target=/data aprove/exact_runtime -i /data/example.koat`

It executes the Docker image of**KoAT**on the file`example.koat`in the current directory. Your current directory is mounted into`/data`to enable file sharing. The result is printed on your console together with the time (in seconds) needed for computing the result. - If you are using cmd.exe on Windows, then instead of the above command, please
execute the following command.

`docker run --mount type=bind,source="%cd%",target=/data aprove/exact_runtime -i /data/example.koat`

You can also test our implementation on the examples listed above without file sharing. To do so please proceed as follows:

- Start Docker.
- To run
**KoAT**on some example listed above, please get the name of the example by clicking on the hyperlink. Let us assume that you would like to analyze`input_format.koat`. - Execute the following command in your shell (independent of your operating
system).

`docker run aprove/exact_runtime -i /data/examples/input_format.koat`

It executes the Docker image of**KoAT**on the file`input_format.koat`in the directory`/data/examples`of the Docker image. The result is printed on your console together with the time (in seconds) needed for computing the result.