Projects per year
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 language | English |
---|---|
Pages (from-to) | 97-112 |
Number of pages | 16 |
Journal | Theoretical Computer Science |
Volume | 744 |
DOIs | |
Publication status | Published - 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.Projects
- 1 Finished
-
Designing software for secrecy: Security-enabled program algebra
McIver, A., Morgan, C., Newton, J. & Butler, M.
1/07/10 → 31/12/13
Project: Research