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 PeterBackward Deterministic PrefixesOn page 6 of the paper (page 365 in the procedings), in line 4 (second line of the definition of dpref ), is the index of the first constraint from that is different to the corresponding constraint from . Thus the line has to be replaced by: Algorithm 1On page 6 of the paper (page 365 in the procedings), in line 8 of Algorithm 1, all edges from to that are subsumed by should be removed. Thus, has to be replaced by: Algorithm 3On page 6 of the paper (page 365 in the procedings), in line 2 of Algorithm 3, has to be picked bigger than . 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 . Thus the and lines of Algorithm 3 have to be replaced by: |