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.

Projects

IGA PrF 2023 026

Martin Trnečka
Jiří Balun, Jiří Valůšek

Links

Link

Authors

Jiří Balun
Petr Osička
Tomáš Masopust

48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), 16:1-16:15, 2023
Discrete-Event Systems and Theoretical Computer Science Research Group
DOI

Downloads

BibTex