Revision as of 10:20, 20 November 2007 edit Hans Adler (talk \| contribs) Autopatrolled, Extended confirmed users, Pending changes reviewers, Rollbackers 26,943 edits rm from category "model theory", as it's already in subcategory "model checking" and is a bit exotic there ← Previous edit		Revision as of 01:36, 7 February 2008 edit undo 70.233.136.36 (talk) →Galois connected: Added link to article on Galois Connection. Cleaned up sentence structure. Next edit →
Line 5: ==Galois connected== The real and the abstract state spaces are ~~galois~~[[Galois connection\|Galois connected]]. ~~which~~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, <math>\eta</math>(<math>\theta</math>(abstract)) = abstract <br/> <math>\theta</math>(<math>\eta</math>(real)) <math>\supset</math> real ==Abstraction refinement loop==

Abstract model checking: Difference between revisions