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

• Model checking
• Stochastic model checking
• Probabilistic models
• Continuous-time Markov Chains (CTMC)
• Infinite-state probabilistic models

Type of tool

Model checker

Expected input

• Infinite-state CTMC model
• Property/properties to check

Format:

• Model: PRISM format (.prism or .sm file)
• Properties: PRISM's Property Specification format (.csl file)

Expected output

Lower and upper bound probabilities for which the property holds.

Internals

Uses PRISM