Errata

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
$\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, j has to be picked bigger than 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 m’. Thus the 6^th and 7^th lines of Algorithm 3
$\cup\ \{ (q, m{\downarrow}_{j-1}^{\mathsf{type'}(q)}, q_b) \}\\ \cup\ \{ (q_b, m{\downarrow}_{\mathsf{type'}(q')-1}^{j}, q') \}$
have to be replaced by
$\cup\ \{ (q, m'{\downarrow}_{j-1}^{\mathsf{type}(q)}, q_b) \}\\ \cup\ \{ (q_b, m'{\downarrow}_{\mathsf{type}(q')-1}^{j}, q') \}$ .