状态转换系统和时间特性
在本章中, 我们将讨论状态变化系统 (State-Changing Systems) 以及它们的形式化: 状态转换系统 (Transition System).
状态变化系统指在各种动作的影响下随时间推移而运行并改变状态的系统, 而状态转换系统是状态变化系统的特殊形式化, 其中系统由一组变量表示, 状态由对这些变量的赋值组成.
我们将从对状态变换系统的讨论引入形式化它们的可行方法, 并通过举例解释状态转换系统中的核心概念: 状态 (State), 状态变量 (State Variable) 和状态转换 (Transition). 我们随后说明如何使用逻辑表示状态转换系统.
11.1 对状态转换系统的讨论
在之前的学习中, 我们已经掌握了谓词逻辑, 有限域上的谓词逻辑 (PLFD) 和量化布尔公式逻辑. 我们同时知道, 这些逻辑系统可以用来表示 静态 的应用场景, 也就是那些状态不随时间推移或动作发生而改变的场景中. 进一步地, 在我们需要讨论和研究更为普适的 动态 场景时, 我们就需要构造一些新的工具.
首先我们考虑收研究的对象: 状态转换系统. 一般地, 状态转换系统具备如下特征:
- 在特定的 时刻 (
Time Moment), 这样的系统会具备某个特定的 状态 (State). - 一般而言系统的状态会随着来自系统内部或源自外部环境的 行为/动作 (
Action) 的发生而变化.
为了对这样的系统进行数学建模, 我们需要进行下列的 抽象化:
- 我们通过引入 变量 描述系统中部分参数的特征, 并假设我们通过某些变量的值来识别 (区分) 不同的状态. 我们称这些可用来区分状态的变量为 状态变量 (
State Variables). - 对 行为/动作 的形式化是通过确定在执行这一行为/动作后, 系统中的哪些状态变量的值会发生变化而实现的. 我们称形式化的行为/动作为 转换 (
Transitions).
对于状态变化系统的形式化一般又包含两个阶段:
- 构造能够描述这个系统功能的形式化模型.
- 使用某种逻辑系统指定和检验系统的属性.
11.2 状态转换系统的核心概念
定义 11.2.1 (状态转换系统)
一个 状态转换系统 表示为一个五元组
\[\mathbb{S} = (S, \text{In}, T, \mathscr{X}, \text{dom}, L),\]其中
- 有限非空集合 $S$ 包含系统中的所有可能状态, 称为 系统 $\mathbb{S}$ 的状态集.
- $\text{In}$ 为 $S$ 的真子集, 称为 系统 $\mathbb{S}$ 的初始状态集.
- $T \in S \times S$ 称为 $\mathbb{S}$ 的转换关系集.
- $\mathscr{X}$ 由系统中的状态变量组成, 也是有限非空集合.
- $\text{dom}$ 为一个从 $\mathscr{X}$ 的映射, 对于任一个状态变量 $x \in \mathscr{X}$, $\text{dom}(x)$ 为一个非空集合, 称为 $x$ 的定义域.
- $L$ 为 $\mathbb{S}$ 的标记函数.
称状态转换系统 $\mathbb{S}$ 为 有限 的, 若对每个状态变量 $x$, 其定义域 $\text{dom}(x)$ 也是有限的, 我们只考虑有限的状态转换系统.
注意对系统 $\mathbb{S} = (S, \text{In}, T, \mathscr{X}, \text{dom}, L)$ 而言, 它的变量集 $\mathscr{X}$ 和映射 $\text{dom}$ 实际上定义了一个 PLFD 实例. 记这个 PLFD 实例的所有解释为 $\mathbb{I}$, 标记函数 $L$ 就可被定义为 $L: S \rightarrow \mathbb{I}$, 也就是说标记函数 将每个状态都映射到一个解释上. 这意味着:
- 对任何变量 $x \in \mathscr{X}$ 和任意状态 $s \in S$, 有 $L(s)(x) \in \text{dom}(x)$.
- 对任何这个
PLFD实例中的公式 $A$, 以及任意状态 $s \in S$, 我们有: $L(s) \vDash A$ 或 $L(s) \nvDash A$.
我们进一步引入下述的两种简化表述:
- 若 $L(s)(x)=v$, 称 变量 $x$ 在状态 $s$ 下的值为 $v$, 并将值 $v$ 表示为 $s(x)$.
- 若 $L(s) \vDash A$, 则称 $s$ 满足 $A$ 或 $A$ 在状态 $s$ 下为真, 记为 $s \vDash A$.
举例而言, 若 $s(x)=v$, 则 $s \vDash x=v$.
我们还可以用 状态转换图 表示状态转换系统:
定义 11.2.2 (状态转换图)
考虑状态转换系统
\[\mathbb{S} = (S, \text{In}, T, \mathscr{X}, \text{dom}, L).\]它的 状态转换图 为一个以 $S$ 为节点集, 以 $T$ 为边集的有向图. 此外, 图中的每个节点 $s$ 都被解释 $L(s)$ 标记.
定义 11.2.3 (可应用性, 确定性和非确定性)
称转换 $t$ 在状态 $s$ 上为 可应用的, 若存在新状态 $s‘$ 满足 $(s, s’) \in t$. 称转换 $t$ 为 确定的, 若对任何状态 $s$, 存在最多一个状态 $s’$, 满足 $(s, s’) \in t$. 反之, 称这个转换为 非确定的.
$\mathbb{S}$ 的 转换关系 记为 $T_{r_{\mathbb{S}}}$, 就是状态系统中所有转换的并.
称状态转换系统 $\mathbb{S}$ 为 有限 的, 若它的状态集为有限的, 反之称其为 无限 的.
11.3 状态转换系统的符号化表示
在本节中我们引入状态转换系统的符号化表示.
定义 11.3.1 (状态集的符号化表示)
考虑状态转换系统 $\mathbb{S}$, 记 $\mathscr{L}(\mathbb{S})$ 为满足下列性质的
PLFD实例:
- $\mathscr{L}(\mathbb{S})$ 的变量集就是 $\mathbb{S}$ 的变量集 $\mathscr{X}$.
- $\mathscr{L}(\mathbb{S})$ 的域映射就是 $\mathbb{S}$ 的域映射 $\text{dom}$.
称 $\mathscr{L}(\mathbb{S})$ 中的公式 $F$ 符号化表示了一系列状态 $S$, 若
\[S = \{s \vert s \vDash F\}.\]和 状态 一样, 转换 也可以被符号化表示. 由于转换是由 一对状态 组成的, 要表示状态, 就需要构造出能够表示两个连续的状态的语法.
我们使用两个变量集合表示转换, 它们分别存储当前态 (Current State) 和下一态 (Next State). 对任何变量集 $\mathscr{X}$ 中的变量 $x$, 在下一态中则被表示为 $x’$.
对状态转换系统
\[\mathbb{S} = (S, \text{In}, T, \mathscr{X}, \text{dom}, L)\]记 $\mathscr{X’}$ 为:
\[\mathscr{X'} \overset{\text{def}}{=} \{x' \vert x \in \mathscr{X}\}.\]同时定义 $\mathscr{L’}(\mathbb{S}) = \mathscr{X} \cup \mathscr{X’}.$
定义 11.3.2 (转换的符号化表示)
称 $\mathscr{L’}(\mathbb{S})$ 中的公式 $F$ 符号化表示转换 $t$, 若:
\[t = \{(s, s') \vert (s, s') \vDash F\}.\]
定理 11.3.1
令 $t_1, \cdots, t_n$ 为 $\mathbb{S}$ 中的全体转换, $F_1, \cdots, F_n$ 分别是这些转换的符号化表示. 则公式
\(F_1 \vee F_2 \vee \cdots \vee F_n\) 即是 $\mathscr{S}$ 转换关系的符号化表示.
定义 11.3.3 (状态转换系统的符号化表示)
考虑状态转换系统
\[\mathbb{S} = (S, \text{In}, T, \mathscr{X}, \text{dom}, L)\]称一对分别属于逻辑 $\mathscr{L}(\mathbb{S}), \mathscr{L’}(\mathbb{S})$ 的公式 $F, F’$ 是 $\mathbb{S}$ 的符号化表示, 若 $F$ 为初始状态集 $\text{In}$ 的符号化表示, 且 $F’$ 为 $\mathbb{S}$ 的状态转换关系 $T_{r_{\mathbb{S}}}$ 的符号化表示.
