by Shufang Zhu

Reactive synthesis can be viewed as a game between the $environment$ and the $agent$, where the agent tries to achieve its task with respect to environment moves. Here we consider agent tasks expressed in LTL$_f$. Intuitively, environment specifications are constraints on the environment that rule out certain environment behaviors. A key observation is that even if we consider an agent with LTL$_f$ tasks on finite traces, environment specifications need to be expressed over infinite traces since accomplishing the agent tasks may require an unbounded number of environment actions. To solve synthesis concerning finite-trace LTL$_f$ tasks under infinite-trace specifications, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTL$_f$ and LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTL$_f$ synthesis. In this article, we first review the advances in LTL$_f$ synthesis and then show that when concerning environment specifications expressed in LTL, we can avoid the detour to LTL synthesis and keep the simplicity of LTL$_f$ synthesis in interesting cases. Furthermore, we can still partially avoid this detour even when the environment specifications are expressed in full LTL.

LTL and LTL$_f$

LTL is one of the most popular specification language for expressing temporal properties [1]. Given a set of propositions $Prop$, the formulas of LTL are generated by the following grammar: \(\varphi ::= p \mid (\varphi_1 \wedge \varphi_2) \mid (\neg \varphi) \mid (\circ \varphi) \mid (\varphi_1 U \varphi_2)\) where $p \in Prop$. We use common abbreviations for $eventually$ $\Diamond \varphi \equiv true U \varphi$ and $always$ $\Box \varphi \equiv \lnot \Diamond \lnot \varphi$.

LTL formulas are interpreted over infinite traces $\pi \in (2^{Prop})^\omega$. A $trace$ $\pi = \pi_0\pi_1\ldots$ is a sequence of propositional interpretations (sets), where for every $i \geq 0$, $\pi_i \in 2^{Prop}$ is the $i$-th interpretation of $\pi$. Intuitively, $\pi_i$ is interpreted as the set of propositions that are $true$ at instant $i$. Given $\pi$, we define when an LTL formula $\varphi$ $holds$ at position $i$, written as $\pi, i \models \varphi$, inductively on the structure of $\varphi$, as follows:

  • $\pi, i \models p \text{ iff } p \in \pi_i\nonumber$ (for $p\in{Prop}$);
  • $\pi, i \models \varphi_1 \land \varphi_2 \text{ iff } \pi, i \models \varphi_1 \text{ and } \pi, i \models \varphi_2\nonumber$;
  • $\pi, i \models \lnot \varphi \text{ iff } \pi, i \not\models \varphi\nonumber$;
  • $\pi, i \models \circ\varphi \text{ iff } \pi,i+1 \models \varphi$;
  • $\pi, i \models \varphi_1 U \varphi_2 \text{ iff }$ there exists $j \geq i$ such that $\pi,j \models\varphi_2$, and for all $k, i\le k < j$ we have that $\pi, k \models \varphi_1$.

We say $\pi$ $satisfies$ $\varphi$, written as $\pi \models \varphi$, if $\pi,0 \models \varphi$.

LTL$_f$ is a variant of LTL interpreted over $finite~traces$, instead of infinite traces [2]. The syntax of LTL$_f$ is the same as the syntax of LTL. We define $\pi, i \models \varphi$, stating that $\varphi$ holds at position $i$, as for LTL, except that for the temporal operators we have:

  • $\pi, i \models \circ \varphi \text{ iff } i< last(\pi)$ and $\pi,i+1 \models \varphi$;
  • $\pi, i \models \varphi_1 U \varphi_2$ iff there exists $j$ such that $i \leq j \leq last(\pi)$ and $\pi,j \models\varphi_2$, and for all $k, i\le k < j$ we have that $\pi, k \models \varphi_1$.

where $last(\pi)$ denotes the last position (i.e., index) in the finite trace $\pi$. In addition, we define the $weak~next$ operator $\bullet$ as abbreviation of $\bullet \varphi \equiv \neg \circ \neg \varphi$. Note that, over finite traces, $\neg \circ \varphi \equiv \circ \neg \varphi$ does not hold anymore, instead it holds that $\neg \circ \varphi \equiv \bullet \neg \varphi$. We say that a trace $satisfies$ an LTL$_f$ formula $\varphi$, written as $\pi \models \varphi$, if $\pi, 0 \models \varphi$.

Reactive Synthesis

Reactive synthesis can be viewed as a game between the $environment$ and the $agent$, contrasting each other by controlling two disjoint sets of variables $\mathcal{X}$ and $\mathcal{Y}$, respectively. The goal of reactive synthesis is to synthesize an agent strategy such that no matter how the environment behaves, the combined trace from two players satisfy desired properties [3].

An environment strategy is a function $\gamma: (2^\mathcal{Y})^+ \to 2^\mathcal{X}$, and an agent strategy is a function $\sigma: (2^{\mathcal{X}})^* \to 2^\mathcal{Y}$. A trace $\pi = (X_0 \cup Y_0) (X_1 \cup Y_1) \dots \in (2^{\mathcal{X} \cup \mathcal{Y}})^\omega$, is $compatible$ with an environment strategy $\gamma$ if $\gamma(Y_0) = X_0$ and $\gamma(Y_0Y_1\ldots Y_i) = X_{i}$ for every $i$. A trace $\pi$ being compatible with an agent strategy $\sigma$ is defined analogously. Sometimes, we write $\sigma(\pi^k)$ instead of $\sigma(X_0 X_1 \cdots X_k)$ for simplicity. We denote the unique infinite sequence that is compatible with $\gamma$ and $\sigma$ as $\pi(\sigma, \gamma)$.

LTL$_f$ Synthesis

The $synthesis~problem$ for an agent task specified as an LTL$_f$ formula $\varphi$ is to find an agent strategy $\sigma: (2^\mathcal{X})^* \to 2^{\mathcal{Y}}$ such that for every environment strategy $\gamma: (2^\mathcal{Y})^+ \to 2^{\mathcal{X}}$, there exists $k \geq 0$, chosen by the agent, such that the finite trace $\pi(\sigma, \gamma)^k \models \varphi$ i.e., $\varphi$ is agent realizable.

Backward Synthesis Techniques

The first solution to LTL$_f$ synthesis problem was based on a reduction to reachability game [4], which proceeds as follows: build the corresponding DFA of the agent task $\varphi$, solve the reachability game over it, and hence return the winning strategy for the agent. However, the size of the constructed DFA can be, in the worst case, doubly-exponential in the size of the formula. In order to combat this difficulty, we proposed a symbolic LTL$_f$ synthesis framework, which essentially represents the DFA as Boolean formulas [5]. Hence, the reachability game can be solved on the symbolic DFA. Moreover, the symbolic DFA is pratically represented in Binary Decision Diagrams (BDDs) [6]. The reachability game is performed on BDDs as well. This symbolic LTL$_f$ synthesis framework is also integrated in state-of-the-art LTL$_f$ synthesizers, e.g., Lisa [7] and Lydia [8]. The main difficulty of this approach is that it requires computing the entire DFA of the LTL$_f$ specification, hence cannot avoid the worst-case double-exponential blowup. Hence, even though the backward fixpoint computation can be performed symbolically, enabling scalable performance, the DFA construction step can become a significant bottleneck [5].

  • Related tool: Syft [5].

Forward Synthesis Techniques

In order to combat the worst-case double-exponential blowup, we investigated LTL$_f$ forward synthesis adopting an AND-OR graph search that is able to create on-the-fly the DFA corresponding to the LTL$_f$ specification [9]. This technique avoids a detour to automata theory and instead builds directly deterministic transitions from a current state. In particular, this technique exploits LTL formula progression [10,11] to separate what happens now (label) and what should happen next accordingly (successor state). Crucially, we exploit the structure that formula progression provides to branch on propositional formulas (representing several evaluations), instead of individual evaluations. This drastically reduces the branching factor of the AND-OR graph to be searched (recall that in LTL$_f$ synthesis, both the agent choices and the environment choices can be exponentially many). More specifically, we label transitions/edges with propositional formulas on propositions controlled by the agent (for OR-nodes) and by the environment (for AND-nodes). Every such propositional formula captures a set of evaluations leading to the same successor node. We leverage Knowledge Compilation (KC) techniques, and in particular Sentential Decision Diagrams (SDDs) [12], to effectively generate such propositional formulas for OR-nodes and AND-nodes, and thus reduce the branching factor of the search space.

  • Related tool: Cynthia [9]

LTL$_f$ Synthesis Under Environment Specifications

In standard synthesis, the agent assumes the environment to be free to choose an arbitrary move at each step, but in AI often the agent has some knowledge of how the environment works, which it can exploit in order to enforce the goal, specified as an LTL$_f$ formula $\varphi$. Here, we specify the environment behaviour by an LTL formula $env$ and call it $environment~specification$ [4,13,14].

Given an LTL formula $env$, we say that an agent strategy (resp. environment strategy) $enforces$ $\varphi$, written $\sigma \ \rhd \ env$ (resp., $\gamma \ \rhd \ env$), if for every environment strategy $\gamma$ (resp. agent strategy $\sigma$), we have $trace(\sigma,\gamma) \models \varphi$. This LTL formula $env$, in particular, specifies the set of environment strategies that enforces $env$. As usual, we require that $env$ must be $environment~realizable$, i.e., the set of environment strategies that enforce $env$ is nonempty.

The problem of synthesis under environment specifications is to find an agent strategy $\sigma$ such that

\[\forall \gamma \ \rhd env, trace(\sigma,\gamma)^k \models \varphi \text{ for some } k \in \mathcal{N}.\]

As shown in [13], this can be reduced to solving the synthesis problem for the implication $env \to ltl(\varphi)$, with $ltl(\varphi)$ being a suitable LTL$_f$-to-LTL transformation [2]. However, LTL synthesis problem is 2EXPTIME-complete [3]. Furthermore, the algorithms available for LTL synthesis are much harder in practice than those for LTL$_f$ synthesis. In particular, the lack of efficient algorithms for the crucial step of automata determinization is a major obstacle for scalable implementations [15]. In spite of several advancements in synthesis, such as reducing to parity games [16], bounded synthesis based on solving iterated safety games [17], or recent techniques based on iterated FOND planning [18], LTL synthesis remains challenging.

In the following, we show the solutions of LTL$_f$ synthesis under LTL environment specifications for different types of environment specifications, which allow us to avoid the detour to LTL synthesis and keep the simplicity of LTL$_f$ synthesis. Furthermore, we can still partially avoid this detour even when the environment specifications are expressed in full LTL.

Stability and Fairness Environment Specifications

We consider here two different basic forms of environment specifications: a basic form of fairness $\Box \Diamond \alpha$ (always eventually $\alpha$), and a basic form of stability $\Diamond \Box \alpha$. Note that in both cases the truth value of $\alpha$ is under the control of the environment. Hence the environment specification $env$ is indeed environment realizable, i.e. the set of environment stratgies that enforce $env$ is not empty. The key idea of solving such problems is integrating the environment specification as the winning condition of the reduced game between the environment and the agent [19].

The algorithm proceeds as follows. First, translate the LTL$_f$ formula $\varphi$ into a DFA $D$. Then, in case of fairness environment specifications, solve the fair DFA game on $D$, in which the environment (resp. the agent) winning condition is to remain in a region (resp., to avoid the region) where $\alpha$ holds infinitely often, meanwhile the accepting states are forever avoidable, by applying a nested fixed-point computation on $D$. Similarly, in case of stability environment specifications, solve the stable \DFA game on $D$, in which the environment (resp. the agent) winning condition is to reach a region (resp., to avoid the region) where $\alpha$ holds forever, meanwhile the accepting states are forever avoidable, by applying a nested fixed-point computation.

  • Related tool: FSyft [19], StSyft [19].

Generalized-Reactivity (1) Specifications

There have been great successes with LTL synthesis on the Generalized-Reactivity (1), or GR(1), approach: focusing on a significant syntatic fragment of LTL that uses safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness. We brought it together with the successes on LTL$_f$ synthesis devising an approach to solve LTL$_f$ synthesis of agent task $\varphi$ under GR(1) environment specification $env_{gr1}$ [20]. In more details, to solve the problem, we first observe that the agent’s goal is to satisfy $\neg env_{gr1} \vee \varphi$, while the environment’s goal is to satisfy $env_{gr1} \land \neg \varphi$. Moreover, we know that $\varphi$ can be represented by a DFA [2]. Then, focusing on the environment point of view, we show that the problem of LTL$_f$ synthesis under GR(1) environment specification can be reduced into a GR(1) game, in which the game arena is the complement of the DFA for $\varphi$, i.e., a deterministic safety automaton expressing safety conditions, and $env_{gr1}$ is the GR(1) winning condition. Since we want a winning strategy for the agent, we need to deal with the complement of the GR(1) game to obtain a winning strategy for the antagonist. We can also enrich the synthesis problem by adding safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of synthesis. Observe though that there is a difference between the safety conditions on the environment and those on the agent: the first must hold forever, while the second must hold until the agent task is terminated, i.e., the LTL$_f$ formula $\varphi$ is fulfilled. The enriched problem can also be reduced to a GR(1) game, where the game arena consists of the DFAs for the environment safety condition, the agent safety condition, and the agent task.

  • Related tool: GFSynth [20].

General LTL Environment Specifications

Regarding LTL$_f$ synthesis with general LTL environment specifications, dealing with LTL synthesis seems to be unavoidable. Nevertheless, we developed a two-stage technique that maximizes the simplicity of LTL$_f$ synthesis and mitages the difficulty of LTL synthesis [21]. Intuitively, the two-stage technique first solely deals with the agent task, LTL$_f$ formula $\varphi$, and thus confines the difficulty of handling the LTL environment specification $env$ to the bare minimum in the second stage. In details, the two-stage techniques proceeds as follows:

  • Stage 1: Build the DFA $D$ of $\varphi$ and solve the reachability game for the agent over $D$. If the agent has a winning strategy $\sigma$ in $D$ then the algorithm returns $\sigma$. Otherwise, continue to Stage 2.
  • Stage 2: Perform the following steps:
    1. Remove from $D$ the agent winning region, obtaining $D’$;
    2. Build the Deterministic Parity Automaton (DPA) $P$ of $env$ and get the product of $D’$ and $P$, obtaining a new DPA $A = D’ \times P$, and solve the parity game for the environment over $A$;
    3. If the agent has a winning strategy in $A$, then the synthesis problem is realizable and hence return the agent winning strategy as a combination of the agent winning strategies in the two stages.
  • Related tool: 2SLS [21].

Conclusion and Future Research

Reactive synthesis on LTL$_f$ has been an exciting research problem. Our work on this problem spans from standard LTL$_f$ synthesis to synthesis concerning environment specifications with efficient solution techniques. In the future, we would like to consider environment specifications expressed in different languages, e.g., PDDL [22], a popular specification language in planning. Furthermore, planning is highly related to synthesis since both concern games between the environment and the agent. One advantage of utilizing PDDL is that the corresponding state space obtained from PDDL only leads to a single-exponential blowup [23] instead of double-exponential as LTL. An interesting question is how to better integrate the synergies of PDDL expressed planning and LTL/LTL$_f$ synthesis.

References

[1] Amir Pnueli: The Temporal Logic of Programs. FOCS 1977: 46-57

[2] Giuseppe De Giacomo, Moshe Y. Vardi: Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. IJCAI 2013: 854-860

[3] Amir Pnueli, Roni Rosner: On the Synthesis of a Reactive Module. POPL 1989: 179-190

[4] Giuseppe De Giacomo, Moshe Y. Vardi: Synthesis for LTL and LDL on Finite Traces. IJCAI 2015: 1558-1564

[5] Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi: Symbolic LTLf Synthesis. IJCAI 2017: 1362-1369

[6] Randal E. Bryant: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Comput. Surv. 24(3): 293-318 (1992)

[7] Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi: Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications. AAAI 2020: 9766-9774

[8] Giuseppe De Giacomo, Marco Favorito: Compositional Approach to Translate LTL$_f$/LDL$_f$ into Deterministic Finite Automata. ICAPS 2021: 122-130

[9] Giuseppe De Giacomo, Marco Favorito, Jianwen Li, Moshe Y. Vardi, Shengping Xiao, Shufang Zhu: LTL$_f$ Synthesis as AND-OR Graph Search: Knowledge Compilation at Work. IJCAI 2022: 2591-2598

[10] E. Allen Emerson: Temporal and Modal Logic. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990: 995-1072

[11] Fahiem Bacchus, Froduald Kabanza: Planning for Temporally Extended Goals. Ann. Math. Artif. Intell. 22(1-2): 5-27 (1998) 1996

[12] Adnan Darwiche: SDD: A New Canonical Representation of Propositional Knowledge Bases. IJCAI 2011: 819-826

[13] Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, Sasha Rubin: Planning under LTL Environment Specifications. ICAPS 2019: 31-39

[14] Giuseppe De Giacomo, Antonio Di Stasio, Giuseppe Perelli, Shufang Zhu: Synthesis with Mandatory Stop Actions. KR 2021: 237-246

[15] Bernd Finkbeiner: Synthesis of Reactive Systems. Dependable Software Systems Engineering 2016: 72-98

[16] Philipp J. Meyer, Salomon Sickert, Michael Luttenberger: Strix: Explicit Reactive Synthesis Strikes Back! CAV (1) 2018: 578-586

[17] Carsten Gerstacker, Felix Klein, Bernd Finkbeiner: Bounded Synthesis of Reactive Programs. ATVA 2018: 441-457

[18] Alberto Camacho, Christian J. Muise, Jorge A. Baier, Sheila A. McIlraith: LTL Realizability via Safety and Reachability Games. IJCAI 2018: 4683-4691

[19] Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y. Vardi: LTL$_f$ Synthesis with Fairness and Stability Assumptions. AAAI 2020: 3088-3095

[20] Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, Shufang Zhu: Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis. IJCAI 2021: 1852-1858

[21] Giuseppe De Giacomo, Antonio Di Stasio, Moshe Y. Vardi, Shufang Zhu: Two-Stage Technique for LTLf Synthesis Under LTL Assumptions. KR 2020: 304-314

[22] Drew McDermott, Malik Ghallab, Adele Howe, Craig Knoblock, Ashwin Ram, Manuela Veloso, Daniel Weld, and David Wilkins. PDDL – The PDDL Planning Domain Definition Language. The AIPS-98 Planning Competition Committee, 1998

[23] Jussi Rintanen: Complexity of Planning with Partial Observability. ICAPS 2004: 345-354

Updated:

LinkedIn