并发系统概率空间的形式化构造方法

• 作者: 张兴元 张毓森 杨华兵 王金双
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 概率空间 Isabelie/HOL/Isar 定理证明
• 年，卷（期）: 2008,（11）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 83-85
• 页数: 3页
• 分类号: TP309
• 字数: 2587字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2008.11.026

摘要

本文用Paulson归纳法描述并发系统,对系统执行的不确定性进行建模,给出了一种适合定义测度的产生集合,利用测度评估函数将产生集合的测度与有限执行序列的测度联系起来;证明执行序列集合上的测度满足非负性和可列可加性,利用测度扩张定理构造并发系统执行序列集合上的概率空间.所有证明脚本经过定理证明工具Isabelle/HOL/Isar的检查.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张毓森	解放军理工大学指挥自动化学院	66	580	12.0	22.0
2	张兴元	解放军理工大学指挥自动化学院	14	20	2.0	3.0
3	王金双	解放军理工大学指挥自动化学院	23	189	4.0	13.0
4	杨华兵	解放军理工大学指挥自动化学院	6	16	3.0	3.0