时间自动机两种模型的构造互模拟研究

基于时间自动机不同模型的验证被工业界广泛应用,本文形式描述了两种这样的模型,给出了从事件时钟自动机到双向时间自动机的构造方法,证明了二者识别语言之间的包含关系。