Editing Model checking (section)

== Techniques ==
Model-checking tools face a combinatorial blow up of the state-space, commonly known as the [[state explosion problem]], that must be addressed to solve most real-world problems.  There are several approaches to combat this problem.

# Symbolic algorithms avoid ever explicitly constructing the graph for the FSM; instead, they represent the graph implicitly using a formula in quantified propositional logic.  The use of binary decision diagrams (BDDs) was made popular by the work of Ken McMillan,<ref>* ''Symbolic Model Checking'', Kenneth L. McMillan, Kluwer, {{ISBN|0-7923-9380-5}}, [http://www.kenmcmil.com/thesis.html also online] {{Webarchive|url=https://web.archive.org/web/20070602185228/http://www.kenmcmil.com/thesis.html |date=2007-06-02 }}.</ref> as well as of Olivier Coudert and Jean-Christophe Madre,<ref>{{Cite book |last1=Coudert |first1=O. |last2=Madre |first2=J.C. |chapter=A unified framework for the formal verification of sequential circuits |date=1990 |title=1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers |chapter-url=https://oliviercoudert.files.wordpress.com/2020/11/iccad90.pdf |publisher=IEEE Comput. Soc. Press |pages=126–129 |doi=10.1109/ICCAD.1990.129859 |isbn=978-0-8186-2055-3}}</ref> and the development of open-source BDD manipulation libraries such as CUDD<ref>{{cite web |url=https://www.cs.rice.edu/~lm30/RSynth/CUDD/cudd/doc/ |title=CUDD: CU Decision Diagram Package }}</ref> and BuDDy.<ref>{{cite web |url=http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.itu.dk/research/buddy/ |title=BuDDy – A Binary Decision Diagram Package}}</ref>
# Bounded model-checking algorithms unroll the FSM for a fixed number of steps, <math>k</math>, and check whether a property violation can occur in <math>k</math> or fewer steps. This typically involves encoding the restricted model as an instance of [[Boolean satisfiability problem|SAT]]. The process can be repeated with larger and larger values of <math>k</math> until all possible violations have been ruled out (cf. [[Iterative deepening depth-first search]]).
# [[abstract interpretation|Abstraction]] attempts to prove properties of a system by first simplifying it.  The simplified system usually does not satisfy exactly the same properties as the original one so that a process of refinement may be necessary. Generally, one requires the abstraction to be ''sound'' (the properties proved on the abstraction are true of the original system); however, sometimes the abstraction is not ''complete'' (not all true properties of the original system are true of the abstraction). An example of abstraction is to ignore the values of non-Boolean variables and to only consider Boolean variables and the control flow of the program; such an abstraction, though it may appear coarse, may, in fact, be sufficient to prove e.g. properties of [[mutual exclusion]].
# Counterexample-guided abstraction refinement (CEGAR) begins checking with a coarse (i.e. imprecise) abstraction and iteratively refines it. When a violation (i.e. [[counterexample]]) is found, the tool analyzes it for feasibility (i.e., is the violation genuine or the result of an incomplete abstraction?). If the violation is feasible, it is reported to the user. If it is not, the proof of infeasibility is used to refine the abstraction and checking begins again.<ref name=Clarke2000>{{citation
 | last1 = Clarke | first1 = Edmund
 | last2 = Grumberg | first2 = Orna
 | last3 = Jha | first3 = Somesh
 | last4 = Lu | first4 = Yuan
 | last5 = Veith | first5 = Helmut
 | title = Computer Aided Verification
 | chapter = Counterexample-Guided Abstraction Refinement
 | year = 2000
 | volume = 1855
 | pages = 154–169
 | doi = 10.1007/10722167_15
| series = Lecture Notes in Computer Science
 | isbn = 978-3-540-67770-3
 | url = http://www.aladdin.cs.cmu.edu/papers/pdfs/y2000/counterex.pdf
 | doi-access = free
 }}</ref>

Model-checking tools were initially developed to reason about the logical correctness of [[Discrete system|discrete state]] systems, but have since been extended to deal with real-time and limited forms of [[hybrid system]]s.