Refinemant verification of fair transition systems can contribute to PLTL model checking

We present a verification approach of dynamic properties under fairness assumptions by PLTL model checking over finite state reactive systems. The systems that we want to verify are specified through a top-down refinement process. They interact with an environment, which is described partly by fairness assumptions. We give a definition of the refinement under fairness assumptions and show how the verification of the refinement can be used as a preprocessor for the verification of the properties under fairness assumptions at the refined level. Indeed, the refinement verification distinguishes the fair executions. So, the verification of a PLTL property P can be model-checked only on the fair executions that are noticed during the refinement verification. We present how to adapt the standard PLTL model checking algorithm to the model which results from the refinement verification