PV3 STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysischecks properties on continuous-time Markov chains

Infinite-state CTMC (Continuous-time Markov Chain) model checker

Application domain/field

Type of tool

Model checker

Expected input

Format:

Expected output

Lower and upper bound probabilities for which the property holds.

Internals

Uses PRISM
Model checking Probabilistic

Links

Repository: https://github.com/fluentverification/stamina

Last commit date

27 October 2021

Related papers

https://doi.org/10.1007/978-3-030-25540-4_31 (CAV '19)

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.