Continuous Optimal Timing
This webpage contains information concerning experiments with computation of time-bounded reachabilities for continuous time Markov decision processes.
It provides supplementary materials for our ATVA 2015 submission. Everything needed for reproducing the experiments in the paper
including the binary files, libraries are bundled in a VirtualBox image and can be downloaded
from here. Some case study sources are included in the bundle, others can be downloaded from this webpage.
Installation and running:
- Import the bundle mentioned above into your VirtualBox via File->Import Appliance...
- Run the cav285_amd64 virtual machine
- Log in as user cav285 with password cav285
- Navigate to /home/cav285/cav285/tbr
- Run ./tbr without command line arguments to print out usage information
Case Studies:
Comprehensive tables of experiments:
Notes:
- The size of state space and goal set in the tables are denoted by |S| and |G|, respectively.
- For Unif+ (referred by U+ in the tables) we report the number of iterations and the accuracy of the last iteration as well as computation time.
- In the tables, AS(a) and AS(na) stand for two variants of adaptive step algorithm. Shortly speaking, for AS(na) in every step, a fixed number of higher order derivatives is considered to estimate the next step size. The number however might be variable along diffrent steps for AS(a). In the paper AS denotes the best of AS(a) and AS(na).
- For some of the experiments you may encounter the "timeout" value in the runtime section. It means that the running time of the algorithm exceeded the selected timeout and we stopped it prematurely. We chose the timeout value to be 15 minutes (900 seconds).
