On-the-fly Synthesis for LTL over Finite Traces


  • Shengping Xiao East China Normal University
  • Jianwen Li East China Normal University
  • Shufang Zhu Sapienza Universit`a di Roma Shanghai Trusted Industrial Control Platform Co., Ltd.
  • Yingying Shi East China Normal University
  • Geguang Pu East China Normal University
  • Moshe Vardi Rice University




Description Logics


We present a new synthesis framework based on the on-the-fly DFA construction for LTL over finite traces (LTLf ). Extant approaches rely heavily on the construction of the complete DFA w.r.t. the input LTLf formula, whose size can be doubly exponential to the size of the formula in the worst case. Under those approaches, the synthesis cannot be conducted unless the whole DFA is completely constructed, which is not only inefficient but also not scalable in practice. Indeed, the DFA construction is the main bottleneck of LTLf synthesis in prior work. To mitigate this challenge, we follow two steps in this paper: Firstly, we present several light-weight pre-processing techniques such that the synthesis result can be obtained even without DFA construction; Secondly, we propose to achieve the synthesis together with the on-the-fly DFA construction such that the synthesis result can be obtained before constructing the whole DFA. The on-the-fly DFA construction is implemented using the SAT-based techniques for automata generation. We compared our new approach with the traditional ones on extensive LTLf synthesis benchmarks. Experimental results showed that the pre-processing techniques have a significant advantage on the synthesis performance in terms of scalability, and the on-the-fly synthesis is able to complement extant approaches on both realizable and unrealizable cases.




How to Cite

Xiao, S., Li, J., Zhu, S., Shi, Y., Pu, G., & Vardi, M. (2021). On-the-fly Synthesis for LTL over Finite Traces. Proceedings of the AAAI Conference on Artificial Intelligence, 35(7), 6530-6537. https://doi.org/10.1609/aaai.v35i7.16809



AAAI Technical Track on Knowledge Representation and Reasoning