Model-based reliability estimation of systems can provide useful insights early in the development process.
However, computational complexity of estimating metrics such as mean time to first failure (MTTF),
turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space
and precision. In this paper we present an alternative to exhaustive model exploration–as in probabilistic
model checking–and partial random exploration–as in statistical model checking. Our hypothesis is that
a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these
quantitative model metrics at lower computation cost. We present a novel automated technique for metric
estimation that combines simulation, invariant inference and probabilistic model checking. Simulation
produces a probabilistically relevant set of traces from which a state invariant is inferred. The invariant
characterises a partial model which is then exhaustively explored using probabilistic model checking. We
report on experiments that suggest that metric estimation using this technique (for both fully probabilistic
models and those exhibiting non-determinism) can be more effective than (full model) probabilistic and
statistical model checking especially for system models where the events of interest are rare.