Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
This work addresses runtime enforcement for formal verification in systems, but it appears incremental as it focuses on a specific logic fragment and monitor type.
The paper tackled the problem of ensuring system correctness by developing bidirectional runtime enforcement strategies for input-output properties, specifically showing that the safety fragment of Hennessy-Milner logic with recursion (sHML) is enforceable via action disabling monitors and providing an automated synthesis function for monitor generation.
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.