Simulation Based Model Checking

Formal verification is a process in which mathematical techniques are used to guaran-tee the correctness of a design with respect to some specified behavior. Automated formal-verification tools based on model-checking technology, have enjoyed a substantial and grow-ing use over the last few years, showing an ability to discover subtle ?aws that result fromextremely improbable events. It is fair to say that automated verification is one of the mostsuccessful applications of automated reasoning in computer science.The automata theoretic approach offers a uniform algorithmic framework for modelchecking linear time properties. The standard approach to linear temporal logic modelchecking consists of translating the negation of a given linear temporal logic formula intoa Büchi automaton, and checking the product of the property automaton and the model oflanguage emptiness. The quality of the translation affects the resources required by themodel checking experiment. This motivates the search for algorithms that generate efficientautomata, i.e.. automata with few states, few transitions ,and simple acceptance conditions.An automaton A can replace another automaton A in model checking if A and A ac-cept the same language. Since checking language equivalence is in general hard, practicalapproaches resort to various notions of simulations that account for the acceptance condi-tions of the automata. Simulation is a stronger notion than language containment becausethe simulating automaton cannot look ahead the moves of the simulated one. On the otherhand, several variants of simulation relations can be computed in polynomial time; amongthem, direct simulation, fair simulation, and delayed simulation. K-simulation, where 1-simulation corresponds to ordinary simulation and its variants for Büchi automata, and K-simulations, for K > 1, generalize the game definition of 1-simulation by allowing theprotagonist to use K pebbles instead of 1 (to"hedge its bets") in response to the antag-onist's move of a single pebble.Based K-simulation we can get more potential reduction in automaton size. We are suggesting an approximate minimization algorithm for Büchiautomata based on K-simulation.Translation of linear temporal logic to Büchi automata results naturally in generalizedBüchi automata,that is, Büchi automata with multiple acceptance sets. A generalized Büchiautomaton with l acceptance conditions and n states can be easily converted to a simpleBüchi automaton with nl states (and one acceptance condition). Thus, it is extremely im-portant to be able to further minimize generalized Büchi automata without first convertingthem to simple Büchi automata. As a result we are suggesting an approximate minimizationalgorithm for direct/fair/delayed simulation.The left and right languages belong to the automata theoretic part of the reduction prob-lem. The left (resp. right) language is the set of calculations leading to (resp. starting from)a state. K-simulations enable a fast detection of these trace inclusions. we are suggestingan approximate minimization algorithm for Kripke structure, Büchi and generalized Büchiautomata based on left and right languages.An obvious method for trying to avoid the state explosion problem is to use the nat-ural decomposition of the system. The goal is verify properties of individual components,infer that these hold in the complete system, and use them to deduce additional proper-ties of the system. When verifying properties of the components, it may also be necessaryto make assumption about the environment. This is approach is exemplified by Pnueli'sassume-guarantee paradigm. The real bottleneck of this framework is checking for simula-tion between models, thus replacing the exists simulation by the fair simulation reduces thiscomplexity to polynomial and eliminates the bottleneck of the framework.In spite of the impressive progress in the development of model checking, it is stilllimited in their ability to handle large systems. It is generally recognized that abstractiontechniques are one of the most general state reduction techniques. A novel efficient algo-rithm for computing abstraction of Kripke structure based on K-simulation is proposed. Thesoundness and completeness of abstraction framework in Linear temporal logic are proved.