发表机构
Department of Informatics Universit \`a degli Studi di Milano , Italy
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究针对高级Petri网结构不变式验证研究不足的问题，利用SNexpression工具的形式化演算，实现对称网符号结构不变式的半自动验证，提出流生成族方法与更广泛不变式验证框架，并通过示例阐明核心概念。
AI 中文摘要
结构分析是Petri网（PN）研究中的核心方法，提供了与状态空间技术互补的视角，同时避免了后者的诸多局限性。该方法在经典Petri网中已得到充分研究，但在高级Petri网（HLPN）中的研究则少得多。对称网（Symmetric Nets, SN）是一种常见的高级Petri网形式化体系，它使用紧凑的标注来编码行为对称性，能够构建符号可达图（在随机对称网中还可构建集总马尔可夫链）并执行符号离散事件仿真。在过去二十年中，研究人员开发了专门针对对称网的结构技术，其中SNexpression工具为其提供了重要支持。该工具实现了一种用于计算符号结构关系的形式化演算，这些关系包括但不限于冲突关系和因果依赖关系。本文重点研究如何利用该演算半自动验证符号结构不变式，这一任务目前仅对某些受限的对称网子类可行。我们特别聚焦于（半）流，并简要讨论了一种至少在理论上能够生成流生成族的方法。我们还进一步简要概述了一个用于更广泛类别不变式性质形式化验证的框架。本文采用了对称网形式化体系的扩展表述，该表述已被证明在基本函数算子方面满足闭包性质。全文通过代表性示例阐明了核心概念。
英文摘要
Structural analysis is a core method in Petri Net (PN) research, offering a perspective complementary to state-space techniques while avoiding many of their limitations. It is well studied for classical PNs but far less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, enabling the construction of a symbolic reachability graph (and a lumped Markov chain in stochastic SN) and the execution of symbolic discrete-event simulations. During the past two decades, structural techniques tailored to SN have been developed, notably supported by the SNexpression tool. This tool implements a formal calculus designed for the computation of symbolic structural relations, including, but not limited to, conflict relations and causal dependencies. Here, we focus on using this calculus to verify semi-automatically symbolic structural invariants, a task currently feasible only for certain restricted SN subclasses. We focus specifically on (semi)flows and briefly discuss an approach through which a flow generative family can be generated, at least theoretically. We further briefly outline a framework for the formal verification of a broader class of invariant properties. An extended formulation of the SN formalism is employed, which demonstrably satisfies the closure property with respect to fundamental functional operators. The core concepts are elucidated by means of representative examples throughout the exposition.
CommentsIn Proceedings ICE 2026, arXiv:2609.30353
Journal refEPTCS 453, 2026, pp. 79-99
