View source for Temporal logic in finite-state verification

In finite-state verification, [[Model checking|model checkers]] examine [[Finite-state machine|finite-state machine]]s representing concurrent [[Software|software]] systems looking for errors in [[Design|design]].  Errors are defined as violations of requirements expressed as properties of the system. In the event that the finite-state machine fails to satisfy the property, a model checker is in some cases capable of producing a counterexample &ndash; an execution of the system demonstrating how the error occurs.

Property specifications are often written as Linear Temporal Logic (LTL) expressions.  Once a [[Requirement|requirement]] is expressed as an LTL formula, a model checker can automatically verify this property against the model.

==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, Avruin, Corbett" />
:<math>\begin{align}\Box((call \lor \Diamond open) \to 
& ((\lnot atfloor \lor \lnot open) ~\mathcal{U}  \\
& (open \lor ((atfloor \land \lnot open) ~\mathcal{U}\\
& (open \lor ((\lnot atfloor \land \lnot open) ~\mathcal{U} \\
& (open \lor ((atfloor \land \lnot open) ~\mathcal{U} \\
& (open \lor (\lnot atfloor ~\mathcal{U}~ open)))))))))))\end{align}</math>

<!-- [[Image:ElevatorLTL.JPG|none|center]] -->

== See also ==
*[[Finite-state machine]]s
*[[Formal methods]]
*[[Formal verification]]
*Kripke structure
*Linear temporal logic
*[[Model checking]]
*[[Philosophy:Temporal logic|Temporal logic]]

== References ==
{{reflist|refs=

<ref name="Dwyer, Avruin, Corbett" >{{Cite conference
  |first=M.  |last=Dwyer
  |first2=G.  |last2=Avruin
  |first3=J.  |last3=Corbett
  |title=Patterns in Property Specification for Finite-State Verification
  |editor=Ardis, M.
  |conference=Proceedings of the Second Workshop on Formal Methods in Software Practice
  |pages=7–15
  |date=March 1998
  |url=http://santos.cis.ksu.edu/esscass04/papers/patterns-survey.pdf
}}</ref> 

}}

== Bibliography ==
# Z. Manna and [[Biography:Amir Pnueli|Amir Pnueli]], ''The Temporal Logic of Reactive and Concurrent Systems: Specification'', [[Company:Springer Science+Business Media|Springer-Verlag]], New York, 1991.
# [[Biography:Amir Pnueli|Amir Pnueli]], The Temporal Logic of Programs. In ''Proceedings of the 18th IEEE Symposium on Foundations of Computer Science (FOCS 1977)'', pages 46–57, 1977.

[[Category:Automata (computation)]]

{{Sourceattribution|Temporal logic in finite-state verification|1}}