In this paper, we mainly focus on solving scheduling problems with model checking, where a finite number of entities needs to be processed as efficiently as possible, for instance by a machine. To solve these problems, we model them in untimed process algebra, where time is modelled using a special tick action. We propose a set of distributed state space explorations to find schedules for the modelled problems, building on the traditional notion of beam search. The basic approach is called distributed (detailed) beam search, which prunes parts of the state space while searching using an evaluation function in order to find near-optimal schedules in very large state spaces. Variations on this approach are presented, such as distributed flexible, distributed g-synchronised, and distributed priority beam search, which can also practically be used in combinations.
|Title of host publication
|Proceedings of the 4th Workshop on Model Checking and Artificial Intelligence
|S. Edelkamp, A. Lomuscio
|Place of Publication
|Published - 2006
|Lecture Notes in Artificial Intelligence