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

买宁 等: 高铁复合无线通信信道形式化建模与验证 2959

分形式描述, 即保证了公式 (3) 成立.

∫
µ(A) = Af(x)dλ(x) (3)
公式 (3) 描述了概率测度和 Lebesgue 测度间的关系. 假设 µ 是随机变量 A 的概率测度, λ 代表 Lebesgue 测度,
则 f(x) 就是随机变量的概率密度函数, 它是概率测度 µ 对 Lebesgue 测度 λ 的 RN 导数.
依据公式 (3) 对 RN 导数进行形式化建模, 需要先建模概率测度 µ, 如定义 9 所示. 基于定义 9, 形式化建模
RN 导数, 如定义 10 所示.
定义 9. Lebesgue 测度的密度测度.

⊢ density_measure m f = (\s. pos_fn_integral m (\x. extreal_mul (f x) (indicator_fn_ext s x)))
定义 10. RN 导数.
⊢ RN_deriv v m =
(@f. f IN gen_measurable (m_space_ext m, measurable_sets_ext m) borel_ext
/\ (!x. extreal_le (extreal_of_num 0) (f x))
/\ (!s. s IN measurable_sets_ext m ==> density_measure m f s = v s))
定义 9 中, “extreal_mul”表示扩展实数的“ × ”运算符, “indicator_fn_ext”定义了扩展实数的指数函数. 定义 10
中, “extreal_of_num”用于将自然数转换为扩展实数, 通过这种转换操作确保变量类型的严格一致性, 从而避免类
型不一致导致的潜在错误.
对于连续型随机变量, 通常使用 Lebesgue 测度来描述其定义的函数测度空间. 本文使用 Lebesgue-Borel 测度,
同时基于 Radon-Nikodym 定理, 将概率密度函数形式化为概率测度相对于 Lebesgue-Borel 测度的 RN 导数, 如定
义 11 所示.
定义 11. 概率密度函数.
⊢ !p X. PDF p X = RN_deriv (distribution_ext p X) lborel
正态随机变量作为概率论中最重要的分布之一, 其在理论分析与实际应用中被广泛使用. 以正态分布为基础
的高斯信道模型, 常用于复合信道模型的建模. 在构建正态随机变量形式化模型时, 先形式化建模正态概率测度,
定义 12 给出了正态分布在特定可测集上的概率测度.
定义 12. 正态概率测度.
⊢ !mu sigma A. normal_pmeasure mu sigma A =
(if A IN measurable_sets_ext lborel then
pos_fn_integral lborel (\x. extreal_mul (Normal (normal_density mu sigma (drop x))) (indicator_fn_ext A x))
else extreal_of_num 0)
定义 12 通过积分表示正态分布的概率测度, 如果 A 是可测集, 则根据正态分布的密度函数进行积分, 否则概率
测度值为 0. 其中, “measurable_sets_ext”表示扩展实数上的可测集合, “normal_density”表示正态分布的概率密度函数.
正态随机变量可描述为与正态测度保持一致的随机变量, 其形式化模型如定义 13 所示.
定义 13. 正态随机变量.
⊢ !p X mu sigma.

normal_rv X p mu sigma <=>
random_variable_ext X p real_borel /\ measurable_distr p X = normal_pmeasure mu sigma
在定义 13 中, 给出了正态随机变量的定义条件: X 必须是定义在某个概率空间 p 上的随机变量, 且其取值空

间是实数集上的 Borel-σ 代数, X 的概率分布必须满足正态分布.
4 信息论基础形式化

本文依据高铁无线通信信道模型形式化建模的需要, 对信息论基础构建高阶逻辑模型. 信息论中的核心概念包