Less is more: Estimating probabilistic rewards over partial system explorations
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 (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both i...
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | JOUR |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_1049331X_v25_n2_p_Pavese |
| Aporte de: |
| id |
todo:paper_1049331X_v25_n2_p_Pavese |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_1049331X_v25_n2_p_Pavese2023-10-03T15:58:38Z Less is more: Estimating probabilistic rewards over partial system explorations Pavese, E. Braberman, V. Uchitel, S. Estimation Model checking Partial verification Probability Quantitativemodelling Estimation Probability Turnaround time Mean time to first failure Partial verification Probabilistic model checking Quantitative measures Quantitativemodelling Reliability estimation Statistical model checking Systematic exploration Model checking 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 (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space, and precision. In this article, 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 nondeterminism) can be more effective than (full-model) probabilistic and statistical model checking, especially for system models for which the events of interest are rare. © 2016 ACM. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_1049331X_v25_n2_p_Pavese |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Estimation Model checking Partial verification Probability Quantitativemodelling Estimation Probability Turnaround time Mean time to first failure Partial verification Probabilistic model checking Quantitative measures Quantitativemodelling Reliability estimation Statistical model checking Systematic exploration Model checking |
| spellingShingle |
Estimation Model checking Partial verification Probability Quantitativemodelling Estimation Probability Turnaround time Mean time to first failure Partial verification Probabilistic model checking Quantitative measures Quantitativemodelling Reliability estimation Statistical model checking Systematic exploration Model checking Pavese, E. Braberman, V. Uchitel, S. Less is more: Estimating probabilistic rewards over partial system explorations |
| topic_facet |
Estimation Model checking Partial verification Probability Quantitativemodelling Estimation Probability Turnaround time Mean time to first failure Partial verification Probabilistic model checking Quantitative measures Quantitativemodelling Reliability estimation Statistical model checking Systematic exploration Model checking |
| description |
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 (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space, and precision. In this article, 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 nondeterminism) can be more effective than (full-model) probabilistic and statistical model checking, especially for system models for which the events of interest are rare. © 2016 ACM. |
| format |
JOUR |
| author |
Pavese, E. Braberman, V. Uchitel, S. |
| author_facet |
Pavese, E. Braberman, V. Uchitel, S. |
| author_sort |
Pavese, E. |
| title |
Less is more: Estimating probabilistic rewards over partial system explorations |
| title_short |
Less is more: Estimating probabilistic rewards over partial system explorations |
| title_full |
Less is more: Estimating probabilistic rewards over partial system explorations |
| title_fullStr |
Less is more: Estimating probabilistic rewards over partial system explorations |
| title_full_unstemmed |
Less is more: Estimating probabilistic rewards over partial system explorations |
| title_sort |
less is more: estimating probabilistic rewards over partial system explorations |
| url |
http://hdl.handle.net/20.500.12110/paper_1049331X_v25_n2_p_Pavese |
| work_keys_str_mv |
AT pavesee lessismoreestimatingprobabilisticrewardsoverpartialsystemexplorations AT brabermanv lessismoreestimatingprobabilisticrewardsoverpartialsystemexplorations AT uchitels lessismoreestimatingprobabilisticrewardsoverpartialsystemexplorations |
| _version_ |
1807319729220616192 |