Synthesis of Real-time Linear Dynamic Logic over Finite Traces

Reactive synthesis, or simply synthesis, is primarily used to automatically generate control-intensive programs. Applications of reactive synthesis span various domains, including robot motion planning, autonomous system control, and communication protocol development. This paper investigates the reactive synthesis for formulas expressed in Real-Time Linear Dynamic Logic over finite traces (RTLDLf). RTLDLf is more expressive than Linear Temporal Logic over finite traces (LTLf). While RTLDLf and Linear Dynamic Logic over finite traces (LDLf) share equivalent expressive power, RTLDLf offers greater simplicity in its logical constructs compared to LDLf. Existing synthesis methods for LDLf predominantly rely on automata-based approaches. In this paper, we propose an RTLDLf synthesis method based on temporal testers. We first translate an RTLDLf specification into a temporal tester, a non-deterministic transducer. The tester is then transformed into a graph game between the system and the environment. We finally propose a symbolic algorithm to solve the game to derive a winning strategy for the system player. The proposed method has two advantages: (1) high composability, enabling convenient and efficient synthesis of complex RTLDLf formulas, and (2) symbolic representation of the tester's transition relations and state space, which facilitates the use of efficient symbolic algorithms based on Ordered Binary Decision Diagrams.