Abstract model checking: Difference between revisions

Revision as of 15:12, 11 December 2021

Latest revision as of 06:36, 31 May 2024

(4 intermediate revisions by 4 users not shown)

Line 1:

In [[computer science]] and in [[mathematics]], '''abstraction model checking''' is a form of [[model checking]] 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 [[Variable (mathematics)|variables]] 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==

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,

Line 24:

==References==

{{Reflist}}

* {{cite journal | author=Edmund M. Clarke and Orna Grumberg and David E. Long | title=Model checking and abstraction | journal=ACM Transactions on Programming Languages and Systems| year=1994| volume=16 | issue=5 | pages=1512–1542 | doi=10.1145/186025.186051| citeseerx=10.1.1.79.3022 | s2cid=207884170 }}

[[Category:Model checking]]

{{Improve categories|date=December 2021}}