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

摘要：

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

关键词： 概率空间 定理证明 并发系统 形式化构造 归纳法 测度评估函数

作者: 王金双 张兴元 杨华兵 张毓森

作者单位: 解放军理工大学指挥自动化学院,江苏,南京,210007

会议类型: 国内会议

会议名称: 2008年全国理论计算机科学学术年会

会议地点: 西安

会议语种:中文

页码: 83-85

在线出版日期: 2008-09-19（万方平台首次上网日期，不代表论文的发表时间）