Verification of initial-and-final-state opacity for unambiguous weighted automata
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Verification of initial-and-final-state opacity for unambiguous weighted automata
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
20205 - Automation and control systems
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2024
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Isa Transactions
ISSN
0019-0578
e-ISSN
1879-2022
Volume of the periodical
148
Issue of the periodical within the volume
May
Country of publishing house
US - UNITED STATES
Number of pages
10
Pages from-to
237-246
UT code for WoS article
001241318800001
EID of the result in the Scopus database
2-s2.0-85189948212