Synthesis United: Linear Temporal Logic: From Infinite to Finite Horizon
- đ¤ Speaker: Moshe Vardi (Rice University)
- đ Date & Time: Monday 18 July 2022, 15:30 - 16:30
- đ Venue: Discussion Room, Newton Institute
Abstract
Linear Temporal Logic (LTL), proposed in 1977 by Amir Pnueli for reasoning about ongoing programs, was defined over infinite traces. The motivation for this was the desire to model arbitrarily long computations. While this approach has been highly successful in the context of model checking, it has been less successful in the context of reactive synthesis, due to the challenging algorithmics of infinite-horizon temporal synthesis. In this talk we show that focusing on finite-horizon temporal synthesis offers enough algorithmic advantages to compensate for the loss in expressiveness. In fact, finite-horizon reasonings is useful even in the context of infinite-horizon applications.
Series This talk is part of the Isaac Newton Institute Seminar Series series.
Included in Lists
- All CMS events
- bld31
- dh539
- Discussion Room, Newton Institute
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)

Moshe Vardi (Rice University)
Monday 18 July 2022, 15:30-16:30