Linear Temporal Logic and Linear Dynamic Logic on Finite Traces
Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. Pages 854-859.
Abstract
In this paper we look into the assumption of interpreting LTL over finite traces. In particular we show that LTLf, 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 LTLf. Indeed, we propose a logic, LDLf 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 LDLf are PSPACE-complete as for LTLf (and LTL).
@inproceedings{ijcai2013p132,
title = {Linear Temporal Logic and Linear Dynamic Logic on Finite Traces},
author = {De Giacomo, Giuseppe and Vardi, Moshe Y.},
booktitle = {Proceedings of the Twenty-Third International Joint Conference on
Artificial Intelligence, {IJCAI-13}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Francesca Rossi},
pages = {854--859},
year = {2013},
month = {8},
url = {https://ijcai.org/proceedings/2013/132},
}
TY - CPAPER TI - Linear Temporal Logic and Linear Dynamic Logic on Finite Traces AU - De Giacomo, Giuseppe AU - Vardi, Moshe Y. T2 - Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI-13 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2013 SP - 854 EP - 859 UR - https://ijcai.org/proceedings/2013/132 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
