Federations: Exact Unions Of DBM Zones

This page answers the next question after DBM Basics: if one DBM already represents one convex zone exactly, what should we do when symbolic manipulation produces a non-convex set?

For UDBM, the answer is a federation: a finite union of DBMs. That is the next exact representation layer above one canonical DBM, and it is the reason why the high-level Python API is centered on pyudbm.Federation rather than on bare matrices alone [DHLP06_FED] [BEHR03_CDD] [UDBM_FED_H] [UDBM_FED_CPP].

This page is still a tutorial page first. So it does not start as a reference sheet. It first explains why federations become necessary at all, then why they matter for UDBM and pyudbm, and only after that does it inventory the current Federation surface in a more systematic way.

The goal is to make the connection between:

• the theory reason for federations,

• the native UDBM federation layer in fed.h / fed.cpp, and

• the current pyudbm API

explicit and easy to scan.

Why One DBM Stops Being Enough

The key limitation to remember from the previous page is simple:

• one DBM represents one convex zone

• symbolic algorithms do not stay inside the convex world forever

Subtraction is the cleanest place to see the break.

Take one outer zone \(Z\) and subtract one inner zone \(H\):

\[Z = \{(x,y) \mid 1 \leq x \leq 5,\; 1 \leq y \leq 5\}\]

\[H = \{(x,y) \mid 2 \leq x \leq 4,\; 2 \leq y \leq 4\}\]

\[R = Z \setminus H\]

The result is not convex anymore. It is one rectangular shell with a hole in the middle:

This is exactly the pressure described in the subtraction paper by David, Larsen, Lime, and Poulsen [DHLP06_FED]: once subtraction leaves the convex world, a single DBM is no longer a sufficient exact target.

In UDBM, the exact result therefore becomes a union of DBMs rather than one new matrix. In the current Python binding, the same example can be written directly:

from pyudbm import Context, IntValuation

c = Context(["x", "y"])
x = c.x
y = c.y

outer = (x >= 1) & (x <= 5) & (y >= 1) & (y <= 5)
hole = (x >= 2) & (x <= 4) & (y >= 2) & (y <= 4)
ring = outer - hole

assert ring.get_size() == 4

inside = IntValuation(c)
inside["x"] = 1
inside["y"] = 1

removed = IntValuation(c)
removed["x"] = 3
removed["y"] = 3

assert ring.contains(inside)
assert not ring.contains(removed)

Mathematically, that means

\[R = D_1 \cup D_2 \cup D_3 \cup D_4\]

with each \(D_i\) still an ordinary convex DBM zone.

What A Federation Means In UDBM

A federation is not a mysterious new constraint language. It is a finite union of ordinary DBM zones:

\[F = D_1 \cup D_2 \cup \cdots \cup D_n\]

where every \(D_i\) is still one convex DBM.

That design choice matters for two reasons.

First, it preserves the DBM machinery instead of replacing it. The algorithms for closure, relation checks, delay, reset, and containment still operate at the DBM level; the federation layer lifts them to finite unions [UDBM_FED_H] [UDBM_FED_CPP].

Second, it keeps non-convex symbolic states exact. In the native code, this is the job of fed_t in fed.h / fed.cpp. The implementation is not a diagram structure like a CDD. It is an explicit federation layer with set operations, subtraction, reduction, predecessor-style operators, and relation checks on unions of DBMs [DHLP06_FED] [BEHR03_CDD].

What Federations Can Do

The current Federation operations and properties can be grouped like this:

This table focuses on the semantics-facing Federation surface currently exposed by the Python binding. It intentionally excludes object-infrastructure helpers such as copy(), plot(), textual rendering, and hashing.

API	Kind	Semantics	Mutation Style	Jump To Details
to_dbm_list()	Representation	Exact	Returns snapshots	Decomposing A Federation With to_dbm_list()
get_size()	Representation	Exact	Query only	Counting Pieces With get_size()
&	Set operation	Exact	Returns new federation	Exact Intersection &
|	Set operation	Exact	Returns new federation	Exact Union |
+	Set operation	Convex over-approximation	Returns new federation	Convex Union +
-	Set operation	Exact	Returns new federation	Exact Difference -
up()	Time transform	Exact	Returns new federation	Delay Successor up()
down()	Time transform	Exact	Returns new federation	Inverse Delay down()
free_clock()	Clock transform	Exact	Returns new federation	Forgetting One Clock With free_clock()
set_zero()	Re-initialization	Exact	Mutates self	Re-initializing To The Origin With set_zero()
has_zero()	Property	Exact	Query only	Zero-Point Queries: has_zero() And is_zero()
set_init()	Re-initialization	Exact	Mutates self	Re-initializing To The Positive Initial Zone With set_init()
convex_hull()	Shape transform	Convex over-approximation	Returns new federation	Convex Hull With convex_hull()
== / !=	Relation	Exact	Query only	Relations: ==, !=, <=, >=, <, >
<= / >= / < / >	Relation	Exact	Query only	Relations: ==, !=, <=, >=, <, >
intern()	Representation maintenance	Geometry-preserving	Mutates internal sharing state	Representation Quality: reduce() And intern()
predt()	Temporal transform	Exact	Returns new federation	Temporal Predecessor predt()
contains()	Membership	Exact	Query only	Containment contains()
update_value()	Clock assignment	Exact	Returns new federation	Updating And Resetting Clocks: update_value() And reset_value()
reset_value()	Clock assignment	Exact	Returns new federation	Updating And Resetting Clocks: update_value() And reset_value()
reduce()	Representation maintenance	Geometry-preserving	Mutates self	Representation Quality: reduce() And intern()
extrapolate_max_bounds()	Abstraction	Over-approximation	Returns new federation	Max-Bound Extrapolation extrapolate_max_bounds()
is_zero()	Property	Exact	Query only	Zero-Point Queries: has_zero() And is_zero()
is_empty()	Property	Exact	Query only	Empty Federations With is_empty()

Representation And Structural Queries

Decomposing A Federation With to_dbm_list()

The most direct way to see what a federation is internally is to export its DBM pieces:

from pyudbm import Context

c = Context(["x", "y"])
x = c.x
y = c.y

fed = ((x >= 1) & (x <= 2) & (y >= 1) & (y <= 3)) | ((x >= 4) & (x <= 5) & (y >= 2) & (y <= 4))
pieces = fed.to_dbm_list()
piece_texts = sorted(dbm.to_string() for dbm in pieces)

assert len(pieces) == 2
assert piece_texts == [
    "(1<=x & 1<=y & x<=2 & y<=3)",  # D1
    "(4<=x & 2<=y & x<=5 & y<=4)",  # D2
]

This is exact representation inspection, not approximation. It is especially useful when subtraction or exact union has produced several convex pieces. In this example the strings make the two pieces explicit: D1 is the left rectangle and D2 is the right one. The sort step is only there so the example does not depend on internal list ordering.

Counting Pieces With get_size()

The same decomposition figure also explains get_size():

assert fed.get_size() == 2

get_size() counts native DBMs, not visible edges, constraints, or vertices. So its meaning is representational: how many convex components are currently stored in the federation.

Representation Quality: reduce() And intern()

Federations are not only about set semantics. Once many DBMs accumulate, their representation quality starts to matter too:

reduce() can simplify a structurally awkward federation without changing its geometry. A compact example is x <= 1 | x >= 1: the left panel stores that set as two DBMs, while the middle panel shows the same region after it has been reduced to one canonical piece:

complex_fed = (x <= 1) | (x >= 1)
assert complex_fed.get_size() == 2

complex_fed.reduce()
assert complex_fed.get_size() == 1
assert complex_fed == (x >= 0)

intern() is different. It is not a geometric or semantic transformation at all. It asks UDBM to share equal canonical DBMs internally through its hash tables:

complex_fed.intern()
assert complex_fed.get_size() == 1
assert complex_fed == (x >= 0)

So the right mental split is:

• reduce() tries to improve the visible DBM list

• intern() tries to improve internal sharing and equality costs

• neither is supposed to change the symbolic set

Set Operations

Exact Intersection &

Intersection stays inside the exact symbolic world:

left = (x >= 1) & (x <= 4) & (y >= 1) & (y <= 4)
right = (x >= 3) & (x <= 5) & (y >= 2) & (y <= 5)
exact_intersection = left & right

The first two panels already overlay the other operand, so the overlapping corner is visible before you even look at the result. In the last panel, A and B stay as dashed references and the filled area is exactly A & B.

The result is exact and usually still convex enough to fit into one DBM.

Exact Union |

Exact union keeps all pieces and keeps all gaps:

The result panel keeps the two convex pieces separate, so the gap remains part of the geometry:

exact = a | b

This is the natural federation-building operation when symbolic branching or subtraction has produced multiple exact components.

Convex Union +

+ is not the same as |. It computes UDBM’s convex-union style addition:

hull_like = a + b

For the separated example in the figure, that fills the gap and introduces new valuations. So + is already an over-approximation-style operation, not a plain exact set union.

This distinction between | and + is exactly where the geometric difference between exact union and convex hull-like combination belongs: the left panel keeps the gap, the right panel fills it. Federation support is therefore not just “store several DBMs in one object”; different operators really do have different symbolic meanings.

Exact Difference -

Subtraction is the cleanest place where one DBM stops being enough, which is why it already appeared in the tutorial motivation above. At the API level the same idea is simply:

ring = outer - hole

Transformations On Federations

Delay Successor up()

up() lifts the usual DBM delay successor to every DBM in the federation:

delayed = fed.up()

Semantically, upper bounds against the zero clock are relaxed so time can elapse.

Inverse Delay down()

down() is the temporal predecessor counterpart:

predecessor = fed.down()

This relaxes lower bounds so that delaying can lead into the current federation.

Forgetting One Clock With free_clock()

Freeing a clock removes the informative constraints involving it:

freed = fed.free_clock(y)

Geometrically, this often turns a bounded shape into a strip or half-space.

Re-initializing To The Origin With set_zero()

set_zero() mutates the federation into the single origin valuation:

zone.set_zero()
assert zone.has_zero()

This is exact, not symbolic shorthand.

Re-initializing To The Positive Initial Zone With set_init()

set_init() replaces the current federation by the standard non-negative initial zone:

zone.set_init()
assert str(zone) == "true"

This is the UDBM-style “all clocks are non-negative, otherwise unconstrained” initial symbolic state.

Convex Hull With convex_hull()

convex_hull() works on one federation and computes one convex over-approximation:

hull = exact.convex_hull()

This differs from + only in arity and use style:

• a + b combines two arguments by convex union

• f.convex_hull() hulls all DBMs already inside one federation

Temporal Predecessor predt()

predt() computes states that may delay into a good region while avoiding a bad one:

pred = good.predt(bad)

This is one of the places where the federation layer clearly behaves like a symbolic-state engine rather than only a container of matrices.

Updating And Resetting Clocks: update_value() And reset_value()

Both operations assign one clock a concrete value:

updated = fed.update_value(x, 2)
reset = fed.reset_value(x)

reset_value(clock) is just the 0-specialized case of update_value(clock, value).

Max-Bound Extrapolation extrapolate_max_bounds()

Extrapolation is where the tutorial leaves exact symbolic semantics and enters abstraction for termination:

abstracted = fed.extrapolate_max_bounds({"x": 100, "y": 100})

The point is not to preserve the exact original federation. The point is to drop constraints that exceed the maximal constants and keep the analysis finite [UDBM_FED_H].

Queries And Properties

Containment contains()

The properties figure contains a direct membership picture:

In the contains panel, one point lies inside the federation and one lies in the gap:

assert fed.contains(inside_point)
assert not fed.contains(outside_point)

This is valuation membership in the most literal sense.

Zero-Point Queries: has_zero() And is_zero()

The same figure distinguishes two related but different questions:

• has_zero() asks whether the origin belongs to the federation at all

• is_zero() asks whether the whole federation is exactly the origin zone

That is why the hasZero panel still shows a nontrivial region, while the isZero panel collapses to the single point \((0,0)\).

Empty Federations With is_empty()

The last panel of the properties figure illustrates the empty case. This is the result of contradictory constraints, for example:

empty = (x == 1) & (x != 1)
assert empty.is_empty()

Relations: ==, !=, <=, >=, <, >

The six comparison operators deserve their own gallery:

Each panel shows one representative witness. For the non-strict operators <= and >=, equality would also be allowed even though the pictured example uses proper containment.

• A == B means same symbolic set

• A != B means different symbolic sets

• A <= B means subset

• A >= B means superset

• A < B means strict subset

• A > B means strict superset

In other words, the comparison operators on federations are set-theoretic, not lexical or object-identity based.

Important Takeaways

Several distinctions matter a lot in practice:

• A federation is still built from DBMs. It does not replace DBMs; it sits one layer above them.

• Subtraction is where federations stop looking optional. Non-convex results are a semantic fact, not a UI choice.

• Exact union and convex union are different operations. They should not be explained as if one were just a faster version of the other.

• Reduction and interning are about representation quality. They matter because federation size and internal sharing affect later symbolic work.

• Extrapolation is not an exact transform. It is an intentional abstraction step.

• The public Python surface follows the native semantic layer closely. This is why the restored API has to center on Federation rather than only on one DBM at a time.

Next

The next natural topic after federations is CDD Basics: How Shared Decision Graphs Compress Non-Convex Symbolic Sets: once finite unions of zones become first-class, the next question is whether an explicit list of DBMs is always the best representation, or whether shared diagram structures sometimes compress the same symbolic set better.

References

[DHLP06_FED] (1,2,3)

Alexandre David, Kim G. Larsen, Didier Lime, and Brian H. Poulsen. Subtracting Clock Zones. Public link: https://homes.cs.aau.dk/~adavid/dhlp06-zones.pdf. Repository guide: https://github.com/HansBug/pyudbm/blob/main/papers/dhlp06/README.md.

[BEHR03_CDD] (1,2)

Gerd Behrmann. Efficient Timed Reachability Analysis using Clock Difference Diagrams. Public link: https://www.brics.dk/RS/98/47/BRICS-RS-98-47.pdf. Repository guide: https://github.com/HansBug/pyudbm/blob/main/papers/behrmann03/paper-c/README.md.

[UDBM_FED_H] (1,2,3)

UPPAALModelChecker. UDBM/include/dbm/fed.h. Public link: https://github.com/UPPAALModelChecker/UDBM/blob/d83b703126fb88b3565c71cca68e360227dfb192/include/dbm/fed.h.

[UDBM_FED_CPP] (1,2)

UPPAALModelChecker. UDBM/src/fed.cpp. Public link: https://github.com/UPPAALModelChecker/UDBM/blob/d83b703126fb88b3565c71cca68e360227dfb192/src/fed.cpp.