Teaching LTL and {\omega}-automata with Spot

技术摘要：利用 Spot 教学 LTL 与 $\omega$-自动机

问题陈述
线性时序逻辑 (LTL) 和 $\omega$-自动机是形式化方法教育中的基础，特别是在程序验证和模型检测领域。虽然教科书提供了理论基础，但深入的理解通常需要学生实验如何将 LTL 公式转化为自动机。具体而言，学习者通过观察公式的变化如何影响生成的自动机，从而建立关于确定性、状态复杂度以及语法结构与语义类（例如 Manna & Pnueli 层级）之间关系的直觉，可以从中获益。然而，有效的教学需要易于使用的工具，以便进行即时的可视化、比较和交互式实验，且无需复杂的安装障碍。

方法论
本文将 Spot——一个成熟的、用于 LTL 和 $\omega$-自动机操作的开源 C++/Python 库及工具集——作为一种教学平台进行介绍。其方法论侧重于利用 Spot 现有的功能来创建“零安装”的教学入口。该方法采用了三种主要的交互界面：

1. Web 应用程序： 一个可通过标准浏览器访问的单页应用（无需本地安装），作为翻译公式、研究属性和比较逻辑的交互式界面。
2. Jupyter Notebooks： 一系列叙事驱动的笔记本，结合了 Python 代码、内联自动机可视化（通过 Graphviz 渲染）和解释性文本。这些笔记本允许进行程序化的探索，包括包含性检查、反例生成和状态重标记。
3. 命令行工具： 一套实用程序，可根据特定标准生成随机示例，以创建练习题集。

核心贡献
本文详细介绍了如何将 Spot 的现有功能重新构建并应用于教学场景：

• 交互式可视化与转换： Web 工具允许用户输入 LTL 或 PSL 公式，并立即生成具有各种接受条件（广义 Büchi、Rabin、Streett、Parity 等）的 $\omega$-自动机。它支持多种输入语法和格式（如 HOA、never claims、LBTT 等）。
• 比较分析与简化：
  • 等价性检查： “比较 (compare)”标签页允许学生输入两个公式，并在它们不等价时提供区分性的 $\omega$-词（$\omega$-words），从而促进对更简单等价公式的发现。
  • 层级导航： “研究 (study)”标签页识别公式在 Manna & Pnueli 时序层级和语法-未来（syntactic-future）层级中的精确类别。它强调了语法分类与语义属性之间的差异（例如，识别出某个公式在语法上属于较高类，但在语义上等价于较低类的案例）。
  • 步进不变性 (Stutter Invariance)： 该工具可检测步进不变性，这是模型检测中部分序约简的关键属性。如果公式不是步进不变的，工具会提供特定的反例词（$w$ 和 $w'$）来演示失效情况。
• 程序化探索： Python API 和 Jupyter notebooks 支持演示高级概念，例如使用非确定性 Büchi 自动机进行语言包含性检查，以及将确定性自动机的状态重标记为其所识别的 LTL 公式。
• 自动化练习生成： 命令行工具（randltl, ltlfilt）允许教师通过暴力生成满足特定约束的随机公式（例如，生成不使用 $X$ 算子但等价于 $a \mathbin{U} b$ 的公式，或生成包含 $X$ 算子但仍具有步进不变性的公式）。

结果
本文通过具体的教学场景展示了这些工具的实际应用：

• 学生可以通过比较它们的自动机或使用比较标签页，验证 $(a \mathbin{R} (a \mathbin{U} b)) \mathbin{W} b$ 是否等价于 $a \mathbin{U} b$。
• 该工具成功识别出 $a \mathbin{W} \mathbin{F}(b)$ 是一个义务属性（Manna & Pnueli $\Delta_1$），尽管它在语法上看起来属于 $\Pi_2$，并确认了它与 $G(a) \lor \mathbin{F}(b)$ 的等价性。
• 命令行示例成功生成了符合复杂标准的公式列表，例如寻找 10 个等价于 $a \mathbin{U} b$ 且排除特定算子的公式，或寻找包含 $X$ 算子但仍具有步进不变性的公式。

意义
本文认为，Spot 提供了一个全面的、易于访问的平台，用于教学时序逻辑公式与其语义自动机之间的联系。通过提供基于 Web、基于 Notebook 以及基于命令行的界面，它适应了多样化的教学环境——从使用平板电脑的课堂到编写代码的研究人员。其意义在于能够超越静态理论，让学生“进行实验：改变一个公式，观察生成的自动机如何变化，并建立直觉”。这些工具被呈现为即插即用的资源，对于 Web 用户无需安装，对于无法在本地安装 Python 的用户则提供了预配置环境（通过 spot-sandbox），从而降低了形式化方法教育的门槛。