Tester-based Symbolic Synthesis of Linear Dynamic Logic on Finite Traces

This paper mainly explores the symbolic synthesis method for Linear Dynamic Logic on Finite Traces (LDLf) based temporal testers. In the field of formal methods, LDLf is a powerful temporal logic capable of expressing complex behaviors and regular properties of discrete systems. However, the efficient synthesis of system models that satisfy LDLf specifications remains a challenge. To meet this challenge, this paper proposes a tester-based symbolic synthesis method, which combines the advantages of symbolic techniques with the characteristics of temporal testers to automatically generate system models that satisfy LDLf specifications. We implemented the proposed method as a prototype LDLf synthesis tool, LDLf-Synt. Preliminary experiments show that LDLf-Synt significantly outperforms Lydia, another similar tool, in terms of time and space consumption. It is worth noting that LDLf-Synt exhibits a trend of exponentially lower time consumption compared to Lydia.