lter

 

Subproject

S3

Categories

Model checker / solver for probabilistic systems

Overview

lter ("long-term expected rewards") computes for a Markov decision process the average reward per step in the long run. It is the implementation of a variant of Howard and Veinott's classical algorithm which intertwines symbolic and explicit data structures and algorithms in order to reduce the memory consumption with little overhead on the runtime.

Publications

R. Wimmer, B. Braitling, B. Becker, E.M. Hahn, P. Crouzen, H. Hermanns, A. Dhama, and O. Theel. Symblicit calculation of long-run averages for concurrent probabilistic systems. In Gianfranco Ciardo and Roberto Segala, editors, Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST), pages 27–36, 2010. 

Benchmarks

Self-stabilizing Minimal Spanning-Tree Algorithm

Download

Click here for the sources.

Manual

Just type ./lter on the command line to see how it can be used.

Status

Prototype