TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915719223967744 |
|---|---|
| author | Gonzalez, Bruno Maria René Jensen, Peter Gjøl Schmid, Stefan Srba, Jiří Zimmermann, Martin |
| author_facet | Gonzalez, Bruno Maria René Jensen, Peter Gjøl Schmid, Stefan Srba, Jiří Zimmermann, Martin |
| contents | Petri nets are a modeling formalism capable of describing complex distributed systems and there exists a large number of both academic and industrial tools that enable automatic verification of model properties. Typical questions include reachability analysis and model checking against logics like LTL and CTL. However, these logics fall short when describing properties like non-interference and observational determinism that require simultaneous reasoning about multiple traces of the model and can thus only be expressed as hyperproperties. We introduce, to the best of our knowledge, the first HyperLTL model checker for Petri nets. The tool is fully integrated into the verification framework TAPAAL and we describe the semantics of the hyperlogic, present the tool's architecture and GUI, and evaluate the performance of the HyperLTL verification engine on two benchmarks of problems originating from the computer networking domain. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_14265 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets Gonzalez, Bruno Maria René Jensen, Peter Gjøl Schmid, Stefan Srba, Jiří Zimmermann, Martin Logic in Computer Science Petri nets are a modeling formalism capable of describing complex distributed systems and there exists a large number of both academic and industrial tools that enable automatic verification of model properties. Typical questions include reachability analysis and model checking against logics like LTL and CTL. However, these logics fall short when describing properties like non-interference and observational determinism that require simultaneous reasoning about multiple traces of the model and can thus only be expressed as hyperproperties. We introduce, to the best of our knowledge, the first HyperLTL model checker for Petri nets. The tool is fully integrated into the verification framework TAPAAL and we describe the semantics of the hyperlogic, present the tool's architecture and GUI, and evaluate the performance of the HyperLTL verification engine on two benchmarks of problems originating from the computer networking domain. |
| title | TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2512.14265 |