经典的ω-有穷自动机用于系统验证时抽离了时间特性，不适用于研究与物理过程发生交互的系统。时间自动机扩充时间因素于经典ω-有穷自动机，从而把握实时系统的行为，提供有穷控制实时系统的验证和特定时间延迟问题的解决方案。目前已成为对实时并发系统进行模拟和验证的有效工具，广泛应用于时态逻辑、Petri网、协议验证和回路验证等。 时间自动机理论的一个重要方面是时间自动机在不同识别条件下识别时间语言的能力及时间语言在布尔运算下的封闭性。不同识别条件决定不同的时间自动机识别模型。目前对时间自动机仅讨论了C₁，C₅，C₃，E，I，L条件下的识别模型。本文提出并深入讨论提出另四种经典识别条件C₂，C₃，C₄，C₆和对C_i（i=1…6）取反所得新条件下的时间自动机识别模型。 时间自动机用于实时验证的关键步骤是区域自动机的构造。经典区域自动机模型存在如下缺陷：时钟常量取值限制在有理数范围不合理；时钟区域划分过于细小，与时间自动机对应关系不直接。本文提出一种新的区域自动机模型；长跨度区域自动机。该模型允许时钟常量取实数值，并增大时钟区域的时间跨度，从而简化构造步骤，取得较优的时间和空间复杂度。这将极大提高实时验证的效率。