On algorithms verifying initial-and-final-state opacity: Complexity, special cases, and comparison

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989592%3A15310%2F25%3A73633772" target="_blank" >RIV/61989592:15310/25:73633772 - isvavai.cz</a>

Výsledek na webu

<a href="https://www.sciencedirect.com/science/article/pii/S0005109825000627" target="_blank" >https://www.sciencedirect.com/science/article/pii/S0005109825000627</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.automatica.2025.112171" target="_blank" >10.1016/j.automatica.2025.112171</a>

Jazyk výsledku

angličtina

Název v původním jazyce

On algorithms verifying initial-and-final-state opacity: Complexity, special cases, and comparison

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

On algorithms verifying initial-and-final-state opacity: Complexity, special cases, and comparison

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2025

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

AUTOMATICA

ISSN

0005-1098

e-ISSN

1873-2836

Svazek periodika

174

Číslo periodika v rámci svazku

APR

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

9

Strana od-do

"112171-1"-"112171-9"

Kód UT WoS článku

001420455400001

EID výsledku v databázi Scopus

2-s2.0-85216600339