Abstract model checking: Difference between revisions

Revision as of 17:47, 26 January 2007

Revision as of 17:51, 26 January 2007

Line 1:

{{categorize}}

Abstraction Model checking is for systems where an actual representation is too complex and and a state space explosion will result in developing the model alone. So, the design undergoes a kind of translation to scaled down "abstract" version. <br />

The set of variables are partitioned into visible and invisible depending on their visible change ( change of values, for instance) and. theThe real state space is summarized into a smaller set of the visible ones.

==Galois connected==

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 />

==References==