重置工作流网的合理性
Soundness of reset workflow nets
AI总结：
本文证明重置工作流网的广义合理性是不可判定的，并发现介于1-合理性与广义合理性之间的“1-中间合理性”具有可判定性，展现出非单调复杂度行为，为算法分析提供了始终正确的输出。
摘要：
工作流网是 Petri 网的一种成熟变体，用于对业务流程等过程活动进行建模。工作流网的标准正确性概念是合理性，它有几种变体。它们的可判定性在几十年前就已得到证明，但其复杂度直到最近才被确定。在本研究中，我们主要关注两种流行的变体：$1$-soundness（1-合理性）和 generalised soundness（广义合理性）。工作流网已通过引入重置机制进行了扩展，以对例如可取消动作的工作流进行建模。人们早就知道，对于这种扩展，除可能存在的 generalised soundness 外，所有合理性变体都是不可判定的。我们通过证明 generalised soundness 对于 reset workflow nets（重置工作流网）同样是不可判定的，从而补全了这一图景。随后，我们通过识别一种被称为“$1$-in-between soundness”（1-中间合理性）的性质，使这种不可判定性的局面变得模糊，该性质介于 $1$-soundness 和 generalised soundness 之间。它揭示了一种不寻常的非单调复杂度行为：一个可判定的合理性性质位于两个不可判定的性质之间。这在 reset workflow nets 的算法分析中可能很有价值，因为我们的过程会产生一个形式为“$1$-sound”或“not generalised sound”的输出，且该输出始终是正确的。
英文摘要：
Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability was shown decades ago, but their complexity was only identified recently. In this work, we are primarily interested in two popular variants: $1$-soundness and generalised soundness. Workflow nets have been extended with resets to model workflows that can, e.g., cancel actions. It has been known for a while that, for this extension, all variants of soundness, except possibly generalised soundness, are undecidable. We complete the picture by showing that generalised soundness is also undecidable for reset workflow nets. We then blur this undecidability landscape by identifying a property, coined ``$1$-in-between soundness'', which lies between $1$-soundness and generalised soundness. It reveals an unusual non-monotonic complexity behaviour: a decidable soundness property is in between two undecidable ones. This can be valuable in the algorithmic analysis of reset workflow nets, as our procedure yields an output of the form ``$1$-sound'' or ``not generalised sound'' which is always correct.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
