This repository contains the models and the properties used for the experimental evaluation of An MM Algorithm to Estimate Parameters in Continuous-Time Markov Chains.
All these models are modified version of model originally from the Quantitative Verification Benchmark Set.
| Model | #States | #non-zero transitions | #parameters to estimate |
|---|---|---|---|
| pollling | 240 | 800 | 2 |
| cluster | 276 | 1120 | 3 |
| tandem | 780 | 2583 | 4 |
| philosophers | 1065 | 4141 | 3 |
| philosophers-gamma | 1065 | 4141 | 4 |