LydiaSyft: A Compositional Symbolic Synthesis Framework for LTLf Specifications

Abstract

Abstract There has been a massive interest in utilizing Linear Temporal Logic on finite traces ( $$\textsc {ltl}_f$$ L T L f ) as a specification language in the last decade, particularly in reactive synthesis. This highlights the need for a unified and efficient framework to fulfil the increasing demand for easy-to-use implementations of synthesis (and reasoning) algorithms for $$\textsc {ltl}_f$$ L T L f . To that end, we introduce , an open-source compositional symbolic synthesis framework that integrates efficient data structures and techniques focused on $$\textsc {ltl}_f$$ L T L f specifications. supports both explicit-DFA and symbolic-DFA construction from $$\textsc {ltl}_f$$ L T L f formulas, essential DFA manipulations, and offers an extensible framework for reactive synthesis of $$\textsc {ltl}_f$$ L T L f specifications, accommodating more complex synthesis scenarios. We demonstrate this feasibility by supporting $$\textsc {ltl}_f$$ L T L f synthesis as well as $$\textsc {ltl}_f$$ L T L f synthesis with ltl environment specifications expressed in various forms. is highly efficient and versatile, providing user-friendly C++ interfaces and extensive benchmarks that cater to a diverse audience, including computer scientists, practitioners, students, and the reactive synthesis research community.