Fully Symbolic Timed Model Checking using Constraint Matrix Diagrams
Rüdiger Ehlers, Daniel Fass, Michael Gerke, and Hans-Jörg Peter
We present constraint matrix diagrams (CMDs), a novel data structure for the fully symbolic reachability analysis of timed automata. CMDs combine matrix-based and diagram-based state space representations generalizing the concepts of difference bound matrices (DBMs), clock difference diagrams (CDDs), and clock restriction diagrams (CRDs). The key idea is to represent convex parts of the state space as (partial) DBMs which are, in turn, organized in a CDD/CRD-like ordered and reduced diagram. The location information is incorporated as a special Boolean constraint in the matrices. We describe all CMD operations needed for the construction of the transition relation and the reachability fixed point computation. Based on a prototype implementation, we compare our technique with the timed model checkers RED and Uppaal, and furthermore investigate the impact of two different reduced forms on the time and space consumption.