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. |
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. |
|
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 |