摘要：本文介绍一种具有优先级扩展的时间自动机模型，并对一种计算DBM减法算法进行改进。这种减法是DBM上操作中的一种，它会产生需要用DBM集来表示的非凸集合。DBM的数量影响符号模型检测的性能，我们的减法算法是有效的，因为它产生的DBM的数量相对于最初算法具有较大程度的约减。DBM减法操作扩展了具有优先级的时间自动机理论，它对于具有紧急行为的变换描述、死锁检测、时间博弈等问题具有非常重要的作用。

关键词：时间自动机 优先级 dbm 减法 

单位：郑州大学信息工程学院 河南郑州450001