Speed Me up if You Can: Conditional Lower Bounds on Opacity Verification
Abstract
Opacity is a property of privacy and security applications asking whether, given a system model, a passive intruder that makes online observations of system's behaviour can ascertain some "secret" information of the system. Deciding opacity is a PSpace-complete problem, and hence there are no polynomial-time algorithms to verify opacity under the assumption that PSpace differs from PTime. This assumption, however, gives rise to a question whether the existing exponential-time algorithms are the best possible or whether there are faster, sub-exponential-time algorithms. We show that under the (Strong) Exponential Time Hypothesis, there are no algorithms that would be significantly faster than the existing algorithms. As a by-product, we obtained a new conditional lower bound on the time complexity of deciding universality (and therefore also inclusion and equivalence) for nondeterministic finite automata.
Keywords
Cite
@article{arxiv.2304.09920,
title = {Speed Me up if You Can: Conditional Lower Bounds on Opacity Verification},
author = {Jiří Balun and Tomáš Masopust and Petr Osička},
journal= {arXiv preprint arXiv:2304.09920},
year = {2023}
}