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

doi:10.1007/978-3-319-06200-6_26

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 proceeding › Conference proceeding contribution

7 Citations (Scopus)

Abstract

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 language	English
Title of host publication	NASA Formal Methods
Subtitle of host publication	6th International Symposium, NFM 2014, proceedings
Editors	Julia M. Badger, Kristin Yvonne Rozier
Publisher	Springer, Springer Nature
Pages	307-312
Number of pages	6
ISBN (Electronic)	9783319062006
ISBN (Print)	9783319061993
DOIs	https://doi.org/10.1007/978-3-319-06200-6_26
Publication status	Published - 2014
Externally published	Yes
Event	6th NASA Formal Methods Symposium (NFM) - Houston Duration: 29 Apr 2014 → 1 May 2014

Publication series

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

Conference

Conference	6th NASA Formal Methods Symposium (NFM)
City	Houston
Period	29/04/14 → 1/05/14

Access to Document

10.1007/978-3-319-06200-6_26

Link to publication in Scopus

Cite this

Jensen, P. G., Larsen, K., Srba, J., Sørensen, M. G., & Taankvist, J. H. (2014). Memory efficient data structures for explicit verification of timed systems. In J. M. Badger, & K. Y. Rozier (Eds.), NASA Formal Methods: 6th International Symposium, NFM 2014, proceedings (pp. 307-312). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8430 LNCS). Springer, Springer Nature. https://doi.org/10.1007/978-3-319-06200-6_26

Jensen, Peter Gjøl ; Larsen, Kim ; Srba, Jiri ; Sørensen, Mathias Grund ; Taankvist, Jakob Haar. / Memory efficient data structures for explicit verification of timed systems. NASA Formal Methods: 6th International Symposium, NFM 2014, proceedings. editor / Julia M. Badger ; Kristin Yvonne Rozier. Springer, Springer Nature, 2014. pp. 307-312 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{efeea869edd04bf1b4f323d9904141cc,

title = "Memory efficient data structures for explicit verification of timed systems",

abstract = "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.",

author = "Jensen, {Peter Gj{\o}l} and Kim Larsen and Jiri Srba and S{\o}rensen, {Mathias Grund} and Taankvist, {Jakob Haar}",

year = "2014",

doi = "10.1007/978-3-319-06200-6_26",

language = "English",

isbn = "9783319061993",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Springer Nature",

pages = "307--312",

editor = "Badger, {Julia M.} and Rozier, {Kristin Yvonne}",

booktitle = "NASA Formal Methods",

address = "United States",

}

Jensen, PG, Larsen, K, Srba, J, Sørensen, MG & Taankvist, JH 2014, Memory efficient data structures for explicit verification of timed systems. in JM Badger & KY Rozier (eds), NASA Formal Methods: 6th International Symposium, NFM 2014, proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8430 LNCS, Springer, Springer Nature, pp. 307-312, 6th NASA Formal Methods Symposium (NFM), Houston, 29/04/14. https://doi.org/10.1007/978-3-319-06200-6_26

Memory efficient data structures for explicit verification of timed systems. / Jensen, Peter Gjøl; Larsen, Kim; Srba, Jiri; Sørensen, Mathias Grund; Taankvist, Jakob Haar.

NASA Formal Methods: 6th International Symposium, NFM 2014, proceedings. ed. / Julia M. Badger; Kristin Yvonne Rozier. Springer, Springer Nature, 2014. p. 307-312 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8430 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution

TY - GEN

T1 - Memory efficient data structures for explicit verification of timed systems

AU - Jensen, Peter Gjøl

AU - Larsen, Kim

AU - Srba, Jiri

AU - Sørensen, Mathias Grund

AU - Taankvist, Jakob Haar

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84901657633&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-06200-6_26

DO - 10.1007/978-3-319-06200-6_26

M3 - Conference proceeding contribution

SN - 9783319061993

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 307

EP - 312

BT - NASA Formal Methods

A2 - Badger, Julia M.

A2 - Rozier, Kristin Yvonne

PB - Springer, Springer Nature

ER -

Jensen PG, Larsen K, Srba J, Sørensen MG, Taankvist JH. Memory efficient data structures for explicit verification of timed systems. In Badger JM, Rozier KY, editors, NASA Formal Methods: 6th International Symposium, NFM 2014, proceedings. Springer, Springer Nature. 2014. p. 307-312. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-06200-6_26