The property to verify is that a process must eventually be scheduled.
[]<>work0

The following defintion is the MS example with size 3.
====================Process Definitions====================
start()=(bang->Stop);
cycle0()=((bang->(a.0->((work0->(init.1->cycle0))[](init.1->(work0->cycle0)))))
[](init.0->(a.0->((work0->(init.1->cycle0))[](init.1->(work0->cycle0))))));
cycle1()=(init.1->(a.1->((work1->(init.2->cycle1))[](init.2->(work1->cycle1)))));
cycle2()=(init.2->(a.2->((work2->(init.0->cycle2))[](init.0->(work2->cycle2)))));
aMilnerScheduler()=(start||cycle0||cycle1||cycle2);

====================LTL Definitions========================
LTL(AlwaysWork0=[]<>work0);