Abstract

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. This would make the process fully automated and ensure that no resources are wasted.

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 performance of 532 different PNML models was determined using LTSMin for 20 selected strategies. 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.