Verification of Strong K-Step Opacity for Discrete-Event Systems
Abstract
In this paper, we revisit the verification of strong K-step opacity (K-SSO) for partially-observed discrete-event systems modeled as nondeterministic finite-state automata. As a stronger version of the standard K-step opacity, K-SSO requires that an intruder cannot make sure whether or not a secret state has been visited within the last K observable steps. To efficiently verify K-SSO, we propose a new concurrent-composition structure, which is a variant of our previously- proposed one. Based on this new structure, we design an algorithm for deciding K-SSO and prove that the proposed algorithm not only reduces the time complexity of the existing algorithms, but also does not depend on the value of K. Furthermore, a new upper bound on the value of K in K-SSO is derived, which also reduces the existing upper bound on K in the literature. Finally, we illustrate the proposed algorithm by a simple example.
Keywords
Cite
@article{arxiv.2204.04698,
title = {Verification of Strong K-Step Opacity for Discrete-Event Systems},
author = {Xiaoguang Han and Kuize Zhang and Zhiwu Li},
journal= {arXiv preprint arXiv:2204.04698},
year = {2022}
}
Comments
6 pages, 2 figures, submitted to IEEE CDC on March 28, 2022