Verification of Strong K-Step Opacity for Discrete-Event Systems

TL;DR

This paper introduces an efficient algorithm for verifying strong K-step opacity in discrete-event systems, improving computational complexity and providing tighter bounds on K, with practical demonstration.

Contribution

It proposes a new concurrent-composition structure for verification, reducing complexity and independence from K, along with a tighter upper bound on K for strong K-step opacity.

Findings

The new algorithm reduces verification time complexity.

Verification does not depend on the value of K.

A tighter upper bound on K is established.

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.