Page 271 - 《软件学报》2026年第7期

2956 软件学报 2026 年第 37 卷第 7 期

灵活性高和可扩展性强的特点. HOL 系列是目前主流的定理证明器之一, 其主要分支有 HOL4 和 HOL Light. HOL4
继承了早期的 HOL 系统并在其基础上进行了扩展和改进, 旨在提供全面的定理证明器. HOL Light 虽然也继承于
HOL 系统, 但其更轻量级, 灵活性更高, 核心设立得较小巧. 其易用性和可用性高于 HOL4, 更适用于科学研究. 尤
其是针对特定的理论研究项目, HOL Light 为用户提供了一个可根据具体需求定制与开发的灵活环境, 其常用特
殊符号及标准含义如表 1 所示. 因此, 本研究使用 HOL Light 来进行高铁复合无线通信信道的形式化建模与验证,
并构建所需的扩展实数数学基础与信息论基础.

表 1 HOL Light 符号表

HOL Light符号 标准符号 含义
| 或 逻辑或
/\ 与 逻辑与
-> → 函数类型映射
! ∀ 对任意的
? ∃ 存在
\x. f(x) λx. f(x) 定义以 x 为自变量的函数
==> ⇒ 蕴含
<=> ⇔ 等价于
@l.P(l) l 从所有使 P(l) 的 l 中选择一个 l
&x x 从自然数到实数的类型转换
-- − 负号
INTER ∩ 交集
IMAGE f s range( f) 函数值域
PREIMAGE f s domain( f) 函数定义域
power2 x 2 平方
1
drop real → real 一维向量投影标量
at_posinfinity +∞ 正无穷

2.2 高架桥场景下高铁复合无线通信信道模型
高架桥场景作为高铁通信最常见的场景之一, 其信道建模与计算较为简便. 在高架桥场景中, 高铁顶部一般
设置有天线, 将信号从基站直接至用户设备这一路径抽象为无线信道 h 1 , 将基站发出信号经天线转发至用户设备
这一路径抽象为无线信道 h 2 . 假定信道 h 1 和 h 2 都服从小尺度衰落信道瑞利信道的分布函数, 令复合信道 h =
c×h 1 ×h 2 , 对复合信道 h 及其特性进行建模与验证.
在这种情况下, 复合信道的概率密度函数如公式 (1) 所示, 其符合第 2 类修正 Bessel 函数 K 0 分布. 与瑞利分
布相比, K 0 分布表现出更强的不对称性, 而非瑞利分布那样平稳衰减. K 0 分布尾部衰减更缓慢, 即复合信道具有长
尾分布的特性. 这种分布特性在高铁无线通信系统的设计和优化中具有重要意义. 通过准确的信道建模, 可以提升
系统设计的可靠性与鲁棒性. 例如, 在信道估计和解码算法的优化中, 考虑长尾分布的特性能够提高误码率性能 [3] .
在高铁场景的站点规划中, 需结合长尾特性计算站点的有效覆盖范围, 以确保列车高速移动时通信连接的连续性
与可靠性.

( )
2h |h|
p(h) = K 0 , h , 0, c = 1 (1)
σ σ 2 σ σ 2
2
2
1 2 1 2
为完成复合信道的建模, 需要对信道模型、衰落信道等信息论基础概念进行形式化建模. 这些概念的形式化
建模依赖于一系列数学基础的定义. 因此, 本文首先基于扩展实数对测度、积分、概率等相关内容进行建模, 以确
保数学基础能够处理复杂条件与极限情况. 基于此, 本文进一步形式化建模信源、信道、互信息等信息论基础的
核心概念. 最后, 基于衰落信道模型, 进行了高铁复合无线通信信道的建模, 并验证复合信道的概率密度函数符合
K 0 分布.