动态进程生成系统中有效的标记等价性检验
Effective Marking Equivalence Checking in Systems with Dynamic Process Creation
摘要：
这项工作的出发点是一个框架，允许对具有动态进程创建的系统进行建模，配备了检测对称执行的过程（即，其区别仅在于过程的身份）。这允许减小状态空间，潜在地减小到指数级更小的大小，并且因为进程标识符从不被重用，所以这还允许将一些无限状态空间减小到有限大小。然而，在这种方法中，检测对称性的过程不允许计算高效的算法，主要是因为每个新计算的状态必须与每个已经达到的状态进行比较。在本文中，我们提出了一种新的方法来检测在这个框架中的对称性，将解决这个问题，从而使有效的算法。我们形式化了状态的规范表示，并确定了所分析模型的充分条件，以保证可以检测到所有对称性。对于不属于这一类的模型，我们的方法仍然是正确的，但不能保证最大限度地减少状态空间。
英文摘要：
The starting point of this work is a framework allowing to model systems with dynamic process creation, equipped with a procedure to detect symmetric executions (ie., which differ only by the identities of processes). This allows to reduce the state space, potentially to an exponentially smaller size, and, because process identifiers are never reused, this also allows to reduce to finite size some infinite state spaces. However, in this approach, the procedure to detect symmetries does not allow for computationally efficient algorithms, mainly because each newly computed state has to be compared with every already reached state. In this paper, we propose a new approach to detect symmetries in this framework that will solve this problem, thus enabling for efficient algorithms. We formalise a canonical representation of states and identify a sufficient condition on the analysed model that guarantees that every symmetry can be detected. For the models that do not fall into this category, our approach is still correct but does not guarantee a maximal reduction of state space.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
