Minimal DBM Substraction

Alexandre David, John Håkansson, Kim G. Larsen, Paul Pettersson

Publikation: Working paperForskning

142 Downloads (Pure)

Resumé

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.
OriginalsprogEngelsk
UdgiverITU Copenhagen
Sider4
StatusUdgivet - 2004

Bibliografisk note

Nordic Workshop on Programming Theory

Citer dette

David, A., Håkansson, J., G. Larsen, K., & Pettersson, P. (2004). Minimal DBM Substraction. (s. 4). ITU Copenhagen.
David, Alexandre ; Håkansson, John ; G. Larsen, Kim ; Pettersson, Paul. / Minimal DBM Substraction. ITU Copenhagen, 2004. s. 4
@techreport{3bfb06d09c2d11db8ed6000ea68e967b,
title = "Minimal DBM Substraction",
abstract = "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.",
keywords = "DBM, Subtraction, Model-checking, UPPAAL",
author = "Alexandre David and John H{\aa}kansson and {G. Larsen}, Kim and Paul Pettersson",
note = "Nordic Workshop on Programming Theory",
year = "2004",
language = "English",
pages = "4",
publisher = "ITU Copenhagen",
type = "WorkingPaper",
institution = "ITU Copenhagen",

}

David, A, Håkansson, J, G. Larsen, K & Pettersson, P 2004 'Minimal DBM Substraction' ITU Copenhagen, s. 4.

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

ITU Copenhagen, 2004. s. 4.

Publikation: Working paperForskning

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 -

David A, Håkansson J, G. Larsen K, Pettersson P. Minimal DBM Substraction. ITU Copenhagen. 2004, s. 4.