${\textsc {ltl}}_f$ Synthesis Under Environment Specifications for Reachability and Safety Properties

Abstract

In this paper, we study ${\textsc {ltl}}_f$ synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time.

1 Introduction

Synthesis under environment specifications consists of synthesizing an agent strategy (aka plan or program) that realizes a given task against all possible environment responses (i.e., environment strategies). The agent has some indirect knowledge of the possible environment strategies through an environment specification, and it will use such knowledge to its advantage when synthesizing its strategy [2, 4, 9, 24]. This problem is tightly related to planning in adversarial nondeterministic domains [20], as discussed, e.g., in [10, 15].

In this paper, we study synthesis under environment specifications, considering both agent task specifications and environment specifications expressed in Linear Temporal Logic on finite traces (${\textsc {ltl}}_f$). These are logics that look at finite traces or finite prefixes of infinite traces. For concreteness, we focus on ${\textsc {ltl}}_f$  [16, 17], but the techniques presented here extend immediately to other temporal logics on finite traces, such as Linear Dynamic Logics on finite traces, which is more expressive than ${\textsc {ltl}}_f$  [16], and Pure-Past ltl, which has the same expressiveness as ltl but evaluates a trace backward from the current instant [11].

Linear temporal logics on finite traces provide a nice embodiment of the notable triangle among Logics, Automata, and Games [21]. These logics are full-fledged logics with high expressiveness over finite traces, and they can be translated into classical regular finite state automata; moreover, they can be further converted into deterministic finite state automata (dfas). This transformation yields a game represented on a graph. In this game, one can analyze scenarios where the objective is to reach certain final states. Finally, despite the fact that producing a dfa corresponding to an ${\textsc {ltl}}_f$ formula can require double-exponential time, the algorithms involved—generating alternating automata (linear), getting the nondeterministic one (exponential), determinizing it (exponential), solving reachability games (poly)—are particularly well-behaved from the practical computational point of view [26, 28, 32].

In this paper, however, we consider ${\textsc {ltl}}_f$ specifications in two contexts which we denote as

$$ \exists \varphi \text { and } \forall \varphi \text { with } \varphi \text { an arbitrary } \textsc {ltl}_f \text { formula}. $$

The first one specifies a reachability property: there exists a finite prefix $\pi _{<k}$ of an infinite trace $\pi$ such that $\pi _{<k} \models \varphi$. This is the classical use of ${\textsc {ltl}}_f$ to specify synthesis tasks [17]. The second one specifies a safety property: every finite prefix $\pi _{<k}$ of an infinite trace $\pi$ is such that $\pi _{<k} \models \varphi$. This is the classical use of ${\textsc {ltl}}_f$ to specify environment behaviours [1, 13]. The formulas $\forall \varphi$ and $\exists \varphi$ with $\varphi$ in ${\textsc {ltl}}_f$ capture exactly two well-known classes of ltl properties in Manna and Pnueli’s Temporal Hierarchy [23]. Specifically, $\exists \varphi$ captures the co-safety properties and $\forall \varphi$ captures the safety properties (in [23], expressed respectively as $\Diamond \psi$ and $\Box \psi$ with $\psi$ an arbitrary Pure-Past ltl formulas, which consider only past operators.)

We let $\mathsf{{Env}}$ and $\mathsf{{Task}}$ denote an environment specification and a task specification, respectively, consisting of a safety ($\forall \varphi$) and/or reachability property ($\exists \varphi$). This gives rise to 12 possible cases: 3 without any environment specifications, 3 with safety environment specifications ($\forall \varphi$), 3 with reachability environment specifications ($\exists \varphi$), and 3 with both safety and reachability environment specifications ($\exists \varphi \wedge \forall \varphi$). For each of these, we provide an algorithm, which is optimal wrt the complexity of the problem, and prove its correctness. When the problem was already solved in literature, we give appropriate references (e.g., $\mathsf{{Task}} = \exists \varphi$ and $\mathsf{{Env}} = true$ is classical ${\textsc {ltl}}_f$ synthesis, solved in [17]). In fact, we handle all the cases involving reachability in the environment specifications by providing a novel algorithm that solves the most general case of $\mathsf{{Env}} = \exists \varphi _1 \wedge \forall \varphi _2$ and $\mathsf{{Task}} = \exists \varphi _3 \wedge \forall \varphi _4$¹.

These algorithms use the common building blocks (combining them in different ways): the construction of the dfas of the ${\textsc {ltl}}_f$ formulas, Cartesian products of such dfas, considering these dfas as the game arena and solving games for reachability/safety objectives. Also, all these problems have a 2EXPTIME-complete complexity. The hardness comes from ${\textsc {ltl}}_f$ synthesis [17], and the membership comes from the ${\textsc {ltl}}_f$-to-dfa construction, which dominates the complexity since computing the Cartesian products and solving reachability/safety games is polynomial². Towards the actual application of our algorithms, we observe that although the dfas of ${\textsc {ltl}}_f$ formulas are worst-case double-exponential, there is empirical evidence showing that the determinization of nfa, which causes one of the two exponential blow-ups, is often polynomial in the nfa  [27, 28, 32]. Moreover, in several notable cases, e.g., in all DECLARE patterns [29], the dfas are polynomial in the ${\textsc {ltl}}_f$ formulas, and so are our algorithms.

2 Preliminaries

Traces. For a finite set $\Sigma$, let $\Sigma ^\omega$ (resp. $\Sigma ^+,\Sigma ^*$) denote the set of infinite strings (resp. non-empty finite strings, finite strings) over $\Sigma$. We may write concatenation of sets using $\cdot$, e.g., $\Sigma \cdot \Sigma$ denotes the set of strings over $\Sigma$ of length 2. The length of a string is denoted $|\pi |$, and may be infinite. Strings are indexed starting at 0. For a string $\pi$ and $k \in \textrm{IN}$ with $k < |\pi |$, let $\pi _{<k}$ denote the finite prefix of $\pi$ of length k. For example, if $\pi = \pi _0 \pi _1 \ldots \pi _n$, then $|\pi |=n+1$ and $\pi _{<2} = \pi _0 \pi _1$. Typically, $\Sigma$ will be the set of interpretations (i.e., assignments) over a set $\textit{Prop}$ of atomic propositions, i.e., $\Sigma = 2^{\textit{Prop}}$. Non-empty strings will also be called traces.

Linear-Time Temporal Logic on Finite Traces. ${\textsc {ltl}}_f$ is a variant of Linear-time temporal logic (ltl) interpreted over finite, instead of infinite, traces [16]. Given a set $\textit{Prop}$ of atomic propositions, ${\textsc {ltl}}_f$ formulas $\varphi$ are defined by the following grammar: where $p \in \textit{Prop}$ denotes an atomic proposition, is read next, and $\mathop {\mathcal {U}}$ is read until. We abbreviate other Boolean connectives and operators.

For a finite trace $\pi \in (2^\textit{Prop})^+$, an ${\textsc {ltl}}_f$ formula $\varphi$, and a position i ($0 \le i < |\pi |$), define $\pi , i \models \varphi$ (read “$\varphi$ holds at position i”) by induction, as follows:

• $\pi , i \models p \ \text {iff}\ p \in \pi _i$ (for $p\in \textit{Prop}$);

• $\pi , i \models \lnot \varphi \ \text {iff}\ \pi , i \not \models \varphi$;

• $\pi , i \models \varphi _1 \wedge \varphi _2 \ \text {iff}\ \pi , i \models \varphi _1 \ \text {and}\ \pi , i \models \varphi _2$;

• ;

• $\pi , i \models \varphi _1 \mathop {\mathcal {U}}\varphi _2$ iff for some $j~(i\le j < |\pi |)$, $\pi ,j \models \varphi _2$, and for all $k~(i\le k < j), \pi , k \models \varphi _1$.

We write $\pi \models \varphi$, if $\pi ,0 \models \varphi$ and say that $\pi$ satisfies $\varphi$. Write $\mathcal {L}(\varphi )$ for the set of finite traces over $\Sigma = 2^{\textit{Prop}}$ that satisfy $\varphi$. In addition, we define the weak next operator . Note that: is not, in general, logically equivalent to , but we have that .

Domains. A domain (aka transition system, aka arena) is a tuple $\mathcal {D}= (\Sigma , Q, \iota , \delta )$, where $\Sigma$ is a finite alphabet, Q is a finite set of states, $\iota \in Q$ is the initial state, $\delta : Q \times \Sigma \rightarrow Q$ is a transition function. For an infinite string $w = w_0 w_1 w_2 \ldots \in \Sigma ^\omega$ a run of $\mathcal {D}$ on w is a sequence $r = q_0 q_1 q_2 \ldots \in Q^\omega$ that $q_0 = \iota$ and $q_{i+1} \in \delta (q_i, w_i)$ for every i with $0 \le i$. A run of $\mathcal {D}$ on a finite string $w = w_0 w_1 \ldots w_n$ over $\Sigma$ is a sequence $q_0 q_1 \cdots q_{n+1}$ such that $q_0 = \iota$ and $q_{i+1} \in \delta (q_i,w_i)$ for every i with $0 \le i < n+1$. Note that every string has exactly one run of $\mathcal {D}$.

Deterministic Finite Automaton (DFA). A DFA is a tuple $\mathcal {M}= (\mathcal {D},F)$ where $\mathcal {D}$ is a domain and $F \subseteq Q$ is a set of final states. A finite word w over $\Sigma$ is accepted by $\mathcal {M}$ if the run of $\mathcal {M}$ on w ends in a state of F. The set of all such finite strings is denoted $\mathcal {L}(\mathcal {M})$, and is called the language of $\mathcal {M}$.

Theorem 1

[17] Every ${\textsc {ltl}}_f$ formula $\varphi$ over atoms $\textit{Prop}$ can be translated into a dfa $\mathcal {M}_\varphi$ over alphabet $\Sigma = 2^{\textit{Prop}}$ such that for every finite string $\pi$ we have that $\pi \in \mathcal {L}(\mathcal {M})$ iff $\pi \models \varphi$. This translation takes time double-exponential in the size of $\varphi$.

Properties of Infinite Strings. A property is a set P of infinite strings over $\Sigma$, i.e., $P \subseteq \Sigma ^{\omega }$. We say that P is a reachability property if there exists a set $T \subseteq \Sigma ^+$ of finite traces such that if $w \in P$ then some finite prefix of w is in T. We say that P is a safety property if there exists a set $T \subseteq \Sigma ^+$ of finite traces such that if $w \in P$, then every finite prefix of w is in T. It is worth noting that the complement of a reachability property is a safety property, and vice versa.

An ${\textsc {ltl}}_f$ formula can be used to denote a reachability (resp., safety) property over $\Sigma = 2^\textit{Prop}$ as follows.

Definition 1

For an ${\textsc {ltl}}_f$ formula $\varphi$, let $\exists \varphi$ denote set of traces $\pi$ such that some finite prefix of $\pi$ satisfies $\varphi$, and let $\forall \varphi$ denote set of traces $\pi$ such that every finite (non-empty) prefix of $\pi$ satisfies $\varphi$.

Note that $\exists \varphi$ denotes a reachability property, and $\forall \varphi$ denotes a safety property. From now on, “prefix” will mean “finite non-empty prefix”. Note also that for an ${\textsc {ltl}}_f$ formula, $\mathcal {L}(\varphi )$ is a set of finite traces. On the other hand, $\mathcal {L}(\exists \varphi )$ (and similarly $\mathcal {L}(\psi )$ where $\psi$ is a Boolean combination of formulas of the form $\exists \varphi$ for ${\textsc {ltl}}_f$ formulas $\varphi$) is a set of infinite traces. In this paper, we consider $\exists \varphi$, $\forall \varphi$, and $\exists \varphi \wedge \forall \varphi$ to specify both agent tasks and environment behaviours.

Deterministic Automata on Infinite Strings (da). Following the automata-theoretic approach in formal methods, we will compile formulas to automata. We have already seen that we can compile ${\textsc {ltl}}_f$ formulas to dfas. We now introduce automata over infinite words to handle certain properties of infinite words. A deterministic automaton (da, for short) is a tuple $\mathcal {A}= (\mathcal {D},\alpha )$ where $\mathcal {D}$ is a transition system, say with the state set Q, and $\alpha \subseteq Q^\omega$ is called an acceptance condition. An infinite string w is accepted by $\mathcal {A}$ if its run is in $\alpha$. The set of all such infinite strings is denoted $\mathcal {L}(\mathcal {A})$, and is called the language of $\mathcal {A}$.

We consider reachability (${\text {reach}}$) and safety (${\text {safe}}$) acceptance conditions, parameterized by a set of target states $T \subseteq Q$:

• ${\text {reach}} (T) = \{ q_0 q_1 q_2 \ldots \in Q^\omega \mid \exists k \ge 0: q_k \in T\}$. In this case, we call $\mathcal {A}$ a reachability automaton.

• ${\text {safe}} ( T)= \{ q_0 q_1 q_2 \ldots \in Q^\omega \mid \forall k \ge 0: q_k \in T\}$. In this case, we call $\mathcal {A}$ a safety automaton.

Remark 1

Every reachability (resp. safety) property expressible in ltl is the language of a reachability automaton (resp. safety automaton) [16, 22, 25].

3 Problem Description

Reactive Synthesis. Reactive Synthesis (aka Church’s Synthesis) is the problem of turning a specification of an agent’s task and of its environment into a strategy (aka policy). This strategy can be employed by the agent to achieve its task, regardless of how the environment behaves. In this framework, the agent and the environment are considered players in a turn-based game, in which players move by picking an evaluation of the propositions they control. Thus, we partition the set $\textit{Prop}$ of propositions into two disjoint sets of propositions $\mathcal {X}$ and $\mathcal {Y}$, and with a little abuse of notation, we denote such a partition as $\textit{Prop} = \mathcal {Y}\cup \mathcal {X}$. Intuitively, the propositions in $\mathcal {X}$ are controlled by the environment, and those in $\mathcal {Y}$ are controlled by the agent. In this work (in contrast to the usual setting of reactive synthesis), the agent moves first. The agent moves by selecting an element of $2^\mathcal {Y}$, and the environment responds by selecting an element of $2^\mathcal {X}$. This is repeated forever, and results in an infinite trace (aka play). From now on, unless specified otherwise, we let $\Sigma = 2^{\textit{Prop}}$ and $\textit{Prop} = \mathcal {Y}\cup \mathcal {X}$. We remark that the games considered in this paper are games of perfect information with deterministic strategies.

An agent strategy is a function $\sigma _ \mathsf{{ag}} :(2^{\mathcal {X}})^* \rightarrow 2^{\mathcal {Y}}$. An environment strategy is a function $\sigma _{\textsf {env}}:(2^\mathcal {Y})^+ \rightarrow 2^\mathcal {X}$. A strategy $\sigma$ is finite-state (aka finite-memory) if it can be represented as a finite-state input/output automaton that, on reading an element h of the domain of $\sigma$, outputs the action $\sigma (h)$. A trace $\pi = (Y_0 \cup X_0) (Y_1 \cup X_1) \dots \in (2^{\mathcal {Y}\cup \mathcal {X}})^\omega$ follows an agent strategy $\sigma _ \mathsf{{ag}} : (2^\mathcal {X})^* \rightarrow 2^\mathcal {Y}$ if $Y_0 = \sigma _ \mathsf{{ag}} (\epsilon )$ and $Y_{i+1} = \sigma _ \mathsf{{ag}} (X_0X_1\ldots X_i)$ for every $i \ge 0$, and it follows an environment strategy $\sigma _{\textsf {env}}$ if $X_i = \sigma _{\textsf {env}}(Y_0 Y_1 \ldots Y_i)$ for all $i \ge 0$. We denote the unique infinite sequence (play) that follows $\sigma _ \mathsf{{ag}}$ and $\sigma _{\textsf {env}}$ as . Let P be a property over the alphabet $\Sigma = 2^\textit{Prop}$, specified by formula or da. An agent strategy $\sigma _ \mathsf{{ag}}$ (resp., environment strategy $\sigma _{\textsf {env}}$) enforces P if for every environment strategy $\sigma _{\textsf {env}}$ (resp., agent strategy $\sigma _ \mathsf{{ag}}$), we have that $\textsf {play}(\sigma _ \mathsf{{ag}} ,\sigma _{\textsf {env}})$ is in P. In this case, we write $\sigma _{ \mathsf{{ag}} } \rhd P$ (resp. $\sigma _{\textsf {env}}\rhd P$). We say that P is agent (resp., environment) realizable if there is an agent (resp. environment) strategy that enforces P.

Synthesis Under Environment Specifications. Typically, an agent has some knowledge of how the environment works, represented as a fully observable model of the environment, which it can exploit to enforce its task [2]. Formally, let $\mathsf{{Env}}$ and $\mathsf{{Task}}$ be properties over alphabet $\Sigma = 2^{\textit{Prop}}$, denoting the environment specification and the agent task, respectively.

Note that while the agent task $\mathsf{{Task}}$ denotes the set of desirable traces from the agent’s perspective, the environment specification $\mathsf{{Env}}$ denotes the set of environment strategies that describe how the environment reacts to the agent’s actions (no matter what the agent does) in order to enforce $\mathsf{{Env}}$. Specifically, $\mathsf{{Env}}$ is treated as a set of traces when we reduce the problem of synthesis under environment specification to standard reactive synthesis.

We require a consistency condition of $\mathsf{{Env}}$, i.e., there must exist at least one environment strategy $\sigma _{\textsf {env}}\rhd \mathsf{{Env}}$. An agent strategy $\sigma _ \mathsf{{ag}}$ enforces $\mathsf{{Task}}$ under the environment specification $\mathsf{{Env}}$, written $\sigma _ \mathsf{{ag}} \ \rhd _ \mathsf{{Env}} \mathsf{{Task}}$, if for all $\sigma _{\texttt {env}}\ \rhd \mathsf{{Env}}$ we have that $\textsf {play}(\sigma _ \mathsf{{ag}} ,\sigma _{\texttt {env}})\models \mathsf{{Task}}$. Note that if $\mathsf{{Env}} = \textit{true}$ then this just says that $\sigma _ \mathsf{{ag}}$ enforces $\mathsf{{Task}}$ (i.e., the environment specification is missing).

Definition 2

(Synthesis under environment specifications). Let $\mathsf{{Env}}$ and $\mathsf{{Task}}$ be properties over alphabet $\Sigma = 2^{\textit{Prop}}$, denoting the environment specification and the agent task, respectively. (i) The realizability under environment specifications problem asks, given $\mathsf{{Task}}$ and $\mathsf{{Env}}$, to decide if there exists an agent strategy enforcing $\mathsf{{Task}}$ under the environment specification $\mathsf{{Env}}$. (ii) The synthesis under environment specifications problem asks, given $\mathsf{{Task}}$ and $\mathsf{{Env}}$, to return a finite-state agent strategy enforcing $\mathsf{{Task}}$ under the environment specification $\mathsf{{Env}}$, or say that none exists.

In [2] is shown that for any linear-time property³, synthesis under environment specifications can be reduced to synthesis without environment specifications. Thus, in order to show that $\mathsf{{Task}}$ is realizable under $\mathsf{{Env}}$ it is sufficient to show that $\mathsf{{Env}} \rightarrow \mathsf{{Task}}$ is realizable. Moreover, to solve the synthesis problem for $\mathsf{{Task}}$ under $\mathsf{{Env}}$, it is enough to return a strategy that enforces $\mathsf{{Env}} \rightarrow \mathsf{{Task}}$.

Table 1. Task and Env considered. Note that, from Alg. 7 we get the remaining cases involving reachability environment specifications by suitably setting $\varphi _1, \varphi _2,\varphi _4$ to true.

In the rest of the paper, we provide a landscape of algorithms for ${\textsc {ltl}}_f$ synthesis considering reachability and safety properties for both agent tasks and environment specifications. However, these synthesis problems are complex and challenging due to the combination of reachability and safety properties. To tackle this issue, one possible approach is to reduce ${\textsc {ltl}}_f$ synthesis problems to ltl synthesis problems through suitable translations, e.g., [12, 14, 30, 31]. However, there is currently no methodology for performing such translations when considering combinations of reachability and safety properties⁴. Additionally, synthesis algorithms for ltl specifications are generally more challenging than those for ${\textsc {ltl}}_f$ specifications, both theoretically and practically [13, 14, 30, 31]. In this paper, we show that for certain combinations, we can avoid the detour to ltl synthesis and keep the simplicity of ${\textsc {ltl}}_f$ synthesis. Specifically, we consider that $\mathsf{{Task}}$ and $\mathsf{{Env}}$ take the following forms: $\exists \varphi _1, \forall \varphi _1, \exists \varphi _1 \wedge \forall \varphi _2$ where the $\varphi _i$ are ${\textsc {ltl}}_f$ formulas, and in addition we consider the case of no environment specification (formally, $\mathsf{{Env}} = \textit{true}$). This results in 12 combinations. Algorithms 1–7, listed in Table 1, optimally solve all the combinations. All these algorithms adopt some common building blocks while linking them in different ways.

Theorem 2

Let each of Task and Env be of the forms $\forall \varphi$, $\exists \varphi$, or $\exists \varphi _1 \wedge \forall \varphi _2$. Solving synthesis for an agent Task under environment specification Env is 2EXPTIME-complete.

4 Building Blocks for the Algorithms

In this section, we describe the building blocks we will use to devise the algorithms for the problem described in the previous section.

DAs for $\exists \varphi$ and $\forall \varphi$. Here, we show how to build the da whose language is exactly the infinite traces satisfying $\exists \varphi$ (resp. $\forall \varphi$). The first step is to convert the ${\textsc {ltl}}_f$ formula $\varphi$ into a dfa $\mathcal {M}_\varphi = (\Sigma , Q, \iota , \delta , F)$ that accepts exactly the finite traces that satisfy $\varphi$ as in Theorem 1. Then, to obtain a da $\mathcal {A}_{\exists \varphi }$ for $\exists \varphi$ define $\mathcal {A}_{\exists \varphi } = (2^{\mathcal {X}\cup \mathcal {Y}}, Q, \iota , \delta , {\text {reach}} (F))$. It is immediate that $\mathcal {L}(\exists \varphi ) = \mathcal {L}(\mathcal {A}_{\exists \varphi })$. To obtain a da $\mathcal {A}_{\forall \varphi }$ for $\forall \varphi$ define $\mathcal {A}_{\forall \varphi } =(2^{\mathcal {X}\cup \mathcal {Y}}, Q , \iota , \delta , {\text {safe}} (F \cup \{\iota \}))$.

The reason $\iota$ is considered a part of the safe set is that the dfa $\mathcal {M}_{\varphi }$ does not accept the empty string since the semantics of ${\textsc {ltl}}_f$ precludes this. It is immediate that $\mathcal {L}(\forall \varphi ) = \mathcal {L}(\mathcal {A}_{\forall \varphi })$. For $\psi \in \{\exists \varphi , \forall \varphi \}$, we let $\textsc {ConvertDA}(\psi )$ denote the resulting da.

Lemma 1

Let $\varphi$ be an ${\textsc {ltl}}_f$ formula, and let $\psi \in \{\exists \varphi , \forall \varphi \}$. Then the languages $\mathcal {L}(\psi )$ and $\mathcal {L}(\textsc {ConvertDA}(\psi ))$ are equal.

For formulas of the form $\forall \varphi$ we will suppress the initial state in the objective and so $\textsc {ConvertDA}(\forall \varphi )$ will be written $(\mathcal {D}_{\forall \varphi },{\text {safe}} (T))$, i.e., T contains $\iota$.

Games over da. The synthesis problems we consider in this paper are solved by reducing them to two-player games. We will represent games by das $\mathcal {A}= (\mathcal {D},\alpha )$ where $\mathcal {D}$ is a transition system, sometimes called an ‘arena’, and $\alpha$ is an acceptance condition, sometimes called a ‘winning condition’. The game is played between an agent (controlling $\mathcal {Y}$) and environment (controlling $\mathcal {X}$). Intuitively, a position in the game is a state $q \in Q$. The initial position is $\iota$. From each position, first the agent moves by setting $Y \in 2^\mathcal {Y}$, then the environment moves by setting $X \in 2^\mathcal {X}$, and the next position is updated to the state $\delta (q,Y \cup X)$. This interaction results in an infinite run in $\mathcal {D}$, and the agent is declared the winner if the run is in $\alpha$ (otherwise, the environment is declared the winner).

Definition 3

An agent strategy $\sigma _ \mathsf{{ag}}$ is said to win the game $(\mathcal {D},\alpha )$ if for every trace $\pi$ that follows $\sigma _ \mathsf{{ag}}$, the run in $\mathcal {D}$ of $\pi$ is in $\alpha$.

In other words, $\sigma _ \mathsf{{ag}}$ wins the game if every trace $\pi$ that follows $\sigma _ \mathsf{{ag}}$ is in $L(\mathcal {D},\alpha )$. For $q \in Q$, let $\mathcal {D}_q$ denote the transition system $\mathcal {D}$ with initial state q, i.e., $\mathcal {D}_q = (\Sigma , Q, q, \delta )$. We say that q is a winning state for the agent if there is an agent strategy that wins the game $(\mathcal {D}_q,\alpha )$; in this case, the strategy is said to win starting from q.

In the simplest settings, we represent agent strategies as functions of the form $f_ \mathsf{{ag}} : Q \rightarrow 2^\mathcal {Y}$, called positional strategies. An agent positional strategy $f_ \mathsf{{ag}}$ induces an agent strategy, $\sigma _ \mathsf{{ag}} = \textsc {Strategy}(\mathcal {D}_q,f_{ \mathsf{{ag}} })$, as follows: define $\sigma _ \mathsf{{ag}} (\epsilon ) = f_ \mathsf{{ag}} (q)$, and for every finite trace $\pi$ let $\rho$ be the run of $\mathcal {D}_q$ on $\pi$ (i.e., starting in state q), and define $\sigma _ \mathsf{{ag}} (\pi ) = f_ \mathsf{{ag}} (q')$ where $q'$ is the last state in $\rho$ (i.e., $q' = \rho _{|\pi |}$). In more complex settings, e.g., in the Algorithm 7, we will construct functions of the form $f_ \mathsf{{ag}} : Q \cdot (2^\mathcal {Y}\cdot 2^\mathcal {X}\cdot Q)^* \rightarrow 2^\mathcal {Y}$, which similarly induce agent strategies $\textsc {Strategy}(\mathcal {D}_q,f_ \mathsf{{ag}} )$ where for every finite trace $\pi = Y_0 \cup X_0, \cdots , Y_k \cup X_k$, and run $q_0, \cdots , q_{k+1}$ of $\pi$ in $\mathcal {D}_q$, define $\sigma _ \mathsf{{ag}} (\pi ) = f_ \mathsf{{ag}} (q_0, Y_0 \cup X_0, q_1, Y_1 \cup X_1, \cdots , q_{k+1})$. Below the agent strategy $\sigma _ \mathsf{{ag}} = \textsc {Strategy}(\mathcal {D}_q,f_{ \mathsf{{ag}} })$ returned by the various algorithms will be finite state, in the sense that it is representable as a transducer. For simplicity, with a little abuse of notation, we will return directly $\sigma _ \mathsf{{ag}}$, instead of its finite representation as a transducer.

Dual definitions can be given for the environment, with the only notable difference being that $f_{\textsf {env}}:Q \times 2^X \rightarrow 2^\mathcal {Y}$ since the moves of the environment depend also on the last move of the agent (since the agent moves first).

In this paper, besides the terms ‘environment’ and ‘agent’, we also consider the terms ‘protagonist’ and ‘antagonist’. If the da $(\mathcal {D},\alpha )$ is a specification for the agent, then the agent is called the protagonist and the environment is called the antagonist. On the other hand, if the da $(\mathcal {D},\alpha )$ is a specification for the environment, then the environment is called the protagonist, and the agent is called the antagonist. Intuitively, the protagonist is trying to make sure that the generated traces are in $\mathcal {L}(\mathcal {D}, \alpha )$, and the antagonist to make sure that the generated traces are not in $\mathcal {L}(\mathcal {D}, \alpha )$. Define $\textsf{Win}_p$ (resp. $\textsf{Win}_a$) as the set of states $q \in Q$ such that q is a protagonist (resp. antagonist) winning state. This set is called protagonist’s (resp. antagonist) winning region. In this paper, all our games (including reachability and safety games) are determined. Therefore:

Lemma 2

For every state $q \in Q$, it holds that $q \in \textsf{Win}_p$ iff $q \notin \textsf{Win}_a$.

The problem of solving a game $(\mathcal {D}, \alpha )$ for the protagonist is to compute the winning region $\textsf{Win}_p$ and a function $f_p$ such that $\textsc {Strategy}(\mathcal {D},f_p)$ wins from every state in $\textsf{Win}_p$⁵. To do this, we will also sometimes compute a winning strategy for the antagonist (that wins starting in its winning region).

Solving Reachability Games and Safety Games. We repeatedly make use of solutions to reachability games and safety games given by das $\mathcal {A}$. Thus, for a protagonist $p \in \{ \mathsf{{ag}} ,{\textsf {env}}\}$ let $\textsc {Solve}_p(\mathcal {A})$ denote the procedure for solving the game $\mathcal {A}$, i.e., p is trying to ensure the play is in $\mathcal {L}(\mathcal {A})$; this procedure returns the protagonist’s winning region $\textsf{Win}_p$ and a function $f_p$ such that $\textsc {Strategy}(\mathcal {D},f_p)$ wins starting from every state in $\textsf{Win}_p$ [19].

Product of Transition Systems. Let $\mathcal {D}_i$ ($1 \le i \le k$) be transition systems over alphabet $\Sigma$. Their product, denoted $\textsc {Product}(\mathcal {D}_1,\cdots ,\mathcal {D}_k),$ is the transition system $\mathcal {D}= (\Sigma ,Q,\iota ,\delta )$ defined as follows: (i) The alphabet is $\Sigma$. (ii) The state set is $Q = Q_1 \times \cdots \times Q_k$. (iii) The initial state is $\iota = (\iota _1, \cdots , \iota _k)$. (iv) The transition function $\delta$ maps a state $(q_1,\cdots ,q_k)$ on input $z \in \Sigma$ to the state $(q'_1,\cdots ,q'_k)$ where $q'_i = \delta _i(q_i,z)$ ($1 \le i \le k$). Also, the lift of a set $F_i \subseteq Q_i$ to $\mathcal {D}$ is the set $\{(q_1,\cdots ,q_k) : q_i \in F_i\} \subseteq Q$.

Restriction of a Transition System. The restriction of a transition system, defined as the procedure $\textsc {Restriction}(\mathcal {D}, S)$, restricts $\mathcal {D}= (\Sigma , Q, \iota , \delta )$ to $S \subseteq Q$ is the transition system $\mathcal {D}'= (\Sigma , S \cup \{sink\}, \iota , \delta ', \alpha ')$ where for all $z \in \Sigma$, $\delta '(sink,z) = sink$, $\delta '(q,z) = \delta (q,z)$ if $\delta (q,z) \in S$, and $\delta '(q,z) = sink$ otherwise. Intuitively, $\mathcal {D}'$ redirect all transitions from S that leave S to a fresh sink state. We may denote the sink by $\bot$⁶.

5 Reachability Tasks, No Env Spec

Algorithm 1 solves the realizability and synthesis for the case of reachability tasks and no environment specification. Formally, $\mathsf{{Task}}$ is of the form $\exists \varphi$ where $\varphi$ is an ${\textsc {ltl}}_f$ formula, and $\mathsf{{Env}} = \textit{true}$. This problem is solved in [17], but here we rephrase the problem in our notation.

Theorem 3

Algorithm 1 solves the synthesis under environment specifications problem with $\mathsf{{Task}} = \exists \varphi , \mathsf{{Env}} = \textit{true}$, where $\varphi$ is an ${\textsc {ltl}}_f$ formula.

6 Safety Tasks, No Env Spec

Algorithm 2 handles the case $\mathsf{{Task}}$ is of the form $\forall \varphi$ where $\varphi$ is an ${\textsc {ltl}}_f$ formula, and $\mathsf{{Env}} = \textit{true}$. We can use the result in [17] to solve the synthesis for $\forall \varphi$ from the point of view of the environment.

Theorem 4

Algorithm 2 solves the synthesis under environment specifications problem with $\mathsf{{Task}} = \forall \varphi , \mathsf{{Env}} = \textit{true}$, where $\varphi$ is an ${\textsc {ltl}}_f$ formula.

7 Reachability and Safety Tasks, No Env Spec

Algorithm 3 handles the case that $\mathsf{{Task}}$ is of the form $\exists \varphi _1 \wedge \forall \varphi _2$ where $\varphi _1$ and $\varphi _2$ are ${\textsc {ltl}}_f$ formulas, and $\mathsf{{Env}} = \textit{true}$.

Intuitively, the algorithm proceeds as follows. First, it computes the corresponding da for $\forall \varphi _2$ and solves the safety game over it. The resulting winning area represents the set of states from which the agent has a strategy to realize its safety task. Then, it restricts the game area to the agent’s winning area. Finally, it solves the reachability game over the game product of the corresponding da of $\exists \varphi _1$ and the remaining part of the da for $\forall \varphi _2$.

In order to obtain the final strategy for the agent we need to refine the strategy $\textit{f}_ \mathsf{{ag}}$ to deal with the sink state, call it $\bot _2$, and combine it with $g_ \mathsf{{ag}}$. Given $f_ \mathsf{{ag}}$ computed in Line 3, define $f''_ \mathsf{{ag}} :Q_1 \times (S_2 \cup \{\bot _2\}) \rightarrow 2^\mathcal {Y}$ over $\mathcal {D}$ by $f_ \mathsf{{ag}} ''(q,s) = f_ \mathsf{{ag}} (s)$ if $s \in S_2$, and $f_ \mathsf{{ag}} ''(q,s) = Y$ (for some arbitrary Y) otherwise. In words, $f_ \mathsf{{ag}} ''$ ensures the second component stays in $S_2$ (and thus in $T_2$). Recall that $g_ \mathsf{{ag}}$ over $\mathcal {D}$ ensures that $T_1$ is reached in the first co-ordinate, while at the same time maintaining the second co-ordinate is in $S_2$. Finally, let $\textsc {Combine}(\mathcal {D}, R, g_ \mathsf{{ag}} ,f_ \mathsf{{ag}} )$ denote the final strategy $h_ \mathsf{{ag}} : Q_1 \times (S_2 \cup \{\bot _2\}) \rightarrow 2^\mathcal {Y}$ defined as follows: $h_ \mathsf{{ag}} ((q,s))=g_ \mathsf{{ag}} ((q,s))$ if $(q,s) \in R$, and $h_ \mathsf{{ag}} ((q,s))=f_ \mathsf{{ag}} ''((q,s))$ otherwise. Intuitively, the agent following $h_ \mathsf{{ag}}$ will achieve the reachability goal while staying safe, whenever this is possible, and stays safe otherwise.

Theorem 5

Algorithm 3 solves synthesis under environment specifications problem with $\mathsf{{Task}} = \exists \varphi _1 \wedge \forall \varphi _2, \mathsf{{Env}} = \textit{true}$, where the $\varphi _i$ are ${\textsc {ltl}}_f$ formulas.

8 Reachability Tasks, Safety Env Specs

Algorithm 4 handles the case that $\mathsf{{Task}}$ is of the form $\exists \varphi _1$ and $\mathsf{{Env}} = \forall \varphi _2$, where $\varphi _1, \varphi _2$ are ${\textsc {ltl}}_f$ formulas. A similar problem of this case was solved in [13], which, more specifically, considers only finite safety of the agent, i.e., the agent is required to stay safe until some point (the bound is related to an additional agent reachability task), and thus can actually be considered as reachability.

Intuitively, the algorithm first computes all the environment strategies that can enforce $\mathsf{{Env}} = \forall \varphi _2$ [7], represented as a restriction of the da for $\forall \varphi _2$, as in the previous section. Then, based on restricting the game arena on these environment strategies, the algorithm solves the reachability game over the product of the corresponding da of $\exists \varphi _1$ and the restricted part of the da for $\forall \varphi _2$.

Theorem 6

Algorithm 4 solves the synthesis under environment specifications problem with $\mathsf{{Task}} = \exists \varphi _1, \mathsf{{Env}} = \forall \varphi _2$, where the $\varphi _i$ are ${\textsc {ltl}}_f$ formulas.

9 Safety Tasks, Safety Env Specs

Algorithm 5 handles the case that $\mathsf{{Task}}$ is of the form $\forall \varphi _1$ and $\mathsf{{Env}} = \forall \varphi _2$, where $\varphi _1, \varphi _2$ are ${\textsc {ltl}}_f$ formulas.

Intuitively, the algorithm proceeds as follows. First, it computes the corresponding da for $\forall \varphi _2$ and solves the safety game for the environment over it. The resulting winning area represents the set of states, from which the environment has a strategy to enforce the environment specification $\mathcal {L}(\forall \varphi _2)$. It is worth noting that restricting the da to considering only such winning area, in fact, captures all the environment strategies that enforce $\mathcal {L}(\forall \varphi _2)$ [7]. Based on the restriction, the algorithm solves the safety game over the product of the corresponding da of $\forall \varphi _1$ and the remaining part of the da for $\forall \varphi _2$.

Theorem 7

Algorithm 5 solves the synthesis under environment specifications problem with $\mathsf{{Task}} = \forall \varphi _1, \mathsf{{Env}} = \forall \varphi _2$, where the $\varphi _i$ are ${\textsc {ltl}}_f$ formulas.

10 Reachability and Safety Tasks, Safety Env Specs

Algorithm 6 handles the case that $\mathsf{{Task}}$ is of the form $\exists \varphi _1 \wedge \forall \varphi _2$ and $\mathsf{{Env}} = \forall \varphi _3$, where $\varphi _1, \varphi _2, \varphi _3$ are ${\textsc {ltl}}_f$ formulas. As mentioned in the previous section, a similar problem of this case that considers only finite safety of the agent was solved in [13] by reducing $\mathsf{{Task}}$ to reachability properties only. Instead, we provide here an approach to the synthesis problem considering infinite agent safety.

Intuitively, the algorithm proceeds as follows. Following the algorithms presented in the previous sections, it first computes all the environment strategies that can enforce $\mathsf{{Env}} = \varphi _3$, represented as a restriction of the da for $\forall \varphi _3$. Then, based on restricting the game arena on these environment strategies, the algorithm solves the safety game for the agent over the product of the corresponding da of $\forall \varphi _2$ and the restricted part of the da for $\forall \varphi _3$. This step is able to capture all the agent strategies that can realize $\forall \varphi _2$ under environment specification $\forall \varphi _3$. Next, we represent all these agent strategies by restricting the product automaton to considering only the computed agent winning states, thus obtaining $\mathcal {D}'$. Finally, the algorithm solves the reachability game over the product of the corresponding da of $\exists \varphi _1$ and $\mathcal {D}'$. In order to abstract the final strategy for the agent, it is necessary to combine the two agent strategies: one is from the safety game for enforcing $\forall \varphi _2$ under $\forall \varphi _3$, the other one is from the final reachability game for enforcing $\exists \varphi _1$ while not violating $\forall \varphi _2$ under $\forall \varphi _3$.

Theorem 8

Algorithm 6 solves synthesis under environment specifications problem with $\mathsf{{Task}} = \exists \varphi _1 \wedge \forall \varphi _2, \mathsf{{Env}} = \forall \varphi _3$, where the $\varphi _i$ are ${\textsc {ltl}}_f$ formulas.

11 Reachability and Safety Tasks and Env Specs

Algorithm 7 handles the case that $\mathsf{{Env}} = \forall \varphi _1 \wedge \exists \varphi _2$ and $\mathsf{{Task}} = \exists \varphi _3 \wedge \forall \varphi _4$ by solving synthesis for the formula $\mathsf{{Env}} \rightarrow \mathsf{{Task}}$ [2], i.e., for $(\exists \lnot \varphi _1 \vee \forall \lnot \varphi _2) \vee (\exists \varphi _3 \wedge \forall \varphi _4).$ Note that, from the general case, we get all cases involving reachability environment specifications by suitably setting $\varphi _1, \varphi _2$ or $\varphi _4$ to true. We remark that for the case $\varphi _4 = \textit{true}$ in which the safety and reachability specifications are presented in the safety-fragment and co-safety fragment of ltl is solved in [10].

We first define two constructions that will be used in the algorithm. Given a transition system $\mathcal {D}= (\Sigma , Q, \iota , \delta )$ and a set of states $T \subseteq Q$, define $\textsc {Flagged}(\mathcal {D}, T)$ to be the transition system that, intuitively, records whether a state in T has been seen so far. Formally, $\textsc {Flagged}(\mathcal {D}, T)$ returns the transition system $D^f = (\Sigma , Q^f, \iota ^f, \delta ^f)$ defined as follows: 1. $Q^f = Q \times \{yes,no\}$. 2. $\iota ^f = (\iota ,b)$, where $b = no$ if $\iota \not \in T$, and $b = yes$ if $\iota \in T$. 3. $\delta ^f((q,b),z) = (q',b')$ if $\delta (q,z)=q'$ and one of the following conditions holds: (i) $b = b' = yes$, (ii) $b = b' = no, q' \not \in T$, (iii) $b = no, b' = yes, q' \in T$. Given a transition system $\mathcal {D}= (\Sigma , Q, \iota , \delta )$ and disjoint subsets $V_0,V_1$ of Q, define $\textsc {RestrictionWithSinks}(\mathcal {D},V_0,V_1)$ to be the transition system on state set $V_0$ that, intuitively, behaves like $\mathcal {D}$ on $V_0$, transitions from $V_0$ to $V_1$ are redirected to a new sink state $\bot$, and transitions from $V_0$ to $Q \setminus (V_0 \cup V_1)$ are redirected to a new sink state $\top$. Formally, $\textsc {RestrictionWithSinks}(\mathcal {D},V_0,V_1)$ is the transition system $(\Sigma , \hat{Q}, \hat{\iota }, \hat{\delta })$ defined as follows: 1. $\hat{Q} = V_0 \cup \{\top ,\bot \}$. 2. $\hat{\iota } = \iota$. 3. $\hat{\delta }(q, z) = \delta (q, z)$ if $\delta (q, z) \in V_0$. Otherwise, define $\hat{\delta }(q,z) = \bot$ if $\delta (q, z) \in V_1$, and $\hat{\delta }(q,z) = \top$ if $\delta (q, z) \in Q \setminus (V_0 \cup V_1)$.

Intuitively, at Line 10, $S_2$ will form part of the agent’s winning region since from here ${\text {safe}} (T_2)$ can be ensured. At Line 12, $R_3$ will also form part of the agent’s winning region since from $R_3$ in $\mathcal {D}'$ ${\text {reach}} (T_3) \cap {\text {safe}} (T_4)$ can be ensured. In the following steps, we identify remaining ways that the agent can win, intuitively by maintaining $T_2 \cap T_4$ either forever (in which case ${\text {safe}} (T_2)$ is ensured), or before the state leaves $T_2 \cap T_4$ either (i) it is in $S_2$ or $R_3$ (in which case we proceed as before), or otherwise (ii) it is in $S_4$ (but not in $S_2$ nor in $R_3$) and has already seen $T_3$ (in which case ${\text {reach}} (T_3) \cap {\text {safe}} (T_4)$ can be ensured).

At the end of the algorithm, we combine the four strategies $f^1_ \mathsf{{ag}} , f^2_ \mathsf{{ag}} , f^3_ \mathsf{{ag}}$ and $f^4_ \mathsf{{ag}}$ through procedure $\textsc {Combine}(\mathcal {D}^f,$ $f^1_ \mathsf{{ag}} , f^2_ \mathsf{{ag}} , f^3_ \mathsf{{ag}} , f^4_ \mathsf{{ag}} , R_1,S_2,R_3,E)$ to obtain the final strategy $f_ \mathsf{{ag}} : (Q^f)^+ \rightarrow 2^\mathcal {Y}$ as follows. For every history $h \in (Q^f)^+$, if the history ever enters $R_1$ then follow $f^1_ \mathsf{{ag}}$, ensuring ${\text {reach}} (T_1)$, otherwise, writing q for the start state of h: 1. if $q \in S_2$ then use $f^2_ \mathsf{{ag}}$, which ensures ${\text {safe}} (T_2)$; 2. if $q \in R_3$ then use $f^3_ \mathsf{{ag}}$ until $T_3$ is reached and thereafter use $f^4_ \mathsf{{ag}}$, which ensures ${\text {safe}} (T_4) \cap {\text {reach}} (T_3)$; 3. if $q \in E$ then use $f^e_ \mathsf{{ag}}$ while the states are in E, ensuring ${\text {safe}} (T_2)$ if play stays in E; if ever, let $q'$ be the first state in the history that is not in E; by construction, this corresponds to $\top$ in $\mathcal {D}^f$ and thus is (i) in $S_2$ or (ii) in $R_3$, and so proceed as before, or else (iii) in $(S_4 \setminus T_2) \setminus (R_3 \cup S_2)$ (which can be simplified to $S_4 \setminus (R_3 \cup T_2)$) with flag value yes in which case switch to strategy $f^4_ \mathsf{{ag}}$. Intuitively, case (i) ensures ${\text {safe}} (T_2)$, and cases (ii) and (iii) each ensure ${\text {safe}} (T_4) \cap {\text {reach}} (T_3)$; 4. and if none of these, then make an arbitrary move. Note that in spite of being a function of the whole history, $f_ \mathsf{{ag}}$ can be represented by a finite-state transducer. So in the Algorithm 7, as before, with a little abuse of notation we write directly $\sigma _ \mathsf{{ag}} = \textsc {Strategy}(\mathcal {D}^f, f_ \mathsf{{ag}} )$, to mean that we return its representation as a transducer.

Theorem 9

  Algorithm 7 solves the synthesis under environment specifications problem with $\mathsf{{Task}} = \exists \varphi _3 \wedge \forall \varphi _4$ and $\mathsf{{Env}} = \forall \varphi _1 \wedge \exists \varphi _2$, where $\varphi _i$ are ${\textsc {ltl}}_f$ formulas.

Comparison to Algorithms 1–6. Note that Algorithm 7 can solve the other six variants by suitably instantiating some of $\varphi _1, \varphi _2, \varphi _3, \varphi _4$ to true. Nevertheless, Algorithm 7 is much more sophisticated than Algorithms 1–6. Hence, in this paper, we present the algorithms deductively, starting with simpler variants and moving to the most difficult. Furthermore, instantiating Algorithm 7 does not always give the same algorithms as Algorithms 1–6. For instance, Algorithm 1 for the synthesis problem of $\mathsf{{Task}} = \exists \varphi$ (no environment specification) can be obtained from Algorithm 7 by setting $\varphi _1, \varphi _2, \varphi _4$ to true, but we cannot get Algorithm 4 for the synthesis problem of $\mathsf{{Env}} = \forall \varphi$ and $\mathsf{{Task}} = \exists \psi$ in this way. This is because Algorithm 7 solves the synthesis problem by reducing to $\mathsf{{Env}} \rightarrow \mathsf{{Task}}$ [2], but Algorithm 4 directly disregards all environment strategies that cannot enforce $\mathsf{{Env}}$ by first solving a safety game for the environment on $\mathsf{{Env}}$ and removing all the states that do not belong to the environment winning region to get a smaller game arena, hence obtaining optimal complexity. Analogously, in Algorithm 3 for the synthesis problem of $\mathsf{{Env}} = true$ and $\mathsf{{Task}} = \exists \varphi _1 \wedge \forall \varphi _2$, we also first disregard all the agent strategies that are not able to enforce $\forall \varphi _2$, obtaining a smaller game arena for subsequent computations, hence getting an optimal complexity in practice compared to constructing the game arena considering the complete state space from the DA of $\forall \varphi _2$.

12 Conclusion

In this paper, we have studied the use of reachability and safety properties based on ${\textsc {ltl}}_f$ for both agent tasks and environment specifications. As mentioned in the introduction, though we have specifically focused on ${\textsc {ltl}}_f$, all algorithms presented here can be readily applied to other temporal logics on finite traces, such as Linear Dynamic Logics on finite traces (${\textsc {ldl}}_f$), which is more expressive than ${\textsc {ltl}}_f$  [16], and Pure-Past ltl  [11], as long as there exists a technique to associate formulas to equivalent dfas.

It is worth noting that all the cases studied here are specific Boolean combinations of $\exists \varphi$. It is of interest to indeed devise algorithms to handle arbitrary Boolean combinations. Indeed, considering that ${\textsc {ltl}}_f$ is expressively equivalent to pure-past ltl, an arbitrary Boolean combination of $\exists \varphi$ would correspond to a precise class of ltl properties in Manna & Pnueli’s Temporal Hierarchy [23]: the so-called obligation properties. We leave this interesting research direction for future work.

Another direction is to consider best-effort synthesis under assumptions for Boolean combinations of $\exists \varphi$, instead of (ordinary) synthesis under assumptions, in order to handle ignorance the agent has about the environment [3, 5, 6, 8, 18].