Verification of initial-and-final-state opacity for unambiguous weighted automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F24%3A00585936" target="_blank" >RIV/67985840:_____/24:00585936 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1016/j.isatra.2024.03.019" target="_blank" >https://doi.org/10.1016/j.isatra.2024.03.019</a>

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

Verification of initial-and-final-state opacity for unambiguous weighted automata

Popis výsledku v původním jazyce

Initial-and-final-state opacity (IFO) is a type of opacity that characterizes a system's ability to prevent the disclosure of information about whether its evolution starts at an initial state and ends at a final state. In this paper, we extend the notion of IFO from the logical automata to the framework of unambiguous weighted automata (UWAs) that do not contain any cycle composed solely of unobservable events. For the verification of IFO, we first construct a labeled observer and a trellis-based initial state estimator for a given UWA. Even though the labeled observer has much smaller state space compared to the trellis-based initial state estimator, it cannot be used when the set of secret state pairs or the set of non-secret state pairs is not in the Cartesian product form. Based on the labeled observer, we present a more efficient method to verify IFO in the case when the set of non-secret state pairs is expressed as a Cartesian product, regardless of whether the set of secret state pairs is in the Cartesian product form. Furthermore, we use the labeled observer to verify initial-state opacity for a UWA.

Název v anglickém jazyce

Verification of initial-and-final-state opacity for unambiguous weighted automata

Popis výsledku anglicky

Initial-and-final-state opacity (IFO) is a type of opacity that characterizes a system's ability to prevent the disclosure of information about whether its evolution starts at an initial state and ends at a final state. In this paper, we extend the notion of IFO from the logical automata to the framework of unambiguous weighted automata (UWAs) that do not contain any cycle composed solely of unobservable events. For the verification of IFO, we first construct a labeled observer and a trellis-based initial state estimator for a given UWA. Even though the labeled observer has much smaller state space compared to the trellis-based initial state estimator, it cannot be used when the set of secret state pairs or the set of non-secret state pairs is not in the Cartesian product form. Based on the labeled observer, we present a more efficient method to verify IFO in the case when the set of non-secret state pairs is expressed as a Cartesian product, regardless of whether the set of secret state pairs is in the Cartesian product form. Furthermore, we use the labeled observer to verify initial-state opacity for a UWA.

Druh

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

CEP obor

—

OECD FORD obor

20205 - Automation and control systems

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

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

Isa Transactions

ISSN

0019-0578

e-ISSN

1879-2022

Svazek periodika

148

Číslo periodika v rámci svazku

May

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

10

Strana od-do

237-246

Kód UT WoS článku

001241318800001

EID výsledku v databázi Scopus

2-s2.0-85189948212