Yoshiki Nakamura

Diego Figueira, Santiago Figueira, Yoshiki Nakamura

We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following reductions: (i) a polynomial-time reduction from the satisfiability problem for GNTC to the satisfiability problem for the unary negation fragment UNTC of GNTC, and (ii) a direct exponential-time reduction from the satisfiability problem for UNTC to the non-emptiness problem for 2-way alternating parity tree automata. Furthermore, we show that the model checking problem for GNTC is $\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$-complete in combined complexity. Our result implies $\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$-completeness for both UNTC and $\mathrm{UNFO}^{\mathrm{reg}}$, which were left open in previous works.

Taisei Nogami, Yoshiki Nakamura, Tachio Terauchi

The regular expression matching problem asks whether a given regular expression of length $m$ matches a given string of length $n$. As is well known, the problem can be solved in $O(nm)$ time using Thompson's algorithm. Moreover, recent studies have shown that regular expression matching extended with a practical extension called lookaround can be solved in the same time complexity. In this work, we consider four well-known extensions to regular expressions called backreference, squaring, intersection and complement. We prove a number of novel time complexity lower bounds for regular expression matching with these extensions under the Orthogonal Vectors Conjecture (OVC), $k$-OVC, $k$-Clique Hypothesis, and Combinatorial $k$-Clique Hypothesis. Some highlights of our results include the fact that none of the matching problems with the extensions can be solved in $n^{2-\varepsilon} \mathrm{poly}(m)$ time for any constant $\varepsilon > 0$ (for backreference, even when restricted to one capturing group) under OVC, and that the problem with complement, also known as extended regular expression (ERE) matching, cannot be solved in time $n^{2-\varepsilon}\mathrm{tower}(o(\sqrt{m}))$ under OVC, $n^{ω-\varepsilon}\mathrm{tower}(o(\sqrt{m}))$ under the $k$-Clique Hypothesis (where $ω$ is the matrix multiplication exponent), and $n^{3-\varepsilon}\mathrm{tower}(o(\sqrt{m}))$ under the Combinatorial $k$-Clique Hypothesis, respectively. In particular, the latter two results show that the $O(n^3 m)$-time ERE matching algorithm introduced by Hopcroft and Ullman in 1979 and recently improved by Bille, Gørtz and Jessen to run in $O(n^ωm)$ time using fast matrix multiplication was already optimal in a sense, and shed light on why the theoretical computer science community has struggled to improve the time complexity of ERE matching with respect to $n$ and $m$ for more than 45 years.

Yoshiki Nakamura

In this paper, we show that the equational theory of relational Kleene algebra with the \emph{graph loop} operator (a.k.a.~\emph{fixset}) is \textsc{PSpace}-complete. Here, the graph loop is the unary operator that restricts a binary relation to the identity relation. We further show that this \textsc{PSpace}-completeness still holds by extending the terms with top, tests, converse, and nominals, over relational models. Notably, for Kleene algebra with tests (KAT), while the equational theory of relational KAT with antidomain is \textsc{ExpTime}-complete, we show that the equational theory of relational KAT with domain is \textsc{PSpace}-complete, thereby resolving a problem left open in previous works. To this end, we introduce a novel automaton model on relational structures (graphs), called \emph{loop-automata}. Loop-automata extend nondeterministic finite automata with a transition type that tests whether the current vertex has a loop. Using this model, we can give a polynomial-time reduction from the equational theories above to the language inclusion problem for 2-way alternating automata.