| AL-SMC: Optimizing Statistical Model Checking by Automatic Abstraction and Learning |
| Download PDF |
| Kaiqiang Jiang,Ping Huang,Hui Zan,Dehui Du. AL-SMC: Optimizing Statistical Model Checking by Automatic Abstraction and Learning. International Journal of Software and Informatics, 2016,10(4):0 |
| Hits: 2984 |
| Download times: 1274 |
|
|
| Abstract:Statistical Model Checking (SMC), as a technique to mitigate the issue of state space explosion in numerical probabilistic model checking, can efficiently obtain an approximate result with an error bound by statistically analysing the simulation traces. SMC however may become very time consuming due to the generation of an extremely large number of traces in some cases. Improving the performance of SMC effectively is still a challenge. To solve the problem, we propose an optimized SMC approach called AL-SMC which effectively reduces the required sample traces, thus to improve the performance of SMC by automatic abstraction and learning. First, we present property-based trace abstraction for simplifying the cumbersome traces drawn from the original model. Second, we learn the analysis model called Prefix Frequency Tree (PFT) from the abstracted traces, and optimize the PFT using the two-phase reduction algorithm. By means of the optimized PFT, the original probability space is partitioned into several sub-spaces on which we evaluate the probabilities parallelly in the final phase. Besides, we analyse the core algorithms in terms of time and space complexity, and implement AL-SMC in our Modana Platform to support the automatic process. Finally we discuss the experiment results for the case study :energy-aware building which shows that the number of sample traces is effectively reduced (by nearly 20\% to 50\%) while ensuring the accuracy of the result with an acceptable error. |
| keywords:statistical model checking statistical abstraction learning principal components analysis prefix frequency tree |
| View Full Text View/Add Comment Download reader |
|
|
|
