上海交通大学学报(英文版)
上海交通大學學報(英文版)
상해교통대학학보(영문판)
JOURNAL OF SHANGHAL JIAOTONG UNIVERSITY
2003年
1期
15-18
,共4页
fairness%Kripke structure%computation-tree logic(CTL)
This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Krip-ke structures were used for partial state spaces model checking, which is a new technique to solve problems of stateexplosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Krip-ke structure, and a 3-valued fair CTL(Computation-Tree Logic) semantics correspondingly. It defines a fair pre-order between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a perti-nent theorem is also given, which indicates the relationship between the partial state spaces and the more completeone by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae.
