Selection of Model Checking Strategies using Machine Learning

Organisation:	University of Twente, The Netherlands
Method:	PNML
Tools used:	LTSmin CADP (Construction and Analysis of Distributed Processes) Scikit-Learn
Domain:	Machine Learning.
Period:	2018-2019
Size:	532 PNML models
Description:	State space methods provide an automated way of verifying models. However, these methods suffer from the state space explosion problem. Many methods have been developed to cope with this problem. As a result, a user has many different strategies to apply state space methods to models. Because there is such a large amount of different strategies, it is hard for a user to select an appropriate strategy. If a bad strategy is selected, the model may be unsolvable, or waste resources. Additionally, the necessary intervention of a user makes the process of validation less automated. Therefore, it would be useful if the model checker itself is able to select an appropriate strategy. To allow the model checker to predict a suitable strategy, it needs to use information present in the model itself. This research investigates to what extent the characteristics of Petri Net models can be used to predict an appropriate strategy. The study considered 532 different Petri net models represented in PNML. The performance of each model, for 20 selected strategies, was determined using LTSMin. Then, to collect its necessary features, each model was first converted from the PNML to the NUPN format by applying the PNML2NUPN tool, and then was fed to the CAESAR.BDD tool of CADP. Once this process was finished, the performance data of every model for each strategy was combined with the feature set collected by CAESAR.BDD. This resulted in 20 datasets, each one containing the name of a model, the features collected for that model, and the average exploration time for a particular strategy. This data was used to create a regressor for every strategy, which predicts the expected runtime when that strategy is applied to a given model. These regressors were then combined into a single classifier which could predict an appropriate strategy. The classifier was compared to the best single strategy, and was shown to predict a strategy which outperforms this fixed strategy in 17% of the predictions, and results in an average time loss of 12.95 seconds.
Conclusions:	The performance of the classifier can be improved by increasing the accuracy of its component regressors. Since some of the regressors perform quite well (with scores of 0.95), the lack of performance may stem from a lack of data rather than a lack of features. Therefore, the first step to improving this classifier would be to collect more data, for instance by allowing a greater time limit for the model checking runs on each PNML model. In addition, this data would be way more varied, since the longer exploration times of big models would also be included.
Publications:	[Hendriks-19] Max Hendriks. "Can Machine Learning Automatically Choose your Best Model Checking Strategy?" BSc Thesis, EEMCS: Electrical Engineering, Mathematics and Computer Science, University of Twente, 2019. Available on-line at: https://essay.utwente.nl/77600/1/Hendriks_BA_EEMCS.pdf or from the CADP Web site in PDF or PostScript
Contact:	Max Hendriks University of Twente Faculty of Electrical Engneering, Mathematics and Computer Science Zilverling building Drienerlolaan 5 7522 NB Enschede The Netherlands Email: m.a.hendriks@student.utwente.nl
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page