Optimal Scheduling Using Branch and Bound with SPIN 4.0

T.C. Ruys

doi:10.1007/3-540-44829-2_1

Optimal Scheduling Using Branch and Bound with SPIN 4.0

T.C. Ruys

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

27 Citations (Scopus)

114 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 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	https://doi.org/10.1007/3-540-44829-2_1
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	United States
City	Portland
Period	9/05/03 → 10/05/03

Keywords

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

Access to Document

10.1007/3-540-44829-2_1

ruys-spin-2003
open
Final published version, 179 KB

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

@inproceedings{70f0b2976aef4e2f83c5f0780cc1dfaa,

title = "Optimal Scheduling Using Branch and Bound with SPIN 4.0",

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.",

keywords = "FMT-MC: MODEL CHECKING, IR-66290, EWI-6541",

author = "T.C. Ruys",

year = "2003",

doi = "10.1007/3-540-44829-2_1",

language = "English",

isbn = "978-3-540-40117-9",

pages = "1--17",

editor = "Thomas Ball and Rajamani, {Sriram K.}",

booktitle = "Model Checking Software",

note = "10th International SPIN Workshop on Model Checking Software 2003 ; Conference date: 09-05-2003 Through 10-05-2003",

}

TY - GEN

T1 - Optimal Scheduling Using Branch and Bound with SPIN 4.0

AU - Ruys, T.C.

N1 - Conference code: 10

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

KW - FMT-MC: MODEL CHECKING

KW - IR-66290

KW - EWI-6541

U2 - 10.1007/3-540-44829-2_1

DO - 10.1007/3-540-44829-2_1

M3 - Conference contribution

SN - 978-3-540-40117-9

SP - 1

EP - 17

BT - Model Checking Software

A2 - Ball, Thomas

A2 - Rajamani, Sriram K.

T2 - 10th International SPIN Workshop on Model Checking Software 2003

Y2 - 9 May 2003 through 10 May 2003

ER -