key: cord-0047690-b2y71n7o
authors: Almagor, Shaull; Kupferman, Orna
title: Good-Enough Synthesis
date: 2020-06-16
journal: Computer Aided Verification
DOI: 10.1007/978-3-030-53291-8_28
sha: bcdcd76fc1128bfbabbb29da6fc97b573d2edef8
doc_id: 47690
cord_uid: b2y71n7o

We introduce and study good-enough synthesis (ge-synthesis) – a variant of synthesis in which the system is required to satisfy a given specification [Formula: see text] only when it interacts with an environments for which a satisfying interaction exists. Formally, an input sequence x is hopeful if there exists some output sequence y such that the induced computation [Formula: see text] satisfies [Formula: see text], and a system ge-realizes [Formula: see text] if it generates a computation that satisfies [Formula: see text] on all hopeful input sequences. ge-synthesis is particularly relevant when the notion of correctness is multi-valued (rather than Boolean), and thus we seek systems of the highest possible quality, and when synthesizing autonomous systems, which interact with unexpected environments and are often only expected to do their best. We study ge-synthesis in Boolean and multi-valued settings. In both, we suggest and solve various definitions of ge-synthesis, corresponding to different ways a designer may want to take hopefulness into account. We show that in all variants, ge-synthesis is not computationally harder than traditional synthesis, and can be implemented on top of existing tools. Our algorithms are based on careful combinations of nondeterministic and universal automata. We augment systems that ge-realize their specifications by monitors that provide satisfaction information. In the multi-valued setting, we provide both a worst-case analysis and an expectation-based one, the latter corresponding to an interaction with a stochastic environment.

prioritize and weight different scenarios. The synthesis algorithm for LTL[F] seeks systems with a highest possible satisfaction value. One can consider either a worst-case approach, where the satisfaction value of a system is the satisfaction value of its computation with the lowest satisfaction value [1] , or a stochastic approach, where it is the expected satisfaction value, given a distribution of the inputs [2] .

Consider, for example, an acceleration controller of an autonomous car. Normally, the car should maintain a relatively constant speed. However, in order to optimize travel time, if a long stretch of road is visible and is identified as low-risk, the car should accelerate. Conversely, if an obstacle or some risk factor is identified, the car should decelerate. Clearly, the car cannot accelerate and decelerate at the same time. We capture this desired behavior with the following LTL[F] formula over the inputs {safe, obs} and outputs {acc, dec}: ψ = G(safe → (acc ⊕ 2 3 Xacc)) ∧ G(obs → (dec ⊕ 3 4 Xdec)) ∧ G(¬(acc ∧ dec)). Thus, in order to get satisfaction value 1, each detection of a safe stretch should be followed by an acceleration during two transactions, with a preference to the first (by the semantics of the weighted average ⊕ λ operator, the satisfaction value of safe → (acc ⊕ 2 3 Xacc) is 1 when safe is followed by two accs, 2 3 when it is followed by one acc, and 1 3 if it is followed by one acc with a delay), and each detection of an obstacle should be followed by a deceleration during two transactions, with a (higher) preference to the first. Clearly, ψ is not realizable with satisfaction value 1, as for some input sequences, namely those with simultaneous or successive occurrences of safe and obs, it is impossible to respond with the desired patterns of acceleration or declaration. Existing frameworks for synthesis cannot handle this challenge. Indeed, we do not want to add an assumption about safe and obs occurring far apart. Rather, we want our autonomous car to behave in an optimal way also in problematic environments, and we want, when we evaluate the quality of a car, to take into an account the challenge posed by the environment. This is exactly what high-quality ge-synthesis does: for each input sequence, it requires the synthesized car to obtain the maximal satisfaction value that is possible for that input sequence.

We show that in the Boolean setting, ge-synthesis can be reduced to synthesis of LTL with quantification of atomic propositions [26] . Essentially, ge-synthesis of ψ amounts to synthesis of (∃O.ψ) → ψ. We show that by carefully switching between nondeterminisitc and universal automata, we can solve the ge-synthesis problem in doubly-exponential time, thus it is not harder than traditional synthesis. Also, our algorithm is Safraless, thus no determinization and parity games are needed [15, 17] .

A drawback of ge-synthesis is that we do not actually know whether the specification is satisfied. We describe two ways to address this drawback. The first goes beyond providing satisfaction information and enables the designer to partition the specification into a strong component, which is guaranteed to be satisfied in all environments, and a weak component, which is guaranteed to be satisfied only in hopeful ones. The second way augments ge-realizing systems by "satisfaction indicators". For example, we show that when a system is lucky to interact with an environment that generates a prefix of an input sequence such that, when combined with a suitable prefix of an output sequence, the specification becomes realizable, then ge-synthesis guarantees that the system indeed responds with a suitable prefix of an output sequence. Moreover, it is easy to add to the system a monitor that detects such prefixes, thus indicating that the specification is going to be satisfied in all environments. Additional monitors we suggest detect prefixes after which the satisfaction becomes valid or unsatisfiable.

We continue to the quantitative setting. We parameterize hope by a satisfaction value v ∈ [0, 1] and say that an input sequence x ∈ (2 I ) ω is v-hopeful for an LTL[F] formula ψ if an interaction with it can generate a computation that satisfies ψ with value at least v. Formally, there is an output sequence y ∈ (2 O ) ω such that [[x ⊗ y, ψ] ] ≥ v, where for a computation w ∈ (2 I∪O ) ω , we use [[w, ψ] ] to denotes the satisfaction value of ψ in w. As we elaborate below, while the basic idea of ge-synthesis, namely "input sequences with a potential to high quality should realize this potential" is as in the Boolean setting, there are several ways to implement this idea.

We start with a worst-case approach. There, a strategy f :

The requirement can be applied to a threshold value or to all values v ∈ [0, 1]. For example, our autonomous car controller has to achieve satisfaction value 1 in roads with no simultaneous or successive occurrences of safe and obs, and value 3 4 in roads that violate the latter only with some obs followed by safe. We then argue that the situation is similar to that of high-quality assume guarantee synthesis [3] , where richer relations between a quantitative assumption and a quantitative guarantee are of interest. In our case, the assumption is the hopefulness level of the input sequence, namely [[x, ∃O.ψ]], and the guarantee is the satisfaction value of the specification in the generated computation, namely [[x ⊗ f (x), ψ]]. When synthesizing, for example, a robot controller (e.g., vacuum cleaner) in a building, the doors to rooms are controlled by the environment, whereas the movement of the robot by the system. A measure of the performance of the robot has to take into an account both the number of "hopeful rooms", namely these with an open door -a projection of this number on [0, 1] serves as the assumption, and the number of room cleaned -which induces the guarantee. We assume that the desired relation between the assumption and the guarantee is given by a function comb : [0, 1] × [0, 1] → [0, 1], which can capture implication, difference, or ratio.

We continue with an analysis of the expected performance of the system. We do so by assuming a stochastic environment, with a known distribution on the input sequences. We introduce and study two measures for high-quality gesynthesis in a stochastic environment. In the first, termed expected ge-synthesis, all input sequences are sampled, yet the satisfaction value in each input sequence takes its hopefulness level into account, for example by a comb function as in the assume-guarantee setting. In the second, termed conditional expected ge-synthesis, only hopeful input sequences are sampled. For both approaches, our synthesis algorithm is based on the high-quality LTL[F] synthesis algorithm of [2] , which is based on an analysis of deterministic automata associated with the different satisfaction values of the LTL[F] specification. Here too, the complexity stays doubly exponential. In addition, we extend the synthesized systems with guarantees for satisfaction and monitors indicating satisfaction in various satisfaction levels.

Consider two finite sets I and O of input and output signals, respectively. For two words x = i 0 · i 1 · i 2 · · · ∈ (2 I ) ω and y = o 0 · o 1 · o 2 · · · ∈ (2 I ) ω , we define x ⊗ y as the word in (2 I∪O ) ω obtained by merging x and y. Thus,

The definition is similar for finite x and y of the same length. For a word w ∈ (2 I∪O ) ω , we use w |I to denote the projection of w on I. In particular, (x ⊗ y) |I = x.

A strategy is a function f : (2 I ) + → 2 O . Intuitively, f models the interaction of a system that generates in each moment in time a letter in 2 O with an environment that generates letters in 2 I . For an input sequence

Note that the environment initiates the interaction, by inputting i 0 . Of special interest are finite-state strategies, induced by finite state transducers. Formally, an I/O-transducer is T = I, O, S, s 0 , M, τ , where S is a finite set of states, s 0 ∈ S is an initial state, M : S × 2 I → S is a transition function, and τ : S → 2 O is a labelling function. For x = i 0 · i 1 · i 2 · · · ∈ (2 I ) * , let M * (x) be the state in S that T reaches after reading x. Thus is, M * ( ) = s 0 and for every j ≥ 0, we have that

We use T (x) and x ⊗ T (x) to denote the output sequence and the computation of T on x, respectively, and talk about T realizing a specification, referring to the strategy f T .

We specify on-going behaviors of reactive systems using the linear temporal logic LTL [19] . Formulas of LTL are constructed from a set AP of atomic proposition using the usual Boolean operators and temporal operators like G ("always"), F ("eventually"), X ("next time"), and U ("until"). Each LTL formula ψ defines a language L(ψ) = {w : w |= ψ} ⊆ (2 AP ) ω . We also use automata on infinite words for specifying and reasoning about on-going behaviors. We use automata with different branching modes (nondeterministic, where some run has to be accepting; universal, where all runs have to be accepting; and deterministic, where there is a single run) and different acceptance conditions (Büchi, co-Büchi, and parity). We use the three letter acronyms NBW, UCW, DPW, and DFW, to refer to nondeterministic Büchi, universal co-Büchi, deterministic parity, and deterministic finite word automata, respectively. Given an LTL formula ψ over AP , one can constructs an NBW A ψ with at most 2 O(|ψ|) states such that L(A ψ ) = L(ψ) [27] . Constructing an NBW for ¬ψ and then dualizing it, results in a UCW for L(ψ), also with at most 2 O(|ψ|) states. Determinization [23] then leads to a DPW for L(ψ) with at at most 2 2 O(|ψ|) states and index 2 O(|ψ|) . For full definitions of LTL, automata, and their relation, see [12] .

Consider an LTL formula ψ over I ∪ O. We say that ψ is realizable if there is a finite-state strategy f :

That is, the computation of f on every input sequence satisfies ψ. We say that a word x ∈ (2 I ) ω is hopeful for ψ if there is y ∈ (2 O ) ω such that x⊗y |= ψ. Then, we say that ψ is good-enough realizable (ge-realizable, for short) if there is a finite-state strategy f : (2 I ) + → 2 O such that for every x ∈ (2 I ) ω that is hopeful for ψ, we have that x ⊗ f (x) |= ψ. That is, if there is some output sequence whose combination with x satisfies ψ, then the computation of f on x satisfies ψ. The LTL ge-synthesis problem is then to decide whether a given LTL formula is ge-realizable, and if so, to return a transducer that ge-realizes it. Clearly, every realizable specification is ge-realizable -by the same transducer. We say that ψ is universally satisfiable if all input sequences are hopeful for ψ. It is easy to see that for universally satisfiable specifications, realizability and ge-realizability coincide. On the other hand, as demonstrated in Sect. 1, there are specifications that are not realizable and are ge-realizable.

Clearly, ψ is not realizable, as an input sequence x ∈ (2 I ) ω is hopeful for ψ iff x |= GFp ∧ GF¬p. Since the system has to assign a value to q before it knowns the value of Xp, it seems that ψ is also not ge-realizable. As we show below, however, the specification ψ is ge-realizable. Intuitively, it follows from the fact that hopeful input sequences consists of alternating p-blocks and (¬p)-blocks. Then, by outputting ¬q in p-blocks and outputting q in (¬p)-blocks, the system guarantees that each last position in a (¬p)-block satisfies q ∧ Xp and each last position in a p-block satisfies (¬q)∧Xp. 

Recall that a strategy f : (2 I ) + → 2 O ge-realizes an LTL formula ψ if its computations on all hopeful input sequences satisfy ψ. Thus, for every input sequence x ∈ (2 I ) ω , either x⊗y |= ψ for all y ∈ (2 O ) ω , or x⊗f (x) |= ψ. The above suggests that algorithms for solving LTL ge-synthesis involve existential and universal quantification over the behavior of output signals. The logic EQLTL extends LTL by allowing existential quantification over atomic propositions [26] . We refer here to the case the atomic propositions are the signals in I ∪ O, and the signals in O are existentially quantified. Then, an EQLTL formula is of the form ∃O.ψ, and a computation w ∈ (2 I∪O ) ω satisfies ∃O.ψ iff there is y ∈ (2 O ) ω such that w |I ⊗ y |= ψ. Dually, AQLTL extends LTL by allowing universal quantification over atomic propositions. We consider here formulas of the form ∀O.ψ, which are equivalent to ¬∃O.¬ψ. Indeed, a computation w ∈ (2 I∪O ) ω satisfies ∀O.ψ iff for all y ∈ (2 O ) ω , we have that w |I ⊗ y |= ψ. Note that in both the existential and universal cases, the O-component of w is ignored. Accordingly, we sometimes interpret EQLTL and AQLTL formulas with respect to input sequences x ∈ (2 I ) ω . Also note that both EQLTL and AQLTL increase the expressive power of LTL. For example, the EQLTL formula ∃q.q ∧ X¬q ∧ G(q ↔ XXq) ∧ G(q → p) states that p holds in all even positions of the computation, which cannot be specified in LTL [29] .

Proof. We start with the upper bound. Given an LTL formula ψ over I ∪ O, we describe an algorithm that returns a transducer T that ge-realizes ψ, or declares that no such transducer exists.

It is not hard to see that T ge-realizes ψ iff T realizes ϕ = ψ ∨ ∀O.¬ψ. Indeed, an input sequence x ∈ (2 I ) ω is hopeful for ψ iff x |= ∃O.ψ, and so the specification ϕ requires all hopeful input sequences to satisfy ψ. A naive construction of an NBW for ϕ involves a universal projection of the signals in O in an automaton for ¬ψ, and results in an NBW that is doubly exponential.

In order to circumvent the extra exponent, we construct an NBW A ¬ϕ for ¬ϕ, and then dualize it to get a UCW for ϕ, as follows.

Let A ¬ψ be an NBW for L(¬ψ) and A ∃O.ψ be an NBW for L(∃O.ψ). Thus, A ∃O.ψ is obtained from an NBW A ψ for L(ψ) by existentially projecting its transitions on 2 I . In more details, if

Let A ¬ϕ be an NBW for the intersection of A ¬ψ and A ∃O.ψ . We can define A ¬ϕ as the product of A ¬ψ and A ∃O.ψ , possibly using the generalized Büchi acceptance condition (see Remark 1), thus its size is exponential in ψ. The language of A ¬ϕ is then {w ∈ (2 I∪O ) ω : w |= ψ and w |= ∃O.ψ}. We then solve usual synthesis for the complementing UCW. Its language is {w ∈ (2 I∪O ) ω : w |= ψ or w |= ∀O.¬ψ}, as required. By [17] , the synthesis problem for UCW can be solved in EXPTIME, and we are done.

The lower bound follows from the 2EXPTIME-hardness of LTL realizability [22] . The hardness proof there constructs, given a 2EXPTIME Turing machine M , an LTL formula ψ that is realizable iff M accepts the empty tape. Since all input sequences are hopeful for ψ, realizability and ge-realizability coincide, and we are done.

Note that working with a UCW not only handles the universal quantification for free but also has the advantage of a Safraless synthesis algorithm -no determinization and parity games are needed [15, 17] . Also note that the algorithm we suggest in the proof of Theorem 1 can be generalized to handle specifications that are arbitrary positive Boolean combinations of EQLTL formulas.

Throughout the paper, we construct products of automata whose state space is 2 cl(ψ) , and states correspond to maximal consistent subsets of cl(ψ), possibly in the scope of an existential quantifier of O. Accordingly, the product can be minimized to include only consistent pairs. Also, since traditional-synthesis algorithms, in particular the Safraless algorithms we use, can handle automata with generalized Büchi and co-Büchi acceptance condition, we need only one copy of the product.

Remark 2 [Determinancy of the ge-synthesis game]. Determinancy of games implies that in traditional synthesis, a specification ψ is not I/O-realizable iff ¬ψ is O/I-realizable This is useful, for example when we want to synthesize a transducer of a bounded size and proceed simultaneously, aiming to synthesize either a system transducer that realizes ψ or an environment transducer that realizes ¬ψ [17] . For ge-synthesis, simple dualization does not hold, but we do have determinancy in the sense that (∃O.ψ)

Accordingly, ψ is not ge-realizable iff the environment has a strategy that generates, for each output sequence y ∈ (2 O ) ω , a helpful input sequence x ∈ (2 I ) ω such that x ⊗ y |= ¬ψ. In the full version, we formalize and study this duality further.

A drawback of ge-synthesis is that we do not actually know whether the specification is satisfied. In this section we describe two ways to address this drawback. The first way goes beyond providing satisfaction information and enables the designer to partition the specification into to a strong component, which should be satisfied in all environments, and a weak component, which should be satisfied only in hopeful ones. The second way augments ge-realizing transducers by flags, raised to indicate the status of the satisfaction.

Recall that ge-realizability is suitable especially in settings where we design a system that has to do its best in all environments. ge-synthesis with a guarantee is suitable in settings where we want to make sure that some components of the specification are satisfied in all environment. Accordingly, a specification is an LTL formula ψ = ψ strong ∧ ψ weak . When we ge-synthesize ψ weak with guarantee ψ strong , we seek a transducer T that realizes ψ strong and ge-realizes ψ weak . Thus, for all input sequences

Theorem 2. The LTL ge-synthesis with guarantee problem is 2EXPTIMEcomplete.

Proof. Consider an LTL formula ψ = ψ strong ∧ ψ weak over I ∪ O. It is not hard to see that a transducer T ge-realizes ψ weak with guarantee ψ strong iff T realizes ϕ = ψ strong ∧((∃O.ψ weak ) → ψ weak ). We can then construct a UCW A ϕ for L(ϕ) by dualizing an NBW for its negation ¬ψ strong ∨ ((∃O.ψ weak ) ∧ ¬ψ weak ), which can be constructed using techniques similar to those in the proof of Theorem 1. We then proceed with standard synthesis for A ϕ . Note that the approach is Safraless. Taking an empty (that is, True) guarantee, a lower bound follows from the 2EXPTIME-hardness of LTL ge-synthesis.

For a language L ⊆ (2 I∪O ) ω and a finite word

That is, L w is the language of suffixes of words in L that have w as a prefix. We say that a word w ∈

x ⊗ y is green for L. When a system is lucky to interact with an environment that generates a green input sequence, we want the system to react in a way that generates a green prefix, and then realizes the specification. Formally, we say that a strategy f :

It is not hard to see that for ge-realizable languages, green and light green coincide. Indeed, if L is universally satisfiable and ge-realizable, then L is realizable. Theorem 3. ge-realizability is strictly stronger than green realizability.

Proof. We first prove that every strategy f : (2 I ) + → 2 O that ge-realizes a specification ψ also green realizes ψ. Consider x ∈ (2 I ) + that is green for ψ. By definition, there is y ∈ (2 O ) + such that L x⊗y is realizable. Then, for every

is green, and so f green realizes ψ.

We continue and describe a specification that is green realizable and not gerealizable. Let I = {p} and O = {q}. Consider the specification ψ = G((Xp) ↔ q). Clearly, ψ is not realizable, as the system has to commit a value for q before a value for Xp is known. Likewise, no word w ∈ (2 I∪O ) * is green for ψ, and so no finite input sequence x ∈ (2 I ) * is green for ψ. Hence, every strategy (vacuously) green realizes ψ. On the other hand, for every input sequences x ∈ (2 I ) ω there is an output sequence y ∈ (2 O ) ω such that x ⊗ y |= ψ. Thus, all input sequences are hopeful for ψ. Thus, synthesis and ge-synthesis coincide for ψ, which is not ge-realizable.

Theorem 3 brings with it two good news. The first is that a ge-realizing transducer has the desired property of being also green realizing. The second has to do with our goal of providing the user with information about the satisfaction status, in particular raising a green flag whenever a green prefix is detected. By Theorem 3, such a flag indicates that the computation generated by our ge-realizing transducer satisfies the specification. A naive way to detect green prefixes for a specification ψ is to solve the synthesis problem for ψ by solving a game on top of a DPW D ψ for ψ. The winning positions in the game are states in D ψ . By defining them as accepting states, we can obtain from D ψ a DFW for green prefixes. Then, we run this DFW in parallel with the ge-realizing transducer, and raise the green flag whenever a green prefix is detected. This, however, requires a generation of D ψ and a solution of parity games. Below we describe a much simpler way, which makes use of the fact that our transducer ge-realizes the specification.

Recall that if L is universally satisfiable and ge-realizable, then L is realizable. Accordingly, given a transducer T that ge-realizes ψ, we can augment it with green flags by running in parallel a DFW that detects light-green prefixes. As we argue below, constructing such a DFW only requires an application of the subset construction on top of an NBW for the existential projection of ψ on 2 I .

Proof. Let A ψ = 2 I∪O , Q, δ, Q 0 , α be an NBW for L(ψ), and let B ψ = 2 I , Q, δ , Q 0 , α be its existential projection on 2 I . Thus, for every q ∈ Q and i ∈ 2 I , we

where M follows the subset construction of B ψ : for every S ∈ 2 Q and i ∈ 2 I , we have M (S, i) = s∈S δ (s, i). Then, F = {S ∈ 2 Q : L(B S ψ ) = (2 I ) ω }. Observe that S rejects x ∈ (2 I ) * iff there is x ∈ (2 I ) ω such that for all y ∈ (2 O ) * and y ∈ (2 O ) ω , no state in δ(Q 0 , x ⊗ y) accepts x ⊗ y . Thus, S rejects x iff x is not light green, and accepts it otherwise. Note that the definition of F involves universality checking, possibly via complementation, yet no determinization is required, and the size of S is 2 2 O(|ψ|) .

Note that once we reach an accepting state in S, we can make it an accepting loop. Indeed, once a green prefix is detected, then all prefixes that extend it are green. Accordingly, once the green flag is raised, it stays up. Also note that if an input sequence is not hopeful for ψ, then none of its prefixes is light green for ψ. The converse, however, is not true: an input sequence may be hopeful and still have no light green prefixes. For example, taking I = {p}, the input sequence {p} ω is hopeful for Gp, yet none of its prefixes is green light, as it can be extended to an input sequence with ¬p.

Green flags provide information about satisfaction. Two additional flags of interest are related to safety and co-safety properties:

for all y ∈ (2 O ) * , we have that x ⊗ y is red for L. Thus, when the environment generates x, then no matter how the system responds, L is not satisfied.

-a word w ∈ (2 I∪O ) * is blue for L when L w = (2 I∪O ) ω , and then define a word x ∈ (2 I ) * as blue for L if there is y ∈ (2 O ) * such that x ⊗ y is blue for L. Thus, when the environment generates x, the system can respond in a way that guarantees satisfaction no matter how the interaction continues.

A monitor that detects red and blue prefixes for L can be added to a transducer that ge-realizes L. As has been the case with the monitor for green prefixes, its construction is based on applying the subset construction on an NBW for L [16] . Also, once a red or blue flag is raised, it stays up. In a way analogous to green realizability, we seek a transducer that ge-realizes the specification and generates a red prefix only if all interactions generate a red prefix, and generates a blue prefix whenever this is possible. In the full version, we show that while ge-realization implies red realization, it may conflict with blue realization.

ge-synthesis is of special interest when the satisfaction value of the specification is multi-valued, and we want to synthesize high-quality systems. We start by defining the multi-valued logic LTL[F], which is our multi-valued specification formalism. We then study LTL[F] ge-synthesis, first in a worst-case approach, where the satisfaction value of a transducer is the satisfaction value of its computation with the lowest satisfaction value, and then in a stochastic approach, where it is the expected satisfaction value, given a distribution of the inputs.

Let The logic LTL can be viewed as LTL [F] for F that models the usual Boolean operators. In particular, the only possible satisfaction values are 0 and 1. We abbreviate common functions as described below. Let x, y, λ ∈ [0, 1]. Then,

x ∈ (2 I ) ω }, namely the satisfaction value of ψ in the worst-case. Then, the synthesis problem is to find, given ψ, a transducer that maximizes its satisfaction value. Moving to a decision problem, given ψ and a threshold value v ∈ [0, 1], we say that ψ is v-realizable if there exists a transducer T such that [[T , ψ]] ≥ v, and the synthesis problem is to find, given ψ and v, a transducer T that v-realizes ψ. 

For a value v ∈ [0, 1], we say that

We study two variants of LTL[F] ge-synthesis:

ψ and a value v ∈ [0, 1], and the goal is to generate a transducer whose computation on every input sequence that is v-hopeful has satisfaction value at least v. Formally, a function f :

to generate a transducer whose computation on every input sequence has the highest possible satisfaction value for this input sequence. Formally, a function f :

In the Boolean case, the two variants coincide, taking v = 1. Indeed, then, for every x ∈ (2 I ) ω , if x is hopeful, then x ⊗ f (x) has to satisfy ψ. We note that ge-realization with a threshold is not monotone, in the sense that decreasing the threshold need not lead to ge-realization. Indeed, the lower is the threshold v, the more input sequences are v-helpful (see Example 2) . Accordingly, we do not search for a maximal threshold, and rather may ask about a desired threshold or about ge-synthesis without a threshold.

Solving the ge-synthesis problem, a naive combination of the automata construction of Theorem 4 with the projection technique of Theorem 1, corresponds to an erroneous semantics of EQLTL[F], as noted in Remark 3. Before describing our construction, it is helpful to state the correct (perhaps less intuitive) interpretation of existential and universal quantification in the quantitative setting: 

x ∈ (2 I ) ω , we have that [[x, ∃O.ψ]] = 1 − [[x, ∀O.¬ψ]]. Accordingly, for every value v ∈ [0, 1], we have that [[x, ∃O.ψ]] < v iff [[x, ∀O.¬ψ]] > 1 − v. Proof. By definition, [[x, ∃O.ψ]] = max y∈(2 O ) ω [[x ⊗ y, ψ]] = 1 − min y∈(2 O ) ω 1 − [[x ⊗ y, ψ]] = 1 − min y∈(2 O ) ω [[x ⊗ y, ¬ψ]] = 1 − [[x, ∀O.¬ψ]]. Then, [[x, ∃O.ψ]] < v iff 1 − [[x, ∃O.ψ]] > 1 − v iff [[x, ∀O.¬ψ]] > 1 − v.

. Similarly, we have the following.

Proof. We show we can adjust the upper bound described in the proof of Theorem 1 to the multi-valued setting. Given an LTL[F] formula ψ over I ∪ O and a threshold v ∈ [0, 1], we describe an algorithm that returns a transducer T that ge-realizes ψ with threshold v, or declares that no such transducer exists.

By definition, we have that T ge-realizes ψ with threshold v if for every input sequence x, we have that f T is v-good for x with respect to ψ. Thus, [17] , the synthesis problem for UCW can be solved in EXPTIME.

The lower bound follows from the 2EXPTIME-hardness of LTL gerealizability.

Proof. We start with the upper bound. Given an LTL[F] specification ψ over I ∪ O, we describe an algorithm that returns a transducer T that ge-realizes ψ or declares that no such transducer exists.

As discussed above, a transducer T ge-realizes ψ iff for every input sequence x ∈ (2 I ) ω and value v ∈ [0, 1], we have that f T is v-good for x with respect to ψ. Accordingly, we construct a UCW whose language is v∈V (ψ) {w ∈ (2 I∪O ) ω :

For for all v ∈ V (ψ). By Theorem 4, the size of V (ψ) is exponential in ψ, and thus so is the size of B. We then solve usual synthesis for the complementing UCW, whose language is as required. By [17] , the synthesis problem for UCW can be solved in EXPTIME. The lower bound follows from the 2EXPTIME-hardness of LTL ge-realizability.

The quantitative setting allows the designer to tune down "satisfaction by hoplessness": rather than synthesizing ψ ∨ ∀O.¬ψ, we can have a factor λ and synthesize ψ ∨ λ ∀O.¬ψ. In Sect. 5.3 below we study additional ways to refer to hopefulness levels.

In Sect. 5 [3] . There, the specification consists of a multi-valued assumption A, which in our case is ∃O.ψ, and a multi-valued guarantee G, which is our case is ψ.

There The choice of an appropriate comb function depends on the setting. Implication is in order when harsh environments may outweigh the actual performance of the system. For example, if our specification measures the uptime of a server in a cluster, then environments that cause very frequent power failures render the server unusable, as the overhead of reconnecting it outweighs its usefulness. In such a case, being shut down is better than continuously trying to reconnect, and so we give a higher satisfaction value for the server being down, which depends only on the environment. Then, as demonstrated with the cleaning robot in Sect. 1, the difference and ratio functions are fairly natural when measuring "realization of potential". We now describe a more detailed example when these measures are in order.

Example 3. Consider a controller for an elevator in an n-floor building. The environment sends to the controller requests, by means of a truth assignment to I = {1, . . . , n}, indicating the subset of floors in which the elevator is requested. Then, the controller assigns values to O = {up, down}, directing the elevator to go up, go down, or stay. The satisfaction value of the specification ψ reflects the waiting time of the request with the slowest response: it is 0 when this time is more than 2n, and is 1 when the slowest request is granted immediately. Sure enough, there is no controller that attains satisfaction value 1 on all input sequences, and so ψ is not realizable with satisfaction value 1. Also, adding assumptions about the behavior of the environment is not of much interest. Using AG ge-realizability, we can synthesize a controller that behaves in an optimal way. For example, using the difference function, we measure the performance of the controller on an input sequence x ∈ (2 I ) ω with respect to the best possible performance on x. Note that such a best performance needs a look-ahead on requests yet to come, which is indeed the satisfaction value of ∃O.ψ in x. Thus, the assumption [[x, ∃O.ψ]] actually gives us the performance of a good-enough off-line controller. Accordingly, using the ratio function, we can synthesize a system with the best competitive ratio for an on-line interaction [7] .

Given an LTL[F] formula ψ and a function comb, we define the ge-AGrealization value of ψ in a transducer T by min{comb(

x ∈ (2 I ) ω }. Then, our goal in AG ge-realizability is to find, given an LTL[F] formula ψ and a function comb, the maximal value v ∈ [0, 1] such that there exists a transducer T whose AG ge-realization value of ψ is v. The AG ge -synthesis problem is then to find such a transducer.

We start by solving the decision version of AG ge-realizability.

The problem of deciding, given an LTL[F] formula ψ, a function comb, and a threshold v ∈ [0, 1], whether there exists a transducer T whose AG ge-realization value of ψ is v, is 2EXPTIME-complete.

Proof. Recall that V (ψ) is the set of possible satisfaction values of ψ (and hence of ∃O.ψ), and that by Theorem 4, we have that |V (ψ)| ≤ 2 |ψ| . Let [[w, ψ] ] that are allowed to be generated by a transducer whose AG ge-realization value of ψ is at least v. By definition, AG ge-realization of ψ with value v coincides with realization of the lan- ≥ v 2 }, and proceed to construct an NBW for L v by taking the union of NBWs A v1,v2 for all v 1 , v 2 ∈ G v , each of which is the product of NBWs A ≤v1 ∃O.ψ and A ≥v2 ψ , as in the proof of Theorem 5. Aiming to proceed Safralessly, we can also construct a UCW for L v , as follows. First, note that by the monotonicity of comb, for every v 1 

we can obtain a UCW for L v by dualizing an NBW that is the union of NBWs A u1,u2 , for all u 1 , u 2 ∈ V (ψ) × V (ψ) \ G v , each of which is the product of NBWs A ≥u1 ∃O.ψ and A ≤u2 ψ . Observe that in all cases, the size of the NBW is 2 O(|ψ|) . Indeed, there are at most 2 2|ψ| pairs in the union, and, by Theorem 4, the size of the NBW for each pair is 2 O(|ψ|) .

The lower bound follows from the 2EXPTIME-hardness of LTL gerealizability.

By Theorem 4, the number of possible satisfaction values for ψ is at most 2 |ψ| . Thus, the number of possible values for comb (A, G) , where A and G are satisfaction values of ψ, is at most 2 2|ψ| . Using binary search over the image of comb, we can use Theorem 7 to obtain the following. However, the solution described in Sect. 5.2 is simpler than the one described here for the general case.

The setting of LTL[F] ge-synthesis studied in Sects. 5.2 and 5.3 takes the different satisfaction values into an account, but is binary, in the sense that a specification is either (possibly AG) ge-realizable, or is not. In particular, in case the specification is not ge-realizable, synthesis algorithms only return "no". In this section we add a quantitative measure also to the underlying realizability question. We do so by assuming a stochastic environment, with a known distribution on the inputs sequences, and analyzing the expected performance of the system.

For completeness, we remind the reader of some basics of probability theory. For a comprehensive reference see e.g., [25] . Let Σ be a finite alphabet, and let ν be some probability distribution over Σ ω . For example, in the uniform distribution over (2 I ) ω , the probability space is induced by sampling each letter with probability 2 −|I| , corresponding to settings in which each signal in I always holds in probability 1 2 . We assume ν is given by a finite Markov Decision Process (MDP). That is, ν is induced by the distribution of each letter i ∈ 2 I at each time step, determined by a finite stochastic control process that takes into account also the outputs generated by the system (see [2] for the precise model). A random variable is then a function X : Σ ω → R. When X has a finite image V , which is the case in our setting, its expected value is E[X] = v∈V v · Pr(X −1 (v)). Intuitively, E[X] is the "average" value that X attains. Next, consider an event

Pr(E) , where 1 E X is the random variable that assigns X(w) to w ∈ E and 0 to w ∈ E. Intuitively, E[X|E] is the average value that X attains when restricting to words in E, and normalizing according to the probability of E itself.

We continue and review the high-quality synthesis problem [2] , where the ge variant is not considered. There, the environment is assumed to be stochastic and we care for the expected satisfaction value of an LTL[F] specification in the computations of a transducer T , assuming some given distribution on the inputs sequences. Formally, let X T ,ψ : (2 I ) ω → R be a random variable that assigns each sequence x ∈ (2 I ) ω of input signals with [[T (x) , ψ]]. Then, when the sequences in (2 I ) ω are sampled according to a given distribution ν of (2 I ) ω , we define [[T , ψ]] ν = E[X T ,ψ ]. Since ν is fixed, we omit it from the notation and use [[T , ψ] ] in the following.

Given an LTL formula ψ, we can view it as an LTL[F] formula with possible satisfaction values {0, 1}, apply to it high-quality synthesis a-la [2] , and find a transducer T that maximizes E[X T ,ψ ]. An interesting observation is that if T ge-realizes ψ, then it also maximizes E[X T ,ψ ]. Indeed, all input sequences that can contribute to the expected satisfaction value, do so.

We introduce and study two measures for high-quality synthesis in a stochastic environment. In the first, termed expected ge-synthesis, all input sequences are sampled, yet the satisfaction value in each input sequence takes its hopefulness level into account. In the second, termed conditional expected ge-synthesis, only hopeful input sequences are sampled.

We start with expected ge-synthesis. There, instead of associating each In [2] , it is shown that the high-quality synthesis problem can be solved in doubly-exponential time, also in the presence of environment assumptions. In the solution, the first step is the translation of the involved formulas to DPWs. In order to extract from [2] the results relevant to us, we describe them by means of discrete quantitative specifications, defined as follows. A discrete quantitative specification Ψ over I ∪ O is given by means of a sequence A 1 , . . . , A n of DPWs, with (2 I∪O 

As in the Boolean setting, also in the high-quality one we would like to add to a ge-realizing transducer guarantees and indications about the satisfaction level. As we detail below, the quantitative setting offers many possible ways to do so.

High-Quality ge-Synthesis with Guarantees. We consider specifications of the form ψ = ψ strong ∧ψ weak , where essentially, we seek a transducer that realizes ψ strong and (possibly AG) ge-realizes ψ weak . Maximizing the realization value of ψ strong may conflict with maximizing the ge-realization value of ψ weak , and there are different ways to trade-off the two goals. Technically, in the decision-problem variant, we are given two thresholds v 1 , v 2 ∈ [0, 1], and we seek a transducer T that realizes ψ strong with value at least v 1 , and ge-realizes ψ weak with value at least v 2 . Then, one may start, for example, by maximizing the value v 1 , and then find the maximal value v 2 that may be achieved simultaneously. Alternatively, one may prefer to maximize v 2 , or some other combination of v 1 and v 2 . Also, it is possible to decompose ψ further, to several strong and weak components, each with its desired threshold.

The solutions in the different settings all involve a construction of a UCW A ≥v1 ψstrong , and its product with the automata constructed in the solutions for the different ge-synthesis variants. We thus have the following. We note that when the solution for ψ weak is Safraless, we can use a UCW for ψ strong to maintain a Safraless construction.

high-quality ge-synthesis with a guarantee can be solved in doubly-exponential time.

Flags by a High-Quality ge-Realizing Transducer. In the quantitative setting, we parameterized the flags raised by the ge-realizing transducer by values in [0, 1], indicating the announced satisfaction level. Thus, rather than talking about prefixes being green, red, or blue, we talk about them being vgreen, v-red, and v-blue, for v ∈ [0, 1], which essentially means that a satisfaction value of at least v is guarantees (in green and blue flags) or is impossible (in red ones). We can think of those as "degrees" of green, red, and blue. Below, we formalize this intuition and argue that even an augmentation of a transducer that ge-realizes ψ by flags for all values in V (ψ) leaves the problem in doublyexponential time.

A quantitative language over 2 I∪O is L : (2 I∪O ) ω → [0, 1]. For a quantitative language L and a word w ∈ (2 I∪O ) * , we define L w as the quantitative language where for all w ∈ (2 I∪O ) ω , we have L w (w ) = L(w · w ). For a value v ∈ [0, 1], a word w ∈ (2 I∪O ) * is v-green for L if L w is v-realizable. That is, there is a transducer T such that [[T, L w ]] ≥ v. A word x ∈ (2 I ) * is v-green for L if there is y ∈ (2 O ) * such that x⊗y is v-green for L. Thus, when the environment generates x, the system can respond in a way that would guarantee v-realizability. Finally, we say that L is green realizable if there is a strategy f : (2 I ) + → 2 O that for every threshold v and for every input x ∈ (2 I ) + that is v-green for L, we have that x ⊗ f (x) is v-green for L. It is not hard to see that Theorem 3 carries over to the quantitative setting, thus quantitative optimal realizability is strictly stronger than quantitative green realizability. In particular, if a transducer T optimally realizes an LTL[F] formula ψ, then T also green realizes ψ. In the full version, we describe quantitative definitions also for red and blue prefixes, and describe monitors for the detection of the various types of prefixes.

We introduced and solved several variants of ge-synthesis. Our complexity results are tight and show that ge-synthesis is not more complex than traditional synthesis. In practice, however, traditional synthesis algorithms do not scale well, and much research is devoted for the development of methods and heuristics for coping with the implementation challenges of synthesis. A natural future research direction is to extend these heuristics and methods for gesynthesis. We mention here two specific examples.

Efficient synthesis algorithms have been developed for fragments of LTL [21] . Most notable is the GR(1) fragment [18] , which supports assume-guarantee reasoning, and for which synthesis has an efficient symbolic solution. Adding existential quantification to GR(1) specifications, which is how we handled LTL ge-synthesis, is not handled by its known algorithms, and is an interesting challenge. The success of SAT-based model-checking have led to the development of SAT-based synthesis algorithms [6] , where the synthesis problem is reduced to satisfiability of a QBF formula. The fact the setting already includes quantifiers suggests it can be extended to ge-synthesis. A related effort is bounded synthesis algorithms [13, 24] , where the synthesized systems are assumed to be of a bounded size and can be represented symbolically [10] .

Formalizing and reasoning about quality

High-quality synthesis against stochastic environments

Quantitative assume guarantee synthesis

Better quality in synthesis through quantitative objectives

Graph games and reactive synthesis

Sat-based methods for circuit synthesis

Online Computation and Competitive Analysis

Environment assumptions for synthesis

Logic, arithmetics, and automata

Symbolic bounded synthesis

Rational synthesis

Automata theory and model checking

Temporal synthesis for bounded systems and environments

Synthesis with rational environments

Safraless compositional synthesis

Model checking of safety properties

Safraless decision procedures

Synthesis of reactive(1) designs

The temporal semantics of concurrent programs

On the synthesis of a reactive module

Playing games with boxes and diamonds

Modular synthesis of reactive systems

On the complexity of ω-automata

Bounded synthesis

A First Course in Probability

The complementation problem for Büchi automata with applications to temporal logic

Reasoning about infinite computations

Playing and Reality

Temporal logic can be more expressive

Open Access This chapter is licensed under the terms of the Creative Commons