[LiZPVH14] LTLf Satisfiability Checking Li, J.; Zhang, L.; Pu, G.; Vardi, M. Y. and He, J. In 21st European Conference on Artificial Intelligence - Including Prestigious Applications of Intelligent Systems (ECAI 2014), pages 513-518, IOS Press, Frontiers in Artificial Intelligence and Applications 263, 2014.
Downloads: pdf, bibURL: http://arxiv.org/abs/1403.1666 Abstract. We consider here Linear Temporal Logic (LTL) formulas interpreted over finite traces. We denote this logic by LTLf. The existing approach for LTLf satisfiability checking is based on a reduction to standard LTL satisfiability checking. We describe here a novel direct approach to LTLf satisfiability checking, where we take advantage of the difference in the semantics between LTL and LTLf. While LTL satisfiability checking requires finding a fair cycle in an appropriate transition system, here we need to search only for a finite trace. This enables us to introduce specialized heuristics, where we also exploit recent progress in Boolean SAT solving. We have implemented our approach in a prototype tool and experiments show that our approach outperforms existing approaches.