Differenzgebundene Matrizen (DBMs) sind effiziente Datenstrukturen, um Taktbeschränkungen in zeitgesteuerten Zustandsautomaten auszudrücken. Sie werden in UPPAAL als die Kerndatenstruktur zur Darstellung von Zeit genutzt. Diese Bibliothek bietet alle üblichen Operationen wie Up (Verzögerung oder Zukunft), Down (Vergangenheit), allgemeine Updates und verschiedene Extrapolationsfunktionen auf DBMs und Föderationen. Die Bibliothek unterstützt auch Subtraktionen und Methoden zum Vereinen von DBMs.