Clock Matrix Diagrams
Daniel Fass
The success of the timed model checker Uppaal heavily relies on the use of Difference Bound Matrices (DBM) as the main data structure for storing reachability information symbolically. However, since DBM are only capable of representing convex sets, they are inappropriate for applications such as game solving where non-convex sets may arise.
There are currently two independent approaches to tackle this problem: Clock Federations and Clock Difference Diagrams. While Clock Federations are based on linear lists of DBM, Clock Difference Diagrams are BDD-like tree structures where each node refers to a single difference constraint. Despite the space-efficiency of difference diagrams, concerning running time they are often outperformed by federations which in turn benefit from the convex efficiency of DBM.
In this thesis, we will present Clock Matrix Diagrams, a novel data structure that combines the space-efficiency of decision diagrams with the convex efficiency of DBM. We show that our data structure is a generalisation of DBM, Clock Federations, and Clock Difference Diagrams, which makes it universally usable.
Bachelor Thesis.