Runtime enforcement is a monitoring technique used to ensure that a system behaves according to a set of formal properties. It employs an enforcer that transforms an untrusted sequence of events into one that satisfies the specified property. In cases of property violation, we allow the enforcer to temporarily delay input events—storing them in memory until the property can be satisfied—or to suppress them if the property can never be satisfied. This paper addresses the enforcement of multiple untimed properties modelled as finite automata, serially, to promote modularity, i.e., rather than synthesizing a single enforcer for all properties, we generate individual enforcers and combine them serially. Also, to handle practical constraints, the paper considers that each enforcer operates with bounded (finite) memory.

We explore whether regular properties—and their subclasses, specifically safety (“nothing bad happens”) and co-safety (“something good eventually happens”)—can be enforced in a compositional setting under memory constraints. We define enforceability in terms of preserving key criteria like soundness, transparency, etc. For properties that are not directly serially enforceable, we identify conditions on their automata, which, when satisfied, enable certain groups of properties to be enforced serially. To formalize and support these ideas, we present the Bounded Compositional Runtime Enforcement framework. Submitted May 05, 04:54