Information Sciences Seminar——On-the-fly Synthesis for LTL over Finite Traces
报告人：Jianwen Li (East China Normal University)
时间：2021-10-28 10:00-12:00
地点：腾讯会议 ID：257 467 627
Abstract:
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.
Short bio:
李建文，华东师范大学研究员，博士生导师，入选上海市青年人才计划，获得上海市浦江人才荣誉称号，主持国家自然科学基金青年项目、重点项目子课题各一项。研究方向主要为形式化自动验证技术，可用于保障计算机软硬件系统的正确性和安全性，重点应用场景包括芯片、航天、轨道交通等安全攸关领域。
腾讯会议 ID：257 467 627
会议链接：https://meeting.tencent.com/dm/4ma3YFF46DJQ
