Fair Preorder for Partial Fair Kripke Structures  

作　　者：徐蔚文 陆鑫达 

机构地区：[1]Dept. of Computer Science and Eng., Shanghai Jiaotong Univ.

出　　处：《Journal of Shanghai Jiaotong university(Science)》2003年第1期15-18,共4页上海交通大学学报（英文版）

基　　金：National Natural Science Foundation of China( No.60 173 10 3 )

摘　　要：This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of state explosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Kripke structure, and a 3 valued fair CTL(Computation Tree Logic) semantics correspondingly. It defines a fair preorder between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a pertinent theorem is also given, which indicates the relationship between the partial state spaces and the more complete one by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae.This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of state explosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Kripke structure, and a 3 valued fair CTL(Computation Tree Logic) semantics correspondingly. It defines a fair preorder between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a pertinent theorem is also given, which indicates the relationship between the partial state spaces and the more complete one by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae.

关 键 词：FAIRNESS Kripke structure computation  tree logic(CTL) 

分 类 号：TU311.4[建筑科学—结构工程] TU317.1