On Algorithms verifying Initial-and-Final-State Opacity: Complexity, Special Cases, and Comparison
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917877769043968 |
|---|---|
| author | Masopust, Tomáš Osička, Petr |
| author_facet | Masopust, Tomáš Osička, Petr |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_17000 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | On Algorithms verifying Initial-and-Final-State Opacity: Complexity, Special Cases, and Comparison Masopust, Tomáš Osička, Petr Formal Languages and Automata Theory Systems and Control 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. |
| title | On Algorithms verifying Initial-and-Final-State Opacity: Complexity, Special Cases, and Comparison |
| topic | Formal Languages and Automata Theory Systems and Control |
| url | https://arxiv.org/abs/2402.17000 |