Abstract
Linear Temporal Logic over finite traces, or LTLf, is a popular logic to describe specifications with finite behaviors in AI scenarios such as motion planning. Satisfiability is one of the fundamental problems of LTLf and extensive studies have been conducted to speed up the process to check whether a given LTLf formula is satisfiable. This paper presents a new approach, namely LSCFP, to solve the problem of LTLf satisfiability checking by leveraging the formula progression technique. Compared to previous work, LSCFP utilizes formula progression to gather more information propagated along with the search path such that it can find satisfiable models more quickly if the input formula is satisfiable. A comprehensive experimental evaluation has been conducted to show the efficiency of LSCFP, and the results suggest that LSCFP is able to gain at least 15% performance improvement on checking satisfiable formulas when compared to the state-of-the-art LTLf satisfiability checker aaltaf.
| Original language | English |
|---|---|
| Pages (from-to) | 357-362 |
| Number of pages | 6 |
| Journal | Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE |
| Volume | 2023-July |
| State | Published - 2023 |
| Event | 35th International Conference on Software Engineering and Knowledge Engineering, SEKE 2023 - Hybrid, San Francisco, United States Duration: 1 Jul 2023 → 10 Jul 2023 |