Solving scheduling problems by untimed model checking: The clinical chemical analyser case study

Anton Wijs, Jaco van de Pol, Elena M. Bortnik

Research output: Contribution to journalArticleAcademicpeer-review

4 Citations (Scopus)

Abstract

In this article, we show how scheduling problems can be modelled in untimed process algebra, by using special tick actions. A minimal-cost trace leading to a particular action, is one that minimises the number of tick steps. As a result, we can use any (timed or untimed) model checking tool to find shortest schedules. Instantiating this scheme to μCRL, we profit from a richer specification language than timed model checkers usually offer. Also, we can profit from efficient distributed state space generators. We propose a variant of breadth-first search that visits all states between consecutive tick steps, before moving to the next time slice. We experimented with a sequential and a distributed implementation of this algorithm. In addition, we experimented with beam search, which visits only parts of the search space, to find near-optimal solutions. Our approach is applied to find optimal schedules for test batches of a realistic clinical chemical analyser, which performs several kinds of tests on patient samples.
Original languageEnglish
Article number375
Pages (from-to)375-392
Number of pages18
JournalInternational Journal on Software Tools for Technology Transfer
Volume11
Issue number5
DOIs
Publication statusPublished - 2009

Fingerprint

Dive into the research topics of 'Solving scheduling problems by untimed model checking: The clinical chemical analyser case study'. Together they form a unique fingerprint.

Cite this