Abstract model checking
In computer science and in mathematics, 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 real and the abstract state spaces are 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.
((abstract)) = abstract
- Edmund M. Clarke and Orna Grumberg and David E. Long (1994). "Model checking and abstraction". ACM Transactions on Programming Languages and Systems. 16 (5): 1512–1542. CiteSeerX 10.1.1.79.3022. doi:10.1145/186025.186051.
This article needs additional or more specific categories. (December 2021)