Optimal Scheduling Using Branch and Bound with SPIN 4.0

T.C. Ruys

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    31 Citations (Scopus)
    122 Downloads (Pure)


    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 languageEnglish
    Title of host publicationModel Checking Software
    Subtitle of host publication10th International SPIN Workshop Portland, OR, USA, May 9–10, 2003 Proceedings
    EditorsThomas Ball, Sriram K. Rajamani
    Number of pages17
    ISBN (Electronic)978-3-540-44829-7
    Publication statusPublished - 2003
    Event10th International SPIN Workshop on Model Checking Software 2003 - Portland, United States
    Duration: 9 May 200310 May 2003
    Conference number: 10


    Conference10th International SPIN Workshop on Model Checking Software 2003
    Country/TerritoryUnited States


    • IR-66290
    • EWI-6541


    Dive into the research topics of 'Optimal Scheduling Using Branch and Bound with SPIN 4.0'. Together they form a unique fingerprint.

    Cite this