Autômatos com relógios ("timed automata") e autômatos híbridos. Ferramentas para análise de sistemas usando técnicas formais envolvendo autômatos com relógios e autômatos híbridos. Complexidade dos formalismos.