一种基于优先级扩展的时间自动机模型中DBM减法算法的改进

Improvement on a DBM Subtraction Algorithm in Timed Automata with Priorities

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

In this paper an extension of timed automata with priorities is introduced, and we present an improved algorithm to compute subtraction on DBMs. The subtraction is one of the few operations on DBMs that result in non-convex set needing sets of DBMs for representation. The number of DBMs influences the per/ormance of model checking. Our subtraction algorithm is efficient in the sense that the number of generated DBMs is significantly reduced compared to a naive algorithrn. The DBM subtraction operation extends the theory of timed automata with priorities. It is useful in the desctription of transition with urgent actions, dead lock checking,and timed games.