31 janvier 2011
Nathalie Tali Sznajder (LSV)We investigate the applicability of automata constructions that avoid determinization for solving language inclusion and synthesis for real time specifications. While timed language inclusion is undecidable for the class of timed languages definable by classical timed automata, there are interesting subclasses of timed languages for which language inclusion is decidable. In particular, it has been shown that the language inclusion problem for event clock automata is PSPACE complete for both finite and infinite words. For infinite words, those results are obtained using an adaptation of the Safra construction to this subclass of timed automata. Realizability problem for timed specifications consists in, given a specification for a timed system interacting with an uncontrollable environment, deciding the existence of a program for such a system such that all its executions (in interaction with the environment) will meet the specification. This problem is undecidable in general, but has been shown decidable when the specification is given in some fragment of Event Clock Logic. Again, the procedure uses the determinization of a Büchi automaton. Unfortunately, Safra construction leads to state spaces that are highly complex and difficult to handle in practice. We show how we can solve this two problems without determinization of automata, by defining Alternating Event Clock Automata.