Using sharing trees in the automated analysis of real-time systems with data

Reachability analysis and model checking of timed automata are now well-established techniques in the analysis of real-time control systems. The major limiting factor in their use, from a technical point of view, remains the state explosion problem. Symbolic representation of the state space often allows for the analysis of much larger systems than the point-wise representation which is common in enumerative analysis. In particular, the use of rooted, ordered binary decision diagrams (ROBDDs) has been successful, mainly in the analysis of hardware systems where the need for a compact representation of boolean functions is prevalent. However in software systems, it is often desirable to represent data types which are more complicated than booleans. The use of sharing trees, which eliminates the requirement to find a boolean encoding of all data types, may offer a more attractive alternative to ROBDDs in these circumstances. This paper considers the use of sharing trees in the context of automata derived from a timed algebra of asynchronous broadcasting systems. It suggests that an encoding of timing constraints may be more easily incorporated into a sharing tree representation of the state space than into one based on ROBDDs