Schedulers and finishers: On generating and filtering the behaviours of an event structure

It is well known that every trace of a transition system can be generated using a scheduler. However, this basic completeness result does not hold in event structure models. The reason for this failure is that, according to its standard definition, a scheduler chooses which action to schedule and, at the same time, observes that the one scheduled last has occurred. Thus, scheduled events will never be able to overlap. We propose to separate scheduling from observing termination and introduce the dual notion of finishers which, together with schedulers, are enough to regain completeness. We then investigate all possible interactions between schedulers and finishers, concluding that simple alternating interactions are enough to express complex resolution. We also observe that when these interactions are independent, they may produce behaviours that are not satisfying some desired property that is intrinsic to the system. To filter these behaviours out, we extend our results by defining permissible pairs of schedulers and finishers. In contrast to independent interactions, this new concept allows us to control and observe concurrent executions with a granularity that is strictly higher than that provided by the bundle relation.