论文部分内容阅读
时间自动机被广泛用于实时系统验证和模型检验．为适应不同类型的系统验证需要。不少时间自动机的相关模型被提出．时间树自动机是这样的新模型之一．目前主要是针对时间树自动机识别的语言类及相关性质的研究．本文提出了时间树自动机识别语言的一个条件，并证明了结论的正确性．如果一个语言不能满足该条件，它一定不能被时间树自动机识别．这为证明一个具体语言不能被时间树自动机识别提供了思路．