Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction

During the past few years, a number of verification tools have been developed for real--time systems in the framework of timed automata (e.g. Kronos and Uppaal). One of the major problems in applying these tools to industrial-size systems is the huge memory--usage for the exploration of the state--space of a network (or product) of timed automata, as the modelcheckers must keep information on not only the control structure of the automata but also the clock values specified by clock constraints. In this paper, we present a compact data structure for representing clock constraints. The data structure is based on an O(n 3 ) algorithm which, given a constraint system over real--valued variables consisting of bounds on differences, constructs an equivalent system with a minimal number of constraints. In addition, we have developed an on--the--fly reduction technique to minimize the space--usage. Based on static analysis of the control structure of a network of timed automata, we are abl..