标号转移系统

形式陈述 ​

从无标号状态到动作转移 ​

标号转移系统写作

$$\mathcal{L}=(S,I,A,⟶),⟶\subseteq S\times A\times S,$$

其中 $S$ 是状态集合，$I\subseteq S$ 是初始状态集合，$A$ 是动作标签集合，三元关系公理库关系Relation · Binary relation带源集与目标集的二元关系，其底层关系图是 A×B 的子集。记录允许的一步行为。若 $(s,a,s^{\prime })\in ⟶$，记作 $s\stackrel{a}{\to }{s}^{\prime }$，读作系统在状态 $s$ 执行动作 $a$ 后可以到达 $s^{\prime }$。

状态机公理库状态机State machine · Transition system用状态集合、初始状态和转移关系描述系统可能执行轨迹的模型。已经给出无标号骨架 $(S,I,\to )$。忘掉动作标签，即令

$$s\to s^{\prime }⟺\mathrm{\exists }a\in A,s\stackrel{a}{\to }{s}^{\prime },$$

便得到它的无标号投影。LTS 的新增信息是“哪一种动作导致了这一步”，不是另造一套与状态机平行的可达性概念。

标签只需是可比较的符号，可以表示程序指令、消息收发、接口调用或环境事件。时间长度、概率与输入输出值若要进入模型，必须由更丰富的标签结构或额外成分明确加入，不能从一个动作名称自动推断。

路径、使能与可达性 ​

有限路径是交替序列

$$s_0\stackrel{a_0}{\to }{s}_1\stackrel{a_1}{\to }\cdots \stackrel{a_{n-1}}{\to }{s}_n,$$

其中 $s_0\in I$ 且每个标出的三元组都属于转移关系。无限路径没有最后状态。状态 $s$ 可达，若某条从初始状态出发的有限路径以 $s$ 结束；动作 $a$ 在 $s$ 处使能，若存在 $s^{\prime }$ 使 $s\stackrel{a}{\to }{s}^{\prime }$。

路径保留每一步前后的内部状态与动作。只抽取动作串 $a_0{a}_1\cdots$ 得到 trace，但隐藏动作和状态标记会怎样投影，属于轨迹与路径语义公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。的中心。本页只建立产生这些行为的局部转移结构。

局部转移的两个维度不能混为一谈。动作确定性要求

$$\mathrm{\forall }s,a,|\{s^{\prime }:s\stackrel{a}{\to }{s}^{\prime }\}|\le 1,$$

若指定输入动作子集 $A_{in}\subseteq A$，输入使能性要求

$$\mathrm{\forall }s,a\in A_{in},\mathrm{\exists }{s}^{\prime },s\stackrel{a}{\to }{s}^{\prime }.$$

前者限制同一状态—动作对至多一个后继，后者要求每个环境输入至少有一个响应。因此动作确定的系统仍可能拒绝输入，输入使能系统也可能因同一输入拥有多个后继而非确定。非确定性只表示模型允许多种行为，不代表随机选择；概率语义还需为后继规定分布。

直觉

自动门的状态轨迹 ​

考虑自动门的状态

$$S=\{\mathtt{closed},\mathtt{opening},\mathtt{open},\mathtt{closing}\},$$

初始状态为 closed。动作 detect 使门从 closed 到 opening，finish-open 使其到 open，timeout 使其到 closing，finish-close 使其回到 closed。一条完整路径是

$$\mathtt{closed}\stackrel{detect}{\to }\mathtt{opening}\stackrel{finish\text{-}open}{\to }\mathtt{open}\stackrel{timeout}{\to }\mathtt{closing}\stackrel{finish\text{-}close}{\to }\mathtt{closed}.$$

若关闭过程中再次 detect，可以加入 closing 到 opening 的转移。模型随后允许两种到达 opening 的历史，但当前状态只保留未来行为所需的信息；如果反向开门速度还依赖已关闭的比例，这个比例也必须进入状态。

该模型能准确回答某动作是否可执行以及什么状态可达，却没有给每个动作持续多久，也没有证明传感器输入会到来。把现实假设遗漏在状态和转移之外，再详尽地枚举图也不能补回它们。

例子与边界

内部动作与弱观察 ​

常用特殊标签 $\tau$ 表示外部观察者看不见的内部步骤。例如请求到达后，服务可以先做缓存查询 $\tau$，再发出 reply。路径中仍记录 $\tau$，对外 trace 可以把它删除。

用 $s\stackrel{\tau }{\Rightarrow }{s}^{\prime }$ 表示零步或多步 $\tau$ 转移。对可见动作 $a\ne \tau$，弱转移定义为

$$s\stackrel{a}{\Rightarrow }{s}^{\prime }⟺\mathrm{\exists }u,v:s\stackrel{\tau }{\Rightarrow }u\stackrel{a}{\to }v\stackrel{\tau }{\Rightarrow }{s}^{\prime }.$$

因此 $s\stackrel{\tau }{\to }u\stackrel{reply}{\to }v\stackrel{\tau }{\to }{s}^{\prime }$ 不是原始的一步 reply，却是一个弱 reply。零步闭包还使 $s\stackrel{\tau }{\Rightarrow }s$ 恒成立。一步模拟匹配原始边，弱模拟匹配上述闭包；若不声明采用哪一种，等价结论没有确定含义。

隐藏也会制造新的非确定性：两条内部路径投影后可能拥有同一可见动作序列，却在以后允许不同响应。由此可见，动作 trace 一般比完整路径遗忘更多分支结构。

推论与应用

终止、死锁与全转移化 ​

没有任何出边的状态在图论上是 terminal state。它可能表示程序按规格正常结束，也可能表示系统仍有义务却无法继续的 deadlock；两者拥有相同的局部图形，差别来自规格和状态标记。

若时序语义只接受无限路径，常给终止状态增加带 stutter 标签的自环以使转移关系 total。该变换会改变含 next 算子的公式如何观察终止，不能当作无语义影响的格式整理。

图已 total 仍不自动保证进展。若 finish-close 从某时刻起持续使能，弱公平性就足以排除调度器永远不执行它；若反复到来的 detect 使 finish-close 只在无限多个间歇位置使能，弱公平性仍允许每次都错过，必须用强公平性才能排除这种调度。公平性只限制被量化的执行，不是协议正确性的默认替代；也可以由协议结构直接消除永远推迟关门的路径。

LTS 适合离散步骤。时间自动机会另行加入时钟、guard 与 reset；Petri 网则把资源和并发使能作为一等结构。给所有离散系统贴上 LTS 表示并不意味着这些扩展信息已经被保留。

参考资料

• Robin Milner, Communication and Concurrency, Prentice Hall, 1989, Chs. 2–4。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Ch. 2。
• Rocco De Nicola, “A Gentle Introduction to Process Algebras,” in Formal Methods for Performance Evaluation, Springer, 2007, §§2–3。