Abstract
The use of model checkers to solve discrete optimisation problems is appealing. A model checker can first be used to verify that the model of the problem is correct. Subsequently, the same model can be used to find an optimal solution for the problem. This paper describes how to apply the new PROMELA primitives of SPIN 4.0 to search effectively for the optimal solution. We show how Branch-and-Bound techniques can be added to the LTL property that is used to find the solution. The LTL property is dynamically changed during the verification. We also show how the syntactical reordering of statements and/or processes in the PROMELA model can improve the search even further. The techniques are illustrated using two running examples: the Travelling Salesman Problem and a job-shop scheduling problem.
Original language | English |
---|---|
Title of host publication | Model Checking Software |
Subtitle of host publication | 10th International SPIN Workshop Portland, OR, USA, May 9–10, 2003 Proceedings |
Editors | Thomas Ball, Sriram K. Rajamani |
Pages | 1-17 |
Number of pages | 17 |
ISBN (Electronic) | 978-3-540-44829-7 |
DOIs | |
Publication status | Published - 2003 |
Event | 10th International SPIN Workshop on Model Checking Software 2003 - Portland, United States Duration: 9 May 2003 → 10 May 2003 Conference number: 10 |
Conference
Conference | 10th International SPIN Workshop on Model Checking Software 2003 |
---|---|
Country/Territory | United States |
City | Portland |
Period | 9/05/03 → 10/05/03 |
Keywords
- FMT-MC: MODEL CHECKING
- IR-66290
- EWI-6541