一个通用的无限状态过程动态网络推理框架
A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
摘要：
我们提出了一个框架推理无界动态网络的无限状态过程。我们提出约束Petri网（CPN）作为这些网络的通用模型。它们可以被看作是Petri网的令牌（代表过程的发生）着色的值在一些潜在的无限的数据域，如整数，实数等，此外，我们定义了一个逻辑，称为CML（彩色标记逻辑），CPN配置的描述。CML是一个基于标记的一阶逻辑，允许推理它们的位置和颜色。CPN和CML都通过颜色逻辑进行参数化，允许表达与标记相关的颜色（数据）上的约束。本文研究了CML可满足性问题的可判定性及其在CPNs验证中的应用。我们确定了一个片段的CML的可满足性问题是可判定的（无论何时它是底层的颜色逻辑的情况下），这是封闭的计算后，前图像的CPNs。这些结果可以用于几种分析，如不变性检查，前后条件推理，和有界可达性分析。
英文摘要：
We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. They can be seen as Petri nets where tokens (representing occurrences of processes) are colored by values over some potentially infinite data domain such as integers, reals, etc. Furthermore, we define a logic, called CML (colored markings logic), for the description of CPN configurations. CML is a first-order logic over tokens allowing to reason about their locations and their colors. Both CPNs and CML are parametrized by a color logic allowing to express constraints on the colors (data) associated with tokens. We investigate the decidability of the satisfiability problem of CML and its applications in the verification of CPNs. We identify a fragment of CML for which the satisfiability problem is decidable (whenever it is the case for the underlying color logic), and which is closed under the computations of post and pre images for CPNs. These results can be used for several kinds of analysis such as invariance checking, pre-post condition reasoning, and bounded reachability analysis.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
