Abstract model checking: Difference between revisions

Revision as of 22:32, 23 April 2007

Revision as of 05:56, 22 May 2007

Line 4:

'''Abstraction Model checking''' is for systems where an actual representation is too complex in developing the model alone. So, the design undergoes a kind of translation to scaled down "abstract" version.

The set of variables[[variable]]s are partitioned into visible and invisible depending on their change of values. The real state space is summarized into a smaller set of the visible ones.

==Galois connected==