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.
@InProceedings{balun_et_al:LIPIcs.MFCS.2023.16, author = {Balun, Ji\v{r}{\'\i} and Masopust, Tom\'{a}\v{s} and Osi\v{c}ka, Petr}, title = {{Speed Me up If You Can: Conditional Lower Bounds on Opacity Verification}}, booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)}, pages = {16:1--16:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-292-1}, ISSN = {1868-8969}, year = {2023}, volume = {272}, editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.16}, URN = {urn:nbn:de:0030-drops-185504}, doi = {10.4230/LIPIcs.MFCS.2023.16}, annote = {Keywords: Finite automata, opacity, fine-grained complexity} }
Feedback for Dagstuhl Publishing