Memory efficient data structures for explicit verification of timed systems

Abstract. Timed analysis of real-time systems can be performed us-ing continuous (symbolic) or discrete (explicit) techniques. The explicit state-space exploration can be considerably faster for models with mod-erately small constants, however, at the expense of high memory con-sumption. In the setting of timed-arc Petri nets, we explore new data structures for lowering the used memory: PTries for efficient storing of configurations and time darts for semi-symbolic description of the state-space. Both methods are implemented as a part of the tool TAPAAL and the experiments document at least one order of magnitude of memory savings while preserving comparable verification times.