迁移系统 （transition system，TS）是一个反应式的系统，直觉上它由一个所有可能状态的集合以及一些迁移（transition）——或者说状态转换（state change）——的集合组成。
比如说，对于交通信号灯来说，当前信号灯的颜色就是这个系统的状态，信号灯颜色的改变就是这个系统的迁移。
再比如说，对于一个程序来说，这个程序中所有变量的值以及 PC 的值就是这个程序的状态，一个程序语句的执行会导致这个程序状态的改变。
当一个状态转换是由于一个外部的事件或者是由于系统的某个行为产生的，那么我们就使用那个事件或者行为来标记这个迁移。
迁移系统是一种描述系统行为的模型，我们可以用有向图来表示，图中的结点表示状态，边表示迁移行为（状态转换）。
下图是一个饮料自动售货机的迁移系统：
定义 9.1
迁移系统是一个五元组 A = ⟨ S , S 0 , T , α , β ⟩ \mathcal{A} = \langle S, S_0, T, \alpha, \beta\rangle A = ⟨ S , S 0 , T , α , β ⟩
S S S S 0 ⊆ S S_0 \subseteq S S 0 ⊆ S T T T α \alpha α β \beta β T T T S S S t ∈ T t \in T t ∈ T α ( t ) \alpha(t) α ( t ) t t t 源 （source）状态，β ( t ) \beta(t) β ( t ) t t t 目标 （target）状态。源状态为 s s s s ′ s' s ′ t t t t : s → s ′ t: s\to s' t : s → s ′
如果 S S S T T T
定义 9.2
一个迁移系统 A = ⟨ S , S 0 , T , α , β ⟩ \mathcal{A} = \langle S, S_0, T, \alpha, \beta\rangle A = ⟨ S , S 0 , T , α , β ⟩ n ( n > 0 ) n(n > 0) n ( n > 0 ) 路径 （path）是一个迁移的序列 t 1 , t 2 , ⋯ , t n t_1, t_2, \cdots, t_n t 1 , t 2 , ⋯ , t n
∀ i , 1 ≤ i < n , β ( t i ) = α ( t i + 1 ) ∧ α ( t 1 ) ∈ S 0 \forall i, 1\le i < n, \beta(t_i) =\alpha(t_{i+1}) \wedge \alpha(t_1) \in S_0 ∀ i , 1 ≤ i < n , β ( t i ) = α ( t i + 1 ) ∧ α ( t 1 ) ∈ S 0
类似的，一个无限的路径是一个无限的迁移序列 t 1 , t 2 , t 3 , ⋯ t_1, t_2, t_3, \cdots t 1 , t 2 , t 3 , ⋯
∀ i ≥ 1 , β ( t i ) = α ( t i + 1 ) ∧ α ( t 1 ) ∈ S 0 \forall i \ge 1, \beta(t_i) = \alpha(t_{i+1}) \wedge \alpha(t_1) \in S_0 ∀ i ≥ 1 , β ( t i ) = α ( t i + 1 ) ∧ α ( t 1 ) ∈ S 0
如果 ∃ t ∈ T , α ( t ) = s ∧ β ( t ) = s ′ \exists t\in T, \alpha(t) = s \wedge \beta(t) = s' ∃ t ∈ T , α ( t ) = s ∧ β ( t ) = s ′ s → s ′ s \to s' s → s ′ ↠ ⊆ S × S \twoheadrightarrow \subseteq S \times S ↠ ⊆ S × S
若 s → s ′ s \to s' s → s ′ s ↠ s ′ s \twoheadrightarrow s' s ↠ s ′ 若 s ↠ s ′ s \twoheadrightarrow s' s ↠ s ′ s ′ ↠ s ′ ′ s' \twoheadrightarrow s'' s ′ ↠ s ′′ s ↠ s ′ ′ s \twoheadrightarrow s'' s ↠ s ′′ 令 A = ⟨ S , S 0 , T , α , β ⟩ \mathcal{A} = \langle S, S_0, T, \alpha, \beta \rangle A = ⟨ S , S 0 , T , α , β ⟩ s s s s ∈ S , s 0 ∈ S 0 , s 0 ↠ s s \in S, s_0 \in S_0, s_0 \twoheadrightarrow s s ∈ S , s 0 ∈ S 0 , s 0 ↠ s s s s s ′ s' s ′ s → s ′ s \to s' s → s ′
如果一个状态 s s s s s s
记 T + T^+ T + T ω T^{\omega} T ω S × S S \times S S × S α \alpha α β \beta β T + × S T^+ \times S T + × S
α ( t 1 ⋯ t n ) = α ( t 1 ) , β ( t 1 ⋯ t n ) = β ( t n ) \alpha(t_1\cdots t_n) = \alpha(t_1), \beta(t_1\cdots t_n) = \beta(t_n) α ( t 1 ⋯ t n ) = α ( t 1 ) , β ( t 1 ⋯ t n ) = β ( t n ) 一个有限的路径 c c c α ( c ) \alpha(c) α ( c ) β ( c ) \beta(c) β ( c ) 类似地，定义 α ( t 1 ⋯ ) = α ( t 1 ) \alpha(t_1\cdots) = \alpha(t_1) α ( t 1 ⋯ ) = α ( t 1 ) α \alpha α T ω × S T^{\omega} \times S T ω × S
一个无限的路径 c c c α ( c ) \alpha(c) α ( c ) 一种 T + T^+ T +
若 c = t 1 t 2 ⋯ t n c = t_1t_2\cdots t_n c = t 1 t 2 ⋯ t n n n n c ′ = t 1 ′ t 2 ′ ⋯ t m ′ c' = t_1't_2'\cdots t_m' c ′ = t 1 ′ t 2 ′ ⋯ t m ′ m m m β ( c ) = α ( c ′ ) \beta(c) = \alpha(c') β ( c ) = α ( c ′ ) 则 c ⋅ c ′ = t 1 ⋯ t n t 1 ′ ⋯ t m ′ c\cdot c' = t_1\cdots t_nt_1'\cdots t_m' c ⋅ c ′ = t 1 ⋯ t n t 1 ′ ⋯ t m ′ n + m n + m n + m α ( c ⋅ c ′ ) = α ( c ) , β ( c ⋅ c ′ ) = β ( c ′ ) \alpha(c\cdot c') = \alpha(c), \beta(c\cdot c') = \beta(c') α ( c ⋅ c ′ ) = α ( c ) , β ( c ⋅ c ′ ) = β ( c ′ ) 类似的，我们也可以定义 T + × T ω T^+ \times T^{\omega} T + × T ω c c c c ′ c' c ′ β ( c ) = α ( c ′ ) \beta(c) = \alpha(c') β ( c ) = α ( c ′ ) c ⋅ c ′ c\cdot c' c ⋅ c ′ α ( c ⋅ c ′ ) = α ( c ) \alpha(c\cdot c') = \alpha(c) α ( c ⋅ c ′ ) = α ( c )
对于每个状态 s ∈ S s \in S s ∈ S ε s \varepsilon_{s} ε s 0 0 0 α ( ε s ) = β ( ε s ) = s \alpha(\varepsilon_{s}) = \beta(\varepsilon_{s}) = s α ( ε s ) = β ( ε s ) = s
若 c c c s = α ( c ) , s ′ = β ( c ) s = \alpha(c), s' = \beta(c) s = α ( c ) , s ′ = β ( c ) ε s ⋅ c = c = c ⋅ ε s ′ \varepsilon_{s} \cdot c = c = c \cdot \varepsilon_{s'} ε s ⋅ c = c = c ⋅ ε s ′ c c c s = α ( c ) s = \alpha(c) s = α ( c ) ε s ⋅ c = c \varepsilon_{s} \cdot c = c ε s ⋅ c = c
定义 9.3
一个被字母表 A A A 带标签的迁移系统 （labeled transition system）是一个 6 元组 A = ⟨ S , S 0 , T , α , β , λ ⟩ \mathcal{A} = \langle S, S_0, T, \alpha, \beta, \lambda\rangle A = ⟨ S , S 0 , T , α , β , λ ⟩
⟨ S , S 0 , T , α , β ⟩ \langle S, S_0, T, \alpha, \beta\rangle ⟨ S , S 0 , T , α , β ⟩ λ \lambda λ T T T A A A T T T A A A λ ( t ) \lambda(t) λ ( t ) 直觉上，一个迁移的标签意味着触发这个迁移的行为或者事件。
我们假设两个不同的迁移不可以具有相同的源状态、目标状态和标签，这是符合逻辑的。因为我们没有必要去区分两个由同样的行为 λ ( t ) = λ ( t ′ ) \lambda(t) = \lambda(t') λ ( t ) = λ ( t ′ ) α ( t ) = α ( t ′ ) \alpha(t) = \alpha(t') α ( t ) = α ( t ′ ) β ( t ) = β ( t ′ ) \beta(t) = \beta(t') β ( t ) = β ( t ′ ) t t t t ′ t' t ′
这就意味着 ⟨ α , λ , β ⟩ : T → S × A × S \langle\alpha,\lambda,\beta\rangle : T\to S\times A\times S ⟨ α , λ , β ⟩ : T → S × A × S
不过对于一个给定的状态，同样的行为或者事件可以引起两个不同的迁移，从而导向不同的状态，也就是说：α ( t ) = α ( t ′ ) \alpha(t) = \alpha(t') α ( t ) = α ( t ′ ) λ ( t ) = λ ( t ′ ) \lambda(t) = \lambda(t') λ ( t ) = λ ( t ′ ) t = t ′ t = t' t = t ′
之前的自动售货机模型的带标签的迁移系统版本如下：
其中 τ \tau τ
定义 9.3
如果 c = t 1 , t 2 , ⋯ c=t_1,t_2,\cdots c = t 1 , t 2 , ⋯ t r a c e ( c ) = λ ( t 1 ) , λ ( t 2 ) , ⋯ trace(c) = \lambda(t_1), \lambda(t_2),\cdots t r a ce ( c ) = λ ( t 1 ) , λ ( t 2 ) , ⋯ 踪迹 （trace）。
首先回忆一下严格的等价关系的定义：
一个关系 R ⊆ X × X R \subseteq X \times X R ⊆ X × X
自反性（reflexive）：∀ x ∈ X , ( x , x ) ∈ R \forall x \in X, (x, x) \in R ∀ x ∈ X , ( x , x ) ∈ R 对称性（symmetric）：∀ x , y ∈ X , ( x , y ) ∈ R → ( y , x ) ∈ R \forall x, y \in X, (x, y) \in R \to (y, x) \in R ∀ x , y ∈ X , ( x , y ) ∈ R → ( y , x ) ∈ R 传递性（transitive）：∀ x , y , z ∈ X , ( x , y ) ∈ R ∧ ( y , z ) ∈ R → ( x , z ) ∈ R \forall x,y,z\in X, (x, y) \in R \wedge (y, z) \in R \to (x, z) \in R ∀ x , y , z ∈ X , ( x , y ) ∈ R ∧ ( y , z ) ∈ R → ( x , z ) ∈ R 不过在迁移系统当中，存在多种对于等价性的表示方法，它们所表示的“等价”的程度是有所区别的，具体地，我们下面会考虑三种等价：
强同构等价（strong isomorphism equivalence） 弱同构等价（weak isomorphism equivalence） 双模拟等价（bisimulation equivalence）
在介绍强同构之前，我们先介绍一下迁移系统同态概念，因为同构是一种特殊的同态。
定义 9.4
令 A = ⟨ S , S 0 , T , α , β ⟩ \mathcal{A} = \langle S, S_0, T, \alpha, \beta \rangle A = ⟨ S , S 0 , T , α , β ⟩ A ′ = ⟨ S ′ , S 0 ′ , T ′ , α ′ , β ′ ⟩ \mathcal{A}' = \langle S', S_0', T', \alpha',\beta'\rangle A ′ = ⟨ S ′ , S 0 ′ , T ′ , α ′ , β ′ ⟩ A \mathcal{A} A A ′ \mathcal{A}' A ′ 迁移系统同态 （transition system homomorphism）h h h ( h σ , h τ ) (h_{\sigma}, h_{\tau}) ( h σ , h τ )
h σ : S → S ′ , h τ : T → T ′ h_{\sigma}:S \to S', h_{\tau}:T\to T' h σ : S → S ′ , h τ : T → T ′
满足对于 T T T t t t
α ′ ( h τ ( t ) ) = h σ ( α ( t ) ) , β ′ ( h τ ( t ) ) = h σ ( β ( t ) ) \alpha'(h_{\tau}(t)) = h_{\sigma}(\alpha(t)), \beta'(h_{\tau}(t)) = h_{\sigma}(\beta(t)) α ′ ( h τ ( t )) = h σ ( α ( t )) , β ′ ( h τ ( t )) = h σ ( β ( t ))
定义 9.5
令 A = ⟨ S , S 0 , T , α , β , λ ⟩ \mathcal{A} = \langle S, S_0, T, \alpha, \beta, \lambda \rangle A = ⟨ S , S 0 , T , α , β , λ ⟩ A ′ = ⟨ S ′ , S 0 ′ , T ′ , α ′ , β ′ , λ ′ ⟩ \mathcal{A}' = \langle S', S_0', T', \alpha',\beta',\lambda'\rangle A ′ = ⟨ S ′ , S 0 ′ , T ′ , α ′ , β ′ , λ ′ ⟩ A \mathcal{A} A A ′ \mathcal{A}' A ′ 带标签的迁移系统同态 （labeled transition system homomorphism）h h h
λ ′ ( h τ ( t ) ) = λ ( t ) \lambda'(h_{\tau}(t)) = \lambda(t) λ ′ ( h τ ( t )) = λ ( t )
我们称一个同态 h h h h σ h_{\sigma} h σ h τ h_{\tau} h τ h h h A \mathcal{A} A A ′ \mathcal{A}' A ′ A ′ \mathcal{A}' A ′ A \mathcal{A} A h h h
定义 9.6
一个迁移系统强同构 （TS strong isomorphism）h h h h σ h_{\sigma} h σ h τ h_{\tau} h τ
如果存在一个从迁移系统 A \mathcal{A} A A ′ \mathcal{A}' A ′ A \mathcal{A} A A ′ \mathcal{A}' A ′ 强同构的 （strong isomorphic）。
一个同构 h = ( h σ , h τ ) h = (h_{\sigma}, h_{\tau}) h = ( h σ , h τ ) g = ( g σ , g τ ) , g σ = h σ − 1 , g τ = h τ − 1 g = (g_{\sigma}, g_{\tau}), g_{\sigma} = h_{\sigma}^{-1}, g_{\tau} = h_{\tau}^{-1} g = ( g σ , g τ ) , g σ = h σ − 1 , g τ = h τ − 1
同构是一种等价关系，并且是一种很强的等价关系。如果两个迁移系统是同构的，那么它们唯一的区别就只能是状态和迁移的命名不同了。
考虑如下的两个迁移系统，它们同构吗？
它们其实是不同构的，但这两个迁移系统的行为其实是肉眼可见地等价的。因此，同构这个等价性的要求有些过于高了，必须除了名字以外一摸一样才行，这往往是不必要的。
对于一个迁移系统的状态 s s s s 0 ∈ S 0 ∧ s 0 ↠ s s_0 \in S_0 \wedge s_0 \twoheadrightarrow s s 0 ∈ S 0 ∧ s 0 ↠ s
考虑两个迁移系统中可达的状态，以及定义在这些状态上的迁移，我们可以得到两个可达子迁移系统。如果这两个可达子迁移系统是同构的，我们称原来的两个迁移系统是弱同构 （weak isomorphic）的。
因此，下面两个系统是弱同构的。
弱同构也是一种等价关系。 如果两个系统是同构的，那么它们一定也是弱同构的。 在实际应用当中，我们更多的用的是这种等价。
定义 9.7
令 A = ⟨ S , S 0 , T , α , β ⟩ \mathcal{A} = \langle S, S_0, T, \alpha, \beta \rangle A = ⟨ S , S 0 , T , α , β ⟩ A ′ = ⟨ S ′ , S 0 ′ , T ′ , α ′ , β ′ ⟩ \mathcal{A}' = \langle S', S_0', T', \alpha',\beta'\rangle A ′ = ⟨ S ′ , S 0 ′ , T ′ , α ′ , β ′ ⟩ A \mathcal{A} A A ′ \mathcal{A}' A ′ 双模拟 （bisimulation） 是一个二元关系 B ⊆ S × S ′ B \subseteq S \times S' B ⊆ S × S ′
B ( S 0 , S 0 ′ ) B(S_0, S_0') B ( S 0 , S 0 ′ ) 如果 B ( s 1 , s 1 ′ ) B(s_1, s_1') B ( s 1 , s 1 ′ ) s 1 → s 2 s_1 \to s_2 s 1 → s 2 s 2 ′ ∈ S ′ s_2'\in S' s 2 ′ ∈ S ′ s 1 ′ → s 2 ′ s_1' \to s_2' s 1 ′ → s 2 ′ B ( s 2 , s 2 ′ ) B(s_2, s_2') B ( s 2 , s 2 ′ ) 如果 B ( s 1 , s 1 ′ ) B(s_1, s_1') B ( s 1 , s 1 ′ ) s 1 ′ → s 2 ′ s_1' \to s_2' s 1 ′ → s 2 ′ s 2 ∈ S s_2 \in S s 2 ∈ S s 1 → s 2 s_1 \to s_2 s 1 → s 2 B ( s 2 , s 2 ′ ) B(s_2, s_2') B ( s 2 , s 2 ′ ) 称 A \mathcal{A} A A ′ \mathcal{A}' A ′ 双模拟等价的 （bisimulation equivalent），当且仅当存在一个 A \mathcal{A} A A ′ \mathcal{A}' A ′
双模拟的含义就是两个迁移系统可以相互模拟对方的运行。下面是一个双模拟的例子。
两个同构或者弱同构的迁移系统一定是可以双模拟的，但是两个可以双模拟的迁移系统不一定具有同构或者弱同构的关系。
此外，一些看似行为等价的迁移系统也不一定会满足双模拟关系。比如说下面的这个例子。
强同构：两个迁移系统除了状态命名不同以外其他都是一样的。 弱同构：两个迁移系统的可达子系统是强同构的。 双模拟：迁移系统具有相同的行为，并在同一时刻做选择。 迁移系统等价性的一个应用是，比如说我想要证明两个建模语言是等价的，我们可以用迁移系统来刻画它们的行为，然后通过证明迁移系统的等价性来证明建模语言行为的等价性。
定义 9.8
考虑 n n n A i = ⟨ S i , S 0 i , T i , α i , β i ⟩ \mathcal{A}_i = \langle S_i, {S_0}_i, T_i, \alpha_i, \beta_i \rangle A i = ⟨ S i , S 0 i , T i , α i , β i ⟩ n n n 自由积 （free product）是一个迁移系统 A = ⟨ S , S 0 , T , α , β ⟩ \mathcal{A} = \langle S, S_0, T, \alpha, \beta \rangle A = ⟨ S , S 0 , T , α , β ⟩
S = S 1 × S 2 × ⋯ × S n T = T 1 × T 2 × ⋯ × T n α ( t 1 , ⋯ , t n ) = ⟨ α 1 ( t 1 ) , ⋯ , α n ( t n ) ⟩ β ( t 1 , ⋯ , t n ) = ⟨ β 1 ( t 1 ) , ⋯ , β n ( t n ) ⟩ S = S_1 \times S_2 \times \cdots \times S_n\\ T = T_1 \times T_2 \times \cdots \times T_n\\ \alpha(t_1, \cdots , t_n) = \langle\alpha_1(t_1),\cdots,\alpha_n(t_n)\rangle\\ \beta(t_1, \cdots , t_n) = \langle\beta_1(t_1), \cdots,\beta_n(t_n)\rangle S = S 1 × S 2 × ⋯ × S n T = T 1 × T 2 × ⋯ × T n α ( t 1 , ⋯ , t n ) = ⟨ α 1 ( t 1 ) , ⋯ , α n ( t n )⟩ β ( t 1 , ⋯ , t n ) = ⟨ β 1 ( t 1 ) , ⋯ , β n ( t n )⟩
此外，若每个 A i \mathcal{A}_i A i A i A_i A i A 1 × A 2 × ⋯ × A n A_1 \times A_2 \times \cdots \times A_n A 1 × A 2 × ⋯ × A n
λ ( t 1 , ⋯ , t n ) = ⟨ λ 1 ( t 1 ) , ⋯ , λ n ( t n ) ⟩ \lambda(t_1, \cdots, t_n) = \langle\lambda_1(t_1), \cdots , \lambda_n(t_n)\rangle λ ( t 1 , ⋯ , t n ) = ⟨ λ 1 ( t 1 ) , ⋯ , λ n ( t n )⟩
下面是一个自由积的例子，左侧是两个迁移系统，右侧是他们的自由积。
从自由积的定义中，我们可以看出，自由积假设在一个全局系统当中，所有的子系统都是同时执行它们的转移的。我们可以将时间分成一系列的时刻，在每个时刻，每个子迁移系统都恰好执行一次迁移。换句话说，我们相当于是使用同一个“时钟”来驱动了多个迁移系统，从而形成了自由积这样的全局系统。
具体地，如果迁移系统 A \mathcal{A} A s = ⟨ s 1 , ⋯ , s n ⟩ s = \langle s_1, \cdots ,s_n \rangle s = ⟨ s 1 , ⋯ , s n ⟩ A i \mathcal{A}_i A i s i s_i s i A i \mathcal{A}_i A i t i t_i t i s i ′ s_i' s i ′ t = ⟨ t 1 , ⋯ , t n ⟩ t = \langle t_1, \cdots ,t_n\rangle t = ⟨ t 1 , ⋯ , t n ⟩ A \mathcal{A} A s ′ = ⟨ s 1 ′ , ⋯ , s n ′ ⟩ s' = \langle s_1' , \cdots , s_n'\rangle s ′ = ⟨ s 1 ′ , ⋯ , s n ′ ⟩ λ ( t ) \lambda(t) λ ( t ) t t t
当进程之间进行交互的时候，并不是所有可能的全局行为都是有用的，因为这些交互会受到进程通信和同步的限制。
因此，描述多进程系统的迁移系统一定是各个进程对应的各自迁移系统的自由积的一个子系统，我们可以用同步积来表达这种受到通信和同步约束的全局系统。
定义 9.9
如果 A i , i = 1 , 2 , ⋯ , n \mathcal{A}_i, i = 1, 2, \cdots, n A i , i = 1 , 2 , ⋯ , n n n n A i , i = 1 , 2 , ⋯ , n A_i, i = 1, 2, \cdots, n A i , i = 1 , 2 , ⋯ , n I ⊆ A 1 × A 2 × ⋯ × A n I \subseteq A_1 \times A_2 \times \cdots \times A_n I ⊆ A 1 × A 2 × ⋯ × A n 同步约束 （synchronous product），那么 A i , i = 1 , 2 , ⋯ , n \mathcal{A}_i, i = 1, 2, \cdots , n A i , i = 1 , 2 , ⋯ , n I I I 同步积 （synchronous product），写作 ⟨ A 1 , ⋯ , A n , I ⟩ \langle \mathcal{A}_1 ,\cdots ,\mathcal{A}_n, I\rangle ⟨ A 1 , ⋯ , A n , I ⟩ A i , i = 1 , 2 , ⋯ , n \mathcal{A}_i, i = 1, 2, \cdots, n A i , i = 1 , 2 , ⋯ , n ⟨ λ 1 ( t 1 ) , ⋯ , λ n ( t n ) ⟩ ∈ I \langle \lambda_1(t_1), \cdots ,\lambda_n(t_n)\rangle \in I ⟨ λ 1 ( t 1 ) , ⋯ , λ n ( t n )⟩ ∈ I ⟨ t 1 , ⋯ , t n ⟩ \langle t_1, \cdots ,t_n\rangle ⟨ t 1 , ⋯ , t n ⟩
换句话说，同步积只允许标签向量在同步约束中的全局迁移发生。
比如说，下图中，右侧迁移系统是左侧两个迁移系统的自由积。
如果加上标签，但是不加同步限制的话，带标签的自由积如下图所示。
但如果我们加上 { ⟨ a , b ⟩ } \{\langle a, b\rangle\} {⟨ a , b ⟩}
其实，同步限制当中的每个元素，就是一个可以同时发生的迁移所组成的向量。
自由积的定义本身有一个同步时钟的限制在里面，即所有的子迁移系统必须“共同进退”，我们可以引入 τ \tau τ τ \tau τ τ \tau τ
下图的右侧就是左侧两个迁移系统引入 τ \tau τ
除了显示的将所有可能同时发生的迁移列出来作为同步限制以外，我们也可以使用共享标签来表示两个迁移必须同时发生，这样在表达上面会更加简洁。不过这并没有拓展同步积的表达能力就是了，只是换了一种更简便的表达方式而已。
比如说下图的左侧是三个具有共享标签的迁移系统，右侧是它们的同步积。
例如，对于具有输入变量 x x x y y y r r r ¬ ( x ⊕ r ) \neg (x \oplus r) ¬ ( x ⊕ r ) x ∨ r x \vee r x ∨ r
Process 1 :
while ( true) { out: a : = true; turn : = true;
wait: await ( ! b or ! turn) ;
cs: a : = false;
} || Process 2 :
while ( true) { out: b : = true; turn : = false;
wait: await ( ! a or turn) ;
cs: b : = false;
} 两个并发执行的进程正在尝试在不违反互斥规定的情况下进入一个临界区（critical section）。
一个程序的状态可以通过其中变量的值以及程序计数器（program counters，pc）的值来捕捉。再我们上面的例子中，有
两个程序计数器：p c 1 pc1 p c 1 p c 2 pc2 p c 2 { o u t , w a i t , c s } \{out, wait, cs\} { o u t , w ai t , cs } 三个布尔变量：t u r n turn t u r n a a a b b b { T r u e , F a l s e } \{True, False\} { T r u e , F a l se } 程序的每个状态就是所有的这些变量的值组成的元组，可以写作 ( p c 1 , p c 2 , t u r n , a , b ) (pc1, pc2, turn, a, b) ( p c 1 , p c 2 , t u r n , a , b )
于是这个程序可能的初始状态有 { ( o , o , F , F , F ) , ( o , o , F , F , T ) , ( o , o , F , T , F ) , ( o , o , F , T , T ) , ( o , o , T , F , F ) , ( o , o , T , F , T ) , ( o , o , T , T , F ) , ( o , o , T , T , T ) } \{(o, o, F, F, F), (o, o, F, F, T), (o, o, F, T, F), (o, o, F, T, T), (o, o, T, F, F), (o, o, T, F, T), (o, o, T, T, F), (o, o, T, T, T)\} {( o , o , F , F , F ) , ( o , o , F , F , T ) , ( o , o , F , T , F ) , ( o , o , F , T , T ) , ( o , o , T , F , F ) , ( o , o , T , F , T ) , ( o , o , T , T , F ) , ( o , o , T , T , T )} p c 1 = p c 2 = o pc1 = pc2 = o p c 1 = p c 2 = o
那么这个程序可能的所有状态有多少个呢？ 3 × 3 × 2 × 2 × 2 = 72 3 \times 3 \times 2 \times 2 \times 2 = 72 3 × 3 × 2 × 2 × 2 = 72
我们以初始状态 ( o , o , F , F , F ) (o, o, F, F, F) ( o , o , F , F , F )
如果进程 1 执行了 out: a := true; turn := true;，则程序的下一个状态是 ( w , o , T , T , F ) (w, o, T, T, F) ( w , o , T , T , F ) 如果进程 2 执行了 out: b := true; turn := false;，则程序的下一个状态是 ( o , w , F , F , T ) (o, w, F, F, T) ( o , w , F , F , T ) 因此，我们的迁移系统中会有 ( o , o , F , F , F ) → ( w , o , T , T , F ) (o, o, F, F, F)\to(w, o, T, T, F) ( o , o , F , F , F ) → ( w , o , T , T , F ) ( o , o , F , F , F ) → ( o , w , F , F , T ) (o, o, F, F, F) \to (o, w, F, F, T) ( o , o , F , F , F ) → ( o , w , F , F , T )
再比如对于如下的程序片段：
其迁移系统为：
像如下一些性质我们称之为时序性质 （temporal properties）：
一旦 r r r 1 1 1 1 1 1 两个程序不可以同时在临界区； 如果你选择了雪碧，那么在你再次支付之前你不能得到啤酒； 没有死锁； …… 时序逻辑（temporal logic）是一种描述一个反应式系统中状态之间迁移序列的形式化方法。像“最终”、“从不”这样的性质可以使用特殊的时序操作符来规定，下面我们来学习一种描述时序逻辑的形式化方法——计算树逻辑 （computation tree logic, CTL），具体地，我们会学习 C T L ∗ CTL^* CT L ∗
计算树展示了从初始状态开始所有可能的执行路径，C T L ∗ CTL^* CT L ∗
C T L ∗ CTL^* CT L ∗
路径量词有两个：
A \mathbf{A} A E \mathbf{E} E 时序操作符有五个：
X \mathbf{X} X X p \mathbf{X}p X p p p p F \mathbf{F} F F p \mathbf{F}p F p p p p G \mathbf{G} G G p \mathbf{G}p G p p p p U \mathbf{U} U p U q p \mathbf{U} q p U q q q q p p p p p p q q q R \mathbf{R} R p R q p \mathbf{R} q p R q q q q p p p p p p q q q p p p 在 C T L ∗ CTL^* CT L ∗
状态公式（state formula）规则的语法如下：
如果 p ∈ A P p \in \mathbf{A}P p ∈ A P p p p A P \mathbf{A}P A P 如果 f f f g g g ¬ f , f ∧ g , f ∨ g \neg f, f\wedge g, f\vee g ¬ f , f ∧ g , f ∨ g 如果 f f f E f \mathbf{E}f E f A f \mathbf{A}f A f 路径公式（path formula）的语法如下：
如果 f f f f f f 如果 f f f g g g ¬ f , f ∧ g , f ∨ g , X f , F f , G f , G f , f U g , f R g \neg f, f \wedge g, f \vee g, \mathbf{X}f, \mathbf{F}f, \mathbf{G}f, \mathbf{G}f, f\mathbf{U}g, f\mathbf{R}g ¬ f , f ∧ g , f ∨ g , X f , F f , G f , G f , f U g , f R g C T L ∗ CTL^* CT L ∗
C T L ∗ CTL^* CT L ∗
如果 f f f M M M s → f s\to f s → f f f f M M M s s s 如果 g g g M M M π → g \pi \to g π → g g g g M M M π \pi π CTL 和 LTL 是 C T L ∗ CTL^* CT L ∗
CTL 是 C T L ∗ CTL^* CT L ∗ G , F , X , U , R \mathbf{G}, \mathbf{F}, \mathbf{X}, \mathbf{U}, \mathbf{R} G , F , X , U , R 例如 A G ( E F p ) , A ( F G p ) \mathbf{A}\mathbf{G}(\mathbf{E}\mathbf{F} p), \mathbf{A}(\mathbf{F}\mathbf{G} p) AG ( EF p ) , A ( FG p ) LTL 是线性时序逻辑逻辑（linear temporal logic），组成 LTL 的逻辑公式都形如 A f \mathbf{A} f A f f f f 例如 A ( F G p ) \mathbf{A}(\mathbf{F}\mathbf{G} p) A ( FG p ) CTL 有 10 个基本的操作符：
A X \mathbf{A}\mathbf{X} AX E X \mathbf{E}\mathbf{X} EX A F \mathbf{A}\mathbf{F} AF E F \mathbf{E}\mathbf{F} EF A G \mathbf{A}\mathbf{G} AG E G \mathbf{E}\mathbf{G} EG A U \mathbf{A}\mathbf{U} AU E U \mathbf{E}\mathbf{U} EU A R \mathbf{A}\mathbf{R} AR E R \mathbf{E}\mathbf{R} ER
并且这 10 个基本操作都可以用 E X , E G , E U \mathbf{E}\mathbf{X}, \mathbf{E}\mathbf{G}, \mathbf{E}\mathbf{U} EX , EG , EU
A X ( f ) = ¬ E X ( ¬ f ) \mathbf{A}\mathbf{X}(f) = \neg \mathbf{E}\mathbf{X}(\neg f) AX ( f ) = ¬ EX ( ¬ f ) E F ( f ) = E ( 1 U f ) \mathbf{E}\mathbf{F}(f) = \mathbf{E}(1 \mathbf{U} f) EF ( f ) = E ( 1 U f ) A G ( f ) = ¬ E F ( ¬ f ) \mathbf{A}\mathbf{G}(f) = \neg \mathbf{E}\mathbf{F}(\neg f) AG ( f ) = ¬ EF ( ¬ f ) A F ( f ) = ¬ E G ( ¬ f ) \mathbf{A}\mathbf{F}(f) = \neg \mathbf{E}\mathbf{G}(\neg f) AF ( f ) = ¬ EG ( ¬ f ) A [ f U g ] = ¬ E [ ( ¬ g ) U ( ¬ f ∧ ¬ g ) ] ∧ ¬ E G ( ¬ g ) \mathbf{A}[f \mathbf{U} g] = \neg \mathbf{E}[(\neg g) \mathbf{U} (\neg f \wedge \neg g)] \wedge \neg \mathbf{E}\mathbf{G}(\neg g) A [ f U g ] = ¬ E [( ¬ g ) U ( ¬ f ∧ ¬ g )] ∧ ¬ EG ( ¬ g ) A [ f R g ] = ¬ E [ ( ¬ f ) U ( ¬ g ) ] \mathbf{A}[f \mathbf{R} g] = \neg \mathbf{E}[(\neg f) \mathbf{U} (\neg g)] A [ f R g ] = ¬ E [( ¬ f ) U ( ¬ g )] E [ f R g ] = ¬ A [ ( ¬ f ) U ( ¬ g ) ] \mathbf{E}[f \mathbf{R} g] = \neg \mathbf{A}[(\neg f) \mathbf{U} (\neg g)] E [ f R g ] = ¬ A [( ¬ f ) U ( ¬ g )] 下面我们来看一些例子，令 P P P Q Q Q
A G . P \mathbf{A}\mathbf{G}.P AG . P E F . P \mathbf{E}\mathbf{F}.P EF . P A F . E G . P \mathbf{A}\mathbf{F}.\mathbf{E}\mathbf{G}.P AF . EG . P E G . A F . P \mathbf{E}\mathbf{G}.\mathbf{A}\mathbf{F}.P EG . AF . P E \mathbf{E} E G \mathbf{G} G A F \mathbf{A}\mathbf{F} AF A ( P U Q ) \mathbf{A}(P \mathbf{U} Q) A ( P U Q ) E ( ( E X . P ) U ( A G . Q ) ) \mathbf{E}((\mathbf{E}\mathbf{X}.P)\mathbf{U}(\mathbf{A}\mathbf{G}.Q)) E (( EX . P ) U ( AG . Q )) A G . Q \mathbf{A}\mathbf{G}.Q AG . Q E X . P \mathbf{E}\mathbf{X}.P EX . P 安全性（safety）：坏事情不会发生 典型例子：A G ( r e a c t o r _ t e m p < 1000 ) \mathbf{A}\mathbf{G}(\mathrm{reactor\_temp} < 1000) AG ( reactor_temp < 1000 ) 通常使用 A G \mathbf{A}\mathbf{G} AG 活跃度（liveness）：好事情会发生 典型例子：A F ( r i c h ) , A F ( x > 5 ) , A G ( s t a r t → A F t e r m i n a t e ) \mathbf{A}\mathbf{F}(\mathrm{rich}), \mathbf{A}\mathbf{F}(x > 5), \mathbf{A}\mathbf{G}(\mathrm{start} \to \mathbf{A}\mathbf{F}\ \mathrm{terminate}) AF ( rich ) , AF ( x > 5 ) , AG ( start → AF terminate ) 通常使用 A F \mathbf{A}\mathbf{F} AF fairness：某件事情会无穷地经常（infinitely often）发生 典型例子：A G A F ( e n a b l e d ) \mathbf{A}\mathbf{G}\mathbf{A}\mathbf{F}(\mathrm{enabled}) AGAF ( enabled ) 通常使用 A G A F \mathbf{A}\mathbf{G}\mathbf{A}\mathbf{F} AGAF CTL 和 LTL 的表达能力是不可比的，实践中会根据应用场景和个人偏好来选择。
