# Difference between revisions of "EECI 2012: Temporal Logic"

(Created page with '{{eeci-sp11 header|prev=Automata Theory|next=Model Checking}} {{righttoc}} In this lecture we introduce ''linear temporal logic'' (LTL), a mathematical language for describing l…') |
|||

(6 intermediate revisions by 2 users not shown) | |||

Line 1: | Line 1: | ||

− | {{eeci- | + | {{eeci-sp12 header|prev=Automata Theory|next=Model Checking}} |

{{righttoc}} | {{righttoc}} | ||

Line 5: | Line 5: | ||

== Lecture Materials == | == Lecture Materials == | ||

− | * Lecture slides: [http://www.cds.caltech.edu/~murray/courses/ | + | * Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L3_ltl-14May12.pdf Linear Temporal Logic] (Presentation and notation follow that in "Principles of Model Checking" chapter 5.1 by Baier and Katoen.) |

== Further Reading == | == Further Reading == | ||

Line 12: | Line 12: | ||

== Additional Information == | == Additional Information == | ||

+ | * [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata. |

## Latest revision as of 09:20, 14 May 2012

Prev: Automata Theory | Course home | Next: Model Checking |

In this lecture we introduce *linear temporal logic* (LTL), a mathematical language for describing linear time properties of transition systems. After a short introduction to the concept of temporal logics, we introduce the syntax and semantics of LTL, including examples. Examples of LTL specifications for control protocols are drawn from the applications given in the introductory lecture. If time permits, we will also briefly introduce other temporal logics and describe some of the differences between various formulations.

## Lecture Materials

- Lecture slides: Linear Temporal Logic (Presentation and notation follow that in "Principles of Model Checking" chapter 5.1 by Baier and Katoen.)

## Further Reading

Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Slides for this lecture follow Chapter 6 of this reference.

*Specifying Systems*, L. Lamport.. Addison-Wesley, 2002. This is a very readable text on specification using temporal logic of actions (LTA).

## Additional Information

- LTL2BA - a web page (and program) for converting LTL formulas to Buchi automata.