## 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 qf to qb that are subsumed by mfb should be removed. Thus

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(qf ). 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 6th and 7th lines of Algorithm 3

have to be replaced by
.