LaTeX 中的下一时刻算子（\bigcirc p）

用途

时序逻辑中的“下一时刻”算子：\bigcirc p 表示 p 在紧接着的下一个状态中成立。

它是 LTL 中唯一与离散时间步相关的算子，也写作 X p。展开律 p \mathcal{U} q \leftrightarrow q \lor (p \land \bigcirc(p \mathcal{U} q)) 利用它把“直到”逐步展开。\bigcirc 是大圆圈，大小与 \Box 和 \Diamond 相当，因此视觉上与它们匹配；\circ 是表示复合的小运算符，在这里使用是错误的。有些论文为了在大量纯文本的规约中更清楚，更喜欢使用 \mathsf{X}。

最小可编译示例

将其粘贴到空白 .tex 文件中，用 pdfLaTeX、XeLaTeX 或 LuaLaTeX 编译。

\documentclass{article}
\usepackage{amssymb}
\begin{document}
Next: $\bigcirc p$

\[ \Box(p \to \bigcirc q) \]
\end{document}

相关符号

• 可达关系w R v
• 直到算子p \mathcal{U} q
• 克里普克模型\mathcal{M}, w \models p
• 最终算子（时序菱形）\Diamond p
• 可能世界w
• 总是算子（时序方框）\Box p

常见问题

如何在 LaTeX 中输入下一时刻算子？

在数学模式中输入 \bigcirc p，例如 $\Box(p \to \bigcirc q)$。无需加载任何宏包即可在标准 LaTeX 中使用。

\bigcirc p 需要哪个宏包？

不需要。\bigcirc p 是标准 LaTeX 的一部分，导言区只需文档类即可编译。

\bigcirc p 能在文本模式中使用，还是只能用于数学模式？

只能用于数学模式。在 $...$ 之外，LaTeX 会报错 "Missing $ inserted"，所以在正文中请写 $\bigcirc p$。