TLDR: A new compositional framework called Cosy improves LTLf synthesis for intelligent agents by combining the strengths of existing backward and forward approaches. It tackles the computational bottleneck of DFA construction by applying composition during game solving, especially for complex specifications with multiple conjunctive parts. Cosy, with its individual and incremental composition variants, outperforms state-of-the-art tools, solving more instances by efficiently managing state space and enabling early unrealizability detection.
Intelligent agents are becoming increasingly sophisticated, capable of autonomously planning and executing complex actions to achieve desired tasks. This capability is closely linked to a field in Formal Methods called reactive synthesis. Reactive synthesis involves designing an agent that can operate effectively in an adversarial environment, where it controls certain variables while the environment controls others. The goal is for the agent to devise a strategy to achieve its task despite potential environmental reactions.
In the realm of Artificial Intelligence, tasks are often specified using a variant of Linear Temporal Logic (LTL) known as LTLf, or Linear Temporal Logic over finite traces. LTLf is particularly popular because intelligent agents typically handle tasks sequentially rather than dedicating their entire operational lifetime to a single, continuous task. Beyond reactive synthesis, LTLf has found applications in automated planning, reinforcement learning, and reasoning about business processes.
The core of LTLf synthesis involves transforming the task specification into a two-player adversarial game played on a Deterministic Finite Automaton (DFA). While solving the DFA game itself is relatively efficient, the major hurdle lies in constructing the DFA. This construction process can be incredibly complex, potentially taking double-exponential time in the worst case, making it the primary bottleneck in LTLf synthesis.
Existing approaches to tackle this challenge generally fall into two categories. The “backward” approach constructs the complete DFA in a compositional manner, using DFA minimization at each step to manage the explosion of states. The “forward” approach, on the other hand, builds the DFA incrementally, “on-the-fly,” as the game is being solved, aiming to avoid constructing the full DFA. However, neither of these methods has proven universally superior, with each showing strengths and weaknesses depending on the specific problem.
A new research paper, titled “A Compositional Framework for On-the-Fly LTLf Synthesis,” introduces an innovative framework that seeks to combine the best aspects of both existing approaches. This framework is particularly effective for LTLf specifications that are expressed as large conjunctions of smaller LTLf formulas, a common scenario in practical applications. Instead of composing intermediate results during the initial DFA construction, this new method applies composition during the game-solving phase. This allows for pruning of intermediate results, which simplifies subsequent compositions and can even enable early detection of whether a task is impossible to achieve (unrealizable).
The framework offers two distinct composition variants. The first, called individual composition, focuses on maximizing the benefits of DFA minimization. It independently computes the “agent-winning region” for each sub-specification (which represents all the ways the agent can win that part of the game), minimizes it, and then combines these minimized regions. The second variant, incremental composition, integrates the on-the-fly synthesis process directly into the composition. It uses the already computed winning regions of previously processed sub-specifications to guide the search for the new sub-specification, performing an implicit combination during the search itself.
The researchers implemented their framework in a prototype tool named Cosy. Through extensive empirical evaluation against leading LTLf synthesis tools like Lisa, LydiaSyft, Nike, and Tople, Cosy demonstrated superior performance. It successfully solved a significantly higher number of instances, particularly those that other solvers struggled with. While both individual and incremental composition variants showed unique merits, the incremental variant generally solved slightly more instances, highlighting its effectiveness in integrating search and composition.
Also Read:
- New Framework for Designing Memory Challenges in Reinforcement Learning Environments
- AI Agents Master Collaboration: A Hybrid Approach to Ad Hoc Teamwork
This compositional approach marks a significant step forward in LTLf synthesis, offering a more efficient way to handle complex task specifications for intelligent agents. Future work aims to reduce the framework’s reliance on Binary Decision Diagrams (BDDs), which can consume exponential space, and to extend the compositional operations to support a wider range of logical operators beyond just conjunctions. You can find the full research paper here: A Compositional Framework for On-the-Fly LTLf Synthesis.
