Searcharxiv⌕ Search

arXiv subjects

Yoshiki Nakamura

Publications and source records attributed to Yoshiki Nakamura.

12 recordsLinked to original sources
arXiv2026

Hardness of Regular Expression Matching with Extensions

Regular expression matching asks whether a given regular expression of length $m$ matches a given string of length $n$, and its time complexity is fairly well understood. Meanwhile, regular expressions have been extended to support various extensions for both theoretical and practical reasons, which can substantially change the time complexity of the matching problem. In this work, we consider four well-known extensions to regular expressions called intersection, squaring, complement and backreference, and we prove a number of novel conditional time complexity lower bounds for the regular expression matching problems with these extensions under the Orthogonal Vectors Conjecture, the $k$-Orthogonal Vectors Conjecture or the $k$-Clique hypotheses. Our lower bounds significantly narrow the gaps to the known upper bounds, with some even being (conditionally) optimal in that the dependence on $n$ cannot be polynomially reduced while keeping the dependence on $m$ polynomial (or even elementary, for complement). Additionally, to obtain our results for intersection, squaring and complement in a unified manner, we introduce novel problems called Dyck Selection, Orthogonal Dyck Selection and Generalized Dyck Selection. They are arguably natural formal language and stringology problems that are based on Greibach's hardest context-free language and capture the essence of why the regular expression matching problems with these extensions are hard.

cs.CC↗
arXiv2026

The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete

In this paper, we show that the equational theory of relational Kleene algebra with the graph loop operator (a.k.a. fixset) is PSpace-complete. Here, the graph loop is the unary operator that restricts a binary relation to the identity relation. We further show that this 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 ExpTime-complete, we show that the equational theory of relational KAT with domain is 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 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.

cs.LO↗
arXiv2026

Guarded Negation Transitive Closure Logic

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.

cs.LO↗
arXiv2026

A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead

We consider (logical) reasoning for regular expressions with lookahead (REwLA). In this paper, we give an axiomatic characterization for both the (match-)language equivalence and the largest substitution-closed equivalence that is sound for the (match-)language equivalence. To achieve this, we introduce a variant of propositional dynamic logic (PDL) on finite linear orders, extended with two operators: the restriction to the identity relation and the restriction to its complement. Our main contribution is a sound and complete Hilbert-style finite axiomatization for the logic, which captures the equivalences of REwLA. Using the extended operators, the completeness is established via a reduction into an identity-free variant of PDL on finite strict linear orders. Moreover, the extended PDL has the same computational complexity as REwLA.

cs.LO↗
arXiv2025

Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure

We prove that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is EXPSPACE-complete. Here, PCoR* terms consist of the following standard operators on binary relations: identity, empty, universality, union, intersection, composition, converse, and reflexive transitive closure (so, PCoR* terms subsume Kleene algebra and allegory terms as fragments). Additionally, we show that the equational theory of PCoR* extended with tests and nominals (in hybrid logic) is still EXPSPACE-complete; moreover, it is PSPACE-complete for its intersection-free fragment. To this end, we design derivatives on graphs by extending derivatives on words for regular expressions. The derivatives give a finite automata construction on path decompositions, like those on words. Because the equational theory has a linearly bounded pathwidth model property, we can decide the equational theory of PCoR* using these automata.

cs.LO↗
arXiv2025

Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops

We show that the emptiness (unsatisfiability) problem is undecidable and $\mathrmΠ^{0}_{1}$-complete for deterministic propositional while programs with (graph) loop. To this end, we introduce a hypothesis elimination using loops. Using this, we give reductions from the complement of the periodic domino problem. Moreover, as a corollary via hypothesis eliminations, we also show that the equational theory is $\mathrmΠ^{0}_{1}$-complete for the positive calculus of relations with transitive closure and difference. Additionally, we show that the emptiness problem is PSPACE-complete for the existential calculus of relations with transitive closure.

cs.LO↗
arXiv2024

Words-to-Letters Valuations for Language Kleene Algebras with Variable and Constant Complements

We investigate the equational theory for Kleene algebra terms with variable complements and constant complements -- (language) complement where it applies only to variables or constants -- w.r.t. languages. While the equational theory w.r.t. languages coincides with the language equivalence (under the standard language valuation) for Kleene algebra terms, this coincidence is broken if we extend the terms with complements. In this paper, we prove the decidability of some fragments of the equational theory: the universality problem is coNP-complete, and the inequational theory $t \le s$ is coNP-complete when $t$ does not contain Kleene-star. To this end, we introduce words-to-letters valuations; they are sufficient valuations for the equational theory and ease us in investigating the equational theory w.r.t. languages. Additionally, we show a completeness theorem of the equational theory for words with variable complements and the non-empty constant.

cs.LO↗
arXiv2023

Words-to-Letters Valuations for Language Kleene Algebras with Variable Complements

We investigate the equational theory of Kleene algebra terms with variable complements -- (language) complement where it applies only to variables -- w.r.t. languages. While the equational theory w.r.t. languages coincides with the language equivalence (under the standard language valuation) for Kleene algebra terms, this coincidence is broken if we extend the terms with complements. In this paper, we prove the decidability of some fragments of the equational theory: the universality problem is coNP-complete, and the inequational theory t <= s is coNP-complete when t does not contain Kleene-star. To this end, we introduce words-to-letters valuations; they are sufficient valuations for the equational theory and ease us in investigating the equational theory w.r.t. languages. Additionally, we prove that for words with variable complements, the equational theory coincides with the word equivalence.

cs.LO↗
arXiv2023

On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation

We introduce the $k$-variable-occurrence fragment, which is the set of terms having at most $k$ occurrences of variables. We give a sufficient condition for the decidability of the equational theory of the $k$-variable-occurrence fragment using the finiteness of a monoid. As a case study, we prove that for Tarski's calculus of relations with bounded dot-dagger alternation (an analogy of quantifier alternation in first-order logic), the equational theory of the $k$-variable-occurrence fragment is decidable for each $k$.

cs.LO↗
arXiv2023

Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations

We study the decidability and complexity of equational theories of the existential calculus of relations with transitive closure (ECoR*) and its fragments, where ECoR* is the positive calculus of relations with transitive closure extended with complements of term variables and constants. We give characterizations of these equational theories by using edge saturations and we show that the equational theory is 1) coNP-complete for ECoR* without transitive closure; 2) in coNEXP for ECoR* without intersection and PSPACE-complete for two smaller fragments; 3) $Π_{1}^{0}$-complete for ECoR*. The second result gives PSPACE-upper bounds for some extensions of Kleene algebra, including Kleene algebra with top w.r.t. binary relations.

cs.LO↗
arXiv2016

The Almost Equivalence by Asymptotic Probabilities for Regular Languages and Its Computational Complexities

We introduce p-equivalence by asymptotic probabilities, which is a weak almost-equivalence based on zero-one laws in finite model theory. In this paper, we consider the computational complexities of p-equivalence problems for regular languages and provide the following details. First, we give an robustness of p-equivalence and a logical characterization for p-equivalence. The characterization is useful to generate some algorithms for p-equivalence problems by coupling with standard results from descriptive complexity. Second, we give the computational complexities for the p-equivalence problems by the logical characterization. The computational complexities are the same as for the (fully) equivalence problems. Finally, we apply the proofs for p-equivalence to some generalized equivalences.

cs.FL↗