Action Language BC+
-
ArXiv URL: http://arxiv.org/abs/2506.18044v1
-
作者: Joohyung Lee
-
发布机构: Arizona State University; School of Computing, Informatics, and Decision Systems Engineering
TL;DR
本文提出了一种名为 BC+ 的新动作语言，通过将其语义建立在通用的稳定模型（Stable Model）之上，成功地统一并扩展了多种现有动作语言（如 \(B\), \(C\), \(C+\), \(BC\)），并自然地集成了现代答案集规划（Answer Set Programming, ASP）中的高级构造（如选择规则和聚合）。
关键定义
本文的核心是提出 BC+ 语言，其理解依赖于以下关键概念：
-
稳定模型语义 (Stable Model Semantics): 本文的理论基石。对于一个命题公式 \(F\) 和一个原子的集合（解释）\(X\)，首先计算 \(F\) 相对于 \(X\) 的归约式 (reduct) \(F^X\)。\(F^X\) 是通过将 \(F\) 中所有不被 \(X\) 满足的极大子公式替换为 \(⊥\) (假) 得到的。如果 \(X\) 是满足 \(F^X\) 的最小模型，那么 \(X\) 就是 \(F\) 的一个稳定模型。这种语义具有非单调性，非常适合知识表示。
- 因果律 (Causal Law): 描述动作领域世界如何运作的基本规则，是 BC+ 语言的语法核心，分为三类：
- 静态律 (Static Law): \(caused F if G\)，描述同一状态下流（fluent）之间的因果依赖关系。
- 动作动态律 (Action Dynamic Law): \(caused F if G\)，其中 \(F\) 是动作公式，描述并发动作之间的依赖。
- 流动态律 (Fluent Dynamic Law): \(caused F if G after H\)，描述动作如何引起状态（流）的变化，即动作的直接和间接效果。
- 流常量 (Fluent Constant): 表示世界状态属性的常量，分为两种：
- 常规流 (Regular Fluent): 其值在没有外力影响时倾向于保持不变（符合惯性定律），其初始值是任意的。
- 静态决定流 (Statically Determined Fluent): 其值完全由同一状态下的其他流决定，没有自身的惯性。
- 唯一性与存在性约束 (Uniqueness and Existence Constraint, UEC): 一个重要的背景约束，确保每个常量在任何时刻都有且仅有一个值。例如，对于常量 \(c\) 及其定义域 \(Dom(c) = {v_1, ..., v_n}\)，UEC 确保 \(c=v_i\) 和 \(c=v_j\)（当\(i≠j\)时）不同时为真，并且 \(c\) 必须取定义域中的一个值。
相关工作
本文旨在解决现有动作语言领域中的两大瓶颈问题。
-
研究现状: 动作语言是用于描述动作效果的形式化语言，如 \(A\), \(B\), \(C\), \(C+\) 等。它们通过提供结构化的、高层次的抽象，简化了对变迁系统（transition systems）的描述，避免了直接编写答案集规划（ASP）的复杂语法。其中，部分语言的语义可以转化为 ASP 程序进行计算。
-
存在问题:
- 缺乏现代ASP特性: 现有动作语言不支持现代ASP中非常实用的语言构造，如选择规则 (choice rules)、聚合 (aggregates)、抽象约束原子 (abstract constraint atoms) 等。这使得在处理复杂问题时，用户不得不放弃动作语言，转而直接使用ASP。
- 语言表达能力局限且分裂: 不同的动作语言各有优劣。例如，语言 \(B\) 强制所有流都遵循惯性定律，难以描述非惯性默认行为（如容器漏水）；语言 \(C\) 和 \(C+\) 虽然解决了这个问题，但不支持 \(B\) 中的递归定义；新提出的 \(BC\) 语言虽然结合了二者优点，但又无法像 \(C+\) 那样描述复杂的动作依赖和动作属性。
本文旨在提出一个更具表达能力的统一框架，即 BC+，它不仅能涵盖现有语言的最佳特性，还能无缝集成现代ASP的强大功能。
本文方法
本文提出了 BC+ 语言，其核心创新在于将其语义直接定义在通用的命题公式稳定模型之上，而不是像早期工作那样局限于受限的逻辑程序或因果理论。这使得 BC+ 成为一个高度概括性的表示法，能自然地利用现代ASP的全部表达能力。
语法核心
BC+ 的语法由常量（流常量和动作常量）和三类因果律构成：
- 静态律: \(caused F if G\)
- 动作动态律: \(caused F if G\)
- 流动态律: \(caused F if G after H\) 其中 \(F\), \(G\), \(H\) 是基于常量的命题公式。由于其语义基础，这些公式可以直接包含聚合、选择规则等高级ASP构造。
语义核心：从 BC+ 到命题公式的转化
一个 BC+ 动作描述 \(D\) 的语义是通过将其转化为一个带时间戳的命题公式 \(PF_m(D)\) 来定义的，该公式的稳定模型对应于系统在 \(m\) 步内的所有可能轨迹。
转化的关键步骤如下：
- 加时间戳: 将所有常量 \(c\) 替换为 \(i:c\)，其中 \(i\) 是时间步。
- 翻译因果律:
- 静态律 \(caused F if G\) 翻译为 \(i:F ← i:G\)。
- 流动态律 \(caused F if G after H\) 翻译为 \(i+1:F ← (i+1:G) ∧ (i:H)\)。
- 引入默认假设和约束:
- 初始状态: 对每个常规流常量 \(c\) 的每个可能值 \(v\)，在初始时刻 \(0\) 加入选择规则 \({0:c=v}^ch\)。这表示初始状态可以是任何合法的状态。静态决定流则不加，因其值由其他流决定。
- 唯一性与存在性 (UEC): 对每个时间步的每个常量，加入约束确保其有且仅有一个值。
创新点
- 基于通用稳定模型的语义: 这是与以往方法最本质的区别。它使得 BC+ 的表达能力不再受限于逻辑程序的特定形式，而是可以利用命题公式的全部能力。 \(A\) 和 \(¬¬A\) 在稳定模型语义下有不同含义，\(¬¬A\) 允许非最小模型，这为模拟 \(C+\) 等语言的行为提供了机制。
- 原生支持现代ASP构造: 像聚合（如 \(l ≤ {a_1, ..., a_n} ≤ u\)）和选择规则（如 \({F}^ch\)）这类在现代ASP中至关重要的工具，本身就可以被视为复杂命题公式的简写。因此，它们能无缝、直接地在 BC+ 的因果律中使用，极大地增强了语言的实用性和简洁性。
- 统一的表达框架: BC+ 能够模拟并超越先前语言的特性。例如，它既能像 \(B\) 一样处理递归定义（通过直接的蕴含），又能像 \(C+\) 那样通过在 \(if\) 子句中添加双重否定 \(¬¬\) 来处理非最小模型的推理，同时还能定义非惯性的默认行为。
可用的简写
为了方便使用，本文定义了一系列直观的简写，例如：
- \(default c=v if F\)：表示 \(caused {c=v}^ch if F\)，用于描述默认值。
- \(inertial c\)：表示 \(default c=v after c=v\)，用于描述惯性定律。
- \(constraint F\)：表示 \(caused ⊥ if ¬F\)，用于表示状态约束。
- \(nonexecutable F if G\)：表示 \(caused ⊥ if ⊤ after F ∧ G\)，用于描述动作的执行前提。
实验结论
本文没有进行传统的数值性能比较实验，而是通过理论证明和示例来验证其方法的优越性和正确性。
关键结果
- 表达能力的验证:
- 形式化嵌入: 本文提供了将语言 \(BC\) 和 \(C+\)（的确定性片段）翻译成等价的 BC+ 描述的形式化方法（见定理4和5）。这从理论上证明了 BC+ 的表达能力至少与这些语言相当，并且能够统一它们。
- Blocks World 示例: 通过一个精心设计的积木世界（Blocks World）例子，展示了 BC+ 的独特优势。该示例综合运用了多种高级特性，而这些特性很难或不可能在任何一个单一的旧语言中同时实现：
- 递归定义: \(InTower(B)\) 的值通过递归方式定义。
- 聚合约束: 使用聚合来限制“一个积木上最多只能放一个积木” (\({b:Loc(b)=B} ≤ 1\)) 以及“桌上最多只能有k个塔” (\({b:Loc(b)=Table} ≤ k\))。
- 动作属性: 使用非布尔动作常量 \(Destination(B)\) 作为 \(Move(B)\) 动作的属性，并通过 \(always\) 约束将二者关联。
- 实现: 本文基于 \(cplus2asp\) 系统（一个将 \(C+\) 翻译为ASP的工具）扩展实现了一个 BC+ 的计算系统。这证明了 BC+ 的理论是可计算的，并且可以有效利用现有高性能 ASP 求解器进行推理。
结论
本文成功设计并提出了一种新的动作语言 BC+。通过将其语义建立在通用的命题公式稳定模型之上，BC+ 弥合了传统动作语言与现代答案集规划（ASP）之间的鸿沟。它不仅统一了多种先前语言（如 \(BC\) 和 \(C+\)）的优点，还原生支持聚合等高级ASP构造，提供了迄今为止表达能力最强的、统一的高层动作描述形式化工具之一。