乐观合同签订协议的模型检测分析

摘要：

从ECSl协议和PFH协议出发,研究三轮乐观合同签订协议的结构.利用协议动作序列及条件图建立协议模型,分析三轮协议满足有限性的条件.在此基础上,结合模型检测工具SPIN,对满足有限性的协议结构的公平性进行分析、验证,并给出反例,说明三轮协议不可能同时满足有限性和公平性.

关键词：合同签订协议、乐观、模型检测、公平性、有限性

所属期刊栏目：37

分类号：TP309.2(计算技术、计算机技术)

资助基金：国家"973"计划基金资助项目2009CB320701;广东省科技计划基金资助项目2007B010400068

在线出版日期：2011-07-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：142-144,147