Efficient Synthesis of Edit Functions for Opacity Enforcement Using Bisimulation-Based Abstractions

This paper investigates the synthesis of edit functions for opacity enforcement using abstraction methods to reduce computational complexity. Edit functions are used to alter system outputs by erasing or inserting events in order to prevent violations of opacity. We introduce two abstraction methods, called opaque observation equivalence and opaque bisimulation, that are used to abstract the original system and its observer before calculating edit functions. We present a set of results on abstraction for opacity and its enforcement by edit functions that prove that edit functions synthesized from abstracted models are “equivalent” to ones synthesized from original ones. Our approach leverages the technique of edit function synthesis using the All Edit Structure from prior works