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

Annabelle McIver, Tahiry Rabehaja*, Georg Struth

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)97-112
Number of pages16
JournalTheoretical Computer Science
Volume744
DOIs
Publication statusPublished - 5 Oct 2018

Keywords

  • Completeness
  • Concurrency
  • Event structure
  • Partial order
  • Specification

Fingerprint

Dive into the research topics of 'Schedulers and finishers: on generating and filtering the behaviours of an event structure'. Together they form a unique fingerprint.

Cite this