K-Step Opacity in Discrete Event Systems: Verification, Complexity, and Relations
Abstract
Opacity is a property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has a limited observation of its behavior. Several notions of opacity have been studied, including current-state opacity, K-step opacity, and infinite-step opacity. We study K-step opacity that generalizes both current-state opacity and infinite-step opacity, and asks whether the intruder cannot decide, at any time, whether or when the system was in a secret state during the last K observable steps. We design a new algorithm deciding K-step opacity the complexity of which is lower than that of existing algorithms and that does not depend on K. We then compare K-step opacity with other opacity notions and provide new transformations among the notions that do not use states that are neither secret nor non-secret (neutral states) and that are polynomial with respect to both the size of the system and the binary encoding of K.
Keywords
Cite
@article{arxiv.2109.02158,
title = {K-Step Opacity in Discrete Event Systems: Verification, Complexity, and Relations},
author = {Jiří Balun and Tomáš Masopust},
journal= {arXiv preprint arXiv:2109.02158},
year = {2021}
}