TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets

TL;DR

This paper presents TAPAAL HyperLTL, a novel tool that extends Petri net verification capabilities to include hyperproperties like non-interference, enabling simultaneous reasoning about multiple execution traces.

Contribution

It introduces the first HyperLTL model checker integrated into TAPAAL for Petri nets, expanding verification to hyperproperties beyond traditional logics.

Findings

Successfully verifies hyperproperties in Petri nets

Integrated into TAPAAL with a user-friendly GUI

Performance evaluated on networking benchmarks

Abstract

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.