On the Complexity of Initial-and-Final-State Opacity for Discrete Event Systems
<|reference_start|>On the Complexity of Initial-and-Final-State Opacity for Discrete Event Systems: Opacity is a general framework modeling security properties of systems interacting with a passive attacker by asserting that a part of the systems behaviour remains secret. In initial-and-final-state opacity (IFO, for short) the secret is whether the system evolved from a given initial state to a given final state or not. Two algorithms for IFO verification are discussed in the literature. One algorithm 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 worst-case time complexity of both algorithms is bounded by a super-exponential function. We show that the super-exponential time complexity is tight for both algorithms; however, we leave open whether there is an algorithm with a lower time complexity. Finally, we use extensive benchmarks based on real data to experimentally compare the existing algorithms.<|reference_end|>
@article{masopust2024on,
    title={On the Complexity of Initial-and-Final-State Opacity for Discrete Event
  Systems},
    author={Tom'av{s} Masopust and Petr Osiv{c}ka},
    journal={arXiv preprint arXiv:2402.17000},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.17000},
    primaryClass={cs.FL cs.SY eess.SY}
}