Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Algorithms verifying Initial-and-Final-State Opacity: Complexity, Special Cases, and Comparison

Tomáš Masopust, Petr Osička

TL;DR

This work examines verification of initial-and-final-state opacity (IFO) for finite automata, introducing two foundational approaches: a trellis-based semigroup method and a reduction to language inclusion. It establishes that both methods have super-exponential worst-case runtimes in the number of states $n$, and it shows that the trellis approach is a special case of the inclusion-based framework. The authors identify several meaningful special cases where complexity collapses to exponential or polynomial, and they develop enhanced language-inclusion techniques that, combined with modern tools, outperform the classic trellis method on large instances. Comprehensive benchmarks demonstrate that advanced inclusion-based verification can handle industrial-scale models, offering practical, scalable alternatives to the traditional approaches. Together, these results deepen the understanding of IFO verification complexity and provide concrete, highly scalable techniques for security analysis in discrete-event systems.

Abstract

Opacity is a general framework modeling security properties of systems interacting with a passive attacker. Initial-and-final-state opacity (IFO) generalizes the classical notions of opacity, such as current-state opacity and initial-state opacity. In IFO, the secret is whether the system evolved from a given initial state to a given final state or not. There are two algorithms for IFO verification. One arises from a trellis-based state estimator, which builds a semigroup of binary relations generated by the events of the automaton, and the other is based on the reduction to language inclusion. The time complexity of both algorithms is bounded by a super-exponential function, and it is a challenging open problem to find a faster algorithm or to show that no faster algorithm exists. We discuss the lower-bound time complexity for both general and special cases, and use extensive benchmarks to compare the existing algorithms.

On Algorithms verifying Initial-and-Final-State Opacity: Complexity, Special Cases, and Comparison

TL;DR

This work examines verification of initial-and-final-state opacity (IFO) for finite automata, introducing two foundational approaches: a trellis-based semigroup method and a reduction to language inclusion. It establishes that both methods have super-exponential worst-case runtimes in the number of states , and it shows that the trellis approach is a special case of the inclusion-based framework. The authors identify several meaningful special cases where complexity collapses to exponential or polynomial, and they develop enhanced language-inclusion techniques that, combined with modern tools, outperform the classic trellis method on large instances. Comprehensive benchmarks demonstrate that advanced inclusion-based verification can handle industrial-scale models, offering practical, scalable alternatives to the traditional approaches. Together, these results deepen the understanding of IFO verification complexity and provide concrete, highly scalable techniques for security analysis in discrete-event systems.

Abstract

Opacity is a general framework modeling security properties of systems interacting with a passive attacker. Initial-and-final-state opacity (IFO) generalizes the classical notions of opacity, such as current-state opacity and initial-state opacity. In IFO, the secret is whether the system evolved from a given initial state to a given final state or not. There are two algorithms for IFO verification. One arises from a trellis-based state estimator, which builds a semigroup of binary relations generated by the events of the automaton, and the other is based on the reduction to language inclusion. The time complexity of both algorithms is bounded by a super-exponential function, and it is a challenging open problem to find a faster algorithm or to show that no faster algorithm exists. We discuss the lower-bound time complexity for both general and special cases, and use extensive benchmarks to compare the existing algorithms.
Paper Structure (6 sections, 9 theorems, 2 equations, 3 figures, 3 tables, 3 algorithms)

This paper contains 6 sections, 9 theorems, 2 equations, 3 figures, 3 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Trellis-Based IFO Verification
  4. Inclusion-Based IFO Verification
  5. Special Cases
  6. Experimental Comparison -- Benchmarks

Key Result

Theorem 1

For every $n\ge 1$, there is an automaton $\mathop{\mathrm{\mathcal{A}}}\nolimits_n$ with $n$ states and $2^{n^2}$ events, all of which are observable, for which Algorithm alg-trellis needs at least $2^{n^2}$ steps.

Figures (3)

  • Figure 1: The automaton $\mathop{\mathrm{\mathcal{A}}}\nolimits_5$ on which Algorithm \ref{['alg-trellis']} makes at least $2^{25}$ steps and fails to terminate in 48 hours.
  • Figure 2: Instances computed in five minutes. The $x$-axis displays the time (0--300 seconds), and the $y$-axis displays the number of solved instances in that time (0--994 for negative and 0--1001 for positive instances).
  • Figure 3: Time to solve negative (left) and positive (right) instances. The $x$-axis displays the size of the instance (0--4000 states), and the $y$-axis displays the time to solve the instance (0--300 s).

Theorems & Definitions (14)

  • Theorem 1
  • proof
  • Corollary 2
  • Theorem 3
  • Lemma 4
  • proof
  • Corollary 5
  • Lemma 6
  • proof
  • Theorem 7
  • ...and 4 more