License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2022.1
URN: urn:nbn:de:0030-drops-172481
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17248/
Vardi, Moshe Y.
Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk)
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 chalenging 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.
BibTeX - Entry
@InProceedings{vardi:LIPIcs.TIME.2022.1,
author = {Vardi, Moshe Y.},
title = {{Linear Temporal Logic: From Infinite to Finite Horizon}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/17248},
URN = {urn:nbn:de:0030-drops-172481},
doi = {10.4230/LIPIcs.TIME.2022.1},
annote = {Keywords: Temporal Logic}
}
|
Keywords: |
|
Temporal Logic |
|
Collection: |
|
29th International Symposium on Temporal Representation and Reasoning (TIME 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
29.10.2022 |
