Difference between revisions of "Publications/carvalho.20.seminar"
From LRDE
Line 4: | Line 4: | ||
| year = 2020 |
| year = 2020 |
||
| number = 2001 |
| 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 |
+ | | 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. |
| type = techreport |
| type = techreport |
||
| id = carvalho.20.seminar |
| id = carvalho.20.seminar |
Latest revision as of 18:22, 9 November 2020
- 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.