Abstraction Model Checking
   HOME

TheInfoList



Click Here for Items Related To - Abstraction Model Checking
OR:
Abstraction Model Checking on:   [Wikipedia]   [Google]   [Amazon]

In
computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
and in
mathematics Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
, abstraction model checking is a form of
model checking In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software syst ...
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 may refer to: Computer science * Variable (computer science), a symbolic name associated with a value and whose associated value may be changed Mathematics * Variable (mathematics), a symbol that represents a quantity in a mathemat ...
are partitioned into visible and invisible depending on their change of values. The real
state space In computer science, a state space is a discrete space representing the set of all possible configurations of a system. It is a useful abstraction for reasoning about the behavior of a given system and is widely used in the fields of artificial ...
is summarized into a smaller set of the visible ones.


Galois connected

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. That is, \eta(\theta(abstract)) = abstract
\theta(\eta(real)) \supseteq real


See also


References

* {{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 Model checking