扩展对称网中符号不变式的半自动验证
Semi-automated Verification of Symbolic Invariants In Extended Symmetric Nets
浏览论文内容
中文总结 AI 辅助
针对高级Petri网中符号结构不变式验证范围受限的问题，研究提出利用SNexpression工具的符号结构关系演算，在扩展对称网形式下半自动验证不变式，还给出流生成族构建方法与更广泛的验证框架。
中文摘要 AI 辅助
结构分析是Petri网（PN）研究的核心，是对状态空间方法的补充，同时避免了其组合爆炸问题。经典Petri网的结构分析已得到充分研究，但针对高级Petri网（HLPN）的相关研究则少得多。对称网（Symmetric Nets, SN）是一种常见的HLPN形式化方法，利用紧凑标注编码行为对称性，可用于构建符号可达图以及随机SN对应的集总马尔可夫链。过去二十年间，针对SN的特定结构技术不断涌现，其中SNexpression工具尤为突出，它实现了一种用于冲突、因果关系等符号结构关系的演算。我们提出利用该演算对符号结构不变式进行半自动验证——目前这类验证仅适用于受限的SN子类，而我们的方法面向在关键函数算子下封闭的扩展SN形式化方法（ESN）。我们聚焦于流（flow），至少在理论层面概述了流生成族的构建方法，同时还勾勒出一个可形式化验证更广泛不变式性质的框架，并通过代表性示例阐释了核心概念。
英文摘要
Structural analysis is central to Petri Net (PN) research, complementing state-space methods while avoiding their combinatorial issues. It is well studied for classical PNs but much less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, allowing symbolic reachability graphs and associated lumped Markov chains for stochastic SN. In the past two decades, specific structural techniques for SN have emerged, notably the SNexpression tool, which implements a calculus for symbolic structural relations such as conflict and causality. We propose using this calculus to semi-automatically verify symbolic structural invariants, currently possible only for restricted SN subclasses, for an extended SN formalism (ESN) closed under key functional operators. We focus on flows and outline, at least in theory, how to construct a flow-generating family. We also sketch a framework for formally verifying a wider range of invariant properties. Representative examples illustrate the main concepts.
发表机构
- Department of Informatics Universit \`a degli Studi di Milano , Italy
机构由 AI 辅助整理，请以论文原文为准。
