Long-run Rewards for Markov Automata (supplementary material)

This webpage contains supplementary materials related to our TACAS’17  paper. An author-generated open-access version of that paper is available as ERC-POWVER-TechRep-2017-02.pdf

Reproducing the experiments

In order to reproduce the results of our paper we provide the virtual machine that includes the implementation of our algorithm as a part of IMCA tool, together with all the case studies used. In order to run the virtual machine one needs Virtual Box (we worked with version 5.1.4). First, import the appliance debian_public.ova. This will create a virtual machine called debian_public. Then start that machine. You will find 2 users available with login/passwd:

  1. root/root
  2. tacas17/tacas17

Login with any of the above mentioned users.
The implementation and the benchmarks are available in /home/tacas17/implementation. Navigate to this folder and either read the README file, or just run ./bin/imca.