Production Scheduling by Reachability Analysis - A Case Study

Gerd Behrmann, Hendrik Brinksma, Martijn Hendriks, Angelika H. Mader

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 20 Citations

Abstract

Schedule synthesis based on reachability analysis of timed automata has received attention in the last few years. The main strength of this approach is that the expressiveness of timed automata allows -- unlike many classical approaches -- the modelling of scheduling problems of very different kinds. Furthermore, the models are robust against changes in the parameter setting and against changes in the problem specification. This paper presents a case study that was provided by Axxom, an industrial partner of the Ametist project. It consists of a scheduling problem for lacquer production, and is treated with the timed automata approach. A number of problems have to be addressed for the modelling task: the information transfer from the industrial partner, the derivation of timed automaton model for the case study, and the heuristics that have to be added in order to reduce the search space. We try to isolate the generic problems of modelling for model checking, and suggest solutions that are also applicable for other scheduling cases. Model checking experiments indicate that -- for this problem -- the timed automata approach is competitive with Axxom's planning tool.
LanguageEnglish
Title of host publicationWorkshop on Parallel and Distributed Real-Time Systems (WPDRTS)
Place of PublicationLos Alamitos, California
PublisherIEEE Computer Society Press
Pages140a-140a
ISBN (Print)0-7695-2312-9
DOIs
StatePublished - Apr 2005
EventWorkshop on Parallel and Distributed Real-Time Systems, WPDRTS 2005 - Denver, United States
Duration: 4 Apr 20055 Apr 2005
http://www.cse.wustl.edu/~cdgill/WPDRTS04/

Publication series

Name
PublisherIEEE Computer Society Press

Conference

ConferenceWorkshop on Parallel and Distributed Real-Time Systems, WPDRTS 2005
Abbreviated titleWPDRTS
CountryUnited States
CityDenver
Period4/04/055/04/05
Internet address

Fingerprint

Scheduling
Model checking
Lacquers
Specifications
Planning
Experiments

Keywords

  • EWI-1903
  • METIS-228770
  • IR-54514

Cite this

Behrmann, G., Brinksma, H., Hendriks, M., & Mader, A. H. (2005). Production Scheduling by Reachability Analysis - A Case Study. In Workshop on Parallel and Distributed Real-Time Systems (WPDRTS) (pp. 140a-140a). Los Alamitos, California: IEEE Computer Society Press. DOI: 10.1109/IPDPS.2005.363
Behrmann, Gerd ; Brinksma, Hendrik ; Hendriks, Martijn ; Mader, Angelika H./ Production Scheduling by Reachability Analysis - A Case Study. Workshop on Parallel and Distributed Real-Time Systems (WPDRTS). Los Alamitos, California : IEEE Computer Society Press, 2005. pp. 140a-140a
@inproceedings{f7f83336461546ffa24d65066f1b9bd6,
title = "Production Scheduling by Reachability Analysis - A Case Study",
abstract = "Schedule synthesis based on reachability analysis of timed automata has received attention in the last few years. The main strength of this approach is that the expressiveness of timed automata allows -- unlike many classical approaches -- the modelling of scheduling problems of very different kinds. Furthermore, the models are robust against changes in the parameter setting and against changes in the problem specification. This paper presents a case study that was provided by Axxom, an industrial partner of the Ametist project. It consists of a scheduling problem for lacquer production, and is treated with the timed automata approach. A number of problems have to be addressed for the modelling task: the information transfer from the industrial partner, the derivation of timed automaton model for the case study, and the heuristics that have to be added in order to reduce the search space. We try to isolate the generic problems of modelling for model checking, and suggest solutions that are also applicable for other scheduling cases. Model checking experiments indicate that -- for this problem -- the timed automata approach is competitive with Axxom's planning tool.",
keywords = "EWI-1903, METIS-228770, IR-54514",
author = "Gerd Behrmann and Hendrik Brinksma and Martijn Hendriks and Mader, {Angelika H.}",
note = "Imported from DIES",
year = "2005",
month = "4",
doi = "10.1109/IPDPS.2005.363",
language = "English",
isbn = "0-7695-2312-9",
publisher = "IEEE Computer Society Press",
pages = "140a--140a",
booktitle = "Workshop on Parallel and Distributed Real-Time Systems (WPDRTS)",

}

Behrmann, G, Brinksma, H, Hendriks, M & Mader, AH 2005, Production Scheduling by Reachability Analysis - A Case Study. in Workshop on Parallel and Distributed Real-Time Systems (WPDRTS). IEEE Computer Society Press, Los Alamitos, California, pp. 140a-140a, Workshop on Parallel and Distributed Real-Time Systems, WPDRTS 2005, Denver, United States, 4/04/05. DOI: 10.1109/IPDPS.2005.363

Production Scheduling by Reachability Analysis - A Case Study. / Behrmann, Gerd; Brinksma, Hendrik; Hendriks, Martijn; Mader, Angelika H.

Workshop on Parallel and Distributed Real-Time Systems (WPDRTS). Los Alamitos, California : IEEE Computer Society Press, 2005. p. 140a-140a.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Production Scheduling by Reachability Analysis - A Case Study

AU - Behrmann,Gerd

AU - Brinksma,Hendrik

AU - Hendriks,Martijn

AU - Mader,Angelika H.

N1 - Imported from DIES

PY - 2005/4

Y1 - 2005/4

N2 - Schedule synthesis based on reachability analysis of timed automata has received attention in the last few years. The main strength of this approach is that the expressiveness of timed automata allows -- unlike many classical approaches -- the modelling of scheduling problems of very different kinds. Furthermore, the models are robust against changes in the parameter setting and against changes in the problem specification. This paper presents a case study that was provided by Axxom, an industrial partner of the Ametist project. It consists of a scheduling problem for lacquer production, and is treated with the timed automata approach. A number of problems have to be addressed for the modelling task: the information transfer from the industrial partner, the derivation of timed automaton model for the case study, and the heuristics that have to be added in order to reduce the search space. We try to isolate the generic problems of modelling for model checking, and suggest solutions that are also applicable for other scheduling cases. Model checking experiments indicate that -- for this problem -- the timed automata approach is competitive with Axxom's planning tool.

AB - Schedule synthesis based on reachability analysis of timed automata has received attention in the last few years. The main strength of this approach is that the expressiveness of timed automata allows -- unlike many classical approaches -- the modelling of scheduling problems of very different kinds. Furthermore, the models are robust against changes in the parameter setting and against changes in the problem specification. This paper presents a case study that was provided by Axxom, an industrial partner of the Ametist project. It consists of a scheduling problem for lacquer production, and is treated with the timed automata approach. A number of problems have to be addressed for the modelling task: the information transfer from the industrial partner, the derivation of timed automaton model for the case study, and the heuristics that have to be added in order to reduce the search space. We try to isolate the generic problems of modelling for model checking, and suggest solutions that are also applicable for other scheduling cases. Model checking experiments indicate that -- for this problem -- the timed automata approach is competitive with Axxom's planning tool.

KW - EWI-1903

KW - METIS-228770

KW - IR-54514

U2 - 10.1109/IPDPS.2005.363

DO - 10.1109/IPDPS.2005.363

M3 - Conference contribution

SN - 0-7695-2312-9

SP - 140a-140a

BT - Workshop on Parallel and Distributed Real-Time Systems (WPDRTS)

PB - IEEE Computer Society Press

CY - Los Alamitos, California

ER -

Behrmann G, Brinksma H, Hendriks M, Mader AH. Production Scheduling by Reachability Analysis - A Case Study. In Workshop on Parallel and Distributed Real-Time Systems (WPDRTS). Los Alamitos, California: IEEE Computer Society Press. 2005. p. 140a-140a. Available from, DOI: 10.1109/IPDPS.2005.363