Fair Preorder for Partial Fair Kripke Structures

IntroductionMany approaches have been proposed to dealwith the problem of model checking large statespaces,such as the composition methods,symbol-ic verification and abstraction techniques.A partialstate spaces model checking method was developedby Bruns[1] ,which explored just a part of statespaces,and those unexplored states and transitionswere often absent in incomplete or“partial”statespaces.In the automatic verification of concurrent fi-nite- state system,the branching time prepositiona…

Fair Preorder for Partial Fair Kripke Structures

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.