Model Checking Timed Automata with Priorities Using DBM Subtraction

@incollection{citeulike:2900502, abstract = {In this paper we describe an extension of timed automata with priorities, and efficient algorithms to compute subtraction on DBMs (difference bounded matrices), needed in symbolic model-checking of timed automata with priorities. The subtraction is one of the few operations on DBMs that result in a non-convex set needing sets of DBMs for representation. Our subtraction algorithms are efficient in the sense that the number of generated DBMs is significantly reduced compared to a naive algorithm. The overhead in time is compensated by the gain from reducing the number of resulting DBMs since this number affects the performance of symbolic model-checking. The uses of the DBM subtraction operation extend beyond timed automata with priorities. It is also useful for allowing guards on transitions with urgent actions, deadlock checking, and timed games.}, author = {David, Alexandre and H\r{a}kansson, John and Larsen, Kim and Pettersson, Paul }, citeulike-article-id = {2900502}, doi = {10.1007/11867340\_10}, journal = {Formal Modeling and Analysis of Timed Systems}, keywords = {modelchecking, timedautomata}, pages = {128--142}, posted-at = {2008-06-17 03:21:49}, priority = {2}, title = {Model Checking Timed Automata with Priorities Using DBM Subtraction}, url = {http://dx.doi.org/10.1007/11867340\_10}, year = {2006} }

TY - CHAP ID - citeulike:2900502 L3 - citeulike-article-id:2900502 TI - Model Checking Timed Automata with Priorities Using DBM Subtraction JF - Formal Modeling and Analysis of Timed Systems SP - 128 EP - 142 N2 - In this paper we describe an extension of timed automata with priorities, and efficient algorithms to compute subtraction on DBMs (difference bounded matrices), needed in symbolic model-checking of timed automata with priorities. The subtraction is one of the few operations on DBMs that result in a non-convex set needing sets of DBMs for representation. Our subtraction algorithms are efficient in the sense that the number of generated DBMs is significantly reduced compared to a naive algorithm. The overhead in time is compensated by the gain from reducing the number of resulting DBMs since this number affects the performance of symbolic model-checking. The uses of the DBM subtraction operation extend beyond timed automata with priorities. It is also useful for allowing guards on transitions with urgent actions, deadlock checking, and timed games. KW - modelchecking KW - timedautomata AU - David, Alexandre AU - Håkansson, John AU - Larsen, Kim AU - Pettersson, Paul PY - 2006/// UR - http://dx.doi.org/10.1007/11867340_10 ER -