Dieses Kapitel befasst sich mit der Entwicklung und den Fähigkeiten eines innovativen Open-Source-Software-Frameworks zur Argumentation und Synthese von Spezifikationen, die in Linear Temporal Logic auf endlichen Spuren ausgedrückt werden. Das auf Benutzerfreundlichkeit und Erweiterbarkeit ausgerichtete Framework nutzt kompositorische Konstruktionstechniken, um eine breite Palette von Syntheseeinstellungen zu handhaben. Es unterstützt explizit-staatliche und symbolisch-staatliche DFA-Konstruktionen, die eine effiziente Manipulation und Transformation von Automaten ermöglichen. Die Architektur des Frameworks ist minutiös detailliert und zeigt seine Fähigkeit, Syntheseprobleme auf Spiele auf DFA zu reduzieren, indem sie verschiedene Szenarien wie Erreichbarkeit, maximal freizügige Strategien und Synthese mit Umweltspezifikationen berücksichtigt. Das Kapitel beleuchtet auch die Leistung des Rahmenwerks, wie sein Erfolg bei der Synthese von SYNTCOMP 2024 zeigt, und gibt einen Einblick in seine potenziellen Anwendungen in verschiedenen Bereichen, einschließlich Planung, Robotik und Verstärkungslernen. Mit seiner modularen C + + -Implementierung und den wiederverwendbaren Bibliotheken bietet das Framework eine robuste Plattform für die weitere Forschung und Entwicklung im Bereich der reaktiven Synthese.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
There has been a massive interest in utilizing Linear Temporal Logic on finite traces (\(\textsc {ltl}_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\) . To that end, we introduce LydiaSyft, an open-source compositional symbolic synthesis framework that integrates efficient data structures and techniques focused on \(\textsc {ltl}_f\) specifications. LydiaSyft supports both explicit-DFA and symbolic-DFA construction from \(\textsc {ltl}_f\) formulas, essential DFA manipulations, and offers an extensible framework for reactive synthesis of \(\textsc {ltl}_f\) specifications, accommodating more complex synthesis scenarios. We demonstrate this feasibility by supporting \(\textsc {ltl}_f\) synthesis as well as \(\textsc {ltl}_f\) synthesis with ltl environment specifications expressed in various forms. LydiaSyft 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.
Hinweise
S. Zhu and M. Favorito—Equal contribution.
1 Introduction
Recently, there has been massive interest in reactive synthesis for specifications expressed in Linear Temporal Logic on finite traces (\(\textsc {ltl}_f\)) [12]. The first \(\textsc {ltl}_f\) synthesizer \(\textsf{Syft}\) demonstrated the practical scalability of \(\textsc {ltl}_f\) synthesis [25], which opened the door to a whole dimension of utilizing \(\textsc {ltl}_f\) in various domains such as planning [11], robotics [16], and reinforcement learning [6]. This massive interest in \(\textsc {ltl}_f\) led to an increasing demand for easy-to-use implementations of synthesis and reasoning algorithms for \(\textsc {ltl}_f\) specifications.
We introduce LydiaSyft, an open-source software framework for \(\textsc {ltl}_f\) reasoning and synthesis. The reasoning component leverages \(\textsc {ltl}_f\)-to-DFA construction, reducing \(\textsc {ltl}_f\) reasoning to automata-based reasoning. LydiaSyft adopts the compositional automata construction technique from \(\textsf{Lydia}\) [9], providing both explicit-state DFA and symbolic-state DFA construction and manipulation. Unlike \(\textsf{Lydia}\) and \(\textsf{Syft}\), which handle only standard \(\textsc {ltl}_f\) synthesis (though \(\textsf{Lydia}\) introduces a novel compositional \(\textsc {ltl}_f\)-to-DFA construction technique), LydiaSyft supports a broader range of synthesis settings for \(\textsc {ltl}_f\) specifications, including \(\textsc {ltl}_f\) synthesis [13, 25], maximally permissive strategy of \(\textsc {ltl}_f\) synthesis [24], \(\textsc {ltl}_f\) synthesis with simple Stability or Fairness environment specification [23], and \(\textsc {ltl}_f\) synthesis with Generalized-Reachability(1) environment specification [7, 8]. LydiaSyft leverages the symbolic game-solving techniques from \(\textsf{Syft}\) [25] to deal with the synthesis problems and offers reusable C++ libraries of two-player game solvers. These solvers support customization, enabling users to create and efficiently solve custom games, e.g., the reachability game solver used in robotics task planning [16].
Anzeige
The primary goal of LydiaSyft is to provide an easy-to-extend platform for \(\textsc {ltl}_f\) reasoning and synthesis, focusing on usability and extensibility over peak performance optimizations, such as those for standard \(\textsc {ltl}_f\) synthesis [10, 15, 21, 22]. Despite this focus, LydiaSyft features an efficient, modular C++ implementation of core data structures and synthesis techniques, earning it 2nd place in the \(\textsc {ltl}_f\) synthesis track of SYNTCOMP 2024. Due to space constraints, additional experimental results and further technical details are provided in the Appendix.
The main components of LydiaSyft ’s architecture are depicted in Figure 1 (All the techniques implemented in LydiaSyft also support Linear Dynamic Logic on finite traces (\(\textsc {ldl}_f\)) [12] specifications). LydiaSyft accepts \(\textsc {ltl}_f\) formulas written in a syntax following the TLSF format [18]. Depending on the synthesis task, LydiaSyft takes additional inputs capturing safety (expressed in \(\textsc {ltl}_f\)), simple Fairness, simple Stability, and Generalized-Reactivity(1) specifications [7, 8, 23].
Anzeige
Explicit-state DFA construction.LydiaSyft leverages the compositional \(\textsc {ltl}_f\)-to-DFA construction techniques from \(\textsf{Lydia}\) [9] to build an explicit-state DFA of the input \(\textsc {ltl}_f\) specification. This process involves a fully compositional technique that aggressively minimizes partial results so that the state space of the DFA is kept at the minimum. A novel contribution of our integration is to provide a better code interface to handle automata, enhancing interoperability with other modules and, potentially, with external tools.
Symbolic-state DFA construction. The constructed explicit-state DFA is then transformed into a symbolic-state DFA, both the state space and the transitions of which are represented symbolically in BDDs. This provides a compact form of the DFA, facilitating subsequent computational steps. In particular, the data structure used is known in the literature as partitioned DFA representation [25]. LydiaSyft provides novel implementations for representing and manipulating symbolic DFAs using the same interface used for explicit-state DFAs.
Game construction. On top of the symbolic automata, LydiaSyft builds a two-player game data structure, possibly incorporating additional specifications like GR(1). These games form the backbone of the synthesis process, where the agent has to find a strategy that wins the game against the environment. LydiaSyft also supports adaptable player orders: agent-first or environment-first. We default to an agent-first setting in the rest of the paper, as in [13].
Games on DFA for synthesis.LydiaSyft supports various synthesis scenarios for \(\textsc {ltl}_f\) specifications through reducing to games on DFA, addressing diverse problems: (i) reachability game, for \(\textsc {ltl}_f\) synthesis [13, 25] (ii) maxset reachability game, for computing the maximally permissive strategy of \(\textsc {ltl}_f\) synthesis [24]. (iii) Büchi-Reachability game, for \(\textsc {ltl}_f\) synthesis with simple Stability environment specifications [23]. (iv) coBüchi-Reachability game, for \(\textsc {ltl}_f\) synthesis with simple Fairness environment specifications [23]. (vi) coGR(1)-Reachability game, for \(\textsc {ltl}_f\) synthesis with GR(1) environment specifications, and possible additional safety conditions to both the environment and the agent [7, 8]. A computed winning strategy, if it exists, can be printed in DOT format.
3 Compositional \(\textsc {ltl}_f\)-to-DFA Construction
The basic building block for LydiaSyft is the \(\textsc {ltl}_f\)-to-DFA construction. This section details how the explicit-state/symbolic-state DFA construction parts work and which data structures and procedures have been used.
\(\textsc {ltl}_f\)Basics.Linear Temporal Logic on finite traces (\(\textsc {ltl}_f\)) [12] is a specification language expressing temporal properties on finite, nonempty traces. In particular, \(\textsc {ltl}_f\) shares syntax with ltl, which is instead interpreted over infinite traces [20]. LydiaSyft also supports the variant that works for empty traces [4]. Given a set of atomic propositions Prop, \(\textsc {ltl}_f\) formulas are generated as follows:
, where \({ tt }\) is the tautology, \(a \in Prop\) is an atom,
(Next) and \(\mathop {\mathcal {U}}\) (Until) are temporal operators. We make use of standard Boolean abbreviations, e.g., \( ff \equiv \lnot { tt }\), \(\vee \) (or) and \(\rightarrow \) (implies), \( true \) and \( false \). In addition, we define the following abbreviations: Weak Next
, Eventually\(\Diamond \varphi \equiv true \mathop {\mathcal {U}}\varphi \) and Always\(\Box \varphi \equiv false \mathop {\mathcal {R}}\varphi \), where \(\mathop {\mathcal {R}}\) is for Release. The detailed semantics of \(\textsc {ltl}_f\) can be found in [12]. It is shown that, for every \(\textsc {ltl}_f\) formula \(\varphi \), one can construct a Deterministic Finite Automaton (DFA) that accepts exactly the same language as the \(\textsc {ltl}_f\) formula [12]. Notably, an \(\textsc {ltl}_f\) formula can be transformed into an equivalent DFA in at most 2EXPTIME [12].
Build explicit-state DFA. An explicit-state DFA [17] is a tuple \(\mathcal {A}= \langle \varSigma , S, s_0, \delta ,\)\( F\rangle \), where: \(\varSigma \) is the alphabet, S is a finite set of states, \(s_0\in S\) is the initial state, \(\delta : S\times \varSigma \rightarrow S\) is a total transition function and \(F\subseteq S\) is the set of accepting states. Given an \(\textsc {ltl}_f\) formula \(\varphi \), LydiaSyft leverages the compositional DFA construction in \(\textsf{Lydia}\) [9], which inductively applies a transformation procedure to each subformula of \(\varphi \). This construction is “bottom-up”, computing the DFAs of subformulas and combining them based on the \(\textsc {ltl}_f\) operator under transformation. LydiaSyft extends \(\textsf{Lydia}\) ’s DFA library, which represents explicit-state DFAs using Shared Multi-terminal Binary Decision Diagrams (ShMTBDDs) [5, 19]. To ensure compatibility with subsequent symbolic-state DFA construction, LydiaSyft provides convenient wrappers for these libraries. Notably, LydiaSyft enhances explicit-state DFA manipulation by offering operations such as complement, product, state and transition restrictions, and printing.
Build symbolic-state DFA. Given an explicit-state DFA \(\mathcal {A}= (2^{\mathcal {X}\cup \mathcal {Y}}, S, s_0, \delta , F)\), the corresponding symbolic-state DFA is defined as \(\mathcal {D}= (\mathcal {X}, \mathcal {Y}, \mathcal {Z}, \iota , \eta , f)\), where \(\mathcal {X}\) and \(\mathcal {Y}\) are as in \(\mathcal {A}\), and \(\mathcal {Z}\) is a set of \(\lceil \log _2|S| \rceil \) propositions, with each state \(s \in S\) corresponding to an interpretation \(Z \in 2^\mathcal {Z}\). The initial state \(s_0\) is represented by \(\iota \in 2^\mathcal {Z}\). The transition function \(\eta = \{\eta _0, \eta _1, \cdots , \eta _k\}~(|\eta | = |\mathcal {Z}|)\) maps interpretations \(X \in 2^\mathcal {X}\), \(Y \in 2^\mathcal {Y}\) and \(Z \in 2^\mathcal {Z}\) to the successor state \(\delta (s, X \cup Y)\) such that \(\eta _i(X, Y, Z) = 1\) iff the value of \(z_i \in \mathcal {Z}\) is 1 in the interpretation \(Z' \in 2^\mathcal {Z}\) corresponding to \(\delta (s, X \cup Y)\). Finally, the set of accepting states f is a Boolean formula over \(\mathcal {Z}\), satisfied by Z iff it corresponds to an accepting state \(s \in F\) [25]. LydiaSyft utilizes the same symbolic-state DFA representation as \(\textsf{Syft}\), which represents a symbolic-state DFA \(\mathcal {D}\) as a sequence of BDDs. However, while \(\textsf{Syft}\) manually converts explicit-state DFAs (represented as ShMTBDDs) into symbolic-state DFAs by traversing the ShMTBDD and generating propositional evaluations for each explicit state, LydiaSyft takes a different approach. It employs Algebraic Decision Diagrams (ADDs) [2] as an intermediate step, leveraging the BDD/ADD library CUDD-3.0.0. We first convert a ShMTBDD to a sequence of ADDs, and then use the rich API functions, in particular \(\textsf{BddIthBit}\), provided by CUDD to obtain the BDD sequence, avoiding the manual conversion. Additionally, LydiaSyft supports a range of symbolic-state DFA manipulations, including complement, product, state and transition restrictions, and printing.
4 Synthesis Settings for \(\textsc {ltl}_f\) Specifications
This section outlines the synthesis settings for \(\textsc {ltl}_f\) specifications supported by LydiaSyft. Let \(\mathcal {X}\) and \(\mathcal {Y}\) be Boolean variables, with \(\mathcal {X}\) controlled by the environment and \(\mathcal {Y}\) controlled by the agent. An agent strategy is a function \(\sigma _ {agn} :(2^{\mathcal {X}})^* \rightarrow 2^{\mathcal {Y}}\), and an environment strategy is a function \(\sigma _ {env} :(2^\mathcal {Y})^+ \rightarrow 2^\mathcal {X}\). An agent strategy induces a trace \(\pi = (X_0 \cup Y_0) (X_1 \cup Y_1) \dots \in (2^{\mathcal {X}\cup \mathcal {Y}})^\omega \) if \(\sigma _ {agn} (\epsilon )=Y_0\) and \(\sigma _ {agn} (X_0 X_1 \cdots X_j) = Y_{j+1}\) for every \(j \ge 0\). An environment strategy induces a trace \(\pi \in (2^{\mathcal {X}\cup \mathcal {Y}})^\omega \) if \(\sigma _ {env} (Y_0 Y_1 \cdots Y_j) = X_j\) for every \(j \ge 0\). The unique trace induced by an agent strategy \(\sigma _ {agn} \) and an environment strategy \(\sigma _ {env} \) is denoted by \(\textsf {play}(\sigma _ {agn} ,\sigma _ {env} )\) or simply \(\pi \) when clear from the context.
\(\textsc {ltl}_f\)Synthesis. The problem is described as a tuple \(\mathcal {P}= (\mathcal {X},\mathcal {Y},\varphi )\), where \(\varphi \) is an \(\textsc {ltl}_f\) formula over \(\mathcal {X}\cup \mathcal {Y}\). Realizability of \(\mathcal {P}\) checks whether \(\exists \sigma _ {agn} \forall \sigma _{env}: \exists k\ge 0. \textsf {play}^k(\sigma _ {agn} , \sigma _{env}) \models \varphi \). Synthesis of \(\mathcal {P}\) computes a strategy \(\sigma _ {agn} \) if exists [13]. LydiaSyft integrates the preprocessing techniques for \(\textsc {ltl}_f\) synthesis introduced in [21] for effective realizability check and unrealizability check. If preprocessing fails, LydiaSyft constructs a symbolic-state DFA \(\mathcal {D}_\varphi \) for \(\varphi \), and builds a reachability game \(G = (\mathcal {D}_\varphi , \texttt{Reach}(t))\), where t is a set of target states. LydiaSyft follows the symbolic synthesis technique presented in [25] to solve \(G = (\mathcal {D}_\varphi , \texttt{Reach}(t))\), providing a C++ library \(\mathsf {Reachability.h}\).
\(\textsc {ltl}_f\)MaxSet Synthesis.\(\textsc {ltl}_f\) maxset synthesis \(\mathcal {P}= (\mathcal {X},\mathcal {Y},\varphi )\) aims at computing the maximally permissive strategy (MaxSet), which represents the set of all agent winning strategies [24]. As shown in [24], MaxSet for \(\mathcal {P}= (\mathcal {X},\mathcal {Y},\varphi )\) can be solved by reasoning about the maxset reachability game on \(\mathcal {D}_\varphi \). LydiaSyft provides a C++ library \(\mathsf {ReachabilityMaxSet.h}\), which takes the reachability game \(G = (\mathcal {D}_\varphi , \texttt{Reach}(t))\) as input and computes two nondeterministic strategies characterizing MaxSet, if there is at least one winning strategy.
\(\textsc {ltl}_f\)Synthesis with Simple Stability/Fairness Env. Specs. We now outline the LydiaSyft-supported synthesis settings for \(\textsc {ltl}_f\) specifications involving two-player games on DFAs that extend beyond reachability, focusing specifically on \(\textsc {ltl}_f\) synthesis with environment specifications. Following [1], we specify the environment behaviour by an ltl formula \( {env} \) and call it environment specification, and the agent goal is an \(\textsc {ltl}_f\) formula \(\varphi \). Formally, given an ltl formula env, we say that an environment strategy enforcesenv, written \(\sigma _ {env} \ \rhd \ env\), if for every agent strategy \(\sigma _{agn}\) we have \(\textsf {play}(\sigma _ {agn} ,\sigma _ {env} ) \models env\). The problem of \(\textsc {ltl}_f\)synthesis with environment specifications is to find an agent strategy \(\sigma _ {agn} \) such that \(\exists \sigma _{agn} \forall \sigma _ {env} \ \rhd {env} :\exists k. \textsf {play}^k(\sigma _ {agn} ,\sigma _ {env} ) \models \varphi .\)
An ltl formula env is considered as a simple Stability specification if it is of the form \(\Diamond \Box (\alpha )\), and a simple Fairness specification if it is of the form \(\Box \Diamond (\alpha )\), where \(\alpha \) is a Boolean formula involving only environment variables [23]. As shown in [23], \(\textsc {ltl}_f\) synthesis with simple Stability/Fairness environment specification can be reduced to Büchi-Reachability and coBüchi-Reachability games on \(\mathcal {D}_\varphi \), respectively. LydiaSyft provides a C++ library \(\mathsf {BuchiReachability.h}\), which takes a constructed Büchi-Reachability game \(G = (\mathcal {D}_\varphi , \texttt{BuchiReach}(t, \beta ))\) as input, performs a nested fixpoint computation to solve the game. The library \(\mathsf {coBuchiReachability.h}\) supports coBüchi-Reachability game solving.
\(\textsc {ltl}_f\)Synthesis with Generalized Reachability(1) Env. Specs. GR(1) is a syntactic fragment of LTL, providing a powerful notion of fairness [3]. The problem of \(\textsc {ltl}_f\) synthesis with GR(1) environment specifications introduced in [7, 8] successfully brought the advances of GR(1) synthesis and \(\textsc {ltl}_f\) synthesis. LydiaSyft employs the solution proposed in [7, 8] reducing the synthesis problem to a coGR(1)-Reachability game. LydiaSyft also allows adding additional safety conditions to both the environment and the agent, expressed in \(\textsc {ltl}_f\) formulas, as in [7, 8]. It provides a C++ library \(\mathsf {coGR1Reachability.h}\), which takes a coGR(1)-Reachability game (with possible safety conditions) as input, reduces it further to a GR(1) game and uses \(\textsf{Slugs}\) [14] to solve it.
An example of using LydiaSyft as a CLI tool for \(\textsc {ltl}_f\) synthesis is shown in Listing 1.1.
5 Conclusion and Future Works
In this paper, we presented LydiaSyft, an open-source synthesis framework that integrates efficient data structure and synthesis techniques, focusing on agent goals expressed in \(\textsc {ltl}_f\) specifications. We believe that LydiaSyft provides a significant foundation to address the increasing demand for synthesis and reasoning of \(\textsc {ltl}_f\) specifications. LydiaSyft offers researchers, practitioners, and students convenient access to flexible automata construction from \(\textsc {ltl}_f\) specifications, and various synthesis settings. Furthermore, it provides a unified and accessible approach for reproducibility. We are actively working on the framework to integrate further and future synthesis settings into LydiaSyft. Using the permissive MIT license, we hope that LydiaSyft will be used and extended by various communities that are closely connected to \(\textsc {ltl}_f\) synthesis, such as reactive synthesis, AI planning, and task planning in robotics.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
, where \({ tt }\) is the tautology, \(a \in Prop\) is an atom,
(Next) and \(\mathop {\mathcal {U}}\) (Until) are temporal operators. We make use of standard Boolean abbreviations, e.g., \( ff \equiv \lnot { tt }\), \(\vee \) (or) and \(\rightarrow \) (implies), \( true \) and \( false \). In addition, we define the following abbreviations: Weak Next
, Eventually \(\Diamond \varphi \equiv true \mathop {\mathcal {U}}\varphi \) and Always \(\Box \varphi \equiv false \mathop {\mathcal {R}}\varphi \), where \(\mathop {\mathcal {R}}\) is for Release. The detailed semantics of \(\textsc {ltl}_f\) can be found in [12]. It is shown that, for every \(\textsc {ltl}_f\) formula \(\varphi \), one can construct a Deterministic Finite Automaton (DFA) that accepts exactly the same language as the \(\textsc {ltl}_f\) formula [12]. Notably, an \(\textsc {ltl}_f\) formula can be transformed into an equivalent DFA in at most 2EXPTIME [12].
