Optimal Scheduling Using Branch and Bound with SPIN 4.0

T.C. Ruys

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

    27 Citations (Scopus)
    107 Downloads (Pure)

    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 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
    Pages1-17
    Number of pages17
    ISBN (Electronic)978-3-540-44829-7
    DOIs
    Publication statusPublished - 2003
    Event10th International SPIN Workshop on Model Checking Software 2003 - Portland, United States
    Duration: 9 May 200310 May 2003
    Conference number: 10

    Conference

    Conference10th International SPIN Workshop on Model Checking Software 2003
    CountryUnited States
    CityPortland
    Period9/05/0310/05/03

    Keywords

    • FMT-MC: MODEL CHECKING
    • IR-66290
    • EWI-6541

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

  • Cite this

    Ruys, T. C. (2003). Optimal Scheduling Using Branch and Bound with SPIN 4.0. In T. Ball, & S. K. Rajamani (Eds.), Model Checking Software: 10th International SPIN Workshop Portland, OR, USA, May 9–10, 2003 Proceedings (pp. 1-17) https://doi.org/10.1007/3-540-44829-2_1