Safraless LTL synthesis considering maximal realizability

Open systems interact continuously with the external environment. When applied to real problems, they must often be highly reliable. These systems are modeled as reactive systems. Linear Temporal Logic (LTL) synthesis is a formal method for checking the realizability [1, 34, 35] of a behavioral specification described in LTL [33] and for automatically composing a reactive system realizing the specification if it is realizable. This method can effectively obtain a reliable system because it does not have a phase that introduces bugs.

In traditional LTL synthesis, if a given LTL specification is unrealizable, we must refine it in LTL. One approach for refining an unrealizable LTL specification \(\varphi \) is to add or strengthen the assumptions \(\psi \) regarding the environment, such that a refined specification \(\psi \rightarrow \varphi \) is realizable. In [14], Chatterjee et al. proposed a method for computing some of these assumptions. However, the computed assumptions are not logical formulae in their naive method and may be difficult to understand intuitively. Additionally, it may be unallowable in a practical sense. Hagihara et al. [25] introduced a method for efficiently extracting an assumption to make a given specification strong satisfiable, where strong satisfiability [31] is a necessary condition of realizability. The extracted assumption is the weakest LTL formula in a certain class and easy to understand. Li et al. [30] provided a method for finding an allowable assumption to make a given specification realizable, where the assumption is mined from given LTL templates. Even if we obtain \(\psi \), we must consider many things when synthesizing a reactive system from \(\psi \rightarrow \varphi \). A system synthesized from \(\psi \rightarrow \varphi \) may stop trying to satisfy \(\varphi \) after an unexpected input that violates \(\psi \), i.e., it may be intolerant [26]. Moreover, such a system may violate \(\psi \) against the wishes of its environment. In [7], Bloem et al. discussed how to deal with environmental assumptions and surveyed existing approaches.

One approach is to weaken some of the partial specifications that cause the unrealizability of the whole specification, \(\varphi =\bigwedge _{\varphi _i \in \varPhi } \varphi _i\). In this approach, we first find a subset of these partial specifications, i.e., \(\varPhi ' \subseteq \varPhi \) such that \(\bigwedge _{\varphi _i \in \varPhi '} \varphi _i\) is unrealizable. In [24], Hagihara et al. proposed a method for finding minimal strongly unsatisfiable subsets of specifications. Even if we find these partial specifications, it is difficult (but preferable) to obtain a refined specification that is realizable and close to the original. The intention of an original partial specification might not be preserved in the refined specification. Hence, handling specification re-refinements associated with changes to the original specifications is difficult.

A whole reactive system specification usually consists of some sub-specifications. If the whole specification is unrealizable, we first try to refine some of the sub-specifications before we drastically reconsider the whole specification. We can divide the specifications into: must specifications, which should never be violated, and desirable specifications, the violation of which may be unavoidable. More precisely, the sub-specifications have a priority order, and each sub-specification may be violated if it competes with other higher-priority sub-specifications. Must specifications have the highest priority, and hence they should never be violated.

In this paper, we propose a method for synthesizing a reactive system that realizes all given must specifications and endeavors to satisfy the given desirable specifications as much as possible considering their priorities.

In the endeavor, we consider it is reasonable that a desirable specification has no assumption. This is because the system is attempting as best as possible, regardless of whether an assumption holds, even though the best effort will depend on the assumption. The general form of the specifications without assumptions is a \(\mathbf{G }\)-formula \(\mathbf{G }\varphi \) which means “\(\varphi \) always holds”, i.e., “\(\varphi \) holds at every step during an infinite-step interaction with the environment”. In our approach, the best effort at satisfying \(\mathbf{G }\varphi \) maximizes the number of steps that satisfy \(\varphi \).

Therefore, we use a mean-payoff objective based on LTL formulae to quantitatively evaluate the number of steps. For each desirable specification \(\mathbf{G }\varphi _i\), we basically consider a positive payoff for each occurrence of a step that satisfies \(\varphi _i\) during an interaction. However, it is often difficult to strictly impose this payoff, because whether \(\varphi \) holds at a step generally depends on the entire subsequent behavior. \(\mathbf{G }\varphi _i\) can be under-approximated into a safety property by assigning a bound k to a universal co-Büchi word automaton (UCWA), which accepts words satisfying \(\mathbf{G }\varphi _i\). We then consider a negative payoff for occurrences of minimal bad prefixes of a safety property represented by a k-bounded UCWA [22] (k-UCWA) that rejects some of the words accepted by the unbounded UCWA. This approximation was inspired by the Safraless approach [8, 18, 22, 27, 28]. Our mean-payoff objective \({\textsf {MP}}(\sum _{1 \le i \le n} c_i \cdot t_i)\) is the limit inferior of averages for a sequence of weighted sums \(\sum _{1 \le i \le n} c_i \cdot t_i\) of payoffs \(t_i\) for desirable specifications \(\mathbf{G }\varphi _i\), considering weights \(c_i\) according to their priorities.

In our method, we first apply a UCWA-based Safraless method [8, 18, 22] to construct an under-approximated safety game from a must LTL specification \(\varphi \). We obtain a winning region \(\mathcal {W}\) on the game as a set of reactive systems realizing an under-approximation of \(\varphi \). Second, we construct mean-payoff games \(\mathcal {M}^{t_i}\) from atomic terms \(t_i\) in the mean-payoff objective \({\textsf {MP}}(\sum _{1 \le i \le n} c_i \cdot t_i)\), reusing the procedures in the Safraless method. Finally, we compose a reactive system as an optimal strategy on a weighted synchronized product of the region \(\mathcal {W}\) and the mean-payoff games \(\mathcal {M}^{t_1},\ldots ,\mathcal {M}^{t_n}\). An outline of our approach is depicted in Fig. 1.

Our method does not require any restriction for a must specification and hence can also deal with an assumption-guarantee type formula \(\psi \rightarrow \varphi \) as the must specification. In this case, our method produces a reactive system that realizes \(\psi \rightarrow \varphi \) and locally maximizes a given mean-payoff objective regardless of whether the environment follows the assumption \(\psi \).

In Sect. 2, we introduce some definitions and concepts concerning reactive systems, LTL, games, and Safraless synthesis. We define our mean-payoff objectives and show how to interpret desirable LTL specification in the mean-payoff objectives in Sect. 3. In Sect. 4, we describe our method for synthesizing a reactive system from a must LTL specification and a mean-payoff objective. We demonstrate the effectiveness of our method using some experiments in Sect. 5. Section 6 contains some information on related works, and Sect. 7 concludes the paper.

A reactive system models an open system that interacts continuously with an external environment. It cannot control a sequence of inputs from the environment and hence must choose an output at each step based on the history of the interaction thus far.

In this paper, we assume that an interaction starts with an output of the system.¹ Let \({ OAP}\) and \({ IAP}\) be disjoint sets of atomic propositions (or signals) for outputs and inputs controlled by the system and environment, respectively. The set of all atomic propositions, i.e., the union \({ IAP}\cup { OAP}\), is denoted by \({ AP}\).The interaction produced by \(\mathcal {R}\) for a sequence \(s=\alpha _{0_{}}^I \alpha _1^I \ldots \in (2^{{ IAP}})^{\omega }\) of inputs is denoted as \({ Intr}_s(\mathcal {R})\). That is, \({ Intr}_s(\mathcal {R}) = (\alpha _0^O \cup \alpha _0^I) (\alpha _1^O \cup \alpha _1^I) \cdots \), where \(\alpha _0^O = \mathcal {R}(\varepsilon )\) and \(\alpha _{i+1}^O = \mathcal {R}(\alpha _0^I \cdots \alpha _i^I)\) for each \(i \in \mathbb {N}\). A set \({ Intr}(\mathcal {R}) = \{{ Intr}_s(\mathcal {R}) \in (2^{{ AP}})^{\omega } \mid s \in (2^{{ IAP}})^{\omega }\}\) of possible interactions of \(\mathcal {R}\) is denoted by \({ Intr}(\mathcal {R})\).

Linear temporal logic [33] is a modal logic used to express temporal properties and is widely used to describe formal behavioral specifications of systems.

When the current state is v in \(V_0\) (resp., \(V_1\)), Player 0 (resp., Player 1) chooses its action \(\gamma \) in \(\varGamma _0\) (resp., \(\varGamma _0\)), and the state moves according to transition function \(E_0\) (resp., \(E_1\)). Let \(\sigma \in \{0,1\}\). If \(E_{\sigma }(v, \gamma ) = v'\), there is a transition to \(v'\) from v with \(\gamma \). If \(E_{\sigma }(v, \gamma )\) is undefined for some action \(\gamma \) (i.e., \(E_{\sigma }\) is a partial function), \(\gamma \) is unavailable on v. In this paper, we assume that all states have at least one available action; i.e., there is no dead-end state. We let \(E_{\sigma }\) be a set \(\{\langle v,\gamma ,v' \rangle \mid E_{\sigma }(v,\gamma )= v'\}\) of triples that represent transitions. For an available transition \(e = \langle v,\gamma ,v' \rangle \), its predecessor state v, successor state \(v'\), and action \(\gamma \) are denoted by \({ pred}(e)\), \({ succ}(e)\), and \({ act}(e)\), respectively.

A play \(\rho \) on \(\mathcal {G}\) is an infinite alternating sequence \(e_0 e_1 e_2 e_3 \cdots \in (E_0 E_1)^{\omega }\) of 0- and 1-transitions, where the starting state \({ pred}(e_0)\) is the initial state \(v_{{ init}}\). It is available if \({ succ}(e_i) = { pred}(e_{i+1})\) for each \(i \in \mathbb {N}\). A set of available plays on \(\mathcal {G}\) is denoted by \({ Play}(\mathcal {G})\).

An outcome of an available play is evaluated according to function \({ outcome}\). When the outcomes are in a binary set, an outcome is often interpreted as either win or loss. In this paper, we use two types of game: safety games and mean-payoff games.

Safraless synthesis [8, 18, 22, 27, 28] is a mainstream method for LTL synthesis.

The outline of a UCWA-based method [8, 18, 22] is given in Algorithm 1. For a given LTL formula \(\varphi \) on a set \({ AP}\) (\(= { IAP}\cup { OAP}\)) of atomic propositions, we first construct a UCWA \(\mathcal {A}^{\varphi }\) accepting \(\mathcal {L}(\varphi )\) (the procedure \(\texttt {LTL2UCWA\_translation}\) at Line 1) and initialize the bound k to 0 (Line 2). Let \(\mathcal {T}\) be an LTL-to-UCWA mapping implemented by LTL2UCWA_translation, i.e., \(\mathcal {A}^{\varphi }=\mathcal {T}({\varphi })\). We next derive an under-approximation to \(\mathcal {A}^{\varphi }\) using k and transform the under-approximated k-UCWA \(\mathcal {T}^k({\varphi })\) into a safety game \(\mathcal {S}^{\varphi ,k}\) (the procedure \(\texttt {BUCWA2SG\_transformation}\) at Line 4). This transformation consists of determinizing \(\mathcal {A}^{\varphi }\) and dividing its states/transitions into system-side and environment-side ones based on the respective sets \({ OAP}\) and \({ IAP}\) of output and input propositions. \(\mathcal {S}^{\varphi ,k}\) has characteristics described in Sect. 2.3.5. Additionally, the winning condition of \(\mathcal {S}^{\varphi ,k}\) corresponds to the under-approximated property \(\mathcal {L}(\mathcal {T}^k({\varphi }))\) of \(\varphi \). Therefore, if the system-side player wins for a play \(\rho \) on \(\mathcal {S}^{\varphi ,k}\), \({ trace}(\rho )\) satisfies \(\varphi \). Then we extract a winning region \(\mathcal {W}^{\varphi ,k}\) for the system-side player on \(\mathcal {S}^{\varphi ,k}\) (the \(\texttt {extract\_winning\_region}\) at Line 5). If the initial state of \(\mathcal {S}^{\varphi ,k}\) is in \(\mathcal {W}^{\varphi ,k}\) (Line 6), there exists a reactive system that realizes \(\varphi \). Otherwise, k is incremented (Line 9), and we repeat a loop from Line 3. Lines 1–10 check the realizability of \(\varphi \), and in practice the unrealizability of \(\varphi \) is also checked in parallel. Finally, we concretely compose a winning strategy \(\nu \) for the system-side player on \(\mathcal {W}^{\varphi ,k}\) (the procedure \(\texttt {winning\_strategy}\) at Line 11).

In this paper, we have omitted the details of the procedure. For simplicity, we assume that the subprocedure \(\texttt {BUCWA2SG\_transformation}\) produces a safety game \(\langle \langle V_0, V_1\), \(\Sigma _0, \Sigma _1,E_0, E_1 \rangle , v_{{ init}}, S \rangle \) such that \(E_0\) is total.

The general form of desirable specifications without assumptions is a \(\mathbf{G }\)-formula \(\mathbf{G }\varphi \). We consider that a preferable reactive system should endeavor to satisfy \(\varphi \) at each step, i.e., to maximize the number of steps satisfying \(\varphi \) to the extent possible.

We fit a mean-payoff to quantitatively evaluate the desirability if the payoff at each step depends on the importance of the desirable specifications \(\mathbf{G }\varphi \) and whether \(\varphi \) holds at the step. Therefore, we propose a mean-payoff objective, which covers the set of desirable specifications. We can optimize a reactive system using the mean-payoff objective, which quantitatively specifies the desirability of interactions with the environment.

We are left with the problem of determining whether \(\varphi \) holds at each step. If \(\varphi \) is bounded, we can determine if \(\varphi \) holds at a step using only the behavior of the next n-steps, where n is the depth of the next-operator \(\mathbf{X }\). That is, the length of a subsequence deciding whether \(\varphi \) holds at each step is less than \(n+1\). An example of when \(\varphi = a \rightarrow \mathbf{X }(b \mathbf{U }^{\le 1} c)\) is shown in Fig. 2. A mean-payoff value is preserved, even if every payoff at a step is given bounded steps later. Hence, it is easy to deal with a bounded LTL formula.

If \(\varphi \) is unbounded, we may need to know the entire behavior after a step to determine whether \(\varphi \) holds at the step. It is difficult to strictly apply an unbounded LTL formula, and hence we use the UCWA approximation. For a desirable specification \(\mathbf{G }\varphi \) and an LTL-to-UCWA mapping \(\mathcal {T}\), consider a b-UCWA \(\mathcal {T}^{b}(\mathbf{G }\varphi )\) that is obtained by giving bound b to UCWA \(\mathcal {T}(\mathbf{G }\varphi )\). An interaction satisfies \(\mathbf{G }\varphi \) if it has no minimal bad prefix of \(\mathcal {L}(\mathcal {T}^{b}(\mathbf{G }\varphi ))\) because \(\mathcal {L}(\mathcal {T}^{b}(\mathbf{G }\varphi )) \subseteq \mathcal {L}(\mathbf{G }\varphi )\). Based on the equivalence between \(\mathbf{G }\varphi \) and \(\mathbf{G }\mathbf{G }\varphi \), trying to avoid violating \(\mathbf{G }\varphi \) at each step can be considered as another attempt to satisfy \(\mathbf{G }\varphi \). In this sense, maximizing the average length (or minimizing the number) of the minimal bad prefixes occurring on interaction corresponds to the attempt. However, it is difficult to maximize strictly the average length. This is because they are overlapping, and their lengths are unbounded in general. Consider an example of an under-approximated safety property of \(\mathbf{G }(p_1 \rightarrow \mathbf{X }(p_2 \mathbf{U }p_3))\) is \(\mathbf{G }(p_1 \rightarrow \mathbf{X }(p_2 \mathbf{U }^{\le 1} p_3))\) and an interaction is \( \{p_1\} \{p_2\} \{p_1,p_3\} \{p_1,p_2\}\{p_2\}\{p_1,p_2\}\{p_1,p_3\} \emptyset \cdots \), as shown in Fig. 3. Figure 2 indicates that in this example only the third, fourth, and seventh occurrences of minimal bad prefixes play a role in the violation of \(\mathbf{G }(p_1 \rightarrow \mathbf{X }(p_2 \mathbf{U }^{\le 1} p_3))\). The others include them as suffixes. In this paper, we focus on the frequency of occurrences of non-overlapping ones, which is inversely proportional to the average length of them. That is, in Fig. 3, the first and sixth occurrences of minimal bad prefixes are counted and the others are not. The first (resp., sixth) occurrences can be considered as a representative subsequence among those that include the third (resp., seventh) one. We can roughly maximize the average length, by giving a negative payoff for each occurrence of non-overlapping ones and maximizing a mean-payoff under the setting.

We now introduce the syntax and semantics for mean-payoff objectives, based on the ideas in the previous subsection.

The syntax of mean-payoff objectives is defined, in a similar manner to [39], as follows.

Intuitively, \({\textsf {S}}(\chi )\) means that a payoff of 1 is given at a step if \(\chi \) holds at the step, i.e., \({\textsf {S}}(\chi )\) strictly captures whether \(\chi \) holds at the step. A value of \({\textsf {S}}(\chi )\) at a step depends on the behavior after the next n-steps, where n is the depth of \(\mathbf{X }\) in \(\chi \). However, \({\textsf {B}}^{b}(\varphi )\) means that a payoff of \(-1\) is given for each occurrence of minimal bad prefixes of \(\mathcal {L}(\mathcal {T}^{b}(\varphi ))\), where the overlapping of the prefixes is not considered. The value of \({\textsf {B}}^{b}(\varphi )\) at a step depends on the preceding behavior. The coefficient c of the product term \(c \cdot t\) is used as a weight that depends on the desirability of t. We abbreviate \(c \cdot {\textsf {S}}(\top )\) to c and \({\textsf {B}}^0(\varphi )\) to \({\textsf {B}}(\varphi )\).

Note that a \({\textsf {B}}\)-term \({\textsf {B}}^{b}(\varphi )\) should be treated attentively because the precise meaning of the \({\textsf {B}}\)-term depends on an LTL-to-automata translation \(\mathcal {T}\) that does not appear in the syntax. From only the syntax, it is impossible to understand the structure of \(\mathcal {T}(\varphi )\), and hence it is not clear what is lost in \(\mathcal {T}^{b}(\varphi )\). For example, a certain translator under-approximates \(\mathbf{G }\mathbf{F }p\) into \(\mathbf{G }\mathbf{F }^{\le b} p\), but another translator outputs \(\mathbf{G }\mathbf{F }^{\le b+1} p\). The loss depends strongly on \(\mathcal {T}\), although, it becomes smaller when b becomes larger. Even if we do not use sufficiently large b, we can estimate the loss for b when we fix \(\mathcal {T}\) and construct experimentally \(\mathcal {T}(\varphi )\) in advance. For instance, the size of the state space and the length of the shortest path reaching to rejecting states from the initial state, etc. of \(\mathcal {T}(\varphi )\) will be important information for the estimation. Another reason is that a \({\textsf {B}}\)-term focuses on only non-overlapped minimal bad prefixes. For the example shown in Fig. 3, the first and sixth occurrences of minimal bad prefixes are counted and the others are not. We do not strictly count occurrences of minimal bad prefixes, which play an important role in the violation of \(\mathcal {T}^{b}(\varphi )\).

The semantics of mean-payoff objectives is given in the following.

Note that \({\textsf {S}}(\chi )\) is not equivalent to \(1 - {\textsf {S}}(\lnot \chi )\) because the limit inferior is not generally equal to the limit superior. Additionally, note that \(- {\textsf {B}}(\mathbf{G }\chi )\) is not equivalent to \({\textsf {S}}(\lnot \chi )\). \({\textsf {S}}(\lnot \chi )\) strictly counts steps that violate \(\chi \), whereas \(- {\textsf {B}}(\mathbf{G }\chi )\) is an approximate count via the set \({ BadPref}(\mathcal {L}(\mathbf{G }\chi ))\) of minimal bad prefixes of \(\mathcal {L}(\mathbf{G }\chi )\). Therefore,Additionally, note that we put no limitation on an argument of a \({\textsf {B}}\)-term.

A mean-payoff objective can be constructed from scratch. However, if a conjunction of must LTL specifications is unrealizable, some of them should be downgraded to desirable specifications. In this subsection, we show how to interpret these desirable LTL specifications in a mean-payoff objective. This interpretation may be conducted along with refining the other must LTL specifications. However, for simplicity, we only consider interpretations without the refinement and assume that all desirable LTL specifications are \(\mathbf{G }\)-formulae.

The set of desirable LTL specifications \(\mathbf{G }\varphi _1, \ldots , \mathbf{G }\varphi _n\) can be reasonably interpreted as the mean-payoff objectivewhere each \(t_i\) is a payoff term interpreted from the desirable LTL specification \(\mathbf{G }\varphi _i\). However, there are many ways of interpreting \(\mathbf{G }\varphi _i\) in \(t_i\). We now address the interpretations, with and without considering the structure and intention of the sub-formulae.

A kind of soft assumption which may be violated by the environment can be included in our mean-payoff objectives.

Consider a desirable LTL specification \(\varphi _{Asmp} \rightarrow \varphi _{Grnt}\) with the assumption-guarantee form, where \(\varphi _{Asmp}\) signifies a property that is assumed to be followed by the environment, and \(\varphi _{Grnt}\) signifies a property that should be guaranteed by a system. A normal LTL synthesis method may involve a system that does not guarantee \(\varphi _{Grnt}\) when \(\varphi _{Asmp}\) does not hold. However, it is often required that a system is robust [5]. Informally, a robust system produces a small number of system errors for a small number of environment errors. Let \(\varphi _{Asmp}\) and \(\varphi _{Grnt}\) be respective \(\mathbf{G }\)-formulae \(\mathbf{G }\varphi _1\) and \(\mathbf{G }\varphi _2\). According to our basic idea, a more robust reactive system should produce a smaller difference in the number of steps violating \(\varphi _2\) from the number of steps violating \(\varphi _1\). Therefore, the desirable LTL specification can be interpreted as the mean-payoff objectivewhen \(t_{ Grnt}\) (resp., \(t_{ Asmp}\)) is a certain term interpreted from \(\varphi _{Grnt}\) (resp., \(\varphi _{Asmp}\)) according to the ideas in Sect. 3.3.

The latter part of our method is given in Algorithm 2. Let \({\textsf {MP}}(t)\) be a given mean-payoff objective, where \(t = \sum _{1 \le i \le n} c_i \cdot t_i\) and each \(t_i \) is either \({\textsf {S}}(\chi _i)\) or \({\textsf {B}}^{b_i}(\varphi _i)\). First, for each atomic term \(t_i\) (either \({\textsf {S}}\)-term or \({\textsf {B}}\)-term), we construct a safety game from \(t_i\) by reusing the procedures LTL2UCWA_translation ⁸ and BUCWA2SG_transformation in Algorithm 1 (either Lines 3–9 or 12–13), where LTL2UCWA_translation implements \(\mathcal {T}\). It is then transformed into a mean-payoff game \(\mathcal {M}^{t_i}\) (using either procedure \(\texttt {SG2MPG\_transformation\_S}\) at Line 10 or \(\texttt {SG2MPG\_transformation\_B}\) at Line 14). For each game \(\mathcal {M}^{t_i}\), its transition functions are total, and an outcome of any play \(\rho \) equals . Second, we construct a weighted synchronized product of an input winning region \(\mathcal {W}^{\varphi ,k}\) and the mean-payoff games \(\mathcal {M}^{t_1}, \ldots , \mathcal {M}^{t_n}\) (the procedure \(\texttt {weighted\_synchronized\_product}\) at Line 17). For the synchronized product mean-payoff game \(\mathcal {M}^{\varphi ,k,t}\), the outcome of a play \(\rho \) is . Finally, we find an optimal strategy \(\nu \) for the system-side player (Player 0) on \(\mathcal {M}^{\varphi ,k,t}\) using the standard technique for solving mean-payoff games [12, 20] (the procedure \(\texttt {optimal\_strategy}\), Line 17).

In this subsection, we explain how to construct a mean-payoff game \(\mathcal {M}^{t}\) from an atomic term \(t \in \{{\textsf {S}}(\chi ), {\textsf {B}}^k(\varphi )\}\), i.e., Lines 3–10 and 12–14 in Algorithm 2.

Let \(\mathcal {W}^{\varphi ,k}\) be a winning region \(\langle \langle V_0^0, V_1^0, 2^{{ OAP}}, 2^{{ IAP}}, E_0^0, E_1^0 \rangle \), \(v_{{ init}}^0\), \(V_0^0 \cup V_1^0 \rangle \) of an input to Algorithm 2. For payoff term \(t = \sum _{1 \le i \le n} c_i \cdot t_i\), let \(\mathcal {M}^{t_i}\) be a mean-payoff game \(\langle \langle V_0^i, V_1^i, 2^{{ OAP}}, 2^{{ IAP}}, E_0^i, E_1^i \rangle , v_{{ init}}^i\), \(W^i \rangle \), constructed from \(t_i\) using either Line 10 or Line 14 in Algorithm 2.

The mean-payoff game \(\mathcal {M}^{\varphi ,k,t}= \langle \langle V_{0}^0 \times V_{0}^1 \times \cdots \times V_{0}^n,V_{1}^0 \times V_{1}^1 \times \cdots \times V_{1}^n, 2^{{ OAP}}, 2^{{ IAP}}\), \(E_0'''', E_1'''' \rangle , \langle v^0_{{ init}},v^1_{{ init}}, \ldots , v^n_{{ init}} \rangle \), \(W''' \rangle \) constructed from them by the procedure \( \texttt {weighted\_synchronized\_product}\) at Line 17 in Algorithm 2 is, for \(\sigma \in \{0,1\}\), From Eqs. (78), (83), and (90), for any play \(\rho \in { Play}(\mathcal {M}^{\varphi ,k,t})\) and its corresponding interaction \({ trace}(\rho ) \in (2^{{ AP}})^{\omega }\), we haveAdditionally, because \(E_0^1, E_1^1, \ldots , E_0^n, E_1^n\) are total, we have

We have the following theorem.

As a result, we can obtain a reactive system that realizes \(\varphi \) and is locally optimal for \({\textsf {MP}}(t)\) in the sense of Eq. (72). Note that our method does not guarantee that the reactive system is globally optimal for \({\textsf {MP}}(t)\) as a trade-off for the memory finiteness. This is because the must LTL specification \(\varphi \) is under-approximated in our method. The winning region \(\mathcal {W}^{\varphi ,k}\) derived from \(\varphi \) is based on the under-approximated safe property via UCWA with bound k, and we find the reactive system from \(\mathcal {W}^{\varphi ,k}\). There generally exists a gap between the original property \(\varphi \) and the under-approximated property. It can be a matter for any large k in our method, unlike in LTL realizability checking. Consider the simple case when a must LTL specification \(\mathbf{G }\mathbf{F }p\) and a mean-payoff objective \({\textsf {MP}}({\textsf {S}}(\lnot p))\), where p is an output proposition. A reactive system realizes \(\mathbf{G }\mathbf{F }p\) and is globally optimal for \({\textsf {MP}}({\textsf {S}}(\lnot p))\), i.e., its value is 1, if and only if the system outputs p infinitely often and the distance between p increases further and further. Our method cannot produce such reactive systems requiring infinite memory. \(\mathbf{G }\mathbf{F }p\) would be under-approximated into \(\mathbf{G }\mathbf{F }^{k} p\) via a naive LTL-to-UCWA translator. Therefore, our method employing the naive translation composes a reactive system outputting p at k-step intervals, i.e., its value of \({\textsf {MP}}({\textsf {S}}(\lnot p))\) is \((k-1)\)/k. Any other translator leads to a similar result. The value approaches the global optimum arbitrarily using larger k in Algorithm 1.

Another concern in optimality regards bounds for \({\textsf {B}}\)-terms in mean-payoff objectives. Our first idea is, for desirable specifications \(\mathbf{G }\varphi _1,\ldots , \mathbf{G }\varphi _n\) with priority weights \(c_1, \ldots , c_n\), to maximize each number of steps satisfying \(\varphi _i\) taking into account all priority weights, i.e., to maximize \({\textsf {MP}}(\sum _{1 \le i \le n} c_i \cdot \mathcal {S}(\varphi _i))\), where the \(\mathcal {S}\)-term is an extension of the \({\textsf {S}}\)-term defined semantically for a non-restricted LTL formula \(\psi \) as follows.This objective cannot be directly represented in our mean-payoff objectives defined in Sect. 3. One question is whether there exist an LTL formula \(\varphi '\) and mean-payoff objective \({\textsf {MP}}(t)\) such that, if a reactive system realizes \(\varphi '\) and maximizes \({\textsf {MP}}(t)\), it also realizes the original must LTL specification \(\varphi \) and maximizes \({\textsf {MP}}(\sum _{1 \le i \le n} c_i \cdot \mathcal {S}(\varphi _i))\). If so (under some restrictions), another question is whether such t can be obtained as a term with a specific form, e.g., \(\sum _{1 \le i \le n} c_i \cdot {\textsf {B}}^{b_i}(\mathbf{G }\varphi _i)\). These are open problems that are out of the scope of this paper.

The time complexity of Algorithm 2 is doubly exponential, so it is in the same class as traditional LTL synthesis and realizability-checking [1, 34, 35].

For each atomic payoff term \(t_i\) with the form \({\textsf {S}}(\chi _i)\), we can construct \(\mathcal {M}^{t_i}\) with at most \(2^{P_i \cdot \lfloor { depth}(\chi _i) \rfloor } \cdot (2^{|{ OAP}|} + 1)\) states, where \(P_i\) is the number of distinct atomic propositions in \(\chi _i\). \(\chi _i\) can be translated into a deterministic safety automaton with at most \(2^{P_i \cdot \lfloor { depth}(\chi _i) \rfloor }\) states. An m-state deterministic automaton can be transformed into a game with at most \(m \cdot (2^{|{ OAP}|} + 1)\) states. For each atomic payoff term \(t_i\) with the form \({\textsf {B}}^{b_i}(\varphi _i)\), we can construct a mean-payoff game \(\mathcal {M}^{t_i}\) with at most \(2^{2^{\mathcal {O}(|\varphi _i|)} \cdot \log ({b}_i+2)} \cdot (2^{|{ OAP}|} + 1)\) states, where \(|\varphi _i|\) is the size of \(\varphi _i\). \(\varphi _i\) (resp., \(\lnot \varphi _i\)) can be translated into an equivalent UCWA (resp., NBWA) with at most \(2^{\mathcal {O}(|\varphi _i|)}\) states [40]. An \(n_i\)-state \(b_i\)-UCWA can be transformed into an equivalent deterministic safety automaton with at most \(2^{n_i \cdot \log (b_i+2)}\) states. We can construct the weighted synchronized product mean-payoff game from input winning region \(\mathcal {W}^{\varphi ,k}\) and mean-payoff objective \({\textsf {MP}}(t)\), which has at most \(|\mathcal {W}^{\varphi ,k}| \cdot T\) states and a largest absolute weight less than or equal to the possible weights of t. Here, T is a product of the sizes of the mean-payoff games for atomic terms in t. The time complexity for solving an m-state l-transition mean-payoff game is \(\mathcal {O}(m^2 \cdot l \cdot d \cdot (\log m + \log d))\) [12], where d is the largest absolute value of the weights. The above discussion implies that the time complexity of Algorithm 2 is doubly exponential.

As mentioned in Sect. 4.4, there is a trade-off between the optimality of the resulting system for \({\textsf {MP}}(t)\) and its computational cost. The size of \(\mathcal {W}^{\varphi ,k}\) (and the resulting system) grows polynomially in k. Therefore, the mean-payoff value of the resulting system approaches the global optimum arbitrary; however, its computational cost increases polynomially as k increases.

The prototype is implemented in C++ and only supports payoff terms without \({\textsf {B}}\)-terms. We can employ an existing LTL-to-NBWA translator, e.g., LTL2BA [23], SPOT [17] and LTL3BA [3], as an LTL-to-UCWA translator. The prototype uses LTL3BA for the LTL-to-UCWA mapping \(\mathcal {T}\). A direction of the implementation is the same as the one in [26]. Each state of automata and games is dealt with explicitly whereas transitions from the state are represented by one multi-terminal binary decision diagram (BDD). We employ CUDD⁹ for manipulating BDDs. On solving mean-payoff games (at Line 18 in Algorithm 2), we employ an iterative algorithm proposed in [42] and introduce a heuristic to check the optimality of a tentative solution after a certain number of iterations, which depends on the size of the games. Furthermore, for solving them efficiently, an abstracted mean-payoff game is constructed from the original game \(\mathcal {M}^{\varphi ,k,t}\). Actions of transitions are omitted in the abstracted game, and thus the state space of the abstracted game can be reduced. That is, its optimal strategy can be computed efficiently. From the optimal strategy and \(\mathcal {M}^{\varphi ,k,t}\), the optimal reactive system is composed as a transition system with the same format to Acacia+¹⁰ [8‐10] that is a well-known LTL synthesis tool.

The experiments were performed on a MacBook Pro (Retina, Mid 2012) with OS X Yosemite 10.10.5, 2.6-GHz CPU (Intel Core i7), and 16-GB memory (1600-MHz DDR3).

Instance 1 First, we focus on the preferability of synthesized systems. Consider synthesizing a reactive system that realizes the nearest property of LTL formula \(\varphi = \varphi _1 \wedge \varphi _2 \wedge \varphi _3\). This is a conjunction of the LTL formulae where \(req_1, req_2 \in { IAP}\) are atomic propositions for the input, and \(res \in { OAP}\) is an atomic proposition for the output. Intuitively, \(\varphi _1\) means that “a system must output res in the next step in response to an input \(req_1\)”, and \(\varphi _2\) means that “a system must output \(\lnot res\) in the next step in response to an input \(req_2\)”. \(\varphi _3\) means that “a system must maintain its current output in the next step”, where \(\varphi _3\) is a desirable specification derived from the performance requirement that “the output of a system should be maintained if unnecessary, to reduce signal switching”. The non-necessity depends on other specifications, and it is impossible to express the meaning of “if unnecessary” in LTL. Therefore, \(\varphi _3\) is a stronger property than this requirement. \(\varphi \) (or, more precisely, \(\varphi _1 \wedge \varphi _2\)) is unrealizable, because if both \(res_1\) and \(res_2\) are simultaneously inputs at a certain step, output res (resp., \(\lnot res\)) in the next step violates \(\varphi _2\) (resp., \(\varphi _1\)). We assume that a specification \(\varphi _i\) has a higher priority than another specification \(\varphi _j\) if \(i < j\). In our approach, a must specification is an LTL formula \(\varphi _1\), and desirable specifications \(\varphi _2\) and \(\varphi _3\) are transformed into a payoff term dependent on their priorities. The discussion in Sect. 3.3 implies that this payoff term is, for example,This term suggests that \(\varphi _2\) has a higher priority than \(\varphi _3\), because their weights are 2 and 1, respectively.

Result 1 Figure 4 shows a reactive system synthesized by our prototype for an input pair to LTL formula \(\varphi _1\) and mean-payoff objective \({\textsf {MP}}(t_{23})\). The system realizes \(\varphi _1\) and tries to satisfy \(\varphi _2\) (resp., \(\varphi _3\)) without violating \(\varphi _1\) (resp., \(\varphi _1\) or \(\varphi _2\)).

Discussion 1 To refine an unrealizable specification by adding assumptions, we can obtain an assumption \(\mathbf{G }(\lnot (req_1 \wedge req_2))\) for unrealizable \(\varphi _1 \wedge \varphi _2\) that is reasonable in some cases. For \(\varphi \), we can derive assumptions \(\mathbf{G }\lnot req_1\) and \(\mathbf{G }\lnot req_2\); however, they are trivially unallowable in a practical sense even if the refined formulae \((\mathbf{G }\lnot req_1) \rightarrow \varphi \) and \((\mathbf{G }\lnot req_2) \rightarrow \varphi \) are realizable. This is because \(\varphi _3\) does not appropriately express the requirement. However, there are many natural requirements that cannot be represented in LTL. As in the above example, we often fail to obtain allowable assumptions. We can also attempt to refine an unrealizable specification by weakening its partial specifications. Unrealizable \(\varphi \) can be refined into, for example, \(\varphi ' = \varphi _1 \wedge \varphi _2' \wedge \varphi _3'\), under the assumption of a priority order for the specifications. Here, \(\varphi _2'\) (resp., \(\varphi _3'\)) is a weakened specification for \(\varphi _2\) (resp., \(\varphi _3\)), and \(\varphi '\) is realized by the reactive system shown in Fig. 4. This example is very simple, and the unrealizable formula \(\varphi \) can be easily refined into the realizable formula \(\varphi '\). In general, we must repeatedly refine a specification and check its realizability. However, in our approach, we need to extract a must specification and interpret the desirable specifications using a mean-payoff objective that is based on their priorities. If the must specification is realizable, we can synthesize a concrete reactive system that considers the mean-payoff objective. Additionally, a mean-payoff objective can easily capture some requirements that are impossible to express in LTL, such as “if possible”.

Instance 2 Next, we focus on the scalability of our implementation. We use a specification of an n-client load balancing system [18] as an instance. The specification is given as a combination of some formulae (for details, see “Appendix 1”). We denote each formula by \(\varphi _i^{\text {LB}}\) where i is its index. As shown in [18], the following formulae \(\varphi _{\text {a}}^{\text {LB}}\), \(\varphi _{\text {b}}^{\text {LB}}\) and \(\varphi _{\text {c}}^{\text {LB}}\) are realizable. However, \(\bigwedge _{i \in \{1,2,3\}} \varphi _i^{\text {LB}}\), \(\bigwedge _{i \in \{1,2,4,5\}} \varphi _i^{\text {LB}}\) or \((\bigwedge _{i \in \{6,7\}} \varphi _i^{\text {LB}}) \rightarrow \bigwedge _{i \in \{1,2,5,8,9\}} \varphi _i^{\text {LB}}\) are not. According to the naive ideas on interpretation given in Sect. 3.3.1, we interpret \(\varphi _3^{\text {LB}}\), \(\varphi _5^{\text {LB}}\) and \(\varphi _9^{\text {LB}}\) into the following payoff terms, respectively. In the interpretation for \(\varphi _3^{\text {LB}}\), we use a formula-based approximation because the current implementation does not support \({\textsf {B}}\)-terms.

Result 2 Table 1 shows an experimental result for the must LTL specification \(\varphi _{\text {a}}^{\text {LB}}\) and mean-payoff objective \({\textsf {MP}}(t_3^{\text {LB}})\) when \(n \in \{2, \ldots , 7\}\). Because \(\varphi _{\text {a}}^{\text {LB}}\) is safe, there is no approximation in Algorithm 1, i.e., k is meaningless in this case. The numbers of clients are given in column “n”. Column “\(\alpha \)” (resp. “\(\beta \)”) gives execution times for transforming UCWAs, which are constructed from the must specification (resp. payoff terms), into safety games (resp. mean-payoff games). This transforming includes a procedure for minimizing state-spaces of the games. Column “\(\gamma \)” gives execution times for solving weighted synchronized product games, i.e., constructing and minimizing action-abstracted games and solving them. Total execution times (including execution times for constructing UCWAs, etc.) are given in column “Total”. We denote timeouts (>20 min) by “TO”. Column “\(|\mathcal {W}|\)” (resp. “\(|\mathcal {M}|\)”) gives the sizes of winning regions which are eventually obtained from the must specifications (resp., synchronized products of mean-payoff games, which are eventually obtained from the payoff terms). The sizes of weighted synchronized products of the winning regions and mean-payoff games are given in column “\(|\mathcal {P}|\)”. Column “\(|\mathcal {P}^{\text {abs}}|\)” gives the sizes of the abstracted and minimized games for the weighted synchronized products. The sizes of resulting systems are listed in column “\(|\mathcal {R}|\)”. Table 2 (resp. Table 3) shows an experimental result for the must LTL specification \(\varphi _{\text {b}}^{\text {LB}}\) (resp. \(\varphi _{\text {c}}^{\text {LB}}\)) and mean-payoff objective \({\textsf {MP}}(t_5^{\text {LB}})\) (resp. \({\textsf {MP}}(t_9^{\text {LB}})\)) when \(n \in \{2, \ldots , 5\}\) (resp. \(n \in \{2, \ldots , 6\}\)). We set the initial value for k as \(n+1\) (resp. n) in this case. This is because it is the minimum value which makes \(\mathcal {L}(\mathcal {T}^k(\varphi _{\text {b}}^{\text {LB}}))\) (resp. \(\mathcal {L}(\mathcal {T}^k(\varphi _{\text {c}}^{\text {LB}}))\)) realizable. These results suggest that our implementation can treat non-trivial scale instances.

Discussion 2 The current implementation is just a prototype and does not support \({\textsf {B}}\)-terms. We conjecture that non-trivial scale instances with \({\textsf {B}}\)-terms will be treated by a complete version. The values in column “\(|\mathcal {W}|\)” in Tables 1, 2 and 3 are used as a basis for the conjecture. This is because constructing a mean-payoff game from a \({\textsf {B}}\)-term is nearly the same as constructing a safety game from an LTL formula with a UCWA approximation. Additionally, Tables 1, 2 and 3 suggest it is very effective to use an abstracted and minimized game of a weighted synchronized product mean-payoff game. The state spaces are significantly reduced in many cases. In Table 1, the sizes of the abstracted and minimized games are the same when the number n of clients is greater than the bound (i.e., 3) for the \(\mathbf{F }\) operators in the payoff term \(t_3^{\text {LB}}\). This fact suggests it may be possible to efficiently treat some types of \({\textsf {S}}\)-terms with many \(\mathbf{X }\) operators (and also \({\textsf {B}}\)-terms with large bounds).

Instance 3 Finally, we confirm the trade-off between the optimality of synthesized systems and bound k in Algorithm 1 (and its computational cost) using a non-trivial scale instance. We use a specification of a 2-floor elevator system [2] as an instance. The specification is given as a combination of some formulae (for details, see “Appendix 2”). We denote by \(\varphi ^{\text {ELV}}\) the specification. \(\varphi ^{\text {ELV}}\) includes the following constraint.where \({ LocBtn}_1,{ LocBtn}_2 \in { IAP}\) and \({ Loc}_1,{ Loc}_2 \in { OAP}\). This formula means that, if the button on the i-th floor is pushed (\({ LocBtn}_i\)), the system must eventually move the cage to the i-th floor (\({ Loc}_i\)). Consider a desirable specification \({\textsf {MP}}(t^{\text {ELV}})\), whereMaximizing \({\textsf {MP}}(t^{\text {ELV}})\) means that the system tries to keep its cage on the same floor as long as possible. This type of desirable specification is required to save power consumption. The desirable specification \({\textsf {MP}}(t^{\text {ELV}})\) conflicts with the unsafe property given by Equation (108) (and also the must specification \(\varphi ^{\text {ELV}}\)).

Result 3 Table 4 shows an experiment result for the must LTL specification \(\varphi ^{\text {ELV}}\) and mean-payoff objective \({\textsf {MP}}(t^{\text {ELV}})\) when \(k_{ init} \in \{3,6,9,12,15,18,19,20,21\}\). Column “MP value” gives mean-payoff values of resulting systems. The other columns are the same as Tables 1, 2 and 3. The size of the product of mean-payoff games for payoff terms in \(t^{\text {ELV}}\) is 9. This result suggests that the mean-payoff value of the resulting system approaches the global optimum (0, for this instance) and its computational cost grows non-linearly, when k increases. For this instance, reasonably good systems are obtained in times that are practical.

We confirmed some advantages of our method with several experiments. They are summarized as follows.

In a naive game-based method for LTL synthesis, a deterministic \(\omega \)-regular word automaton (e.g., deterministic parity word automaton) \(\mathcal {D}^{\varphi }\) is translated from a given LTL specification \(\varphi \). Next, an \(\omega \)-regular game \(\mathcal {G}^{\varphi }\) is transformed from \(\mathcal {D}^{\varphi }\). Finally, a reactive system is composed as a winning strategy on \(\mathcal {G}^{\varphi }\). The first phase can be performed by translating \(\varphi \) to a nondeterministic \(\omega \)-regular word automaton \(\mathcal {N}^{\varphi }\) [3, 17, 23, 40], and, using Safra’s construction [32, 36‐38], to determinize \(\mathcal {N}^{\varphi }\) to \(\mathcal {D}^{\varphi }\). However, Safra’s construction is very complicated and difficult to implement efficiently. Recently, Esparza and Křetínský proposed another method for directly constructing a deterministic \(\omega \)-regular automaton from an LTL formula [21]. Their method constructs transition-based automata, which are in most cases smaller than state-based automata obtained by Safra’s construction, but is also complicated.

Therefore, some Safraless LTL synthesis methods were proposed [8, 18, 22, 27, 28]. In these methods, \(\varphi \) is appropriately under-approximated into a tractable automaton (e.g., safety automaton), which is used to construct a reactive system. Some tools are available for Safraless LTL synthesis, e.g., Lily¹¹ [27], Acacia+ [8‐10], and Unbeast¹² [18]. In some Safraless LTL synthesis methods [8, 18, 22], \(\varphi \) is under-approximated by giving a bound k to UCWA \(\mathcal {A}^{\varphi }\) equivalent to \(\varphi \). A k-UCWA \(\mathcal {A}^{\varphi ,k}\) represents a safety property and can easily be determinized by a type of powerset (i.e., Safraless) construction. Therefore, a reactive system is composed as a winning strategy on a safety game \(\mathcal {S}^{\varphi ,k}\) corresponding to \(\mathcal {A}^{\varphi ,k}\). The state space of this winning strategy is typically minimized [19].

In our method, we apply the UCWA-based Safraless method to construct an under-approximated safety game from a must LTL specification and then compose a reactive system as a winning strategy on the game. This is also optimal for a given mean-payoff objective that represents weighted desirable specifications.

Our problem is similar to the weighed partial maximum satisfiability (MAX-SAT) problem [29].¹³

The weighed partial MAX-SAT problem considers a set of hard clauses, which must be satisfied, and a set of weighted soft clauses, which are satisfied if possible. The solution is a valuation that satisfies all the hard clauses and maximizes the total weight of the satisfied soft clauses. The input formulae of the problem are not temporal; the objective is given as the total weight of the satisfied soft clauses, and the problem considers satisfiability.

However, our problem considers a must LTL specification and a mean-payoff objective that represents weighted desirable specifications. The solution is a synthesized reactive system that realizes all the must specifications and maximizes the objective. The input formula for our problem is temporal, the objective is given as a mean-payoff of a sequence of weights that depend on LTL formulae, and our problem considers realizability.

In our approach, a set of weighted desirable specifications is represented by a naive mean-payoff objective based on LTL formulae with weights. The syntax of our objective is based on that of the mean-payoff constraints in [39]. In this paper, an argument of a \({\textsf {S}}\)-term must be bounded, but it may be unbounded in [39] (i.e., \(\mathcal {S}\)-terms defined in Equation (95) are considered). This restriction is derived from the difficulty of dealing with non-determinacy (on payments) in the synthesis. [39] studied an LTL with multiple mean-payoff constraints and methods for model- and satisfiability-checking. Non-determinacy does not affect the model- or satisfiability-checking. In this paper, we instead used a new type of term, \({\textsf {B}}^{b}(\varphi )\), to capture the violation of the approximated safety property using UCWA. Therefore, the expressive power of payoff terms in this paper is incomparable with that in [39]. The semantics of the mean-payoff constraints in [39] was purely based on LTL formulae. However, our objective in this paper is also based on an LTL-to-UCWA translator.

Our method synthesizes an optimal reactive system in a set of reactive systems that realize a certain under-approximation of a must LTL specification. This is an optimal memoryless strategy on a naive mean-payoff game that is constructed from a mean-payoff objective. This strategy can be efficiently computed [12]. Our problem can be strictly reduced to finding an optimal (or \(\varepsilon \)-optimal) strategy on a mean-payoff parity game [13], which is a synchronized product of a parity game constructed from the must LTL specification and the naive mean-payoff game. However, this reduction generally requires that we construct a deterministic parity word automaton that accepts words satisfying the must LTL specification. That is, Safra’s or the Esparza-Křetínský construction.¹⁴ Furthermore, the algorithm for solving the game in [13] requires recursively solving parity and mean-payoff games; its optimal (resp., \(\varepsilon \)-optimal) strategy generally requires infinite (resp., large) memory.

In [6], Bloem et al. studied lexicographic mean-payoff (parity) games with multi-dimensional weights. The mean-payoffs are lexicographically ordered based on the priority of the dimensions. Any lexicographic mean-payoff (parity) game can be reduced to a naive mean-payoff (parity) game [6]. Therefore, our method can be easily extended to allow such multi-dimensional lexicographical weighting. However, the time complexity of extending our method is exponential to the number of dimensions [6]. Bloem et al. also proposed a method for reducing an automata-based mean-payoff objective (and \(\omega \)-regular specification) into a lexicographic mean-payoff (parity) game [6]. They composed an optimal strategy for the game. However, our method deals with an LTL specification and a formula-based mean-payoff objective.

In [15], Chatterjee et al. studied multi-dimensional mean-payoff games, and proposed a method for finding a winning strategy that guarantees that the multi-dimensional mean-payoff for any play is greater than or equal to a given threshold vector. Acacia+ supports synthesis from an LTL formula with multiple mean-payoff constraints [9] (based on [15]) and also one with optimization for a naive mean-payoff objective under a Markov decision process environment [10]. However, the mean-payoff constraints and objectives supported in Acacia+ are only based on \({\textsf {S}}\)-terms. Strictly speaking, Acacia+ only supports payoffs for literals. Hence, if we use \({\textsf {S}}(\chi )\) with a non-Boolean and bounded argument \(\chi \), we need to add a fresh atomic proposition \(\hat{p} \in 2^{{ OAP}}\) for output and an additional LTL specification \(\mathbf{G }(\chi \leftrightarrow \mathbf{X }^{\lceil { depth}(\chi ) \rceil } \hat{p})\). Our mean-payoff objective can be expressed by \({\textsf {B}}\)-terms that capture the violations of approximated safety properties using UCWAs.

A reactive system specification is often given as an LTL formula with the implication form \(\varphi _{Asmp} \rightarrow \varphi _{Grnt}\), where \(\varphi _{Asmp}\) is an assumption regarding the behavior of the environment, and \(\varphi _{Grnt}\) is a property that the system should guarantee. In [7], Bloem et al. presented some goals for a reliable system synthesized from such a specification. The be-correct goal is “to fulfill \(\varphi _{Grnt}\) if the environment fulfills \(\varphi _{Asmp}\)”. This is the aim for a reactive system obtained by traditional LTL synthesis. Some approaches for the other goals were surveyed in [7]. In our method, we can include assumptions in must specifications in a naive sense.

As suggested in [7], synthesis with mean-payoff optimization can work against the don’t-be-lazy goal, which is “to fulfill \(\varphi _{Grnt}\) as well as possible for as many situations as possible, even when \(\varphi _{Asmp}\) are not fulfilled”. In our approach, the don’t-be-lazy goal is accomplished by a system synthesized from the must LTL specification \(\varphi _{Asmp} \rightarrow \varphi _{Grnt}\) and the mean-payoff objective interpreted from (sub-formulae of) \(\varphi _{Grnt}\). The synthesized system realizes \(\varphi _{Asmp} \rightarrow \varphi _{Grnt}\) and tries to satisfy (the sub-formulae of) \(\varphi _{Grnt}\) to the extent possible, even if \(\varphi _{Asmp}\) is violated. In [26], we focused on this type of synthesis and regarded the goal as maximizing the degree of environmental tolerance which is given by the mean-payoff objective with \(\mathcal {S}\)-terms and without B-terms, as in [39]. However, atomic terms occurring in the mean-payoff objective for a synthesis method in [26] is restricted to be S-terms.

Our approach also satisfies the never-give-up goal, which is “to try to satisfy \(\varphi _{Grnt}\) when you can if you cannot satisfy \(\varphi _{Grnt}\) for every environment behavior”. In [7], Bloem et al. suggested that this goal can be achieved by adding a reasonable property \(L \subseteq (2^{{ AP}})^{\omega }\), such that \(\mathcal {L}(\varphi _{Grnt}) \cup L\) is realizable and then synthesizing a system that realizes \(\mathcal {L}(\varphi _{Grnt}) \cup L\). Existing approaches can define this property, L. For example, the negation of a new assumption \(\psi _{Asmp}\) on the behavior of the environment such that \(\psi _{Asmp} \rightarrow \varphi _{Grnt}\) (\(\equiv \lnot \psi _{Asmp} \vee \varphi _{Grnt}\)) is realizable. In [14], Chatterjee et al. proposed a method for computing this assumption. However, we must still check that it is reasonable. In [16], Damm and Finkbeiner introduced the admissibility of specifications and proposed a method for synthesizing a distributed system consisting of dominant reactive systems. A specification \(\varphi \) is admissible if there exists a dominant reactive system for \(\varphi \). A reactive system \(\mathcal {R}\) (or strategy) is dominant for \(\varphi \) if, for any sequence \(s \in (2^{{ IAP}})^{\omega }\) of inputs, \({ Intr}_s(\mathcal {R}) \models \varphi \) if there exists \(\mathcal {R}'\) such that \({ Intr}_s(\mathcal {R}') \models \varphi \). In other words, this reactive system realizes \(\mathcal {L}(\varphi ) \cup CSS(\varphi )\), where \(CSS(\varphi )\) is a set of possible interactions produced by counterexample input-sequences for strong satisfiability [31] of \(\varphi \). That is,Similar to the above studies, Damm and Finkbeiner used \(CSS(\varphi _{Grnt})\) as an additional property, L. Both of these existing methods do not satisfy the don’t-be-lazy goal. For the additional property L (i.e., \(\mathcal {L}(\lnot \psi _{Asmp})\) or \(CSS(\varphi _{Grnt})\)) considered in their methods, a system synthesized from a supplemented specification \(\mathcal {L}(\varphi _{Grnt})\cup L\) may stop trying to satisfy \(\varphi _{Grnt}\) if L is satisfied. Our method can be extended to fit this problem. For example, a system realizing \(\mathcal {L}(\varphi _{Grnt})\cup L\) and optimizing a mean-payoff objective based on (the sub-formulae of) \(\varphi _{Grnt}\) is expected to satisfy the don’t-be-lazy and never-give-up goals. The dominant reactive system is also a type of best-effort system. However, note the difference between the interpretations of “best effort”. In their view, a system can stop trying to satisfy \(\varphi \) for only the worst input-sequences in \(CSS(\varphi )\). This type of “best effort” will be reasonable in some cases, e.g., in compositional synthesis for distributed systems, as in [16]. In our view, \(\varphi \) should be divided into must specifications and desirable specifications in the first place if \(\varphi \) is unrealizable. Additionally, we assume that each desirable specification has no assumption because a system tries to make the best effort possible regardless of whether the assumption holds. \(\mathbf{G }\)-formula is basic form of reactive system specifications without assumptions, so that the best effort to satisfy a desirable specification \(\mathbf{G }\varphi _i\) can be regarded to maximize the number of steps that satisfy \(\varphi _i\). That is, try to satisfy \(\varphi _i\) at each step, even if \(\varphi _i\) is repeatedly violated. Synthesizing robust systems is another approach to obtain the don’t-be-lazy goal. In [5], Bloem et al. proposed a method to synthesize a robust reactive system from a combination of safety- and liveness- properties. For safe \(\varphi _{Asmp} \) and \(\varphi _{Grnt}\), Bloem et. al. focused on the ratio of the number of violations for \(\varphi _{Grnt}\) to the number of violations for \(\varphi _{Asmp}\); a synthesized robust system that makes the ratio as small as possible. They suggested some types of violations for safety properties, and their reset-on-error heuristic corresponds to our idea of \({\textsf {B}}\)-terms, which is based on the non-overlapped minimal bad prefixes. In our approach, minimizing the ratio for the heuristic can be interpreted as maximizing the mean-payoff objective given by Eq. (71).