监管合规性检查：我们能看到成果吗？

### 监管合规性检查：我们能看到成果吗？ #### 1. 执行与追踪 在检查结构化流程模型的监管合规性时，我们首先需要了解流程的执行和追踪情况。以下是一个标注流程的执行和追踪示例： | Σ(B) | Θ(B, ann) | | --- | --- | | (start, t1, t3, t4, end) | ((start, ∅), (t1, {a}), (t3, {a, c, d}), (t4, {¬a, c, d}), (end, {¬a, c, d})) | | (start, t2, t3, t4end) | ((start, ∅), (t2, {b, c}), (t3, {b, c, d}), (t4, {¬a, b, c, d}), (end, {¬a, b, c, d})) | | (start, t3, t1, t4end) | ((start, ∅), (t3, {c, d}), (t1, {a, c, d}), (t4, {¬a, c, d}), (end, {¬a, c, d})) | | (start, t3, t2, t4end) | ((start, ∅), (t3, {c, d}), (t2, {b, c, d}), (t4.{¬a, b, c, d}), (end, {¬a, b, c, d})) | 从这个表格中，我们可以清晰地看到不同执行路径下的状态变化。 #### 2. 监管框架 监管框架通过义务来定义，义务是流程模型为了被认为合规而需要满足的条件。义务可以分为全局义务和局部义务： - **全局义务**：用 $O_o⟨c⟩$ 表示，其中 $o \in \{a, m\}$ 表示义务是成就型还是维护型，$c$ 表示义务的条件。全局义务在整个执行过程中都有效。 - **局部义务**：用 $O_o⟨c, t, d⟩$ 表示，其中 $o \in \{a, m\}$ 同样表示义务类型，$c$ 是义务条件，$t$ 是触发条件，$d$ 是截止条件。局部义务的有效区间由触发条件和截止条件决定。 义务的触发、截止和条件通常被定义为命题公式。当一个状态包含的文字为真时，就可以评估该状态下的命题公式。 #### 3. 义务评估 义务是否被履行或违反取决于其有效区间内的追踪状态。不同类型的义务有不同的履行条件： - **成就型义务**：在一个区间内有效时，执行过程必须在截止条件满足之前的某个点满足规定的履行条件，否则义务被违反。 - **维护型义务**：在一个区间内有效时，执行过程必须在截止条件满足之前的所有点连续满足履行条件，否则义务被违反。 #### 4. 流程合规性 判断一个流程是否符合监管框架有不同的结果： - **完全合规**：如果流程的每个追踪都符合监管框架，则称该流程完全合规，即 $(P, ann) \vdash_F O$ 当且仅当 $\forall\theta \in \Theta(P, ann), \theta \vdash O$。 - **部分合规**：如果存在至少一个追踪符合监管框架，则称该流程部分合规，即 $(P, ann) \vdash_P O$ 当且仅当 $\exists\theta \in \Theta(P, ann), \theta \vdash O$。 - **不合规**：如果没有追踪符合监管框架，则称该流程不合规，即 $(P, ann) \not\vdash O$ 当且仅当 $\neg\exists\theta \in \Theta(P, ann), \theta \vdash O$。 #### 5. 现有复杂度结果 在分析问题的复杂度之前，我们先引入一个缩写系统来表示不同的问题变体： - **1/n**：表示结构化流程是针对单个（1）还是一组（n）义务进行检查。 - **G/L**：表示义务的有效区间是全局（G）还是局部（L）。 - **−/+**：表示义务的元素是由文字（−）还是命题公式（+）组成。 例如，1G− 表示检查结构化流程模型是否符合单个全局义务，且义务条件由命题文字表示。 以下是现有复杂度结果的表格： | 问题 | 来源 | 合规性 | 复杂度类 | | --- | --- | --- | --- | | 1G− | Colombo Tosatto 等人 [23] | 完全和部分 | P | | nL− | Colombo Tosatto 等人 [22] | 部分 | NP - 完全 | | 1L+ | Colombo Tosatto 等人 [22] | 完全 | coNP - 完全 | | nL+ | Colombo Tosatto 等人 [22] | 部分 | NP - 完全 | 从这些结果可以看出，当义务变为局部，并且义务数量多于一个或者义务元素可以用命题公式表示时，问题的计算复杂度从 P 类跃升至 NP 类。 #### 6. 部分合规性复杂度关系 我们可以用以下 mermaid 流程图来表示部分合规性的复杂度关系： ```mermaid graph LR classDef process fill:#E5F6FF,stroke:#73A6FF,stroke-width:2px; 1G-:::process --> 1G+:::process 1G-:::process --> nG-:::process 1L-:::process --> 1L+:::p ```