The Containment Problem for Unambiguous Register Automata and Unambiguous Timed Automata

Abstrakt

We investigate the complexity of the containment problem "Does L(A) SUBSET OF OR EQUAL TO 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.

Klíčová slova

• Containment
• Problem
• for
• Register
• Unambiguous
• Timed
• Automata