LaTeX 中的直到算子（p \mathcal{U} q）

用途

时序逻辑中的“直到”算子：当 q 最终成立且在此之前的每个时刻 p 都成立时，p \mathcal{U} q 成立。

强直到要求 q 一定发生；弱直到 p \mathcal{W} q 还允许 p 永远成立。“最终”可以由它导出：\Diamond q \equiv \top \mathcal{U} q。直接书写时 \mathcal{U} 是普通符号，因此 p\mathcal{U}q 中 U 两侧没有间距；写成 p \mathbin{\mathcal{U}} q 可获得二元运算符间距，也可以定义 \newcommand{\until}{\mathbin{\mathcal{U}}}。许多 LTL 论文使用正体 U，即 \mathbin{\mathsf{U}}，而不是花体字母。过去时逻辑还增加了“自从”算子，它是向后看的镜像。

最小可编译示例

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

\documentclass{article}
\usepackage{amssymb}
\begin{document}
Until: $p \mathcal{U} q$

\[ \Diamond q \leftrightarrow \top \mathbin{\mathcal{U}} q \]
\end{document}

相关符号

• 下一时刻算子\bigcirc p
• 最终算子（时序菱形）\Diamond p
• 可达关系w R v
• 总是算子（时序方框）\Box p
• 克里普克模型\mathcal{M}, w \models p
• 公共知识C_G p

常见问题

如何在 LaTeX 中输入直到算子？

在数学模式中输入 p \mathcal{U} q，例如 $\Diamond q \leftrightarrow \top \mathbin{\mathcal{U}} q$。无需加载任何宏包即可在标准 LaTeX 中使用。

p \mathcal{U} q 需要哪个宏包？

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

p \mathcal{U} q 能在文本模式中使用，还是只能用于数学模式？

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