Intersection Non-Emptiness Problem¶
The decision problem asking whether a finite list of deterministic finite automata accepts at least one common string, a PSPACE-complete problem when the number of automata is part of the input.
Core Idea¶
The problem converts conjunction of regular-language constraints into reachability. Every input symbol advances all automata, and success occurs only when the resulting state tuple is jointly accepting.
Finite automata are individually simple, yet the combined state space grows multiplicatively. That succinctly represented explosion explains why the general decision problem occupies PSPACE.
Scope of Application¶
- Formal verification. Checks simultaneous regular constraints.
- String constraint solving. Tests existence of a common satisfying word.
- Automata theory. Illustrates complexity under intersection.
- Complexity reductions. Provides a canonical PSPACE-complete target.
Clarity¶
State automaton model, common alphabet, completeness conventions, number of automata, input encoding, acceptance condition, whether k is fixed, decision versus witness output, and complexity measure. Inclusion test: Require a finite collection of automata with a shared word domain and a yes/no question about existence of one word accepted by all of them. Exclusion test: Exclude emptiness of one automaton, union nonemptiness, pairwise-overlap checks that do not ensure one global witness, language equivalence, and intersection of arbitrary representations with different complexity assumptions. Nearest boundary: Pairwise nonempty intersections do not imply the total intersection is nonempty; the defining witness must satisfy every automaton simultaneously. Exit condition: The standard PSPACE-completeness claim changes when k is fixed, automata are of another type, alphabets are encoded differently, or succinct representations alter input size. Common misclassifications: Pairwise overlap does not guarantee total overlap. It is not the union non-emptiness problem. PSPACE-completeness assumes the automata list is part of the input. An explicit product is conceptually useful but need not be stored in full. Nearest named distinctions: DFA nonemptiness: Asks whether one automaton accepts any word. Union nonemptiness: Needs acceptance by at least one language. Language equivalence: Asks whether two languages contain the same words. Pairwise intersection: Does not establish a witness shared by the whole list.
Manages Complexity¶
Conjunction appears harmless at the language level while multiplying state dimensions. On-demand reachability preserves polynomial memory but cannot erase the combinatorial search implied by the compact input.
Abstract Reasoning¶
- Normalize alphabets and DFA transition conventions.
- Form the conceptual product start tuple and joint acceptance rule.
- Search synchronized reachable tuples without necessarily storing the full product.
- If successful, recover a common word from predecessor information or a second pass.
- State complexity under the exact automaton and input-parameter assumptions.
Knowledge Transfer¶
Synchronized-product reasoning transfers to concurrent verification and constraint conjunction, but PSPACE classification depends on representation and variable family size. Other automata may change decidability or complexity.
Relationships to Other Abstractions¶
Current abstraction Intersection Non-Emptiness Problem Domain-specific
Parents (1) — more general patterns this builds on
-
Intersection Non-Emptiness Problem is a kind of Computational problem Domain-specific
Intersection Non-Emptiness Problem is a strict kind of Computational problem: it asks a finite encoded yes/no question about whether automata share an accepted string.
Hierarchy path (1) — routes to 1 parentless root
- Intersection Non-Emptiness Problem → Computational problem → Function (Mapping)
Neighborhood in Abstraction Space¶
Intersection Non-Emptiness Problem sits in a crowded region of the domain-specific corpus (32nd percentile for distinctiveness): several abstractions share nearly its structure, so a description that fits it tends to fit its neighbors too.
Family — Formal Systems & Discrete Structures (18 abstractions)
Nearest neighbors
- Generalized Büchi Automaton — 0.92
- Superpermutation — 0.88
- Dyck language — 0.88
- Regular Expression — 0.88
- Formal Syntax — 0.88
Computed from structural-signature embeddings · 2026-10-08