Maximum Realizability for LTL Modulo Theories

Abstract The synthesis of systems from formal specifications is a fundamental problem in symbolic AI and formal methods where the goal is to automatically construct implementations that meet desired requirements. In practice, specifications often include both hard constraints (critical requirements) and soft constraints (desirable properties). However, when specifications are unrealizable (due to conflicts between requirements) traditional synthesis methods fail to provide meaningful implementations or guidance. This problem has been addressed with maximum realizability , a framework for synthesizing systems that satisfy hard constraints while maximizing the satisfaction of soft constraints. However, the literature only solves this technique for classic discrete Linear Temporal Logic (LTL), whereas its extension to richer LTL modulo theories ( $LTL _{\mathcal {T}}$ L T L T ) remains unexplored. In this paper, we bridge this gap and we propose two approaches: (1) a method based on exhaustively traversing a set of abstractions and (2) an alternative method that incrementally refines abstractions during synthesis. Additionally, (3) we introduce lattice-based optimization techniques to further improve scalability by pruning uninteresting combinations of soft constraints. Our methods are evaluated on benchmarks from synthesis competitions and practical case studies, demonstrating their scalability and effectiveness.