Synthesis United: Linear Temporal Logic: From Infinite to Finite Horizon

Add to your list(s) Download to your calendar using vCal

• Moshe Vardi (Rice University)
• Monday 18 July 2022, 15:30-16:30
• Discussion Room, Newton Institute.

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

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.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Discussion Room, Newton Institute
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• bld31

Note that ex-directory lists are not shown.