Editing Model checking (section)

===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".