Name
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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/s10009-009-0110-9 | International Journal on Software Tools for Technology Transfer |
Keywords | DocType | Volume |
breadth first search,model checking,search space,scheduling problem,process algebra,state space,specification language,profitability | Journal | 11 |
Issue | ISSN | Citations |
5 | 1433-2787 | 3 |
PageRank | References | Authors |
0.44 | 28 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Anton J. Wijs | 1 | 26 | 1.88 |
| Jaco Van De Pol | 2 | 1022 | 78.19 |
| Elena M. Bortnik | 3 | 3 | 0.44 |