Abstract model checking: Difference between revisions

Revision as of 17:53, 26 January 2007

Revision as of 17:54, 26 January 2007

Line 6:

The real and the abstract state spaces are galois connected which means that if we take an element from the abstract space, concretize it and abstract the concretized version, the result will be equal to the original. On the other hand, if you pick an element from the real space, abstract it and concretize the abstract version, the final result will be a super set of the original. <br /> That is,

<math>\eta</math>(<math>\theta</math>(abstract)) = abstract but <br/>

<math>\theta</math>(<math>\eta</math>(real)) <math>\supset</math> real