## Errata to the paper “Fully Symbolic Timed Model Checking using Constraint Matrix Diagrams” by Rüdiger Ehlers, Daniel Fass, Michael Gerke, and Hans-Jörg Peter

### Backward Deterministic Prefixes

On page 6 of the paper (page 365 in the procedings), in line 4 (second line of the definition of *dpref* ), *i* is the index of the first constraint from *Λp* that is diffrent to the corresponding constraint from *m*. Thus the line

has to be replaced by

.

### Algorithm 1

On page 6 of the paper (page 365 in the procedings), in line 8 of Algorithm 1, all edges from *q _{f}* to

*q*that are subsumed by

_{b}*m*should be removed. Thus

_{fb}has to be replaced by

.

### Algorithm 3

On page 6 of the paper (page 365 in the procedings), in line 2 of Algorithm 3, *j* has to be picked bigger than *type(q _{f} )*. Thus the second line of Algorithm 3

has to be replaced by

.

Furthermore, in lines 6 and 7 of Algorithm 3, the new edges should be annotated with the projection of

*m’*. Thus the 6

^{th}and 7

^{th}lines of Algorithm 3

have to be replaced by

.