Alexandre David

BRICS, Aalborg University, Denmark.

Time: Wednesday 3.11.2004, 14:30
Place: Room A4-108, Fr. Bajersvej 7

The DBM Library of UPPAAL and DBM Substractions

DBMs (Difference Bound Matrices) are efficient data structures to represent clock constraints for verification of timed systems, in particular timed automata. A DBM stores constraints of the form x_i-x_j