用基于流事件结构的偏序时序逻辑刻画并发系统多诱因特征

• 作 者: 闫炜 吴尽昭 高新岩
• 机 构: 电子科技大学计算机科学与工程学院,中国科学院成都计算机应用研究所
• 出 处: 四川大学学报：工程科学版
• 发表日期: 2008年1期
• 关键词: 流事件结构 偏序时序逻辑 格局 公理系统 flow event structure partial order temporal logic confi
• 基金项目: 国家自然科学基金资助项目（60373113）,国家973计划资助项目（2004CB318000）

针对如何利用偏序时序逻辑刻画并发系统多诱因性的问题，提出了一种依赖流关系的流事件结构逻辑（FESL），作为多诱因特征的刻画语言。FESL以流事件结构作为框架模型，并且依据格局量词，建立了自己的公理系统。证明了FESL不仅能有效表达多诱因特性，而且还能描述涉及多个运行实例的特性；同时也证明了FESL的完备性、合理性以及可判定性。