Branching data structures for real-time model checking not as good as thought

Abstract

Clock Difference Diagrams (CDDs), BDD-like data structures for model checking of timed automata, were presented as alternatives for classic DBM representation. However, work on them seems to have stopped, although there are still important open questions. CDD definition required that repeated subtrees were aliased, but no clear algorithm was presented for producing such compact representation, which seems costly to achieve. In this article we describe our implementation of such aliased subtrees and revisit CDDs by comparing their performance against DBMs on current case studies, with and without repeated subtrees. Our experiments show that CDDs still require more time and memory than DBMs, suggesting that eliminating repetitions is still not enough. Thus, this article re-opens issues that previous work on the topic considered closed.