Linear Temporal Logic and Linear Dynamic Logic on Finite Traces
Abstract
In this paper we look into the assumption of interpreting LTL over finite traces. In particular we show that LTL f , i.e., LTL under this assumption, is less expressive than what might appear at first sight, and that at essentially no computational cost one can make a significant increase in expressiveness while maintaining the same intuitiveness of LTL f . Indeed, we propose a logic, LDL f for Linear Dynamic Logic over finite traces, which borrows the syntax from Propositional Dynamic Logic PDL, but is interpreted over finite traces. Satisfiability, validity and logical implication (as well as model checking) for LDL f are PSPACE-complete as for LTL f (and LTL).
Cite
Text
De Giacomo and Vardi. "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces." International Joint Conference on Artificial Intelligence, 2013.Markdown
[De Giacomo and Vardi. "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces." International Joint Conference on Artificial Intelligence, 2013.](https://mlanthology.org/ijcai/2013/giacomo2013ijcai-linear/)BibTeX
@inproceedings{giacomo2013ijcai-linear,
title = {{Linear Temporal Logic and Linear Dynamic Logic on Finite Traces}},
author = {De Giacomo, Giuseppe and Vardi, Moshe Y.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2013},
pages = {854-860},
url = {https://mlanthology.org/ijcai/2013/giacomo2013ijcai-linear/}
}