Consider system of equations of the form

where variables are interpreted as sets of integers, and are expressions built from variables , constants sets , addition (interpreted element-wise as , union ,  and a restricted form of intersection. Namely, we allow expressions of the form  with and expression and a constant denoting a semilinear subset of .

(The study of such systems of equations stems from the analysis of pushdown automata over timed atoms [1], where equations in the form above are used to represent the delays of the timestamps of stack symbols between the time of push and the time of the corresponding pop.)

A solution is an assignment of a subset of integers to each variable . We are interested in the emptiness problem: is empty in the least solution of a given system of equations as above? For example, natural numbers are the least solution to and even integers are the least solution to . Finite sets of constants like can be succinctly expressed by small equations using their binary expansion.

Note that the use of intersection in  is severely restricted. If intersections of the form for two variables are allowed, then the emptiness problem is equivalent to the emptiness problem of conjunctive grammars, and the latter problem is undecidable  [2].

On the other hand, emptiness is in PTIME if no intersection is allowed: By interpreting the commutative as the noncommutative language concatenation  (which preserves emptiness in the absence of intersections), we reduce to a context-free grammar—whose emptiness problem is solvable in PTIME.

Not all decision problems need be computationally simple, even in the absence of intersections. The -membership problem, which asks whether  (i.e., a word with the same number of ‘s and ‘s in the noncommutative view) is in the least solution, is NP-complete. This is an interesting example where parsing is harder than emptiness—it is usually the other way around, e.g., for conjunctive grammars emptiness is undecidable, while parsing is decidable (even in PTIME [2]).

Emptiness for equations where only intersections with finite are allowed, is NP-complete too. This can be shown by a simple iterative algorithm computing coarser and coarser under-approximations of the least solution, using at each step an oracle for the -membership problem for intersection-less equations.

The general case of intersections with semilinear is open. The emptiness problem in this case is equivalent to the emptiness problem for the class of timed poshdown automata [1]. We conjecture that the problem decidable in this case, and that, moreover, the least solution is semilinear.

REFERENCES

[1] L. Clemente and S. Lasota, “Timed Pushdown Automata”, LICS’15.

[2] A. Jez and A. Okhotin, “Conjunctive grammars over a unary alphabet: Undecidability and unbounded growth,” Theory Comput. Syst., vol. 46, no. 1, pp. 27–58, 2010.