Editing Model checking (section)

== Symbolic model checking ==

Instead of enumerating reachable states one at a time, the state space can sometimes be traversed more efficiently by considering large numbers of states at a single step. When such state-space traversal is based on representations of a set of states and transition relations as logical formulas, [[binary decision diagrams]] (BDD) or other related data structures, the model-checking method is ''symbolic''.

Historically, the first symbolic methods used [[Binary decision diagram|BDDs]]. After the success of [[propositional satisfiability]] in solving the [[automated planning and scheduling|planning]] problem in [[artificial intelligence]] (see [[satplan]]) in 1996, the same approach was generalized to model checking for [[linear temporal logic]] (LTL): the planning problem corresponds to model checking for safety properties. This method is known as bounded model checking.<ref>{{Cite journal | last1 = Clarke | first1 = E. | last2 = Biere | first2 = A. | last3 = Raimi | first3 = R. | last4 = Zhu | first4 = Y. | journal = Formal Methods in System Design | volume = 19 | pages = 7–34 | year = 2001 | doi = 10.1023/A:1011276507260|title=Bounded Model Checking Using Satisfiability Solving| s2cid = 2484208 }}</ref> The success of [[Boolean satisfiability problem|Boolean satisfiability solvers]] in bounded model checking led to the widespread use of satisfiability solvers in symbolic model checking.<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | pages = 2021–2035 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking| s2cid = 10190144 }}</ref>

===Example===
One example of such a system requirement:  
''Between the time an elevator is called at a floor and the time it opens its doors at that floor, the elevator can arrive at that floor at most twice''. The authors of "Patterns in Property Specification for Finite-State Verification" translate this requirement into the following LTL formula:<ref name="Dwyer, Avrunin, Corbett" >{{Cite conference
  |first1=M.  |last1=Dwyer
  |first2=G.  |last2=Avrunin
  |first3=J.  |last3=Corbett
  |title = Patterns in Property Specification for Finite-State Verification
  |chapter=Patterns in property specifications for finite-state verification
 |conference = Proceedings of the 21st international conference on Software engineering
  |pages = 411–420
  |date = May 1999
  |doi=10.1145/302405.302672
 |isbn=1581130740
 |url = https://dl.acm.org/doi/pdf/10.1145/302405.302672
}}</ref>
:<math>\begin{align}\Box\Big((\texttt{call} \land \Diamond \texttt{open}) \to 
& \big((\lnot \texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U}  \\
& (\texttt{open} \lor ((\texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U}\\
& (\texttt{open} \lor ((\lnot \texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U} \\
& (\texttt{open} \lor ((\texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U} \\
& (\texttt{open} \lor (\lnot \texttt{atfloor} ~\mathcal{U}~ \texttt{open}))))))))\big)\Big)\end{align}</math>

Here, <math>\Box</math> should be read as "always", <math>\Diamond</math> as "eventually", <math>\mathcal{U}</math> as "until" and the other symbols are standard logical symbols, <math>\lor</math> for "or", <math>\land</math> for "and" and <math>\lnot</math> for "not".