线性时序逻辑(Linear Temporal Logic, LTL)

线性时序逻辑(Linear Temporal Logic, LTL)常用于形式化交错序列的性质。相比于一阶逻辑和命题逻辑，LTL更能反映状态之间的动态性质。LTL在一个静态逻辑\(U\)的基础上定义，以下我们取\(U\)为一阶和命题逻辑作为例子来定义LTL。

线性时序逻辑的语法
1. 每个\(U\)的公式(formula)也是LTL的公式。
2. 如果\(\varphi,\psi\)是LTL的公式，则以下公式也是LTL的公式：
\((\lnot \varphi),(\varphi\land\psi),(\varphi\lor\psi)\); \((\bigcirc\varphi),(\Diamond\varphi),(\Box\varphi),(\varphi\bigcup\psi),(\varphi\bigvee\psi).\)

线性时序逻辑的语义
一个LTL公式的解释(interpretation)定义在一个无穷状态序列\(\xi = x_0x_1x_2\cdots\)上。
记\(\xi ^k = x_kx_{k+1}x_{k+2}\)为从第k项开始的状态序列，则LTL公式的语义可如下定义：
(1) \(\xi^k\vDash\eta\)，若\(\eta\)是静态逻辑\(U\)的公式满足\(x_k\vDash\eta\).
(2) \(\xi^k\vDash(\lnot\varphi)\)，如果不成立\(\xi^k\vDash\varphi.\)
(3) \(\xi^k\vDash(\varphi\land\psi),\) 若同时成立\(\xi^k\vDash\varphi,\xi^k\vDash\psi.\)
(4) \(\xi^k\vDash(\varphi\lor\psi),\) 若至少成立一个\(\xi^k\vDash\varphi,\xi^k\vDash\psi.\)
(5) \(\xi^k\vDash(\bigcirc\varphi)\)，若\(\xi^{k+1}\vDash\varphi\)，称为"下次成立"(nexttime)
(6) \(\xi^k\vDash(\Diamond\varphi)\)，若存在\(i\ge k,\xi^i\vDash\varphi\)，称为"最终成立"(eventtually).
(7) \(\xi^k\vDash(\Box\varphi)\)，若对任意\(i\ge k,\xi^i\vDash\varphi\)，称为"恒成立"(always).
(8) \(\xi^k\vDash(\varphi\bigcup\psi)\)，若存在\(i\ge k\)，使得对\(\forall k\le j \le i-1\), 有\(\xi^j\vDash\varphi\)，并且\(\xi^i\vDash \psi\), 称为\(\varphi\)成立直到(until)\(\psi\)成立.
(9) \(\xi^k\vDash(\varphi\bigvee\psi)\)，若至少以下之一成立：
(i) 对每个\(i\ge k,\xi^i\vDash\psi.\)
(ii) 存在\(j\ge k,\) \(\xi^j\vDash \varphi\), 且\(\forall k\le i \le j, \xi^i\vDash \psi.\)
称为\(\varphi\) 释放(release) \(\psi\). 这意味着，\(\psi\)需要保持一直成立，直到\(\varphi\)成立（有可能不会发生），并且如果\(\varphi\)成立，则最后一步二者要同时成立。

\(\Box\Diamond\varphi\)表示在序列\(\xi\)中有无穷多个\(\xi_k\)满足\(\varphi\), 而\(\Diamond\Box\varphi\)表示序列\(\xi\)从某一项\(\xi_k\)开始恒满足\(\varphi\)。
\(\Diamond\varphi\)和\((true\bigcup\varphi)\)等价，即true一直成立，直到\(\varphi\)成立（且一定会发生）；而\(\Box\varphi\)和\((false\bigvee\varphi)\)等价，即false释放\(\varphi\)，但释放条件false永远不成立。
此外，我们还有\(\mu\bigvee\eta = \lnot((\lnot\mu)\bigcup(\lnot\eta)).\)

对于一个系统P，如果其每个执行的状态序列\(\xi\)都满足\(\xi\vDash\varphi\)，我们称\(P\vDash\varphi\), 否则\(P\not\vDash\varphi.\)

    所属分类：Formal Methods     发表于2022-01-31