The paper entitled Runtime Enforcement Using Büchi Games has been accepted for publication in SPIN 2017, the 24th International SPIN Symposium on Model Checking of Software.
Below is an abstract of the paper.
We leverage Büchi games for the runtime enforcement of regular properties with uncontrollable events. Runtime enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modelled by an automaton. We revisit runtime enforcement with uncontrollable events and propose a framework where we model the runtime enforcement problem as a Büchi game and synthesise sound, compliant, and optimal enforcement mechanisms as strategies. We present algorithms and a tool implementing enforcement mechanisms. We reduce the complexity of the computations performed by enforcement mechanisms at runtime by pre-computing decisions of enforcement mechanisms ahead of time.
The preprint of the paper can be downloaded here.
This is joint work with Matthieu Renard and Antoine Rollet from University of Bordeaux (France).