# Transforming opacity verification to nonblocking verification in modular systems

## TL;DR

This paper introduces a novel compositional method for verifying opacity in systems by transforming the problem into a nonblocking verification task, enabling efficient analysis of large systems.

## Contribution

It presents a new abstraction-based approach that reduces opacity verification to nonblocking verification, applicable to current-state and K-step opacity in modular automata.

## Key findings

- Efficient verification of current-state opacity in large systems
- Transformation ensures equivalence between opacity and nonblocking properties
- Applicable to both current-state and K-step opacity

## Abstract

We consider the verification of current-state and K-step opacity for systems modeled as interacting non-deterministic finite-state automata. We describe a new methodology for compositional opacity verification that employs abstraction, in the form of a notion called opaque observation equivalence, and that leverages existing compositional nonblocking verification algorithms. The compositional approach is based on a transformation of the system, where the transformed system is nonblocking if and only if the original one is current-state opaque. Furthermore, we prove that $K$-step opacity can also be inferred if the transformed system is nonblocking. We provide experimental results where current-state opacity is verified efficiently for a large scaled-up system.