Model classification in model checking using random forest

Authors

Thomas De Carvalho

Type

techreport

Year

2020

Number

2001

Abstract

Model checking aims to verify that a system meets the given specification by exploring all its possible states. To achieve that, there are several techniques. The Multi-Core Nested Depth-First Search (CNDFS) has a low memory requirement and works well with the simplest Büchi automatons. The Multi-Core On-The-Fly SCC Decomposition (UFSCC) has a greater memory requirement and works well with generalized Büchi automatons. The Symbolic method has a lower memory requirement but depends a lot on the order of the variables. The performances of these algorithms can be very different and choosing the best one given a specific model without testing all of them is not something easy. Here, we are trying to use machine learning to predict the best method to use for a given model. For that purpose, we train a random forest, an ensemble learning method that uses a multitude of decision treesusing only the first states of the state space.