Back to University of Twente portal
Optimal Scheduling Using Branch and Bound with SPIN 4.0
Ruys, T.C. (2003) Optimal Scheduling Using Branch and Bound with SPIN 4.0. In: Model Checking Software, Proceedings of the 10th International SPIN Workshop.
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 179Kb |
| 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. |
| Item Type: | Conference or Workshop Item |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Link to this item: | http://purl.utwente.nl/publications/66290 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page