Memory efficient data structures for explicit verification of timed systems

Peter Gjøl Jensen, Kim Larsen, Jiri Srba, Mathias Grund Sørensen, Jakob Haar Taankvist

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

7 Citations (Scopus)


Timed analysis of real-time systems can be performed using continuous (symbolic) or discrete (explicit) techniques. The explicit state-space exploration can be considerably faster for models with moderately small constants, however, at the expense of high memory consumption. 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.

Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication6th International Symposium, NFM 2014, proceedings
EditorsJulia M. Badger, Kristin Yvonne Rozier
PublisherSpringer, Springer Nature
Number of pages6
ISBN (Electronic)9783319062006
ISBN (Print)9783319061993
Publication statusPublished - 2014
Externally publishedYes
Event6th NASA Formal Methods Symposium (NFM) - Houston
Duration: 29 Apr 20141 May 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8430 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference6th NASA Formal Methods Symposium (NFM)

Cite this