关键词: 时间自动机 优先级 DBM 减法

Abstract:

In this paper an extension of timed automata with priorities is introduced, and we present an improved algorithm to compute subtraction on DBMs. The s ubtraction 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.

Key words: timed automata, priorities ;DBM, subtraction