标号转移系统

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

标号转移系统写作

$$\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以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。的中心。本页只建立产生这些行为的局部转移结构。

若同一对 $(s,a)$ 有多个可能后继，系统对动作 $a$ 非确定。非确定性表示模型允许多种行为，不等于实现随机选择；若需要概率，必须给每个状态—动作对规定概率分布。

自动门的状态轨迹 ​

考虑自动门的状态

$$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$ 转移。允许在可见动作前后插入内部闭包，便得到弱转移；但是否使用这种约定必须写明。一步模拟与弱模拟的差别正取决于它们匹配的是原始转移还是这种闭包。

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

终止、死锁与全转移化 ​

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

若时序语义只接受无限路径，常给终止状态增加一个带 stutter 标签的自环，使转移关系 total。这个技术变换会改变含 next 算子的公式如何观察终止，因此必须显式说明，不能把“补自环”当作无语义影响的格式整理。

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。