摘要：为了对一种特定的时间Petri网模型的性质进行分析和验证,给出了一种将时间Petri网转化为时间自动机的方法。将时间Petri网转化为时间自动机后,就可用常见的基于时间自动机的模型检测工具去验证系统是否满足某些必要的性质。

关键词：时间petri网 时间自动机 模型验证 性质分析 

单位：中国科学院计算机科学国家重点实验室 山东建筑大学计算机科学与技术学院