Finite state transducers framework for monitors conflict detection and resolution

Runtime monitoring and verification systems monitor target's events and verify them against specifications during program execution. For such systems the same event might trigger different monitors remedial actions, which can be contradictory in behavior or complementary (with a specific order). This urges the need to have a method to detect and resolve potential conflict between monitors. In this paper, we present a formal model for modeling monitors based on Finite State Transducers. Monitors in the model are transducers with events as their input and output alphabet. Monitors composition is used for those monitors in conflict, where each monitor can add to the output set of events, but it can never remove an event. The output set of events is later evaluated using 2 rewrite rules and resulting in non-conflicting behavior.