TAPAAL and Reachability Analysis of P/T Nets

Jonas Finnemann Jensen, Thomas Søndersø Nielsen, Lars Kærlund Østergaard, Jiri Srba

Publikation: Bidrag til bog/antologi/rapport/konference proceedingBidrag til bog/antologiForskningpeer review

10 Citationer (Scopus)

Resumé

We discuss selected model checking techniques used in the tool TAPAAL for the reachability analysis of weighted Petri nets with inhibitor arcs. We focus on techniques that had the most significant effect at the 2015 Model Checking Contest (MCC). While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their efficient implementation and the evaluation of their performance on a large variety of nets from MCC'15.
OriginalsprogEngelsk
TitelTransactions on Petri Nets and Other Models of Concurrency XI
Antal sider12
ForlagSpringer
Publikationsdato2016
Sider307-318
ISBN (Trykt)978-3-662-53400-7
ISBN (Elektronisk)978-3-662-53401-4
DOI
StatusUdgivet - 2016
NavnLecture Notes in Computer Science
Vol/bind9930
ISSN0302-9743

Fingerprint

Model checking
Petri nets

Citer dette

Jensen, J. F., Nielsen, T. S., Østergaard, L. K., & Srba, J. (2016). TAPAAL and Reachability Analysis of P/T Nets. I Transactions on Petri Nets and Other Models of Concurrency XI (s. 307-318). Springer. Lecture Notes in Computer Science, Bind. 9930 https://doi.org/10.1007/978-3-662-53401-4_16
Jensen, Jonas Finnemann ; Nielsen, Thomas Søndersø ; Østergaard, Lars Kærlund ; Srba, Jiri. / TAPAAL and Reachability Analysis of P/T Nets. Transactions on Petri Nets and Other Models of Concurrency XI. Springer, 2016. s. 307-318 (Lecture Notes in Computer Science, Bind 9930).
@inbook{907f8a9ca1c04478b18c905640ffeabe,
title = "TAPAAL and Reachability Analysis of P/T Nets",
abstract = "We discuss selected model checking techniques used in the tool TAPAAL for the reachability analysis of weighted Petri nets with inhibitor arcs. We focus on techniques that had the most significant effect at the 2015 Model Checking Contest (MCC). While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their efficient implementation and the evaluation of their performance on a large variety of nets from MCC'15.",
keywords = "model checking, Petri nets, verification, reachability",
author = "Jensen, {Jonas Finnemann} and Nielsen, {Thomas S{\o}nders{\o}} and {\O}stergaard, {Lars K{\ae}rlund} and Jiri Srba",
year = "2016",
doi = "10.1007/978-3-662-53401-4_16",
language = "English",
isbn = "978-3-662-53400-7",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "307--318",
booktitle = "Transactions on Petri Nets and Other Models of Concurrency XI",
address = "Germany",

}

Jensen, JF, Nielsen, TS, Østergaard, LK & Srba, J 2016, TAPAAL and Reachability Analysis of P/T Nets. i Transactions on Petri Nets and Other Models of Concurrency XI. Springer, Lecture Notes in Computer Science, bind 9930, s. 307-318. https://doi.org/10.1007/978-3-662-53401-4_16

TAPAAL and Reachability Analysis of P/T Nets. / Jensen, Jonas Finnemann; Nielsen, Thomas Søndersø; Østergaard, Lars Kærlund; Srba, Jiri.

Transactions on Petri Nets and Other Models of Concurrency XI. Springer, 2016. s. 307-318 (Lecture Notes in Computer Science, Bind 9930).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingBidrag til bog/antologiForskningpeer review

TY - CHAP

T1 - TAPAAL and Reachability Analysis of P/T Nets

AU - Jensen, Jonas Finnemann

AU - Nielsen, Thomas Søndersø

AU - Østergaard, Lars Kærlund

AU - Srba, Jiri

PY - 2016

Y1 - 2016

N2 - We discuss selected model checking techniques used in the tool TAPAAL for the reachability analysis of weighted Petri nets with inhibitor arcs. We focus on techniques that had the most significant effect at the 2015 Model Checking Contest (MCC). While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their efficient implementation and the evaluation of their performance on a large variety of nets from MCC'15.

AB - We discuss selected model checking techniques used in the tool TAPAAL for the reachability analysis of weighted Petri nets with inhibitor arcs. We focus on techniques that had the most significant effect at the 2015 Model Checking Contest (MCC). While the techniques are mostly well known, our contribution lies in their adaptation to the MCC reachability queries, their efficient implementation and the evaluation of their performance on a large variety of nets from MCC'15.

KW - model checking, Petri nets, verification, reachability

U2 - 10.1007/978-3-662-53401-4_16

DO - 10.1007/978-3-662-53401-4_16

M3 - Book chapter

SN - 978-3-662-53400-7

T3 - Lecture Notes in Computer Science

SP - 307

EP - 318

BT - Transactions on Petri Nets and Other Models of Concurrency XI

PB - Springer

ER -

Jensen JF, Nielsen TS, Østergaard LK, Srba J. TAPAAL and Reachability Analysis of P/T Nets. I Transactions on Petri Nets and Other Models of Concurrency XI. Springer. 2016. s. 307-318. (Lecture Notes in Computer Science, Bind 9930). https://doi.org/10.1007/978-3-662-53401-4_16