PPT Slide
A run through a model consists of a sequence of states s1 s2 ... that don㦙 need to be connected by an agent.
A run is non-simultaneous if there is an agent for every step sk � sk+1 in the run whose knowledge is identical for both states and who can㦙 therefor distinguish between them.