AI 中文总结
本文证明Petri网、因果网、流程树和BPMN四种流程发现记号可统一为基于活动与类型化接口的规范签名，实现不依赖记号的模型比较，并以对象中心日志实验验证其区分并发与选择的能力。
AI 中文摘要
对同一事件日志运行两种流程发现算法，它们会返回同一流程的两幅不同图景。Petri网、因果网、流程树和BPMN各自依赖自身的路由机制，它们唯一的共同点是所生成的轨迹。轨迹逐一列出活动，因此丢弃了这些记号旨在表达的并发性，而具有相同轨迹语言的两种模型可以描述真正不同的流程。因此，两个被发现的模型是否含义相同，并没有独立于记号的答案。我们证明，这四种记号都承认一种规范表示，即一个签名，记录模型的活动以及它们组合所沿的带类型接口，而不包含任何路由机制。四个构造定理逐一按记号确立这种表示，因此两种模型以一种每种记号自身确定的形式进行比较。签名相等蕴含轨迹等价，并且严格更细，能够区分真正的并发与交错选择，而轨迹比较无法做到；签名包含蕴含轨迹包含。在一项针对一个以对象为中心日志的恢复研究中，发现的因果网恰好具有真实签名的签名，而发现的Petri网的签名严格包含它，并定位了Petri网在其静默结构中添加的每个行为。对于以对象为中心的数据，收益最大，因为单个日志同时支持多种记号。这四种记号变成一种演算，其中它们之间的翻译是一种可以被检验的主张。
英文摘要
Run two process-discovery algorithms on the same event log and they return two different pictures of the same process. Petri nets, causal nets, process trees and BPMN each rely on routing machinery of their own, and their only common ground is the traces they generate. A trace lists activities one after another, so it discards the concurrency the notations exist to express, and two models with identical trace languages can describe genuinely different processes. Whether two discovered models mean the same thing therefore has no notation-independent answer. We show that all four notations admit one canonical presentation, a signature recording a model's activities and the typed interfaces along which they compose, and nothing of the routing machinery. Four construction theorems establish this presentation notation by notation, so two models are compared in a form that each notation determines on its own. Signature equality implies trace equivalence and is strictly finer, separating genuine concurrency from interleaved choice, which a trace comparison cannot, and signature inclusion implies trace inclusion. In a recovery study on one object-centric log, the discovered causal net has exactly the ground-truth signature, while the discovered Petri net's signature strictly contains it and locates every behaviour the Petri net adds in its silent structure. The gain is largest for object-centric data, where a single log supports several notations at once. The four notations become one calculus, in which a translation between them is a claim that can be checked.
Comments67 pages, 22 figures, 4 tables
