A Semi-decision Procedure for Testing Language Inclusion of Nondeterministic Timed Automata

Abstract: We give a new semi-decision procedure for testing language inclusion of nondeterministic timed automata (NTA). We show that the language generated by a {\em progressive} timed automaton can be tested for inclusion against the language generated by {\em any} NTA. In practice, many timed automata models of actual physical systems are progressive, so that the full expressiveness of NTA can be used to specify real-time properties. These include models of asynchronous digital circuits. The semi-decision procedure is also a reduction of the language inclusion problem for NTA to the language inclusion problem for nondeterministic effective infinite-state $\omega$-automata.



Resumo: Nós apresentamos um novo procedimento de semidecisão para testar inclusão de linguagem de autômatos temporais não determinísticos (NTA). Mostramos que a linguagem gerada por um autômato temporal {\em progressivo} pode ser testada para inclusão contra a linguagem gerada por qualquer NTA. Na prática, muitos modelos de autômatos temporais de sistemas físicos reais são progressivos, de modo que toda a expressividade de NTA pode ser usada para especificar propriedades de tempo-real. Entre esses, estão modelos de circuitos digitais assíncronos. O procedimento de semidecisão é, também, uma redução do problema de inclusão de linguagem de NTA para o problema de inclusão de linguagem para $\omega$-autômatos não determinísticos, efetivos e de estados infinitos.

2000