Polynomial algorithms to check opacity in discrete event systems

Because of its importance, opacity has been investigated in the literature. Recently, we propose general definitions of strong opacity and weak opacity that capture other properties such as secrecy, anonymity, observability, diagnosability, and detectability as special cases of opacity. In this paper, we investigate the problem of checking opacity. By using a detector rather than an observer, we show that weak opacity can be determined in polynomial complexity by providing an algorithm of polynomial complexity to check weak opacity. The results and algorithm are illustrated by examples.