Minimal DBM Substraction

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

Research output: Working paperResearch

149 Downloads (Pure)

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.
Original languageEnglish
PublisherITU Copenhagen
Pages4
Publication statusPublished - 2004

Bibliographical note

Nordic Workshop on Programming Theory

Keywords

  • DBM
  • Subtraction
  • Model-checking
  • UPPAAL

Cite this

David, A., Håkansson, J., G. Larsen, K., & Pettersson, P. (2004). Minimal DBM Substraction. (pp. 4). ITU Copenhagen.
David, Alexandre ; Håkansson, John ; G. Larsen, Kim ; Pettersson, Paul. / Minimal DBM Substraction. ITU Copenhagen, 2004. pp. 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, pp. 4.

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

ITU Copenhagen, 2004. p. 4.

Research output: Working paperResearch

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, p. 4.