Optimal Scheduling Using Branch and Bound with SPIN 4.0


Share/Save/Bookmark

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]
Preview
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

 

Repository Staff Only: item control page