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 ), is the index of the first constraint from lambda that is different to the corresponding constraint from . Thus the line

$exists p in mathsf{dpaths}(M,i) : big( bigwedge{p} big){downarrow}_{i}^{0} = m{downarrow}_{i}^{0} wedge$

has to be replaced by:

$exists p in mathsf{dpaths}(M,i) : big( bigwedge{p} big){downarrow}_{i-1}^{0} = m{downarrow}_{i-1}^{0} wedge$

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_b that are subsumed by $m_{fb}$ should be removed. Thus,

$E' := E' setminus { (q_f, m'', q_b) in E' mid m_mathit{fb} Rightarrow m'' }$

has to be replaced by:

$E' := E' setminus { (q_f, m'', q_b) in E' mid m'' Rightarrow m_mathit{fb} }$

Algorithm 3

On page 6 of the paper (page 365 in the procedings), in line 2 of Algorithm 3, has to be picked bigger than $mathit{type}(q_f)$ . Thus the second line of Algorithm 3

$max(mathsf{type}(q_f)+1, j) mathrm{is minimal})$

has to be replaced by:

$j = mathrm{min}({j' mid (x,j') in mathsf{dsuf}(M,m) wedge j' > mathsf{type}(q_f)})$

Furthermore, in lines 6 and 7 of Algorithm 3, the new edges should be annotated with the projection of . Thus the $6^mathit{th}$ and $7^mathit{th}$ lines of Algorithm 3

$begin{array}{l} cup { (q, m{downarrow}_{j-1}^{mathsf{type'}(q)}, q_b) } cup { (q_b, m{downarrow}_{mathsf{type'}(q')-1}^{j}, q') } end{array}$

have to be replaced by:

$begin{array}{l} cup { (q, m'{downarrow}_{j-1}^{mathsf{type}(q)}, q_b) } cup { (q_b, m'{downarrow}_{mathsf{type}(q')-1}^{j}, q') } end{array}$