### Abstract

Original language | English |
---|---|

Publisher | ITU Copenhagen |

Pages | 4 |

Publication status | Published - 2004 |

### Bibliographical note

Nordic Workshop on Programming Theory### Keywords

- DBM
- Subtraction
- Model-checking
- UPPAAL

### Cite this

*Minimal DBM Substraction*. (pp. 4). ITU Copenhagen.

}

**Minimal DBM Substraction.** / David, Alexandre; Håkansson, John; G. Larsen, Kim; Pettersson, Paul.

Research output: Working paper › Research

TY - UNPB

T1 - Minimal DBM Substraction

AU - David, Alexandre

AU - Håkansson, John

AU - G. Larsen, Kim

AU - Pettersson, Paul

N1 - Nordic Workshop on Programming Theory

PY - 2004

Y1 - 2004

N2 - In this paper we present an algorithm to compute DBM substractions with a guaranteed minimal number of splits and disjoint DBMs to avoid any redundance. The substraction is one of the few operations that result in a non-convex zone, and thus, requires splitting. It is of prime importance to reduce the number of generated DBMs in an exploration loop, e.g., for reachability, because the result is propagated and serves to compute further successors later.

AB - In this paper we present an algorithm to compute DBM substractions with a guaranteed minimal number of splits and disjoint DBMs to avoid any redundance. The substraction is one of the few operations that result in a non-convex zone, and thus, requires splitting. It is of prime importance to reduce the number of generated DBMs in an exploration loop, e.g., for reachability, because the result is propagated and serves to compute further successors later.

KW - DBM

KW - Subtraction

KW - Model-checking

KW - UPPAAL

M3 - Working paper

SP - 4

BT - Minimal DBM Substraction

PB - ITU Copenhagen

ER -