The Containment Problem for Unambiguous Register Automata and Unambiguous Timed Automata

摘要

We investigate the complexity of the containment problem "Does L(A) subset of L(B) hold?" for register automata and timed automata, where B is assumed to be unambiguous and A is arbitrary. We prove that the problem is decidable in the case of register automata over (N,=), in the case of register automata over (Q,) when B has a single register, and in the case of timed automata when B has a single clock. We give a 2-EXPSPACE algorithm in the first case, whose complexity is a single exponential in the case that B has a bounded number of registers. In the other cases, we give an EXPSPACE algorithm.