Model checking is a powerful technique for software verification. However, the approach notably suffers from the infamous state space explosion problem. To tackle this, in this paper, we introduce a novel symbolic method for encoding Petri net markings. It is based on the use of generalised intervals on vectors, as opposed to existing methods based on vectors of intervals such as Interval Decision Diagrams. We develop a formalisation of these intervals, show that they possess homomorphic operations for model checking CTL on Petri nets, and define a canonical form that provides good performance characteristics. Our structure facilitates the symbolic evaluation of CTL formulas in the realm of global model checking, which aims to identify every state that satisfies a formula. Tests on examples of the model checking contest (MCC 2022) show that our approach yields promising results. To achieve this, we implement efficient computations based on saturation and clustering principles derived from other symbolic model checking techniques.

翻译：模型检验是一种强大的软件验证技术。然而，该方法显著地受到著名的状态空间爆炸问题的困扰。为解决此问题，本文提出了一种新颖的用于编码Petri网标识的符号方法。该方法基于向量上的广义区间，而非现有方法（如区间决策图）所采用的区间向量。我们建立了这些区间的形式化表示，证明了它们具备对Petri网进行CTL模型检验的同态运算，并定义了一种具有良好性能特征的规范形式。我们的结构有助于在全局模型检验领域中对CTL公式进行符号求值，其目标是识别满足公式的所有状态。在模型检验竞赛（MCC 2022）的实例测试表明，我们的方法取得了有希望的结果。为实现这一目标，我们基于从其他符号模型检验技术衍生的饱和与聚类原理，实现了高效计算。