Opaque Superlanguages and Sublanguages in Discrete Event Systems

In this article, we further investigate opacity of discrete event systems. In our previous work, we defined three types of opacity: strong opacity, weak opacity, and no opacity. Strong opacity can be used to study security-related problems whereas no opacity can be used to study fault detection and diagnosis problems. In this study, we investigate the properties of (strong, weak, and no) opacity. We show that opacity is often closed under union, but may not be closed under the intersection. We also investigate the largest opaque sublanguages and the smallest opaque superlanguages of a language if the language is not opaque. We derive formulas for these sublanguages and superlanguages. We then extend these results from centralized opacity to decentralized opacity, when more than one observer or controller is observing the system. Finally, we apply the results to the Dining Cryptographers Problem. We show that the protocol proposed in the literature satisfies both no opacity (the cryptographers know if the boss is paying) and strong opacity (the cryptographers do not know who is paying if the boss is not paying). We also use the formulas derived in this article to synthesize the protocol, which is much more difficult to do than verifying the protocol.