[Automata] Ch9 变迁系统 TS

学习Automata PPT的记录.

wiki的定义:
在计算机科学和控制理论中，“变迁系统”用数学的方法描述离散系统的行为。变迁系统主要由“状态”和状态之间的“状态迁移”组成。 有标号的变迁系统可以从已定义的标签集合中选择相应标签来标记状态迁移，而且相同的标签可能被应用在多个状态迁移上。 变迁系统也可以是无标记的，此时也可以认为标签集合中只有单一标签元素，从而省略了状态迁移上的标签记号。

变迁系统在数学定义上和有向图一致，但与有限状态自动机有一定不同。

变迁系统的特点有：

• 系统状态的集合不一定是有限的或可数的；
• 状态迁移的集合不一定是有限的或可数的；
• 变迁系统并不需要给出“开始”状态或“最终”状态；
• 变迁系统可以表示为有向图，有限状态自动机则不能。

因此某种程度上, 可以将TS当成有向图来看待.

---

定义

• 一个变迁系统包含一系列状态及状态之间的转移. (类似图里的点和边)
• transition is labeled with event or action (边上有标签)

迁移系统是一个五元组 A=⟨S,S0,T,α,β⟩ ，其中

• S 是一个有限的或者无限的状态(states)集合；
• S0⊆S 是初始状态集；
• T 是一个有限的或者无限的转移(transitions)集合；
• α 和 β 是两个从 T 到 S 的映射，对于任意的迁移 t∈T ， α(t) 表示迁移 t 的 源(source) 状态， β(t)表示迁移 t 的 目标(target) 状态。

源状态为 s ，目标状态为 s′ 的迁移 t 写作 t:s→s′ 。多个迁移可以有相同的源状态或者目标状态。

Paths: 类似自动机里 $\vdash$ 符号的定义. 是一系列的迁移组成的序列.

根据 t:s→s′, 我们可以定义关系 $\rightarrow$ . 进一步地, 可以定义一个更泛化的概念 $\twoheadrightarrow$, 类似 $\vdash ^*$. 它是表征可到达性的关系.

• 同样可以定义reachable和terminal的概念.
• 如果一个节点既是reachable的, 也是terminal的, 那么它是一个 deadlock state. (能够到达, 且到达后无路可走)

记 $T^+$ 是所有有限路径的集合， $T_w$ 是所有无限路径的集合。我们可以将原本定义在 S×SS×S 上的 $\alpha$ 和 $\beta$ 拓展到 $T^+\times S$ 上。

• $\alpha(t_1​ ... t_n​)=\alpha(t_1​),\beta(t_1​ ... t_n​)=\beta(t_n​)$
• 一个有限的路径 $c$ 代表了一个迁移系统从状态 $\alpha(c)$ 到状态 $\beta(c)$ 的一个有限的演化过程。

类似地，定义 $\alpha(t1 ... )=\alpha(t1)\alpha(t1​ ... )=\alpha(t1​)$ 可以将 $\alpha$ 拓展到 $T_w \times S$ 上。

• 一个无限的路径 $c$ 代表了一个迁移系统从状态 $\alpha(c)$ 开始的一个无限的演化过程。

进一步的, 可以定义 $T^+$上的偏积 $\cdot$ 以及 $T^+ \times T_\omega$上的运算. 它们类似路径的拼接. 并且可以在每个节点上定义一个空路径, 其长度为0. (路径的长度为它包含的边的数量, 即包含的转移的数量. )

带标签的迁移系统

可以为系统中的每一个迁移加上一个标签, 用于表示导致迁移的动作 $\lambda (t) \in A$.
当两个迁移的源状态, 目标状态, 标签均相同时, 将他们视为一个迁移. 即, 认为 $T \rightarrow <S, A, S>$是一个单射.

“空动作”: $\tau$, 表示不需要事件驱动的内部行为或者观察不到的行为。

迁移对应的踪迹:
如果 $c=t1​,t2​,...$ 是一个带标签的迁移系统中的路径，那么触发这些迁移的行为的序列 $trace(c)=\lambda(t1),\lambda(t2),...$  称作这个路径的 踪迹(trace) 。

迁移系统的等价性

严格的等价关系的定义: (需要满足下面的三条性质)

• 自反性
• 对称性
• 传递性

不过在迁移系统当中，存在多种对于等价性的表示方法，它们所表示的“等价”的程度是有所区别的，具体地，我们下面会考虑三种等价：

• 强同构等价(strong isomorphism equivalence)
• 弱同构等价(weak isomorphism equivalence)
• 双模拟等价(bisimulation equivalence)

Transition system homomorphism

令 $A=(S,S0,T,\alpha,\beta)$和 $A' = (S',S0',T',\alpha',\beta ')$ 是两个迁移系统。从 $A$ 到 $A'$ 的一个 迁移系统同态(transition system homomorphism) $h$ 是一个映射的二元组 $(h\sigma,h\tau)$ ，其中

$$h_\sigma:S \rightarrow S',h_\tau:T\rightarrow T'$$

满足对于 $T$ 中的每一个转移 $t$ ，都有

$$\alpha'(h_\tau(t))=h_\sigma(\alpha(t)),\beta'(h_\tau(t))=h_\sigma(\beta(t))$$

即, 一个迁移系统同态将一个迁移系统映射为另一个, 通过将原始状态和原始迁移映射为新的状态和迁移. 这种映射一定程度上不改变原始系统的结构.

带标签的迁移系统同态(labeled transition system homomorphism) h:
类似上面的迁移系统同态, 只是此时这个映射同时需要满足标签对应关系不变的要求.

我们称一个同态 $h$ 是满射的(surjective)，如果两个映射 $h_\sigma$​ 和 $h_\tau$​ 都是满射。如果 $h$ 是一个从 $A$ 到 $A′$ 的满射同态，迁移系统 $A′$ 就称为 $A$ 在 $h$ 下的商。
(满射: 对应值域中的每一个点, 都存在一个定义域中的点与之对应. )

一个 迁移系统强同构(TS strong isomorphism) $h$ 是一个迁移系统同态，并且 $h_\sigma$​ 和 $h_\tau$​ 都是双射。强同构简称同构。

如果存在一个从迁移系统 $A$ 到迁移系统 $A′$ 的强同构，我们称这 $A$ 与 $A′$ 是 强同构的(strong isomorphic) 。

同态是普通的映射 / 函数; 商是满足满射的函数; 同构则满足一一映射的性质.
同态可以是很损失信息量的操作. 例如, 一个同态可以将所有的状态映射为 $s$ , 所有的转移映射为 $t$ (空转移), 此时虽然系统的结构已经被破坏, 仍然可以符合同态的定义; 而同构则保留的系统的结构.

同构是一个很强的等价性质. 同构的逆同样也是一个同构关系. 同构关系表明, 两个系统间"除了名字之外的结构一模一样. "

但是很多时候, 两个不那么一样的系统是会表现出等价的行为的. (例如考虑一个包含了一些无用状态的系统). 因此, 同构关系有些太强大了.

弱同构等价

• 对于一个迁移系统, 考虑它的可达状态以及可达状态上定义的转移关系, 称为"可达子迁移系统".
• 若两个系统的可达子迁移系统是同构的, 则称这两个系统是弱同构等价的.
• 弱同构关系也是一种等价关系.
• 若两个系统同构, 则它们一定弱同构.

双模拟等价 (行为上的等价)

在实际应用当中，我们更多的用的是这种等价。

令 $A=(S,S0,T,\alpha,\beta)$ 和 $A'=(S',S0',T',\alpha',\beta')$ 是两个迁移系统，在 $A$ 和 $A'$ 之间的一个 双模拟(bisimulation) 是一个二元关系 $B \subseteq S \times S'$ ，使得

• $B(S0​,S0')$ ；
• 如果 $B(s1,s1')$ 且 $s1\rightarrow s2$ ，则存在一个 $s2'\in S'$ ，使得 $s1'\rightarrow s2'$​ 且 $B(s2,s2′)$ ；
• 如果 $B(s1,s1')$ 且 $s1'\rightarrow s2'$​ ，则存在一个 $s2\in S$ ，使得 $s1\rightarrow s2$​ 且 $B(s2,s2')$ 。

称 $A$ 和 $A'$ 是 双模拟等价的（bisimulation equivalent） ，当且仅当存在一个 $A$ 和 $A'$ 之间的双模拟。

双模拟的含义就是两个迁移系统可以相互模拟对方的运行.

• 只要求了关系的一个方向, 没有要求另一个方向.
• 两个同构或者弱同构的迁移系统一定是可以双模拟的，但是两个可以双模拟的迁移系统不一定具有同构或者弱同构的关系。

总结

• 强同构：两个迁移系统除了状态命名不同以外其他都是一样的。
• 弱同构：两个迁移系统的可达子系统是强同构的。
• 双模拟：迁移系统具有相同的行为，并在同一时刻做选择。

迁移系统等价性的一个应用是，比如说我想要证明两个建模语言是等价的，我们可以用迁移系统来刻画它们的行为，然后通过证明迁移系统的等价性来证明建模语言行为的等价性。

迁移系统的运算

自由积(free product)

n个迁移系统的自由积, 相当于把他们的状态作为一个统一的向量进行处理, 并也对转移函数做相应的更改.

类似将n个子系统的内容合并为一个总系统.
同一个时钟, 子系统各自进行局部迁移, 它们的结果总和作为全局迁移.

同步积(synchronous product)

只包含符合同步约束的转移, 相当于自由积的一个子集, 排除了那些不可能发生的行为组合.
换句话说，同步积只允许标签向量在同步约束中的全局迁移发生。

$tau$ 迁移和共享标签

自由积的定义本身有一个同步时钟的限制在里面，即所有的子迁移系统必须“共同进退”，我们可以引入 $\tau$ 迁移的方式来消解这种限制。
此时, 总系统发生一步迁移时, 不一定要求所有子系统都发生迁移. 子系统可以选择迁移或停留在原处.

共享标签: 让子系统的迁移标签进行共享, 表明执行这个共享的标签时会发生同时的迁移. 它于同步约束进行的限制是等价的, 只是换用了一种更加简洁的形式.

利用迁移系统建模

例如, 对于一个并发程序的建模, 我们可以将程序中的逻辑变量作为状态的分量, 并构造对应的转移函数.

时序性质

系统在进行转移的过程中有一些有用的性质, 我们介绍一种表征时序性质的形式化方法—— 计算树逻辑(computation tree logic, CTL)

计算树逻辑(computation tree logic, CTL)

计算树展示了从初始状态开始所有可能的执行路径，$CTL^∗$ 公式描述了计算树的性质。

$CTL^∗$ 逻辑公式由路径量词和时序操作符组成。

在 $CTL^∗$ 中有两种类型的逻辑公式：状态公式（在某个特定的状态下成立）、路径公式（沿着某个路径成立）。

路径量词: $A, E$

• $A$ 表示被修饰的逻辑公式对于所有的(for all)计算树路径都成立；
• $E$ 表示被修饰的逻辑公式存在(exist)某些计算树路径成立。

时序操作符: $X, F, G, U, R$

• $X$ ： $Xp$ 表示性质 $p$ 在路径的第二个(next)状态下成立； $s_2(p)$
• $F$ ： $Fp$ 表示性质 $p$ 会在路径将来的的某个状态下成立； $\exists s, s.t.\ \ s(p)$
• $G$ ： $Gp$ 表示性质 $p$ 会在路径的全部(globally)状态下都成立；$\forall s, s(p)$
• $U$ ： $pUq$ 表示 $q$ 成立的状态的前驱状态下 $p$ 一定会成立，也就是说 $p$ 成立，直到(until) $q$ 成立为止。$\exists s_k, s.t.\ \ s_k(p), s_0, ..., s_{k-1}(q)$
• $R$ ： $pRq$ 表示 $q$ 沿着路径一直保持，直到第一个 $p$ 成立的状态（含这个状态）为止，即 $p$ 释放(release)了 $q$ ，$p$ 不需要一直保持。$\exists s_k, s.t.\ \ s_k(p), s_0, ..., s_{k}(q)$

在 $CTL^∗$  中有两种类型的逻辑公式：状态公式（在某个特定的状态下成立）、路径公式（沿着某个路径成立）。

状态公式(state formula)规则的语法如下：

• 如果 $p\in AP$ ，那么 $p$ 是一个状态公式，其中 $AP$ 表示原子命题(atomic propsitions) ；
• 如果 $f$ 和 $g$ 是状态公式，那么 $\lnot f,f\cap g,f\cup g$ 也是状态公式。
• 如果 $f$ 是一个路径公式，那么 $Ef$ 和 $Af$ 是状态公式。

路径公式(path formula)的语法如下：

• 如果 $f$ 是一个状态公式，那么 $f$ 也是一个路径公式；
• 如果 $f$ 和 $g$ 是路径公式，那么 $\lnot f,f \cap g,f \cup g,Xf,Ff,Gf,Gf,fUg,fRg$ 都是路径公式。

路径公式: 接收路径作为输入的算子; 状态公式: 接收状态作为输入的算子.

$CTL^∗$ 的语意：

• 如果 $f$ 是一个状态公式， $M$ 是一个迁移系统，$s\rightarrow f$ 意味着 $f$ 在迁移系统 $M$ 的状态 $s$ 下保持。
• 如果 $g$ 是一个路径公式， $M$ 是一个迁移系统， $\pi \rightarrow g$ 意味着 $g$ 沿着迁移系统 $M$ 的路径 $\pi$ 保持。

CTL和LTL

都是 $CTL^*$ 的子逻辑. 是对 $CTL^*$的公式形式进行某些限制得到的产物.

CTL: 只允许分时逻辑(branching-time logic), 每个线性时间的操作符 $G,F,X,U,R$ 都必须立即被一个路径量词修饰。

LTL: 线性时序逻辑逻辑(linear temporal logic)，组成LTL的逻辑公式都形如 $A f$(只被一个 $A$量词修饰), $f$ 是一个路径公式, 其中的子状态公式只能是原子命题(即, f只通过原子命题和$Xf,Ff,Gf,Gf,fUg,fRg$构成)

CTL有10个基本操作符, 为 $A, E$ 与 $X, F, G, U, R$组合得到.
并且这10个基本操作都可以用 $EX,EG,EU$ 来表达：

表达性质

• 安全性(safety)：坏事情不会发生

  • 典型例子：$AG(reactor_temp<1000)$
  • 通常使用 $AG$ 。

• 活跃度(liveness)：好事情会发生

  • 典型例子： $AF(rich),AF(x>5),AG(start \rightarrow AF terminate)$
  • 通常使用 $AF$ 。

• fairness：某件事情会无穷地经常(infinitely often)发生 (任选一个节点, 事情总是会在后面发生)

  • 典型例子： $AGAF$(enabled)
  • 通常使用 $AGAF$

CTL和LTL的表达能力是不可比的，实践中会根据应用场景和个人偏好来选择(不存在子集关系)。