基于有限轨迹的LTL和LDL业务元约束监控及分层声明式建模

### 基于有限轨迹的LTL和LDL业务元约束监控及分层声明式建模 在当今的业务流程设计领域，我们面临着诸多挑战，例如如何有效地监控动态业务约束，以及如何构建易于理解和管理的复杂业务流程模型。下面将为大家详细介绍两种相关的技术方案。 #### 基于有限轨迹的LTL和LDL业务元约束监控 在业务流程执行过程中，动态约束的监控至关重要。传统的方法可能存在一定的局限性，而这里提出了一种基于线性动态逻辑（LDLf）的有效监控方法。 ##### 元约束公式与局限性 借助定理4，我们可以得到标准的LDLf公式：\((⟨pref¬ϕ_{canc}⟩end ∧¬⟨prefϕ_{canc}⟩end) →ϕ_{dopay}\)。然而，这种形式的元约束存在一个限制，即右侧部分\(Ψ_{exp}\)从轨迹开始就被监控。在许多情况下，这是可以接受的，比如在某些场景中，用户在订单取消导致约束\(ϕ_{canc}\)被违反之前就已经支付了附加费用是可以的。但在其他情况下，这并不令人满意，我们希望仅在\(Φ_{pre}\)评估为真之后，例如检测到给定约束被违反之后，才强制执行补偿行为。 ##### 扩展元约束模式 为了解决上述问题，我们可以将元约束模式扩展为：\(Φ_{pre} →[ρ]Ψ_{exp}\)，其中\(ρ\)是一个正则表达式，表示在哪些路径之后\(Ψ_{exp}\)应该被强制执行。通过将\(ρ\)构建为表示使\(Φ_{pre}\)为真的路径的正则表达式，我们可以利用这个改进的元约束来表达在当前轨迹的所有使\(Φ_{pre}\)为真的前缀之后，\(Ψ_{exp}\)应该变为真。 例如，修改示例3的补偿约束，以反映当关闭的订单被取消（即\(ϕ_{canc}\)被违反）时，之后必须支付附加费用。这可以通过以下元约束来捕获：\(\{[ϕ_{canc}]RV = false\} →[re\{[ϕ_{canc}]RV =false\}]ϕ_{dopay}\)，其中\(re\{[ϕ_{canc}]=false\}\)表示语言\(L(\{[ϕ_{canc}] = false\}) = L(⟨pref¬ϕ_{canc}⟩end ∧¬⟨prefϕ_{canc}⟩end)\)的正则表达式，该正则表达式描述了所有包含约束\(ϕ_{canc}\)违反的路径。 ##### 实现方案 整个方法已作为PROM 6流程挖掘框架的操作决策支持（OS）提供者实现。PROM 6提供了一个通用的OS环境，支持外部工作流管理系统在运行时（产生事件）与PROM之间的交互。具体来说，它提供了一个OS服务，从外部世界接收事件流，更新和编排注册的OS提供者，对事件流应用不同类型的在线分析，并将产生的结果报告回外部世界。 在插件的后端，有一个专门用于从LDLf公式构建和操作非确定性有限自动机（NFAs）的软件模块，具体实现了相关技术。为了操作正则表达式和自动机，我们使用了快速且知名的库dk.brics.automaton。 下面是该实现方案的流程图： ```mermaid graph LR A[外部工作流管理系统] --> B[PROM 6的OS服务] B --> C[注册的OS提供者] C --> D[LDLf公式处理模块] D --> E[NFAs构建与操作] E --> F[结果报告回外部世界] ``` #### 分层声明式建模与细化及子流程 在业务流程建模中，我们常常需要处理复杂的流程结构，而传统的建模方法可能无法很好地应对这些挑战。因此，我们提出了一种新的声明式模型，具有流程的组合和分层定义。 ##### 现有业务流程设计的问题 目前，业务流程设计技术主要基于面向流程的符号，如业务流程模型和符号（BPMN）标准。这些符号虽然可以描述流程如何从开始到结束，但在处理业务流程的合规性规则时存在不足。业务流程通常需要符合各种法规和约束，而面向流程的符号只能描述如何满足这些规则，对于规则的描述和验证需要其他符号和技术。这给流程设计师带来了三个建模任务：描述合规规则、描述流程以及验证流程是否符合规则。 在大多数工业设计工具中，流程图往往不是基于正式模型的，因此不支持设计时验证。这意味着流程设计师需要手动解释约束，并且合规性通常在执行后进行非正式验证。在这种情况下，业务流程很容易出现不符合规则或过度约束的问题，而过度约束的流程往往不适合现实情况或知识密集型流程。 ##### DCR图的优势与不足 为了解决上述问题，一些声明式流程建模符号和技术被提出，其中动态条件响应（DCR）图具有独特的优势。DCR图支持简单高效的运行时执行，减轻了理解约束的复杂性，并允许运行时适应。它比命题线性时间逻辑（LTL）更具表达力，可以描述正则语言和ω-正则语言的任意并集。 然而，当前实现的DCR图模型在一定规模下变得难以理解和呈现，缺乏封装、模块化和层次结构。此外，实际建模工作表明，DCR图需要一个“动态创建”或“实例化”子流程的概念。 ##### 新方法的贡献 为了弥补DCR图的这些不足，我们提出了以下贡献： 1. **引入DCR图的组合细化**：通过组合的方式对DCR图进行细化，确保细化过程不会意外删除现有模型的约束。 2. **添加动态生成子流程的概念**：定义了Hi - DCR图，子流程可以与父流程进行交互，具有多种启动方式和不同的可观察结果。 3. **实例演示**：通过一个从实际案例管理解决方案中提取的示例，展示了增量式流程设计的使用。 4. **提供公开可用的Hi - DCR图工具**：该工具允许进行模拟、有限片段的模型检查、自动可视化等操作。 下面是新方法与传统方法的对比表格： | 对比项 | 传统方法 | 新方法（Hi - DCR图） | | ---- | ---- | ---- | | 模型复杂度 | 大，缺乏封装、模块化和层次结构 | 支持分层定义，降低复杂度 | | 子流程交互 | 无或有限 | 子流程可与父流程交互 | | 流程设计方式 | 手动解释约束，设计时验证困难 | 支持增量式设计，工具辅助操作 | | 表达能力 | 有限 | 比ω-正则语言更具表达力 | ##### DCR图基础 DCR图是一种图形化的建模工具，通过事件和它们之间的关系来描述业务流程。下面以一个丹麦资助机构的工作流为例，介绍DCR图的基本概念。 在这个示例中，有四个事件：开始申请轮次（Start round）、接收申请（Receive application）、申请提交截止日期（Application deadline）和董事会会议（Board meeting）。这些事件之间存在三种基本关系： - **条件关系（e →• e′）**：表示前者事件必须在后者事件之前发生。例如，开始申请轮次必须在接收申请之前发生。 - **响应关系（e •→e′）**：表示如果前者事件发生，那么后者事件必须随后发生。例如，如果接收了申请，那么必须召开董事会会议。 - **排除关系（e →% e′）**：表示一旦前者事件发生，后者事件将被排除，不再参与后续的工作流。例如，申请提交截止日期发生后，接收申请事件将被排除。 下面是DCR图执行过程的示例列表： 1. **初始状态**：所有事件处于初始状态，开始申请轮次未发生，接收申请事件不可执行（灰色显示）。 2. **执行开始申请轮次**：开始申请轮次事件执行，有检查标记，接收申请事件的条件满足，变为可执行状态。 3. **执行接收申请**：接收申请事件执行，董事会会议事件产生待响应标记（红色文本和感叹号）。 4. **再次执行接收申请**：图状态无变化，因为接收申请已标记为已执行，董事会会议仍有待响应。 5. **执行申请提交截止日期**：接收申请事件被排除，用虚线框表示。 6. **执行董事会会议**：董事会会议事件执行，待响应标记消失，文本恢复黑色。 一个DCR图是可接受的，如果它没有包含未完成的待响应事件。通过这个示例，我们可以看到DCR图直接表示执行状态，设计时和运行时没有区别。 综上所述，无论是基于有限轨迹的LTL和LDL业务元约束监控，还是分层声明式建模与细化及子流程的方法，都为解决业务流程设计和监控中的问题提供了有效的解决方案。它们可以帮助我们更好地管理复杂的业务流程，确保流程的合规性和高效执行。 ### 基于有限轨迹的LTL和LDL业务元约束监控及分层声明式建模 #### 相关工作对比 在业务流程建模领域，已经有一些相关的工作，下面将新提出的方法与其他相关方法进行对比分析。 ##### 与DECLARE层次结构的比较 之前有研究为DECLARE添加了复杂活动，强调了层次结构对于构建可理解的声明式模型的必要性。在该研究中，复杂活动包含一个嵌套的DECLARE模型，该模型控制活动何时可以完成。嵌套模型在复杂活动打开时启动，复杂活动只有在嵌套模型完成后才能关闭，并且嵌套模型与父模型之间没有其他交互。 而我们提出的Hi - DCR图中的子流程可以与父流程进行交互。子流程有多种启动方式，不同的可观察结果，并且允许与父流程中的其他活动进行交互。此外，之前的研究没有报告正式的语义，也没有复杂活动交织的示例，而在Hi - DCR图中，子流程的执行自然地与其他事件甚至同一子流程的其他实例交织在一起。 ##### 与GSM方法的比较 Guard - Stage - Milestone（GSM）方法是一种以数据为中心的业务建模方法，具有声明式的特点。该方法由阶段组成，每个阶段有控制其启动和关闭的守卫和里程碑。阶段可以包含子阶段，因此具有固有的层次结构。 虽然GSM方法以数据为中心，而我们的Hi - DCR图以事件为基础，但Hi - DCR图中的子流程与GSM阶段有很强的相似性，Hi - DCR图的接口事件类似于GSM中的守卫和里程碑。在未来的工作中，我们计划进一步研究两者之间的相似性，以建立它们之间的正式联系。 下面是这些方法的对比表格： | 对比项 | DECLARE层次结构 | GSM方法 | Hi - DCR图 | | ---- | ---- | ---- | ---- | | 子流程与父流程交互 | 无 | 未提及 | 支持交互 | | 正式语义 | 未报告 | 未提及 | 完全形式化 | | 子流程交织示例 | 无 | 未提及 | 支持且自然交织 | | 核心基础 | 逻辑模型 | 数据 | 事件 | #### Hi - DCR图的优势与特性 Hi - DCR图不仅解决了DCR图的不足，还具有一些独特的优势和特性。 ##### 形式化与正确性 Hi - DCR图是完全形式化的，我们证明了细化的正确性，即细化过程不会意外删除现有模型的约束。这确保了在对模型进行细化时，不会引入错误或丢失重要的约束信息。 ##### 表达能力 Hi - DCR图比ω - 正则语言更具表达力。这意味着它可以描述更复杂的业务流程和约束，能够更好地适应现实世界中的各种业务场景。 ##### 工具支持 我们提供了一个公开可用的Hi - DCR图工具。该工具允许进行多种操作，如模拟、有限片段的模型检查、自动可视化等。所有在示例中展示的组合和细化都是由该工具执行的，这大大提高了建模的效率和准确性。 下面是Hi - DCR图工具的功能列表： 1. **模拟功能**：可以模拟业务流程的执行，帮助用户直观地了解流程的运行情况。 2. **模型检查**：对有限片段进行模型检查，验证模型是否满足特定的约束和条件。 3. **自动可视化**：自动生成DCR图的可视化表示，使模型更加直观易懂。 4. **组合与细化执行**：自动执行模型的组合和细化操作，减少手动操作的工作量。 #### 实际应用示例 为了更好地说明Hi - DCR图的实际应用，我们以一个丹麦资助机构的案例管理解决方案为例。 ##### 案例背景 该资助机构的工作流涉及多个环节，包括申请提交、截止日期管理、董事会决策等。我们从这个实际案例中提取了一个示例，展示如何使用Hi - DCR图进行增量式流程设计。 ##### 设计过程 我们从一个非常抽象的模型开始，逐步对其进行细化。首先，我们使用基本的DCR图描述了资助机构工作流的主要事件和关系，如开始申请轮次、接收申请、申请截止日期和董事会会议等。然后，通过组合和细化操作，我们逐步添加更多的细节和约束，使模型更加具体和准确。 下面是这个设计过程的流程图： ```mermaid graph LR A[抽象模型] --> B[第一次细化] B --> C[第二次细化] C --> D[最终具体模型] ``` ##### 工具应用 在整个设计过程中，我们使用了Hi - DCR图工具。该工具自动执行了所有的组合和细化操作，生成了所有的DCR图。所有的示例都是完全可执行的，用户可以通过工具模拟流程的执行，检查模型的正确性。 #### 总结与展望 通过本文的介绍，我们可以看到基于有限轨迹的LTL和LDL业务元约束监控以及分层声明式建模与细化及子流程的方法为业务流程设计和监控提供了有效的解决方案。 在业务元约束监控方面，我们提出的方法通过扩展元约束模式和使用LDLf公式，能够更准确地监控动态业务约束，并在PROM 6流程挖掘框架中得到了有效的实现。 在分层声明式建模方面，Hi - DCR图解决了DCR图的不足，引入了组合细化和动态子流程的概念，具有形式化、表达能力强和工具支持等优势。通过实际案例的演示，我们展示了如何使用Hi - DCR图进行增量式流程设计，提高了业务流程建模的效率和准确性。 未来，我们计划进一步扩展这些方法。例如，在业务元约束监控方面，我们将纳入恢复机制，为现有的临时恢复机制提供正式的基础。在分层声明式建模方面，我们将研究如何将方法扩展到数据感知的业务约束，结合时态运算符和对监控事件附加数据的一阶查询，以更好地适应现实世界中复杂的业务场景。 总之，这些方法为业务流程的设计、监控和管理提供了新的思路和工具，有望在未来的业务领域中得到广泛应用。