Abstract model checking: Difference between revisions

Revision as of 15:13, 11 December 2021

Revision as of 13:54, 23 December 2022

Line 4:

==Galois connected==

The real and the abstract state spaces are [[Galois connection|Galois connected]]. This 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.

That is,