时间自动机被广泛用于实时系统验证和模型检测。一方面出现了很多算法和工具;另一方面有不少基于时间自动机的不同模型被提出,以适应不同类型的系统验证。信号自动机与时间树自动机是两个新提出的模型。 时间树自动机理论还很不完善,目前主要是基于时间树自动机识别的语言类及相关性质的研究。本文提出了一个时间树自动机识别语言的一个条件,并证明了结论的正确性。如果一个语言不能满足该条件,它一定不能被时间树自动机识别。这为证明一个具体语言不能被时间树自动机识别提供了思路。 信号自动机为一类实时系统建立了比普通时间自动机更适合的模型。本文通过对信号自动机与时间自动机的模型对比与深入分析,证明了两种模型的行为等价关系,并提出了互模拟算法,这样信号自动机验证问题被归约为时间自动机验证问题。如果把这样的互模拟算法与时间自动机验证算法组合在一起,就可以得到信号自动机验证算法,以便在此基础上开发出信号自动机验证工具。 在基因工程中,形式化方法被用于预测人工基因网络控制生物基因网络的行为结果,这种预测已经在生物医药研制与开发领域发挥了很大作用。目前已有的基于有限状态自动机的方法的局限是不能描述系统时间约束。本文提出了基于时间自动机的基因网络逻辑模型,以计算时间约束下控制基因网络的行为。