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.

翻译：Petri网是一种能够描述复杂分布式系统的建模形式化方法，目前存在大量学术及工业工具支持模型性质的自动验证。典型问题包括可达性分析以及针对LTL和CTL等逻辑的模型检验。然而，这些逻辑在描述如非干涉性和观测确定性等性质时存在局限，此类性质需要对模型的多条轨迹进行同步推理，因而只能表述为超性质。据我们所知，本文首次提出了针对Petri网的HyperLTL模型检验器。该工具已完全集成至验证框架TAPAAL中，我们阐述了该超逻辑的语义，介绍了工具的整体架构与图形用户界面，并在源自计算机网络领域的两个基准问题集上评估了HyperLTL验证引擎的性能。