Solving scheduling problems by untimed model checking

In this paper, we show how scheduling problems can be modelled in untimed process algebra, by using special tick actions. A minimal-time trace leading to a particular action, is one that minimizes 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