Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets

Bruno Maria René Gonzalez, Peter Gjøl Jensen, Stefan Schmid, Jiří Srba, Martin Zimmermann

TL;DR

The paper introduces TAPAAL HyperLTL, the first HyperLTL model checker for Petri nets, integrated into the TAPAAL verification framework to enable verification of multi-trace hyperproperties such as congestion and latency in distributed systems.It defines a Petri-net–oriented HyperLTL fragment, describes the tool architecture and GUI, and presents an on-the-fly verification engine that uses product automata and nested DFS to detect counterexamples.Through extensive networking-based case studies, the approach is shown to outperform self-composition and to be competitive with the state-of-the-art MCHyper, with favorable scalability for large trace sets and constants.The work demonstrates practical applicability for verifying hyperproperties in network routing scenarios and outlines future work to import heuristic techniques from MCHyper to further improve positive-query performance.

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.

TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets

TL;DR

The paper introduces TAPAAL HyperLTL, the first HyperLTL model checker for Petri nets, integrated into the TAPAAL verification framework to enable verification of multi-trace hyperproperties such as congestion and latency in distributed systems.It defines a Petri-net–oriented HyperLTL fragment, describes the tool architecture and GUI, and presents an on-the-fly verification engine that uses product automata and nested DFS to detect counterexamples.Through extensive networking-based case studies, the approach is shown to outperform self-composition and to be competitive with the state-of-the-art MCHyper, with favorable scalability for large trace sets and constants.The work demonstrates practical applicability for verifying hyperproperties in network routing scenarios and outlines future work to import heuristic techniques from MCHyper to further improve positive-query performance.

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.

Paper Structure

This paper contains 15 sections, 3 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Related work.
  3. Modeling Formalism and HyperLTL Logic
  4. Petri nets
  5. HyperLTL
  6. Tool Implementation and Graphical User Interface
  7. Congestion Case Study
  8. Latency Case Study
  9. TAPAAL HyperLTL Encoding
  10. MCHyper Encoding
  11. Experimental Setup
  12. Binary vs. Unary Encoding in MCHyper
  13. Scaling of Constants and TAPAAL HyperLTL vs. MCHyper Comparison
  14. Conclusion
  15. Acknowledgements.

Figures (10)

  • Figure 1: Example of a Petri net and HyperLTL formulae
  • Figure 2: TAPAAL HyperLTL screenshot (simulator mode with a query dialog)
  • Figure 3: Self-composition with the LTL query $(\mathop{\mathbf{F}\newline}\nolimits v_1^1=1) \wedge (\mathop{\mathbf{F}\newline}\nolimits v_1^2=1$)
  • Figure 4: Ratio plot of TAPAAL HyperLTL vs. Self-composition
  • Figure 5: Ratio plot of TAPAAL HyperLTL with and without LP Check
  • ...and 5 more figures