Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors.

@article{paperbot2235,
  title = {Bidirectional Runtime Enforcement of First-Order Branching-Time Properties},
  author = {Luca Aceto and Ian Cassar and Adrian Francalanza and Anna Ingolfsdottir},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 19, Issue 1},
  year = {2023},
  doi = {10.46298/lmcs-19(1:14)2023}
}