Hello, my name is David Benoist I work in the Interuniversity Health Library in Paris, Where I am in charge of (some of) the online services.

You can see there a picture of the main room, dating back from the nineteenth century.

It is some kind of subliminal advertising : as it is one of the libraries you can visit in the Quartier Latin tour, on August the twentieth-second.

In one week, if you are still in France.

Today, I was asked to speak about the links between health and libraries, as a short conclusion for this meeting.

As you already know the importance of these connections, my speech will be a subjective one, from a French point of view, About the challenges we face in our practice, and the chances we have… Some things I will say might seem obvious to you, but I felt they were important to remind in a time of change.

Librarianship is a job with lots of variety.

But in health it has some very specific aspects.

Most of us work in particular environments : universities, professional schools, hospitals…

Which is hardly insignificant.

Let me quote Steven Chang, who recently wrote a blog post about his new job as a hospital librarian in Melbourne : "In many ways, medical librarianship isn't radically different from other library fields. The fundamental principles don't change. But it's still noticeably different, and in certain aspects, entirely unique.

The first immediately obvious signal that jumped out at me was hearing the continuous kaleidoscope of colour-coded emergencies and announcements over the hospital PA. We are here to help students become good physicians, to help physicians take relevant decisions, and in the end to help the healing process.

Health is a domain in which we are all interested one day or another : as we all have been, or will be patients.

That makes our jobs so special and rewarding.

In libraries, we deal with huge amounts of data : until now, bibliographic references.

And sometimes data produced by researchers, leading to scientific articles. This question of data was very important today.

And now, everyone is producing health data :

Informations we write online, data from apps, smart watches and other objects monitoring our bodies… All these data are useful for medical care, medical institutions, governments, insurance companies, banks… Understanding and exploiting these resources are a challenge for our patrons, and thus for us.

We will have to learn how to treat these, as it was said during this meeting.

Beyond these specifics, we also face more traditional problems.

These statements are well-known, but important to consider:

There are more and more scientific publications : for instance, more than twentyfour millions references in PubMed.

And tens of thousands scientific journals, more or less serious. Most of all, the cost of serial is disturbing.

Number of articles in

On the contrary, budgets tend to go just the opposite way.

I picked out a random example, of a big health library in France I will pretend not to know.

On one side, we have decision makers proclaiming that important trends are research and pedagogy.

On the other side, the same people cut budgets, only interested in displaying wide opening hours. This paradox might be a good thing in the end, as the system is no more sustainable :

We cannot continue to pay so much for scientific papers.

For all these reasons, it is an unsettling time for science and medical libraries, all around the world. Some scientific libraries closed down recently, for instance in the United States, in Canada, in France… More broadly, public libraries are being questioned, like in the United Kingdom.

And other examples could be quoted.

A situation creating anxiety among professionals and patrons, with good reason.

[Picture from the collections of Fisheries and Oceans Canada library in Mont-Joli] [Ex: William H. Welch Medical Library at Johns Hopkins University in Baltimore]

Problems which raise two questions: First, will there be health libraries in the future? Of this I am not really sure, at least in France.

-Medical students have little time, even if they always need work spaces without noise (but with some coffee).

-As for physicians, they need access to articles and databases, but they do not always come to us -even if we try to develop personalized appointments.

-It is an interesting trend in my library for instance, with nearly two hundred rendez-vous a year.

-And unfortunately, there are many physicians in France, and I met some, who believe all publications already exist online.

According to them, you can turn libraries into classrooms without books.

And will there be health librarians in the future?

Or will we be replaced by algorithms answering patrons' questions?

I am convinced that the time of retirement has not yet come.

And I think I am not the only one, or you would not have come here today.

For some reasons already mentioned here:

-There are more and more health informations to deal with;

-With these new data physicians and librarians have to exploit.

-And even "traditional" information is not easy to identify:

-Because of indexation getting poorer in some databases, -Because of differences between tools : you do not interrogate MeSH like you do with Emtree in Embase.

-Because of paywalls, interfering with access.

For the moment, humans are still needed to do the job.

But to maintain links, we have to continue to go out of the library, to meet and support patrons.

This statement is true in all fields, but maybe more important for us.

It can be online, as we already do with digital reference, And more and more on social networks, to meet patrons where there are, and help them use these tools, as they require specific precautions in health.

And physically we will have to get closer as well :

In some countries, there are clinical librarians, and for a long time.

In other places, like France, there is no tradition of embedded librarians. I believe it is important to develop that in the future.

To maintain links, we must evolve as our patrons do.

And become familiar with new devices shaping these evolutions :

Smartphones, tablets, and soon Google glasses and connected objects -with their inherent dangers.

The timing is good as these tools allow us to work out of the office.

We must understand how these tools operate and how our patrons use them.

To finally be able to help our patrons:

For instance, some of us already give advices about applications worth using in medical practice.

We will also have to develop new skills, as we have seen today.

And it was really inspiring to hear the different speeches of this meeting and to see what new roles are possible.

-We will have to be teachers (some of us already are), in flesh and blood or online.

-We will have to be publishers;

-or at least to help publishing : informing about copyright issues, promoting Open Access which may be a part of the solution for our problems.

-And the real Open Access, not a greenish or golden way where institutions pay twice for the same articles.

-We will have to maintain repositories to welcome the fruits of research.

-We will have to become data managers.

-We will certainly have to learn more about medicine, to work hand-in-hand with physicians.

-For example helping them for systematic reviews.

In one word, we may have to become what is sometimes called an « informationist ».

And all these things, we should continue to do in a fast and visible way.

It will be more and more important to promote our services: make medical staff aware that there is a library designed for them, to make their work easier...

To show what value we can add with our new skills, even if (or particularly if) the services we provide are dematerialized.

Especially in countries like France, where librarians do not have a natural place in research teams.

Online, this visibility might be increased via semantic web services, which lead us to data, once again.

Data have been quoted a lot today.

Even if we become data managers, some principles we must not forget, especially in medicine.

Health data are very personal and sensitive. We must help people understand how these data are produced, how there are used, and by whom.

And how they can keep control.

Health data are very precious and useful : We have to fight to make science results accessible for those who need them, professional or patients, especially when research is done on public fundings.

In short, we must not forget that health data are produced by people, for peoplewith respect for the individual and privacy.

  […] It's a constant reminder that you serve at an institution where the core mission is to preserve human life […]. There's something unsettling yet exciting about it even after you begin to adapt." http://queryinglibraries.wordpress.com/2014/06/05/what-is-it-like-to-be-a-hospitallibrarian-my-first-month/ We work in special places and we often have demanding and time poor patrons. -Students between night shifts and courses, -Doctors treating new patients, -Or rather their secretaries, as they do not have time to come, -Researchers writing articles, -And sometimes the patient himself.

  PubMed http://casesblog.blogspot.fr/2011/03/there-are-25400-scientific-journals-and.html And as you know, they are more and more expensive. You may have already seen this chart from the Association of Research Libraries about the cost of publications, from the past twenty-five years.

Thank you for your attention

And enjoy your stay in France.


Alberto Camacho
email: acamacho@cs.toronto.edu

Meghyn Bienvenu
email: meghyn@lirmm.fr

Sheila A Mcilraith
email: sheila@cs.toronto.edu

Finite LTL Synthesis with Environment Assumptions and Quality Measures

In this paper, we investigate the problem of synthesizing strategies for linear temporal logic (LTL) specifications that are interpreted over finite traces -a problem that is central to the automated construction of controllers, robot programs, and business processes. We study a natural variant of the finite LTL synthesis problem in which strategy guarantees are predicated on specified environment behavior. We further explore a quantitative extension of LTL that supports specification of quality measures, utilizing it to synthesize high-quality strategies. We propose new notions of optimality and associated algorithms that yield strategies that best satisfy specified quality measures. Our algorithms utilize an automata-game approach, positioning them well for future implementation via existing state-of-the-art techniques.

Introduction

The problem of automatically synthesizing digital circuits from logical specifications was first proposed by [START_REF] Church | Applications of recursive arithmetic to the problem of circuit synthesis[END_REF]. In 1989, Pnueli and Rosner examined the problem of synthesizing strategies for reactive systems, proposing Linear Temporal Logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] as the specification language. In a nutshell, LTL is used to express temporally extended properties of infinite state sequences (called traces), and the aim of LTL synthesis is to produce a winning strategy, i.e. a function that assigns values to the state variables under the control of the system at every time step, in such a way that the induced infinite trace is guaranteed to satisfy the given LTL formula, no matter how the environment sets the remaining state variables.

In 2015, De Giacomo and Vardi introduced the problem of LT L f synthesis in which the specification is described in a variant of LTL interpreted over finite traces [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF]. Finite interpretations of LTL have long been exploited to specify temporally extended goals and preferences in AI automated planning (e.g., [START_REF] Bacchus | Using temporal logics to express search control knowledge for planning[END_REF][START_REF] Baier | A heuristic search approach to planning with temporally extended preferences[END_REF]). In contrast to LTL synthesis, which produces programs that run in perpetuity, LTL f synthesis is concerned with the generation of terminating programs. Two natural and important application domains are automated synthesis of business processes, including web services; and automated synthesis of robot controllers, in cases where program termination is desired.

Despite recent work on LTL f synthesis, there is little written on the nature and form of the LTL f specifications and how this relates to the successful and nontrivial realization of strategies for such specifications. LTL f synthesis is conceived as a game between the environment and an agent. The logical specification that defines the problem must not only define the desired behavior that execution of the strategy should manifest -what we might loosely think of as the objective of the strategy, but must also define the context, including any assumptions about the environment's behavior upon which realization of the objective is predicated. As we show in this work, if assumptions about environment behavior are not appropriately taken into account, specifications can either be impossible to realize or can be realized trivially by allowing the agent to violate assumptions upon which guaranteed realization of the objective is predicated.

We further examine the problem of how to construct specifications where the realization of an objective comes with a quality measure, and where strategies provide guarantees with respect to these measures. The addition of quality measures is practically motivated. In some instances we may have an objective that can be realized in a variety of ways of differing quality (e.g., my automated travel assistant may find a myriad of ways for me to get to KR2018 -some more preferable than others!). Similarly, we may have multiple objectives that are mutually unachievable and we may wish to associate a quality measure with their individual realization (e.g., I'd like my home robot to do the laundry, wash dishes, and cook dinner before its battery dies, but dinner is most critical, followed by dishes).

In this paper we explore finite LTL synthesis with environment assumptions and quality guarantees. In doing so, we uncover important observations regarding the form and nature of LTL f synthesis specifications, how resulting strategies are computed, and the nature of the guarantees we can provide regarding the resulting strategies. In Section 3 we examine the problem of LTL f synthesis with environment assumptions, introducing the notion of constrained LTL f synthesis in Section 4. In Section 5, we propose algorithms for constrained LTL f synthesis, including a reduction to Deterministic Büchi Automata games for the fragment of environment constraints that are conjunctions of safe and cosafe LTL formulae. In Section 6, we examine the problem of augmenting constrained LTL f synthesis with quality mea-sures. We adopt a specification language, LTL f [F ], proposed by [START_REF] Almagor | Quantitative assume guarantee synthesis[END_REF]) and define a new notion of optimal strategies. In Section 7, we provide algorithms for computing high-quality strategies for constrained LTL f synthesis. Section 8 summarizes our technical contributions. Some proofs are deferred to the appendix. This paper (without the appendix proofs) will appear in the Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018).

Preliminaries

We recall the syntax and semantics of linear temporal logic for both infinite and finite traces, as well as the basics of finite state automata and the link between LTL and automata.

Linear Temporal Logic (LTL)

Given a set P of propositional variables, LTL formulae are defined as follows:

ϕ ⊤ | ⊥ | p | ¬ϕ | ϕ 1 ∧ ϕ 2 | ϕ 1 ∨ ϕ 2 | ϕ | ϕ 1 U ϕ 2 | ϕ 1 R ϕ 2
where p ∈ P. Here ¬, ∧, and ∨ are the usual Boolean connectives, and (next), U (until), and R (release) are temporal operators. The formula ϕ states that ϕ must hold in the next timepoint, ϕ 1 U ϕ 2 stipulates that ϕ 1 must hold until ϕ 2 becomes true, and ϕ 1 R ϕ 2 expresses that ϕ 2 remain true until and including the point in which ϕ 1 is made true (or forever if ϕ 2 never becomes true). For concision, we do not include logical implication (→), eventually (♦, 'sometime in the future') and always ( , 'at every point in the future') in the core syntax, but instead view them as abbreviations: α → β ¬α ∨ β, ♦ϕ ⊤ U ϕ and and ϕ ⊥ R ϕ.

LTL formulae are traditionally interpreted over infinite traces π, i.e., infinite words over the alphabet 2 P . Intuitively, an infinite trace π describes an infinite sequence of (time)steps, with the i-th symbol in π, written π(i), specifying the propositional symbols that hold at step i. We use π ⊑ π ′ to indicate that π is a prefix of π ′ . We define what it means for an infinite trace π to satisfy an LTL formula ϕ at step i, denoted π | = i ϕ:

• π | = i ⊤, π ̸ | = i ⊥, and π | = i p iff p ∈ π(i), for each p ∈ P; • π | = i ¬ϕ iff π ̸ | = i ϕ; • π | = i ϕ 1 ∧ ϕ 2 iff π | = i ϕ 1 and π | = i ϕ 2 ; • π | = i ϕ 1 ∨ ϕ 2 iff π | = i ϕ 1 or π | = i ϕ 2 ; • π | = i ϕ iff π | = i+1 ϕ; • π | = i ϕ 1 U ϕ 2 iff there exists j ≥ i such that π | = j ϕ 2 , and for each i ≤ k < j, π | = k ϕ 1 ; • π | = i ϕ 1 R ϕ 2 iff for all j ≥ i either π | = j ϕ 2 or there exists i ≤ k < j such that π | = k ϕ 1 . A formula ϕ is satisfied in π, written π | = ϕ, if π | = 1 ϕ. Two formulas ϕ and ψ are equivalent if π | = ϕ iff π | =
ψ for all traces π. Observe that, in addition to the usual Boolean equivalences, we have the following:

ϕ 1 U ϕ 2 ≡ ¬(¬ϕ 1 R ¬ϕ 2 ) and ¬ ϕ ≡ ¬ϕ.
We consider two well-known syntactic fragments of LTL. The safe fragment is defined as follows [START_REF] Sistla | Safety, liveness and fairness in temporal logic[END_REF]:

ϕ ⊤ | ⊥ | p | ¬p | ϕ 1 ∧ ϕ 2 | ϕ 1 ∨ ϕ 2 | ϕ | ϕ 1 R ϕ 2
The complementary co-safe fragment is similarly defined, using U in place of R . It is known that if ϕ is a safe formula and π ̸ | = ϕ, then there is a finite bad prefix π b ⊑ π such that π ′ ̸ | = ϕ for every infinite trace π ′ with π b ⊑ π ′ . Similarly, if ϕ is a co-safe formula and π | = ϕ, then there exists a finite good prefix π g ⊑ π such that π ′ | = ϕ for every infinite trace π ′ with π g ⊑ π ′ . This means that violation of safe formulae and satisfaction of co-safe formulae can be shown by exhibiting a suitable finite prefix [START_REF] Kupferman | Model checking of safety properties[END_REF].

In this paper, our main focus will be on a more recently studied finite version of LTL, denoted LTL f [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF], in which formulae are interpreted over finite traces (finite words over 2 P ). We will reuse the notation π(i) (i-th symbol) and introduce the notation |π| for the length of π. LTL f has precisely the same syntax as LTL and the same semantics for the propositional constructs, but it differs in its interpretation of the temporal operators:

• π | = i ϕ iff |π| > i and π | = i+1 ϕ; • π | = i ϕ 1 U ϕ 2 iff there exists i ≤ j ≤ |π| such that π | = j ϕ 2 ,
and

π | = k ϕ 1 , for each i ≤ k < j; • π | = i ϕ 1 R ϕ 2 iff for all i ≤ j ≤ |π| either π | = j ϕ 2 or there exists i ≤ k < j such that π | = k ϕ 1
We introduce the weak next operator ( ) as an abbreviation: ϕ ϕ ∨ ¬ ⊤. Thus, ϕ holds if ϕ holds in the next time step or we have reached the end of the trace. Over finite traces, ¬ ϕ ¬ϕ, but we do have ¬ ϕ ≡ ¬ϕ. As before, we say that ϕ is satisfied in π, written π | = ϕ, if π | = 1 ϕ. Note that we can unambiguously use the same notation for LTL and LTL f so long as we specify whether the considered trace is finite or infinite.

Finite State Automata

We recall that a non-deterministic finite-state automaton (NFA) is a tuple A = ⟨Σ, Q, δ, Q 0 , F⟩, where Σ is a finite alphabet of input symbols, Q is a finite set of states, Q 0 ⊆ Q is a set of initial states, F ⊆ Q is a set of accepting states, and δ : Q × Σ → 2 Q is the transition function. NFAs are evaluated on finite words, i.e. elements of Σ * . A run of A on a word w = θ 1 • • • θ n is a sequence q 0 • • • q n of states, such that q 0 ∈ Q 0 , and q i+1 ∈ δ(q i , θ i+1 ) for all 0 ≤ i < n. A run q 0 • • • q n is accepting if q n ∈ F, and A accepts w if some run of A on w is accepting. The language of an automaton A, denoted L(A), is the set of words accepted by A.

Deterministic finite-state automata (DFAs) are NFAs in which |Q 0 | = 1 and |δ(q, θ)| = 1 for all (q, σ) ∈ Q × Σ. When A is a DFA, we write δ : Q×Σ → Q and q ′ = δ(q, θ) in place of q ′ ∈ δ(q, θ), and when Q 0 = {q 0 }, we will simply write q 0 (without the set notation). For every NFA A, there exists a DFA that accepts the same language as A and whose size is at most single exponential in the size of A. The powerset construction is a well-known technique to determinize NFAs [START_REF] Rabin | Finite automata and their decision problems[END_REF].

Non-deterministic Büchi automata (NBA) are defined like NFAs but evaluated on infinite words, that is, elements of Σ ω . A run of A on an infinite word w = θ 1 θ 2 • • • is a sequence ρ = q 0 q 1 q 2 • • • of states, such that q 0 ∈ Q 0 , and q i+1 ∈ δ(q i , θ i+1 ) for every i ≥ 0. A run ρ is accepting if inf(ρ) ∩ F ∅, where inf(ρ) is the set of states that appear infinitely often in ρ. We say that an NBA A accepts w if some run of A on w is accepting. Analogous definitions apply to deterministic Büchi automata (DBAs).

We will also consider deterministic finite-state transducers (also called Mealy machines, later abbreviated to 'transducers'), given by tuples T = ⟨Σ, Ω, Q, δ, ω, q 0 ⟩, where Σ and Ω are respectively the input and output alphabets, Q is the set of states, δ : Q × Σ → Q is the transition function, ω : Q × Σ → Ω is the output function, and q 0 the initial state. The run of T on w = θ 1 θ 2 . . . ∈ Σ ω is an infinite sequence of states q 0 q 1 q 2 . . . with q i+1 ∈ δ(q i , θ i+1 ) for every i ≥ 0, and the output sequence of T on w is ω(q 0 , θ 1 )ω(q 1 , θ 2 ) . . ..

Given an LTL f formula ϕ, one can construct an NFA that accepts precisely those finite traces π with π | = ϕ (e.g. [START_REF] De Giacomo | Synthesis for LTL and LDL on finite traces[END_REF]). For every safe formula ϕ s (resp. co-safe formula ϕ c ), one can construct an NFA that accepts all bad prefixes of ϕ s (resp. good prefixes of ϕ c ) [START_REF] Kupferman | Model checking of safety properties[END_REF]. In these constructions, the NFAs are worst case single exponential in the size of the formula. By determinizing these NFAs, we can obtain DFAs of doubleexponential size that recognize the same languages.

LTL and LTL f Synthesis

To set the stage for our work, we recall the definition of LTL synthesis in the infinite and finite trace settings and the relationship between planning and synthesis.

LTL Synthesis

An LTL specification is a tuple ⟨X, Y, ϕ⟩ where ϕ is an LTL formula over uncontrollable variables X and controllable variables Y. A strategy is a function

σ : (2 X ) * → 2 Y . The infinite trace induced by X = {X i } i≥1 ∈ (2 X ) ω and σ is π[σ, X] = (X 1 ∪ σ(X 1 )) (X 2 ∪ σ(X 1 X 2 )) . . .
The set of all infinite traces induced by σ is denoted

traces(σ) = {π[σ, X] | X ∈ (2 X ) ω }.
The realizability problem ⟨X, Y, ϕ⟩ consists in determining whether there exists a winning strategy, i.e., a strategy σ such that π | = ϕ for every π ∈ traces(σ). The synthesis problem is to compute such a winning strategy when one exists.

LTL synthesis can be viewed as a 2-player game between the environment (X) and the agent (Y). In each turn, the environment makes a move by selecting X i ⊆ X, and the agent replies by selecting Y i ⊆ Y. The aim is to find a strategy σ for the agent that guarantees the resulting trace satisfies ϕ.

Finite LTL Synthesis

We now recall LTL f realizability and synthesis, where the specification formula is interpreted on finite traces. An LTL f specification is a tuple ⟨X, Y, ϕ⟩, where ϕ is an LTL f formula over uncontrollable variables X and controllable variables Y. A strategy is a function σ : (2 X ) * → 2 Y∪{end} such that for each infinite sequence X = {X i } i≥1 ∈ (2 X ) ω of subsets of X, there is exactly one integer n σ,X ≥ 1 with end ∈ σ(X 1 • • • X n σ,X ). The induced infinite trace π[σ, X] is defined as before, and the finite trace induced by X and σ is

π f [σ, X] = (X 1 ∪ σ(X 1 )) . . . X n σ,X ∪ σ(X 1 • • • X n σ,X ) but with end removed from σ(X 1 • • • X n σ,X ). The set of all fi- nite traces induced by σ is denoted traces f (σ) = {π f [σ, X] | X ∈ (2 X ) ω }. A finite trace π is compatible with σ if π ⊑ π ′
for some π ′ ∈ traces f (σ), with ptraces(σ) ('p' for 'partial') the set of all such traces. We call σ a winning strategy for an LTL f specification ⟨X, Y, ϕ⟩ if π | = ϕ for every π ∈ traces f (σ). The realizability and synthesis problems for LTL f are then defined in the same way as for LTL.

Comparison with prior formulations Prior work on LTL f synthesis defined strategies as functions σ : (2 X ) * → 2 Y that do not explicitly indicate the end of the trace [START_REF] De Giacomo | Synthesis for LTL and LDL on finite traces[END_REF][START_REF] Zhu | Symbolic LTLf synthesis[END_REF]Camacho et al. 2018a). In these works, a strategy σ is winning iff for each π ∈ traces(σ) there exists some finite prefix π ′ ⊑ π such that π ′ | = ϕ. Note that in general, multiple prefixes π ′ that satisfy ϕ may exist. We believe that it is cleaner mathematically to be precise about which trace is produced, and it will substantially simplify our technical developments. The two definitions give rise to the same notion of realizability, and existing results and algorithms for LTL f synthesis transfer to our slightly different setting.

Planning as LTL f Synthesis

It has been observed that different forms of automated planning can be recast as LTL f synthesis (see e.g. [START_REF] De Giacomo | Synthesis for LTL and LDL on finite traces[END_REF][START_REF] D'ippolito | Fully observable non-deterministic planning as assumption-based reactive synthesis[END_REF]Camacho et al. 2018b)). We recall that planning problems are specified in terms of a set of fluents (i.e., atomic facts whose value may change over time), a set of actions which can change the state of the world, an action theory whose axioms give the preconditions and effects of the actions (i.e., which fluents must hold for an action to be executable, and how do the fluents change as a result of performing an action), a description of the initial state, and a goal. In classical planning, actions are deterministic (i.e. there is a unique state resulting from performing an action in a given state), and the aim is to produce a sequence of actions leading from the initial state to a goal state. In fully observable non-deterministic (FOND) planning, actions have nondeterministic effects, meaning that there may be multiple possible states that result from performing a given action in a given state (with the effect axioms determining which states are possible results). Strong solutions are policies (i.e., functions that map states into actions) that guarantee eventual achievement of the goal.

We briefly describe how FOND planning can be reduced to LTL f synthesis,1 as the reduction crucially relies on the use of environment assumptions. We will use the set F of fluents as the uncontrollable variables, and the set of actions A for the controllable variables. The high-level structure of the LTL f specification formula is: Φ = (Ψ init ∧ Ψ eff ) → (Ψ pre ∧ Ψ goal ) Intuitively, Φ states that under the assumption that the environment sets the fluents in accordance with the initial state and effect axioms (captured by Ψ init and Ψ eff ), the agent can choose a single action per turn (Ψ one ) in such a way that the preconditions are obeyed (Ψ pre ) and the goal is achieved (Ψ goal ). We set

Ψ goal = ♦(γ ∧ ¬ ⊤),
where γ is a propositional formula over F describing goal states. The formula Ψ one = ψ one with ψ one = ( ⊤ ↔ a∈A a) ∧ a,a ′ ∈A,a a ′ (¬a ∨¬a ′ ) enforces that a single action is performed at each step. The formula Ψ pre can be defined as a∈A (a → ρ a ), where ρ a is a propositional formula over F (typically, a conjunction of literals) that gives the preconditions of a. The formula Ψ init will simply be the conjunction of literals over F corresponding to the initial state. Finally, Ψ eff will be a conjunction of formulae of the form

((κ ∧ a ∧ ρ a ∧ ψ one ) → β) (1)
where a ∈ A, and κ and β are propositional formulas over F . Intuitively, the latter formula states that if the current state verifies κ and action a is correctly performed by the agent (i.e. the preconditions are met and no other action is simultaneously performed) then the next state must satisfy β. We discuss later why it is important to include ρ a ∧ ψ one .

Illustrative Example

We now give a concrete example of an LTL f synthesis problem, which illustrates the importance of environment assumptions. Consider synthesizing a high-level control strategy for your Roomba-style robot vacuum cleaner. You want the robot to clean the living room (LR) and bedroom (BR) when they are dirty, but you don't want it to vacuum a room while your cat is there (the robot scares her). We now describe how this problem can be formalized as LTL f synthesis.

Taking inspiration from the encoding of planning, we will use {clean(z), catIn(z) | z ∈ {LR, BR}} (the fluents 2 in our scenario) as the set of uncontrollable variables, and take the robot's actions {vac(BR), vac(LR)} as the controllable variables. As was the case for planning, it is natural to conceive of the specification as having the form of an implication Ψ cat env → Ψ cat robot , with Ψ cat env describing the rules governing the environment's behavior and Ψ cat robot the desired behavior of the robot. We define Ψ cat robot as the conjunction of: • for z ∈ {LR, BR}, the formula (vac(z) → ρ vac(z) ), with ρ vac(z) = ¬clean(z) ∧ ¬catIn(z) the precondition of vac(z) (we can only vacuum dirty cat-free rooms); • (¬vac(LR) ∨ ¬vac(BR)) (we cannot vacuum in two places at once); • ♦(clean(LR) ∧ clean(BR)) (our goal: both rooms clean). We let ϕ vac(z) = vac(z) ∧ ρ vac(z) ∧ ¬vac(z ′ ) (with z ′ the other room) encode a correct execution of vac(z), and let Ψ cat env be a conjunction of the following:

• for z ∈ {LR, BR}: clean(z) ∨ ϕ vac(z) → clean(z) (if room z is currently clean, or if the robot correctly per- forms action vac(z), then room z is clean in the next state 3 ) • for z ∈ {LR, BR}: (¬clean(z) ∧ ¬vac(z) → ¬clean(z)) (a room can only become clean if it is vacuumed); • (¬catIn(LR) ∨ ¬catIn(BR)) and
(catIn(LR) ∨ catIn(BR)) (the cat is in exactly one of the rooms). As the reader may have noticed, while the assumptions in Ψ cat env are necessary, they are not sufficient to ensure realizability, as the cat may stay forever in a dirty room. If 2 We use notation reminiscent of first-order logic to enhance readability, but the variables (e.g. clean(LR)) are propositional.

3 For simplicity, we assume once a room is clean, it stays clean.

we further assume that the cat eventually leaves each of the rooms (ϕ leaves = ♦¬catIn(BR) ∧ ♦¬catIn(LR)), there is an obvious solution: vacuum a cat-free room, and then simply wait until the other room is cat-free and then vacuum it. However, rather unexpectedly, adding ϕ leaves to Ψ cat env makes the specification Ψ cat env → Ψ cat robot realizable in a trivial and unintended way: by ending execution in the first move, ¬Ψ cat env trivially holds in the resulting length-1 trace π. Indeed, there are three possibilities:

(i) π | = catIn(BR) (so π ̸ | = ♦¬catIn(BR)), (ii) π | = catIn(LR) (so π ̸ | = ♦¬catIn(LR)), or (iii) π | = ¬catIn(LR) ∧ ¬catIn(BR) (so π ̸ | = ( (catIn(LR) ∨ catIn(BR)))).
Clearly, this length-1 strategy is not the strategy that we wanted to synthesize. In Section 4, we propose a new framework for handling environment assumptions which avoids the generation of such trivial strategies and makes it possible to find the desired strategies.

Constrained LTL f Synthesis

To the aim of properly handling environment assumptions, we introduce a generalization of LTL f synthesis, in which the assumptions are separated from the rest of the specification formula and given a different interpretation. Essentially, the idea is that the environment is allowed to satisfy the assumption over the whole infinite trace, rather than on the finite prefix chosen by the agent. This can be accomplished using LTL semantics for the environment assumption, but keeping LTL f semantics for the formula describing the objective.

Formally, a constrained LTL f specification is a tuple ⟨X, Y, α, ϕ⟩, where X and Y are the uncontrollable and controllable variables, ϕ is an LTL f formula over X ∪ Y, and α is an LTL formula over X ∪ Y. Here ϕ describes the desired agent behavior when the environment behaves so as to satisfy α. We will henceforth call ϕ the objective, and will refer to α as the (environment) assumption or constraint (as it acts to constrain the allowed environment behaviors).

A strategy for ⟨X, Y, α, ϕ⟩ is a function σ : (2 X ) * → 2 Y∪{end} such that for each infinite sequence

X = {X i } i≥1 ∈ (2 X ) ω of subsets of X, there is at most one integer n σ,X ≥ 1 with end ∈ σ(X 1 • • • X n σ,X
). If none exists, we write n σ,X = ∞. To account for traces that do not contain end, we redefine traces f (σ) as follows: {π

f [σ, X] | X ∈ (2 X ) ω and n σ,X < ∞}. A strategy σ is an α-strategy if for every X ∈ (2 X ) ω , ei- ther n σ,X < ∞ or π[σ, X] ̸ | = α, i.e. σ terminates on every trace that satisfies α. A winning strategy (w.r.t. ⟨X, Y, α, ϕ⟩) is an α-strategy such that π | = ϕ for every π ∈ traces f (σ).
In other words, winning strategies are those that guarantee the satisfaction of the objective ϕ under the assumption that the environment behaves in a way that constraint α is satisfied. The realizability and synthesis problems for constrained LTL f specifications are defined as before, using this notion of winning strategy.

Because the constraints are interpreted using infinite LTL semantics, we are now able to correctly handle liveness constraints (♦ψ) and fairness constraints as studied in LTL synthesis ( ♦ψ) and FOND planning ( ♦ψ 1 → ♦ψ 2 ) (D'Ippolito, Rodríguez, and Sardiña 2018).

Example 1. Returning to our earlier example, consider the constrained synthesis problem with assumption Ψ cat env (which includes ϕ leaves ) and objective Ψ cat robot . The obvious strategy (vacuum dirty rooms as soon as they are cat-free) gives rise to a winning strategy, in which we output end if we manage to clean both rooms, and otherwise, produce an infinite trace without end in which Ψ cat env is not true. Trivial strategies that terminate immediately will not be winning strategies, as there will be infinite traces that satisfy the constraint but where the length-1 finite trace falsifies the objective.

We remark that if we are not careful about how we write the constraint α, we may unintentionally allow the agent to block the environment from fulfilling α. Remark 1. Suppose that instead of using Equation 1to encode the effects of actions, we employ the simpler ((κ ∧ a) → β). While intuitive, this alternative formulation does not properly encode FOND planning, as the specification may be realized in an unintended way: by performing multiple actions with conflicting effects, or a single action whose precondition is not satisfied, the agent can force the environment to satisfy a contradictory set of formulae β in the next state, causing the assumption to be violated. [START_REF] Chatterjee | Environment assumptions for synthesis[END_REF] discuss this phenomenon in the context of LTL synthesis, and suggest that a reasonable environment constraint is one which is realizable for the environment. We note that the constraints we considered in Section 3 all satisfy this property.

Correspondence with Finite LTL Synthesis We begin by observing that (plain) LTL f synthesis is a special case of constrained LTL f synthesis in which one uses the trivial constraint ⊤ for the environment assumption: Theorem 1. Every winning strategy σ for the LTL f specification ⟨X, Y, ϕ⟩ is a winning strategy for the constrained LTL f specification ⟨X, Y, ⊤, ϕ⟩, and vice-versa. In particular, ⟨X, Y, ϕ⟩ is realizable iff ⟨X, Y, ⊤, ϕ⟩ is realizable.

A natural question is whether a reduction in the other direction exists. Indeed, it is well-known that in the infinite setting, assume-guarantee LTL synthesis 4 with an assumption α and objective ϕ corresponds to classical LTL synthesis w.r.t. α → ϕ (that is, the two synthesis problems have precisely the same winning strategies). The following negative result shows that a simple reduction via implication does not work in the finite trace setting: Theorem 2. There exists an unrealizable constrained

LTL f specification S = ⟨X, Y, α, ϕ⟩ such that the LTL f specifica- tion S → = ⟨X, Y, α → ϕ⟩ is realizable. Proof. Consider the constrained LTL f specification S = ⟨{x, x ′ } , {y} , α, ϕ⟩ with α = ¬x ∧ ♦x and ϕ = ♦(x ′ ∧ y).
We claim that S is unrealizable. Indeed, take any X = X 1 X 2 . . . such that x X 1 , x ∈ X 2 , and x ′ X i for all i ≥ 1. Then no matter which strategy σ is used, the infinite trace π[σ, X] 4 Here we refer to assume-guarantee synthesis as considered in [START_REF] Chatterjee | Environment assumptions for synthesis[END_REF][START_REF] Almagor | Quantitative assume guarantee synthesis[END_REF], where given a pair (α, ϕ), the aim is to construct a strategy such that every induced infinite trace either violates α or satisfies ϕ. This is different from the assume-guarantee synthesis of [START_REF] Chatterjee | Assume-guarantee synthesis[END_REF], in which N agents each have their own goals, and the objective is for each agent to satisfy its own goals.

will satisfy α, and the induced finite trace π f [σ, X], if it exists, will falsify ϕ (as x ′ never holds).

Next consider S → = ⟨{x} , {y} , α → ϕ⟩, and observe that α → ϕ ≡ x∨( ¬x)∨♦(x ′ ∧ y). A simple winning strategy exists: output end in the first time step. Indeed, every induced trace has length 1 and hence trivially satisfies x ∨ ¬x.

With the next theorem, we observe a more fundamental difficulty in reducing constrained LTL f synthesis problems to standard LTL f synthesis: winning strategies for constrained problems may need an unbounded number of time steps to realize the specification, a phenomenon that does not occur in standard LTL f synthesis.

Theorem 3. An LTL f specification is realizable iff it admits a bounded winning strategy, i.e. a strategy for which there exists B > 0 such that every induced finite trace has length at most B. There exist realizable constrained LTL f specifications that do not possess any bounded winning strategy.

Proof. A straightforward examination of the LTL f synthesis algorithm5 in [START_REF] De Giacomo | Synthesis for LTL and LDL on finite traces[END_REF] shows that when ⟨X, Y, ϕ⟩ is realizable, the produced strategy guarantees achievement of ϕ in a number of time steps bounded by the number of states in a DFA for ϕ.

For the second point, consider the constrained LTL f specification S = ⟨{x} , {y} , ♦x, ¬y U (x ∧ y)⟩. Observe that S is realizable, as it suffices to output ¬y until the first x is read, then output {y, end}. Assume for a contradiction that there is a winning strategy σ for S and constant

B > 0 such that n σ,X ≤ B for every X ∈ X ω . Define X B = X B 1 X B 2 . . . as fol- lows: X B i = {x} if i = B + 1 and X B i = ∅ otherwise. The induced trace π = π f [σ, X B
] has length at most B and hence does not contain x. It follows that π ̸ | = ϕ, contradicting our assumption that σ is a winning strategy.

While the implication-based approach does not work in general, we show that it can be made to work for environment assumptions that belong to the safe fragment: Theorem 4. When α is a safe formula, the constrained LTL f specification S = ⟨X, Y, α, ϕ⟩ is realizable iff the LTL f specification S ′ = ⟨X, Y, α ′ → ϕ⟩ is realizable, where α ′ is obtained from α by replacing every occurrence of ψ by ψ.

Proof sketch. Let σ ′ be a winning strategy for ⟨X, Y, α ′ → ϕ⟩, with α a safe formula. To define a winning strategy σ for ⟨X, Y, α, ϕ⟩, we set σ(X

1 • • • X n ) equal to • σ(X 1 • • • X n ) \ {end}, when end ∈ σ(X 1 • • • X n ) and (X 1 ∪ σ(X 1 )) . . . (X n ∪ σ(X 1 • • • X n )) ̸ | = α ′ ; • σ(X 1 • • • X n ), otherwise.
For the other direction, given a winning strategy σ for ⟨X, Y, α, ϕ⟩, we can define a winning strategy

σ ′ for ⟨X, Y, α ′ → ϕ⟩ by setting σ ′ (X 1 • • • X n ) equal to • σ(X 1 • • • X n ) ∪{end}, if (X 1 ∪σ(X 1 )) . . . (X n ∪σ(X 1 • • • X n ))
is a bad prefix for α, and

end σ ′ (X 1 • • • X k ) for k < n; • σ(X 1 • • • X n )\{end}, if end ∈ σ ′ (X 1 • • • X k ) for some k < n; • σ ′ (X 1 • • • X n ) = σ(X 1 • • • X n ), otherwise.
The following example shows that it is essential in the preceding theorem to use α ′ → ϕ rather than α → ϕ:

Example 2. If we let α = (¬x ∨ x) and ϕ = ¬x ∧ y, then the constrained specification ⟨X, Y, α, ϕ⟩ is not realizable (as the environment can output x in the first step), but the LTL f specification ⟨X, Y, α → ϕ⟩ is realizable with a strategy that outputs {y, end} in the first step. Indeed, if the environment outputs x, then ¬α ≡ ♦(x ∧ ¬ x) holds in the induced length-1 trace; if we have ¬x instead, then ϕ holds.

Note however that the negative result in the general case (Theorem 2) continues to hold if α ′ → ϕ is used instead of α → ϕ, since the formulas in that proof do not involve .

Another interesting observation is the environment assumptions Ψ init and Ψ eff used to encode the initial state and action effects in planning are safe formulas. This explains why these constraints can be properly encoded in LTL f using implication and rather than . We note that if we encode planning using constrained LTL f synthesis, then we can use in the effect axioms, which is arguably more natural.

Reduction to LTL Synthesis Every LTL f formula ϕ over P can be polynomially transformed into an LTL formula ϕ inf over P ∪ {alive} such that π | = ϕ inf iff π ′ | = ϕ for some finite prefix π ′ ⊑ π (De Giacomo and Vardi 2013). Intuitively, alive holds for the duration of the (simulated) finite trace. Formally, ϕ inf τ(ϕ) ∧ alive ∧ (alive U ( ¬alive)), where:

τ(p) = p τ(¬ϕ) = ¬τ(ϕ) τ(ϕ 1 ∧ ϕ 2 ) = τ(ϕ 1 ) ∧ τ(ϕ 2 ) τ( ϕ) = (alive ∧ τ(ϕ)) τ(ϕ 1 U ϕ 2 ) = τ(ϕ 1 ) U (alive ∧ τ(ϕ 2 ))
We extend this transformation as follows:

ψ end (end ↔ alive ∧ ¬alive) ∧ (end → ¬end) ψ α,ϕ ψ end ∧ ((α ∨ ♦end) → ϕ inf )
Here ψ end forces the agent to trigger variable end when the end of the trace is simulated and also ensures that end occurs at most once. Formula ψ α,ϕ ensures that ϕ inf is satisfied -i.e., a finite trace that satisfies ϕ and ends is simulated -when either the environment assumption α holds or end occurs.

Theorem 5. The constrained LTL f specification S = ⟨X, Y, α, ϕ⟩ is realizable iff LTL specification S ∞ = ⟨X, Y ∪ {alive, end} , ψ α,ϕ ⟩ is realizable. Moreover, for every winning strategy σ for S ∞ , the strategy σ ′ defined by σ

′ (X 1 • • • X n ) σ(X 1 • • • X n ) \ {alive} is a winning strategy for S.
5 Algorithms for Constrained LTL f Synthesis LTL and LTL f realizability are both 2EXP-complete [START_REF] Pnueli | On the synthesis of a reactive module[END_REF][START_REF] De Giacomo | Synthesis for LTL and LDL on finite traces[END_REF], and we can show the same holds for constrained LTL f problems. The upper bound exploits the reduction to LTL (Theorem 5), and the lower bound is inherited from (plain) LTL f synthesis, which is a special case of constrained LTL f synthesis (Theorem 1). Theorem 6. Constrained LTL f realizability (resp. synthesis) is 2EXP-complete (resp. in 2EXP).

It follows from Theorem 6 that the reduction to infinite LTL realizability and synthesis yields worst-case optimal algorithms. However, we argue that the reduction to LTL does not provide a practical approach. Indeed, while LTL and LTL f synthesis share the same worst-case complexity, recent experiments have shown that LTL f is much easier to handle in practice [START_REF] Zhu | Symbolic LTLf synthesis[END_REF]. Indeed, state-ofthe-art approaches to LTL synthesis rely on first translating the LTL formula into a suitable infinite-word automata, then solving a two-player game on the resulting automaton. The computational bottleneck is the complex transformations of infinite-word automata, for which no efficient implementations exist. Recent approaches to LTL f synthesis also adopt an automata-game approach, but LTL f formulae require only finite-word automata (NFAs and DFAs), which can be manipulated more efficiently.

The preceding considerations motivate us to explore an alternative approach to constrained LTL f synthesis, which involves a reduction to DBA games. Importantly, the DBA can be straightforwardly constructed from DFAs for the constraint and objective formulae, allowing us to sidestep the difficulties of manipulating infinite-word automata.

DBA for Constrained Specifications

For the rest of this section, we assume α = α s ∧ α c , where α s is a safe formula and α c is a co-safe formula6 , both defined over X ∪ Y. Safe and co-safe formulae are well-known LTL fragments [START_REF] Kupferman | Model checking of safety properties[END_REF] of proven utility. Safe formulas are prevalent in LTL specifications and a key part of the encoding of planning as LTL f synthesis (see Section 3.3); the usefulness of co-safe formulas can be seen from our example (Section 3.4) and their adoption in work on robot planning (see e.g. [START_REF] Lahijanian | This time the robot settles for a cost: A quantitative approach to temporal logic planning with partial satisfaction[END_REF]).

Our aim is to construct a DBA that accepts infinite traces π over 2 X∪Y∪{end} such that either (i) π contains a single occurrence of end which induces a finite prefix π ′ with π ′ | = ϕ, or (ii) π doesn't contain end and π ̸ | = α s ∧ α c . Such a DBA A α s ,α c ϕ can be defined by combining three DFAs: A s = ⟨2 P , Q s , δ s , (q 0 ) s , F s ⟩ accepts the bad prefixes of α s ; A c = ⟨2 P , Q c , δ c , (q 0 ) c , F c ⟩ accepts the good prefixes of α c ; and A g = ⟨2 P , Q g , δ g , (q 0 ) g , F g ⟩ accepts models of ϕ. Recall that these DFAs can be built in double-exponential time.

Formally, we let A α s ,α c ϕ = ⟨2 P∪{end} , Q, δ, q 0 , F⟩, where Q, q 0 , and F are defined as follows:

• Q (Q s ∪ {q bad }) × (Q c ∪ {q good }) × Q g ) ∪ {q ⊤ , q ⊥ } • q 0 (
(q 0 ) s , (q 0 ) c , (q 0 ) g ) • F {(q s , q c , q g ) ∈ Q | q s = q bad or q c q good } ∪ {q ⊤ } For 'regular' symbols θ ∈ 2 P (i.e., end θ), we set δ((q s , q c , q g ), θ) = (δ * s (q s , θ), δ * c (q c , θ), δ g (q g , θ)) where:

δ * s (q s , θ) = q bad , if q s = q bad or δ s (q s , θ) ∈ F s δ s (q s , θ), otherwise δ * c (q c , θ) = q good , if q c = q good or δ c (q c , θ) ∈ F c δ c (q c , θ), otherwise
For θ with end ∈ θ, we set δ((q s , q c , q g ), θ) = q ⊤ if δ g (q g , θ) ∈ F g , and δ((q s , q c , q g ), θ) = q ⊥ in all other cases. Accepting state q ⊤ is quasi-absorbing: δ(q ⊤ , θ) = q ⊤ when end θ, and δ(q ⊤ , θ) = q ⊥ otherwise. This forces winning strategies to output variable end at most once. Finally, q ⊥ is an absorbing state: δ(q ⊥ , θ) = q ⊥ for every θ ∈ 2 P∪{end} . Theorem 7. The DBA A α s ,α c ϕ accepts infinite traces π such that either: (i) π( 1

DBA Games

Once a specification has been converted into a DBA, realizability and synthesis can be reduced to DBA games. We briefly recall next the definition of such games and how winning strategies can be computed.

A DBA (or Büchi) game (see e.g. [START_REF] Chatterjee | Algorithms for Büchi games[END_REF]) is a two-player game given by a tuple ⟨X, Y, A⟩, where X and Y are disjoint finite sets of variables and A is a DBA with alphabet 2 X∪Y . A play is an infinite sequence of rounds, where in each round, Player I selects

X i ⊆ X, then Player II selects Y i ⊆ Y. A play is winning if it yields a word (X 1 ∪ Y 1 )(X 2 ∪ Y 2 ) . . .

that belongs to L(A).

A game is winning if there exists a strategy σ : (2 X ) * → 2 Y such that for every infinite sequence X 1 X 2 . . . ∈ X ω , the word (X 1 ∪σ(X 1 ))(X 2 ∪σ(X 1 X 2 )) . . . obtained by following σ belongs to L(A). In this case, we call σ a winning strategy.

Existence of a winning strategy for a DBA game G = ⟨X, Y, A⟩ based upon A = ⟨2 X∪Y , Q, δ, q 0 , F⟩ can be determined by computing the winning region of G. This is done in two steps. First, we compute the set RA(G) of recurring accepting states, i.e. those q ∈ F such that Player II has a strategy from state q to revisit F infinitely often. Next, we define the winning region Win(G) of G as those states in q ∈ Q for which Player II has a strategy for reaching a state in RA(G). The sets RA(G) and Win(G) can be computed in polynomial time by utilizing the controllable predecessor operator:

CPre(S ) = {q ∈ Q | ∀X ⊆ X ∃Y ⊆ Y : δ(q, X ∪ Y) ∈ S }.
We set Reach 0 (S ) = S and Reach i+1 (S ) = Reach i (S ) ∪ CPre(Reach i (S )). Intuitively, Reach i (S ) contains those states from which Player II has a strategy for reaching (or returning to) S in at most i rounds. The limit lim i Reach i (S ) exists because Reach i (S ) ⊆ Reach i+1 (S ), and convergence is achieved in a finite number of iterations bounded by |Q|. To compute RA(G), we set S 1 = F and let S k+1 = S k ∩ lim i Reach i (S k ). The set S k contains those accepting states from which Player II has a strategy for visiting S k no less than k times. The limit lim k S k exists because S k ⊆ S k+1 , and convergence is achieved in a finite number of iterations bounded by |F|. RA(G) is the finite limit of S k , and the set Win(G) is then the finite limit of Reach i (RA(G)). It is easy to see that Win(G) can be computed in polynomial time w.r.t. the size of the DBA A. The following well-known result shows how we can use Win(G) to decide if G is winning. Theorem 8. G is winning iff q 0 ∈ Win(G).

We sketch the proof of the right-to-left implication here, since it will be needed for later results. We suppose that q 0 ∈ Win(G) and show how to construct a transducer T G that implements a winning strategy. Intuitively, the transducer's output function ensures that the transducer stays within Win(G), always reducing the 'distance' to RA(G). More precisely, we can define T G as ⟨2 X , 2 Y , Q, δ ′ , ω, q 0 ⟩, where: the set of states Q and initial state q 0 are the same as for the DBA A, and the transition function δ ′ mirrors the transition function δ of A: δ ′ (q, X) = δ(q, X ∪ ω(q, X)). We define the output function ω as follows:

• Case 1: there exists Y * such that δ(q, X ∪ Y * ) ∈ Win(G).

In this case, we let ω(q, X) be any7 Y ∈ 2 Y such that (a) δ(q, X∪Y) ∈ Reach i+1 (RA(G)), and (b) there is no Y ′ with δ(q, X ∪ Y ′ ) ∈ Reach i (RA(G)). • Case 2: no such Y * exists. We let ω(q, X) be any Y ∈ 2 Y . According to this definition, after reading X, the transducer T G chooses an output symbol Y that allows the underlying automaton A to transition from the current state via X ∪ Y to a state in Win(G) (if some such symbol exists). Moreover, among the immediately reachable winning states, preference is given to those that are closest to RA(G), i.e. those belonging to Reach i (RA(G)) for the minimal value i.

Constrained LTL f Synthesis via DBA Games

Given a constrained LTL f synthesis specification ⟨X, Y, α, ϕ⟩ with α = α s ∧ α c , we proceed as follows:

1. Construct the DBA game G α s ,α c ϕ = ⟨X, Y ∪ {end}, A α s ,α c ϕ ⟩. 2. Determine whether G α s ,α c ϕ is winning: build Win(G α s ,α c ϕ )
and check whether ((q 0 ) s , (q 0 ) c , (q 0 ) g ) ∈ Win(G α s ,α c ϕ ).

3. If G α s ,α c ϕ is not winning, return 'unrealizable'. 4. Otherwise, compute a winning strategy for G α s ,α c ϕ using the transducer from Section 5.2. Using Theorems 7 and 8, we can show that this method is correct and yields optimal complexity: Theorem 9. Consider a constrained LTL f specification S =⟨X, Y, α s ∧ α c , ϕ⟩ where α s (resp. α c ) is a safe (resp. co-safe) formula. Then: • S is realizable iff the DBA game G α s ,α c ϕ is winning; • Every winning strategy for G α s ,α c ϕ is a winning strategy for S, and vice-versa;

• Deciding whether G α s ,α c ϕ is winning, and constructing a winning strategy when one exists, can be done in 2EXP.

Synthesis of High-Quality Strategies

This section explores the use of a quantitative specification language to compare strategies based upon how well they satisfy the specification. We adopt the LTL f [F ] language from [START_REF] Almagor | Formally reasoning about quality[END_REF] and propose a new more refined way of defining optimal strategies.

The Temporal Logic LTL f [F ]

We recall here the language LTL f [F ] proposed by [START_REF] Almagor | Formally reasoning about quality[END_REF]. The basic idea is that instead of a formula being either totally satisfied or totally violated by a trace, a value between 0 and 1 will indicate its degree of satisfaction. In order to allow for different ways of aggregating formulae, the basic LTL syntax is augmented with a set F ⊆ {f : [0, 1] k → [0, 1] | k ∈ N} of functions, with the choice of which functions to include in F being determined by the application at hand.

Formally, the set of LTL f [F ] formulae is obtained by adding f (ϕ 1 , . . . , ϕ k ) to the grammar for ϕ, for every f ∈ F . We assign a satisfaction value to every LTL f [F ] formula, finite trace π, and time step 1 ≤ i ≤ |π|, as follows8 :

⟦π, ⊤⟧ i = 1 ⟦π, ⊥⟧ i = 0 ⟦π, p⟧ i = 1 if p ∈ π(i) 0 otherwise ⟦π, ¬ϕ⟧ i = 1 -⟦π, ϕ⟧ i ⟦π, ϕ 1 ∧ ϕ 2 ⟧ i = min{⟦π, ϕ 1 ⟧ i , ⟦π, ϕ 2 ⟧ i } ⟦π, ϕ⟧ i = ⟦π, ϕ⟧ i+1 ⟦π, f (ϕ 1 , . . . , ϕ k )⟧ i = f (⟦π, ϕ 1 ⟧ i , . . . , ⟦π, ϕ k ⟧ i ) ⟦π, ϕ 1 U ϕ 2 ⟧ i = max i≤i ′ ≤|π| min ⟦π, ϕ 2 ⟧ i ′ , min i≤ j<i ′ {⟦π, ϕ 1 ⟧ j }
The (satisfaction) value of ϕ on π, written ⟦π, ϕ⟧, is ⟦π, ϕ⟧ 1 . We define V(ϕ) ⊆ [0, 1] as the set of values ⟦π, ϕ⟧ i , ranging over all traces π and steps 1 ≤ i ≤ |π|. The following proposition, proven by [START_REF] Almagor | Formally reasoning about quality[END_REF], shows that an LTL f [F ] formula can take on only exponentially many different values.

Proposition 1. For every LTL f [F ] formula ϕ, |V(ϕ)| ≤ 2 |ϕ| .
The functions f allow us to capture a diversity of methods for combining a set of potentially competing objectives (including classical preference aggregation methods like weighted sums and lexicographic ordering).

Example 3. For illustration purposes, consider two variants of our robot vacuum example, with specifications ϕ 1 and ϕ 2 , in which the goal ♦(clean(LR) ∧ clean(BR)) is replaced by ♦(clean(LR)) and ♦(clean(BR)), respectively. We can include in F a binary weighted sum operator sum 0.3,0.7 , where the satisfaction value of sum 0.3,0.7 (ϕ 1 , ϕ 2 ) on trace π is 0.

3 if π | = ϕ 1 ∧ ¬ϕ 2 , 0.7 if π | = ¬ϕ 1 ∧ ϕ 2 , 1 if π | = ϕ 1 ∧ ϕ 2 ,
and zero otherwise. We can thus express that we'd like to clean both rooms, but give priority to the bedroom.

Defining Optimal Strategies

Henceforth, we consider a constrained synthesis LTL f [F ] problem ⟨X, Y, α, ϕ⟩, defined as before except that now ϕ is an LTL f [F ] formula. Such formulae assign satisfaction values to traces, allowing us to rank traces according to the extent to which they satisfy the expressed preferences. It remains to lift this preference order to strategies.

Perhaps the most obvious way to rank strategies is to consider the minimum value of any trace induced by the strategy, preferring strategies that can guarantee the highest worst-case value. This is the approach adopted by [START_REF] Almagor | Formally reasoning about quality[END_REF] for LTL[F ] synthesis. We formalize it for constrained LTL f [F ] synthesis as follows:

Definition 1. The best guaranteed value of strategy σ, denoted bgv(σ), is the minimum value of ⟦π, ϕ⟧ over all π ∈ traces f (σ) (or 0 if traces f (σ) = ∅). A strategy σ is bgvoptimal w.r.t. (α, ϕ) if it is a α-strategy and no α-strategy σ ′ exists with bgv(σ ′ ) > bgv(σ).

Optimizing for the best guaranteed value seems natural, but can be insufficiently discriminative. Consider a simple scenario with X = {x} and Y = {y}. If the environment plays x, then we get value 0 no matter what, and if ¬x is played, a value of 1 is achieved by playing y, and 0 if ¬y is played. Clearly, we should prefer to play y after ¬x, yet the strategy that plays ¬y following ¬x is bgv-optimal, since like every strategy, its bgv is 0. This motivates us to introduce a stronger, context-aware, notion of optimality: Definition 2. Given a strategy σ, trace π ∈ ptraces(σ) that does not contain end, and X ∈ 2 X , the best guaranteed value of σ starting from π•X, written bgv π,X (σ), is the minimum of ⟦π ′ , ϕ⟧ over all traces π ′ ∈ traces f (σ) such that π • (X ∪ Y) ⊑ π ′ for some Y ∈ Y (or 0 if no such trace exists). A strategy σ is a strongly bgv-optimal w.r.t. (α, ϕ) if it is an α-strategy, and there is no α-strategy σ ′ , trace π ∈ ptraces(σ) ∩ ptraces(σ ′ ) without end, and X ∈ 2 X such that bgv π,X (σ ′ ) > bgv π,X (σ).

Strongly bgv-optimal strategies take advantage of any favorable situation during execution to improve the best worstcase value. In the preceding example, they allow us to say that the first strategy is better than the second.

7 Algorithms: High-Quality LTL f Synthesis

In this section, we present novel techniques to compute bgv-optimal and strongly bgv-optimal strategies for a constrained LTL f [F ] synthesis problem ⟨X, Y, α, ϕ⟩. As in Section 5.1, we focus on the case where α is a conjunction α s ∧ α c of safe and co-safe formulae.

Automaton for LTL f [F ]

It has been shown in [START_REF] Almagor | Formally reasoning about quality[END_REF] how to construct, for a given LTL f [F ] formula ϕ and set of values V ⊆ [0, 1], an NFA A ϕ,V = ⟨2 P , Q, δ, Q 0 , F⟩ that accepts finite traces π with ⟦π, ϕ⟧ ∈ V. We briefly recall the construction here. We denote by sub(ϕ) the set of subformulas of ϕ, and let C ϕ be the set of functions g : sub(ϕ) → [0, 1] such that g(ψ) ∈ V(ψ) for all ψ ∈ sub(ϕ). Q contains all consistent functions in C ϕ , where a function g is consistent if, for every ψ ∈ sub(ϕ), the following hold:

• if ψ = ⊤, then g(ψ) = 1, and if ψ = ⊥, then g(ψ) = 0 • if ψ ∈ P then g(ψ) ∈ {0, 1} • if ψ = f (ψ 1 , . . . , ψ k )), then g(ψ) = f (g(ψ 1 ), . . . , g(ψ k ))
The transition function δ is such that g ′ ∈ δ(g, σ) whenever:

• σ = {p ∈ P | g(p) = 1} • g( ψ 1 ) = g ′ (ψ 1 ) for every ψ 1 ∈ sub(ϕ)) • g(ψ 1 U ψ 2 ) = max {g(ψ 2 ), min {g(ψ 1 ), g ′ (ψ 1 U ψ 2 )}} for ev- ery ψ 1 U ψ 2 ∈ sub(ϕ) Finally, the set of initial states is Q 0 = {q ∈ Q | g(ϕ) ∈ V}, and F = {g | g(ψ 2 ) = g(ψ 1 U ψ 2 ) for all ψ 1 U ψ 2 ∈ sub(ϕ)} ∩ {g | g( ψ) = 0 for all ψ ∈ sub(ϕ)}.
The NFA A ϕ,V can be constructed in single-exponential time, and L(A ϕ,V ) = {π | ⟦π, ϕ⟧ ∈ V} [START_REF] Almagor | Formally reasoning about quality[END_REF]. By determinizing A ϕ,V , we obtain a DFA Âϕ,V that accepts the same language and can be constructed in double-exponential time. In what follows, V will always take the form [b, 1], so we'll use Âϕ≥b in place of Âϕ,[b,1] .

Synthesis of bgv-optimal strategies

We describe how to construct a bgv-optimal strategy. First note that given b ∈ [0, 1], we can construct a DBA A α ϕ≥b that recognizes traces such that either (i) α = α s ∧ α c is violated and end does not occur, or (ii) end occurs exactly once and the induced finite trace π is such that ⟦π, ϕ⟧ ≥ b. Indeed, we simply reuse the construction from Section 5.1, replacing the DFA A g with the DFA Âϕ≥b . We next observe that an α-strategy σ with bgv(σ) ≥ b exists iff the DBA game ⟨X, Y ∪ {end}, A α ϕ≥b ⟩ is winning. Thus, by iterating over the values in V(ϕ) in descending order, we can determine the maximal b * for which an α-strategy σ with bgv(σ) ≥ b * exists. A bgv-optimal strategy can be computed by constructing a winning strategy for the DBA game ⟨X, Y ∪ {end}, A α ϕ≥b * ⟩, using the approach in Section 5.2. As there are only exponentially many values in V(ϕ) (Prop. 1), the overall construction takes double-exponential time. Theorem 10. A bgv-optimal strategy can be constructed in double-exponential time.

Synthesis of strongly bgv-optimal strategies

To compute a strongly bgv-optimal stategy, we build a transducer that runs in parallel DBAs A α ≥b for different values b, and selects outputs symbols so as to advance within the 'best' applicable winning region. This idea can be formalized as follows. As in Section 7. We now proceed to the definition of the desired transducer T str = ⟨2 X , 2 Y∪{end} , Q str , δ str , ω str , q str 0 ⟩, obtained by taking the cross product of the set of DBAs A α ≥b with b ∈ B, in order to keep track of the current states in these automata:

• q str 0 = (q b 1 0 , q b 2 0 , . . . , q b m 0 ) and

Q str = Q b 1 × . . . × Q b m • δ str ((q 1 , . . . , q m ), X) = (δ b 1 (q 1 , X ∪ Y), . . . , δ b m (q m , X ∪ Y)),
where Y = ω str ((q 1 , q 2 , . . . , q m ), X) After reading X, the output function identifies the maximal value b ∈ B such that current state q b of A α ≥b can transition, via some symbol X∪Y, into a state in Win(G b ), and it returns the same output as the transducer

T G b in state q b : • ω str ((q 1 , . . . , q m ), X) = ω b (q b , X), where b = max({v ∈ B | ∃Y δ v (q v , X ∪ Y) ∈ Win(G v )})
We note that the transducer T G b can be defined as in Section 5.2 even when q b 0 Win(G b ), but it only returns 'sensible' outputs when it transitions to Win(G b ). Theorem 11. T str implements a strongly bgv-optimal strategy and can be constructed in double-exponential time.

Discussion and Concluding Remarks

It has been widely remarked in the (infinite) LTL synthesis literature that environment assumptions are ubiquitous: the existence of winning strategies is almost always predicated on some kind of environment assumption. This was observed in the work of [START_REF] Chatterjee | Environment assumptions for synthesis[END_REF], motivating the introduction of the influential assume-guarantee synthesis model, and in work on rational synthesis [START_REF] Fisman | Rational synthesis[END_REF], where the environment is assumed to act as a rational agent, and synthesis necessitates finding a Nash equilibrium. Interesting reflections on the role of assumptions in LTL synthesis, together with a survey of the relevant literature, can be found in [START_REF] Bloem | How to handle assumptions in synthesis[END_REF].

In this paper, we explored the issue of handling environment assumptions in LTL f synthesis (De Giacomo and Vardi 2013), the counterpart of LTL synthesis for programs that terminate. Our starting point was the observation that the standard approach to handling assumptions in LTL synthesis (via logical implication) fails in the finite-trace setting. This led us to propose an extension of LTL f synthesis that explicitly accounts for environment assumptions. The key insight underlying the new model of constrained LTL f synthesis is that while the synthesized program must realize the objective in a finite number of steps, the environment continues to exist after the program terminates, so environment assumptions should be interpreted under infinite LTL semantics.

We studied the relationships holding between constrained LTL f synthesis and (standard) LTL f and LTL synthesis. In particular, we identified a fundamental difficulty in reducing constrained LTL f synthesis to LTL f synthesis -the former problem can require unbounded strategies, while bounded strategies suffice for the latter. Nevertheless, when the constraints were restricted to the safe LTL fragment, a reduction from constrained LTL f synthesis to LTL f synthesis is possible. Interestingly, this explains why planning -more naturally conceived as a constrained LTL f synthesis problemcan also be encoded as LTL f synthesis. The connection between synthesis and planning has been remarked in several works (see e.g., [START_REF] De Giacomo | Synthesis for LTL and LDL on finite traces[END_REF][START_REF] D'ippolito | Fully observable non-deterministic planning as assumption-based reactive synthesis[END_REF]Camacho et al. 2018a;2018b;2018c)). We also showed how to reduce constrained LTL f synthesis to (infinite) LTL synthesis, which provides a worstcase optimal means of solving constrained LTL f synthesis problems, in the general case, using (infinite) LTL synthesis tools. In the case where our constraint is comprised of a conjunction of safe and co-safe formulae, we showed that the constrained LTL f synthesis problem can be reduced to DBA games and the winning strategy determined from the winning region. What makes our approach interesting is that the DBA is constructed via manipulation of DFAs, much easier to handle in practice than infinite-word automata.

We next turned our attention to the problem of augmenting constrained LTL f synthesis with quality measures. We were motivated by practical concerns surrounding the ability to differentiate and synthesize high-quality strategies in settings where we may have a collection of mutually unrealizable objective formulae and alternative strategies of differing quality. Our work builds on results for the infinite case, e.g., [START_REF] Almagor | Formally reasoning about quality[END_REF][START_REF] Almagor | Quantitative assume guarantee synthesis[END_REF]; Kupferman 2016) with and without environment assumptions. We adopted LTL f [F ] as our language for specifying quality measures. While the syntax of LTL f [F ] is utilitarian, many more compelling preference languages are reducible to this core language. We defined two different notions of optimal strategies -bgv-optimal and strongly bgv-optimal. The former adapts a similar definition in [START_REF] Almagor | Formally reasoning about quality[END_REF] and the latter originates with us. We focused again on assumptions that can be expressed as conjunctions of safe and co-safe formulae and provided algorithms to compute bgv-and strongly bgv-optimal strategies with optimal (2EXP) complexity.

Proper handling of environment assumptions and quality measures, together with the design of efficient algorithms for such richer specifications, is essential to putting LTL f synthesis into practice. The present paper makes several important advances in this direction and also suggests a number of interesting topics for future work including: the study of other types of assumptions in the finite-trace setting (e.g. rational synthesis), the exploitation of more compelling KR languages for specifying preferences, and the exploration of further ways of comparing and ranking strategies (perhaps incorporating notions of cost or trace length).

Relation to Conference Version

This paper appears in the Proceedings of the 16th International Conference on Knowledge Representation and Reasoning (KR 2018) without the appendix proofs. The body of this paper is the same as the KR 2018 paper, except that a minor typographic error in the translation of LTL into LTL f (the definition of τ(ϕ 1 U ϕ 2 ) on page 6), which originally appeared in (De Giacomo and Vardi 2013) and was repeated in the KR 2018 paper, has been corrected.

• σ ∞ (X 1 • • • X n ) = σ(X 1 • • • X n ) ∪ {alive}, if there is no k < n such that end ∈ σ(X 1 • • • X k ) • σ ∞ (X 1 • • • X n ) = σ(X 1 • • • X n ), otherwise
We claim that σ ∞ is a winning strategy for S ∞ . Take some

X = X 1 X 2 . . ., let π = π[σ, X] and π ∞ = π[σ ∞ , X]. We first show that π ∞ | = ψ end . First note that if end ∈ π ∞ (i), then end ∈ π(i), which means end π(i + 1) (since π contains at most one end). It follows that alive ∈ π ∞ (i) and alive π ∞ (i + 1). Next suppose that alive ∈ π ∞ (i) but alive π ∞ (i + 1)
. This can only occur if end ∈ π(i), which implies that end ∈ π ∞ (i). We have thus shown that π ∞ | = (end ↔ alive ∧ ¬alive). We also have π ∞ | = (end → ¬end), since end ∈ π ∞ (i) iff end ∈ π(i), and π contains at most one occurrence of end.

We next show that π ∞ | = ((α ∨ ♦end) → ϕ inf ). First consider the case (i) where π has a finite prefix of length n σ,X < ∞ that satisfies ϕ. Then end ∈ π ∞ (n σ,X ), so alive ∈ π ∞ (i) for 1 ≤ i ≤ n σ,X and alive π ∞ (i) for i > n σ,X . It follows that π ∞ | = ϕ inf . Next suppose that (ii) holds, i.e. n σ,X = ∞ and π ̸ | = α. Since α only involves variables from X ∪ Y, and π ∞ coincides with π on X ∪ Y, it follows that π ∞ ̸ | = α. As n σ,X = ∞, we know that end does not occur in π. The same must hold for π ∞ , hence π ∞ ̸ | = ♦end. We thus obtain

π ∞ | = ¬(α ∨ ♦end), hence π ∞ | = ((α ∨ ♦end) → ϕ inf ).
For the other direction, suppose S ∞ is realizable, and let σ ∞ be a winning strategy for S. We define σ as follows: σ(X 1 . . . X n ) = σ ∞ (X 1 . . . X n ) \ {alive}. Our aim is to show that σ is a winning strategy for S. Consider some X = X 1 X 2 . . ., and let π ∞ = π[σ ∞ , X] and π = π[σ, X]. First note that since π ∞ | = (end → ¬end), π ∞ contains at most one occurrence for end, and the same holds for σ. It follows that σ is a valid strategy. Next suppose that end ∈ π

∞ (n). Then π f [σ, X] = π(1) . . . π(n). As π ∞ | = ((α ∨ ♦end) → ϕ inf ) and π ∞ | = ♦end, we have π ∞ | = ϕ inf .
When combined with π ∞ | = (end ↔ alive ∧ ¬alive), we get that alive ∈ π ∞ (i) for i ≤ n and alive π ∞ (i) for i > n. This, together with the definition of ϕ inf , implies that the induced finite trace π(1) . . . π(n) satisfies ϕ. Finally, consider the case where end does not occur in π ∞ . We know that π

∞ | = ((α ∨ ♦end) → ϕ inf ). Note that we cannot have π ∞ | = ϕ inf since it implies, when combined with π ∞ | = (end ↔ alive ∧ ¬alive), that end occurs in π ∞ . It follows that π ∞ | = ¬(α ∨ ♦end), or equivalently, π ∞ | = ¬α ∧ ¬end.
From this, we can derive that π ̸ | = α and π does not contain end. We have thus established that σ is a winning strategy.

Theorem 7

The DBA A α s ,α c ϕ accepts infinite traces π such that either: (i) π( 1 Proof. First, we prove that the language of A α s ,α c ϕ contains the set of traces that satisfy one of the conditions (i) and (ii). Then, we prove that the language of A α s ,α c ϕ is contained in the set of traces that satisfy one of the conditions (i) and (ii). The construction of A α s ,α c ϕ is polynomial in the size of A s , A c , and A g , which can be constructed in double-exponential time in |α s |, |α c |, and |α g |, respectively.

(⊇) (i) If π(1) • • • π(n) | = ϕ and end occurs only in π(n), then the run of A g on π(1) • • • π(n) is accepting, i.e. its last state belongs to F g . It then follows from the definition of A α s ,α c ϕ that the run of A α s ,α c ϕ on π will transition to q ⊤ after reading π(n) and, because end occurs only in π(n), it will then loop at q ⊤ . As q ⊤ is an accepting state of A α s ,α c ϕ , this shows that A α s ,α c , the run of A α s ,α c ϕ on π transitions to a state (q s , q c , q g ) where q s = q bad . Because end does not occur in π, after having read π(n), the run of A α s ,α c ϕ on π will remain among the states whose third component is q bad . By construction, these states are accepting, so A α s ,α c ϕ accepts π. In the second case (π ̸ | = α g ), the run of A c on finite prefix π(1) • • • π(n) is not accepting for any n < ∞. It follows that the run of A α s ,α c ϕ on π will not visit any state (q s , q c , q g ) with q c = q good , and since π does not contain end, it also cannot contain the state q ⊥ . Thus, the run of π will only visit accepting states, so A α s ,α c ϕ accepts π. (⊆) Let π be an infinite trace that is accepted by A α s ,α c ϕ . We distinguish three cases: (a) end does not occur in π; (b) end occurs exactly one time in π; (c) end occurs more than one time in π. Case (a): if end does not occur in π, then q ⊤ does not occur in the run of A α s ,α c ϕ on π. As this run is accepting but does not contain q ⊤ , it must either hit infinitely often states with q bad , or hit infinitely often states without q good . In the first case, let π(1) • • • π(n) be the smallest prefix of π such that after reading π(1) • • • π(n), the DBA A α s ,α c ϕ enters a state (q s , q c , q g ) with q s = q bad . By construction of A α s ,α c ϕ , it must be that the run of A s on π(1)

• • • π(n) is accepting. Thus, π(1) • • • π(n) is a bad prefix of α s , which means π ̸ | = α s .
In the second case, we observe that if a run enters a state (q s , q c , q g ) with q c = q good , then it remains in a state with good in the second component unless a symbol with end is read. As the considered trace π does not contain end, it follows that the run of A α s ,α c ϕ on π does not hit any state (q s , q c , q g ) with q c = q good . Hence, A c must not accept any finite prefix of π, so π does not contain any good prefixes for α c , i.e. π ̸ | = α c . This concludes that case (a) implies case (ii). Case (b): suppose that end occurs exactly one time in π, say in the nth symbol π(n). Immediately after reading π(n), the DBA A α s ,α c ϕ will transition to either q ⊤ or q ⊥ . However, since the run of A α s ,α c ϕ on π is accepting, it cannot contain q ⊥ . We thus have a transition of the form δ((q s , q c , q g ), π(n)) = q ⊤ with δ g (q g , π(n)) ∈ F g . It follows that the finite prefix π(1)

• • • π(n) is accepted by the DFA A g , i.e., π(1) • • • π(n) | = ϕ.
We have thus shown that case (b) implies case (i). To conclude the proof, observe that Case (c) is not possible. Indeed, the first symbol with end forces an automaton transition to either q ⊤ or q ⊥ , and the second symbol with end forces an automaton transition to q ⊥ . Because state q ⊥ is absorbing and not accepting, A α s ,α c ϕ does not accept traces where end occurs more than one time.

Theorem 9 Consider a constrained LTL f specification S =⟨X, Y, α s ∧ α c , ϕ⟩ where α s (resp. α c ) is a safe (resp. co-safe) formula. Then: • S is realizable iff the DBA game G α s ,α c ϕ is winning;

• Every winning strategy for G α s ,α c ϕ is a winning strategy for S, and vice-versa;

• Deciding whether G α s ,α c ϕ is winning, and constructing a winning strategy when one exists, can be done in 2EXP.

Proof. By Theorem 7, the language of the DBA A α s ,α c ϕ contains all, and only, the infinite traces π such that either: ) and check whether ((q 0 ) s , (q 0 ) c , (q 0 ) g ) ∈ Win(G α s ,α c ϕ ). If the latter holds, then we construct a winning strategy in the form of a transducer. This step is also polynomial w.r.t. |A α s ,α c ϕ |, and thus the entire procedure can be performed in double-exponential time.

(i) π(1) • • • π(n) | = ϕ
Theorem 10 A bgv-optimal strategy can be constructed in double-exponential time.

Proof. We first argue that the described construction yields an bgv-optimal strategy. We know from [START_REF] Almagor | Formally reasoning about quality[END_REF]) that the Âϕ,V accepts finite traces π such that ⟦π, ϕ⟧ ≥ b. By reusing the arguments from the proof of Theorem 7, we can show that A α ϕ≥b recognizes infinite traces such that either (i) α = α s ∧ α c is violated and end does not occur, or (ii) end occurs exactly once and the induced finite trace π is such that ⟦π, ϕ⟧ ≥ b. It follows that an α-strategy σ with bgv(σ) ≥ b exists iff the DBA game ⟨X, Y ∪ {end}, A α ϕ≥b ⟩ is winning. We can use the techniques described in Section 5.2 to decide whether such a DBA is winning. By considering the values in V(ϕ) in descending order, we can determine the maximal b * for which an α-strategy σ with bgv(σ) ≥ b * exists. We can then compute such a strategy, for the identified best value b * , by constructing a winning strategy for the DBA game ⟨X, Y ∪ {end}, A α ϕ≥b * ⟩, again using the techniques from Section 5.2.

For each value b, we can construct the DFA Âϕ,V in double-exponential time, and the DFAs for safe and co-safe constraints can also be constructed in double-exponential time. It follows that A α ϕ≥b can also be constructed in doubleexponential time. Determining whether the DBA game ⟨X, Y ∪ {end}, A α ϕ≥b ⟩ is winning, and constructing a winning strategy for the game, is also in double-exponential time. Finally, we note that all of the preceding doubleexponentional time operations are performed at most once per value b ∈ V(ϕ), so the overall procedure runs in doubleexponential time.

The next two lemmas will be used to prove Theorem 11.

In what follows, it will be convenient to slightly abuse notation and use δ(q, π), with π a finite trace, to indicate the automata state resulting from reading π starting from state q (and similarly for the output function ω of transducers on a finite string X

1 . . . X n ). Lemma 1. For every π = (X 1 ∪ Y 1 ) . . . (X n ∪ Y n ) ∈ 2 X∪Y , X n+1 ∈ 2 X ,
and b ∈ [0, 1], the following are equivalent:

1. there exists an α-strategy σ such that π ∈ ptraces(σ) and bgv

π,X n+1 (σ) ≥ b 2. δ b (q b 0 , π•(X n+1 ∪Y n+1 )) ∈ Win(G b ) for some Y n+1 ∈ 2 Y∪{end} . Proof. (⇒) Suppose that σ is an α-strategy such that π ∈ ptraces(σ) and bgv π,X n+1 (σ) ≥ b. Set Y n+1 = σ(X 1 . . . X n X n+1 ), and let q * = δ b (q b 0 , π (X n+1 ∪ Y n+1 )). Con- sider the DBA A α ≥b,q * = ⟨2 X∪Y∪{end} , Q b , δ b , q * , F b ⟩
, which is the same as A α ≥b but with q * for the initial state. Define a strategy σ * for the DBA game G * b = ⟨X, Y ∪ {end}, A α ≥b,q * ⟩ as follows:

σ * (X ′ 1 . . . X ′ h ) = σ(X 1 . . . X n+1 X ′ 1 . . . X ′ h )
We claim that σ * is a winning strategy for G * b . To see why, take any X ∈ (2 X ) * , and let π * X = π[σ * , X]. We need to show that π * X is accepted by A α ≥b,q * . Let us consider π X = π[σ, X 1 . . . X n+1 X], and let s 0 s 1 s 2 . . . be the infinite run of A α ≥b on π X . Note that since π ∈ ptraces(σ), we know that π ⊑ π X , hence either (i) π X does not contain end and π X ̸ | = α, or (ii) π X contains exactly one occurrence of end (at some position k ≤ n + 1, since π does not contain end) and the induced finite trace π

f X = π f [σ, X 1 . . . X n+1 X] is such that ⟦π f X , ϕ⟧ ≥ b.
It follows that π X is accepted by A α ≥b , and thus the infinite run s 0 s 1 s 2 . . . of A α ≥b on π X contains infinitely many s j ∈ F b . We then observe that s n+1 = q * . Since A α ≥b,q * has the same transitions as A α ≥b , it follows that s n+1 s n+2 s n+3 . . . is the run of A α ≥b,q * on π * X . Note that s n+1 s n+2 s n+3 . . . must also contain infinitely many s j ∈ F b , so it is an accepting run. We have thus shown that σ * is a winning strategy for G * b . As the game G * b is winning, we must have q * ∈ Win(G * b ). We then remark that since G * b and G b only differ in their initial states, the two games have precisely the same winning regions. We thus obtain q

* = δ b (q b 0 , π (X n+1 ∪ Y n+1 )) ∈ Win(G b ). (⇐) Suppose that q * = δ b (q b 0 , π • (X n+1 ∪ Y n+1 )) ∈ Win(G b )
. By following the strategy of the transducer T G b from this point on, we are guaranteed to produce a trace that is accepted by the automaton A α ≥b . More precisely, consider the strategy σ defined as follows:

• σ(X ′ 1 . . . X ′ k ) = Y k , if X ′ 1 . . . X ′ k = X 1 . . . X k (1 ≤ k ≤ n + 1) • σ(X ′ 1 . . . X ′ n+1 . . . X ′ h ) = ω b (δ ′ b (q * , X ′ n+1 . . . X ′ h-1 ), X ′ h ), if X ′ 1 . . . X ′ n+1 = X 1 . . . X n+1 • σ(X ′ 1 ) = end, if X ′ 1 X 1 • σ(X ′ 1 . . . X ′ k X ′ k+1 ) = end, if X ′ i = X i for 1 ≤ k < n + 1 and X ′ k+1 X k+1 • σ(X ′ 1 . . . X ′ h ) = ∅
, in all other cases where δ ′ b and ω b are respectively the transition and output functions of the transducer T G b . The first bullet concerns prefixes of X 1 . . . X n+1 and ensures that (X 1 ∪ Y 1 ) . . . (X n+1 ∪ Y n+1 ) ∈ ptraces(σ)). The second bullet states that once X 1 . . . X n+1 has been read, we start following the transducer T G b . The remaining points ensure that all infinite traces π ′ ∈ traces(σ) such that π (X n+1 ∪Y n+1 ) π ′ contain a single occurrence of end.

We claim that σ is an α-strategy such that (X 1 ∪ Y 1 ) . . . (X n+1 ∪ Y n+1 ) ∈ ptraces(σ) and bgv π,X n+1 (σ) ≥ b. As noted above, the first bullet of the definition ensures that (X 1 ∪ Y 1 ) . . . (X n+1 ∪ Y n+1 ) ∈ ptraces(σ). The last three bullets make sure that every π ′ ∈ traces(σ) with (X 1 ∪ Y 1 ) . . . (X n+1 ∪ Y n+1 )

π ′ contains exactly one occurrence of end. It remains to consider the infinite traces that begin with (X 1 ∪ Y 1 ) . . . (X n+1 ∪ Y n+1 ). Consider some such trace π ′ = (X 1 ∪ Y 1 )(X 2 ∪ Y 2 ) . . . ∈ traces(σ), and let s 0 s 1 s 2 . . . be the infinite run of A α ≥b on π ′ . Because (X 1 ∪ Y 1 ) . . . (X n+1 ∪ Y n+1 ) ⊑ π ′ , we know that s n+1 = q * . The latter can be combined with the second bullet to show that for every i ≥ n+1, Y i+1 = ω b (s i , X i+1 ) and s i+1 = δ ′ b (s i , X i+1 ). As s n+1 = q * ∈ Win(G b ), and ω b is defined so as to always remain within Win(G b ), we have s i ∈ Win(G b ) for every i ≥ n + 1. Furthermore, since ω b always reduces the distance to RA(G), there are infinitely many i ≥ n + 1 such that s i ∈ F b . This establishes that s 0 s 1 s 2 . . . is an accepting run, and thus, π ′ must either be such that π ′ ̸ | = α, or it contains a single occurrence of end such that the finite induced trace π ′′ is such that ⟦π ′′ , ϕ⟧ ≥ b. We have thus shown that every infinite trace produced by σ either violates α or contains end, i.e. σ is an α-strategy. Moreover, for every π ′′ ∈ traces f (σ) with (X 1 ∪ Y 1 ) . . . (X n+1 ∪ Y n+1 ) ⊑ π ′′ , we have ⟦π ′′ , ϕ⟧ ≥ b, as desired.

In the following lemma, we use σ str to denote the strategy implemented by the transducer T str . To simplify the formulation, we extend the notation bgv π,X (σ) to all finite traces that can be produced by strategy σ (recall that Definition 2 only defines this notation for compatible traces that do not contain end). Formally, given a trace π = (X 1 ∪ Y 1 ) . . . (X n ∪ Y n ) that is a prefix of some infinite trace in π[σ, X] and contains end at position k ≤ n, we set bgv π,X (σ) = ⟦π ′ , ϕ⟧, where π ′ = (X 1 ∪ Y 1 ) . . . (X k ∪ Y k \ {end}).

Lemma 2. For every X 1 . . . X n ∈ (2 X ) * , X n+1 ⊆ X, and v ∈ [0, 1]: if π = (X 1 ∪ω str (q str 0 , X 1 )) . . . (X n ∪ω str (q str 0 , X 1 . . . X n )), (q 1 , q 2 , . . . , q m ) = δ str (q str 0 , X 1 . . . X n ), and u is such that ω str ((q 1 , q 2 , . . . , q m ), X n+1 ) was set equal to ω u (q u , X n+1 ), then bgv π,X n+1 (σ str ) ≥ u.

Proof. Fix X 1 . . . X n ∈ (2 X ) * and X n+1 ⊆ X. Consider some X ∈ (2 X ) ω such that X = X 1 . . . X n X n+1 X n+2 . . .. Let π ′ = π[σ str , X] = (X 1 ∪ Y 1 )(X 2 ∪ Y 2 ) . . ., and for all i ≥ 0 let (q 1 i+1 , . . . , q m i+1 ) = δ str (q str 0 , X 1 . . . X i+1 ). Define a function ζ : N → {b 1 , . . . , b m } by letting ζ(i) be the unique value b in {b 1 , . . . , b m } such that ω str ((q 1 i , . . . , q m i ), X 1 . . . X i ), X i+1 ) was set equal to ω b (q b i , X i+1 ). Basically, ζ(i) = b means that we used transducer T G b to generate Y i+1 after reading X i+1 from state (q 1 i , . . . , q m i ). Note that the value u from the lemma statement is equal to ζ(n). Observe that q b X 0 q b X 1 q b X 3 . . . is the run of A α ≥b X on π ′ and that q b X h+1 ∈ Win(G b X ). From the definition of ω b X , we can infer that q b X i ∈ Win(G b X ) for all i > h, and further that there are infinitely many q b X i ∈ F b X . This means that q b X 0 q b X 1 q b X 3 . . . is an accepting run of A α ≥b X on π ′ . Thus, either π ′ does not contain end and violates α, or π ′ contains end and the induced finite trace π f [σ str , X] has value at least b X = ζ(h) ≥ ζ(n) = u. We have shown that every trace π ′′ ∈ traces f (σ str ) is such that ⟦π ′′ , ϕ⟧ ≥ ζ(n) = u, and hence that bgv π,X n+1 (σ str ) ≥ u.

We now proceed to the proof of Theorem 11.

Theorem 11 T str implements a strongly bgv-optimal strategy and can be constructed in double-exponential time.

Proof. We first show that T str implements a strongly bgvoptimal strategy. Suppose for a contradiction that this is not the case. Then there exists a finite trace π = (X 1 ∪ Y 1 ) . . . (X n ∪ Y n ) ∈ ptraces(σ) that does not contain end, X ∈ X, and an α-strategy such that π ∈ ptraces(σ ′ ) and bgv π,X (σ ′ ) > bgv π,X (σ). Suppose that bgv π,X (σ) = b and bgv π,X (σ ′ ) = b ′ . From Lemma 1, we know that δ b ′ (q b ′ 0 , π (X n+1 ∪ Y n+1 )) ∈ Win(G b ′ ) for some Y n+1 ∈ 2 Y∪{end} . It follows that ω str (δ str (q str 0 , X 1 . . . X n ), X n+1 ) = ω v (q v , X n+1 ) for some v ≥ b ′ . From Lemma 2, bgv π,X n+1 (σ str ) ≥ v ≥ b ′ , a contradiction.

We know from Section 7.2 and Theorem 10 that for each v ∈ V(ϕ), the DBA A α ≥v , winning region Win(G v ), and transducer T G v can be constructed in double-exponential time. As there are only single exponentially many values in V (hence B), the transducer T str can also be constructed double-exponential time.

  ) • • • π(n) | = ϕ and end occurs only in π(n), or (ii) π ̸ | = α s ∧ α c and end does not occur in π. A α s ,α c ϕ can be constructed in double-exponential time in |α s | + |α c | + |ϕ|.

  2, we first determine the maximal b * ∈ V(ϕ) for which a α-strategy σ with bgv(σ) ≥ b * exists, and set B = V(ϕ) ∩ [b * , 1]. In the process, we will compute, for each b ∈ B, the sets Win(G b ) and RA(G b ) for the DBA game G b = ⟨X, Y, A α ≥b ⟩ based on the DBA A α ≥b = ⟨2 P∪{end} , Q b , δ b , q b 0 , F b ⟩. In the sequel, we will assume that the elements of B are ordered as follows: b 1 < b 2 . . . < b m , with b * = b 1 and b m = 1.

  ) • • • π(n) | = ϕ and end occurs only in π(n), or (ii) π ̸ | = α s ∧ α c and end does not occur in π. A α s ,α c ϕ can be constructed in double-exponential time in |α s | + |α c | + |ϕ|.

ϕ

  accepts π. (ii) If π ̸ | = α s ∧ α c and end does not occur in π, then either π ̸ | = α s or π ̸ | = α c . In the first case (π ̸ | = α s ), the trace π contains a bad prefix π(1) • • • π(n), and w.l.o.g. we can suppose that this is the shortest such prefix. It follows that the run of A s on π(1) • • • π(n) is accepting. From the definition of A α s ,α c ϕ

  and end occurs only in π(n), or (ii) π ̸ | = α s ∧ α c and end does not occur in π. By definition, a strategy σ is a winning strategy for G α s ,α c ϕ iff every induced infinite trace π[σ, X] is accepted by A α s ,α c ϕ . It follows that winning strategies for G α s ,α c ϕ are winning strategies for S, and vice versa. By Theorem 7, we can construct the DBA A α s ,α c ϕ in double-exponential time. We can then construct, in polynomial time in |A α s ,α c ϕ | the set Win(G α s ,α c ϕ

  Claim: For all i ≥ 0, ζ(i + 1) ≥ ζ(i). Proof of claim: Suppose that ζ(i) = b, which means that b = max({v ∈ B | ∃Y δ v (q v i , X i+1 ∪ Y) ∈ Win(G v )}). Then we have Y i+1 = ω b (q b i , X i+1 ).From the definition of ω b , and the fact that there exists someY with δ b (q b i , X i+1 ∪ Y) ∈ Win(G b ), we know that δ b (q b i , X i+1 ∪ Y i+1 ) ∈ Win(G b ). It follows that there must exist Y ′ such that δ b (q b i+1 , X i+2 ∪ Y ′ ) ∈ Win(G b ), and hence max({v ∈ B | ∃Y ′ δ v (q v i+1 , X i+2 ∪ Y ′ ) ∈ Win(G v )}) ≥ b. Thus, ζ(i + 1) ≥ b = ζ(i). (end proof of claim)Due to the preceding claim, and the finiteness of B, there exists h ≥ 0 such that ζ(i) = ζ(h) for all i ≥ h, andζ(i) < ζ(h) for i < h. Let b X = ζ(h).

Our high-level presentation combines elements of the reductions in(De Giacomo and

Vardi 2015; Camacho et al. 2018a). Its purpose is to illustrate the general form and components of an LTL f encoding of planning (not to provide the most efficient encoding).

The algorithm can be easily modified to output end once ϕ has been satisfied to match our definition of strategy.

If we want to have only a safe (resp. co-safe) constraint, it suffices to use a trivial constraint α c = ⊤ (resp. α s = ⊥ R (p ∨ ¬p)).

Several Y may satisfy the conditions, and choosing any such Y yields a suitable transducer. Alternatively, one can use nondeterministic transducers (called strategy generators in (De Giacomo and Vardi 2015)) to encode a family of deterministic transducers.

We omit ∨ and R , as they can be defined using ¬, ∧, and U .

Acknowledgements

This work was partially funded by the Natural Sciences and Engineering Research Council of Canada (NSERC) and the ANR project GoAsQ (ANR-15-CE23-0022).

Proofs

Theorem 4. When α is a safe formula, the constrained LTL f specification S = ⟨X, Y, α, ϕ⟩ is realizable iff the LTL f specification S ′ = ⟨X, Y, α ′ → ϕ⟩ is realizable, where α ′ is obtained from α by replacing every occurrence of ψ by ψ.

Proof. Let σ ′ be a winning strategy for S ′ = ⟨X, Y, α ′ → ϕ⟩, with α a safe formula. We define a strategy σ for S = ⟨X, Y, α, ϕ⟩ by setting σ(X

To show that σ is a winning strategy, take some X ∈ (2 X ) ω . Then n σ ′ ,X < ∞, and the finite trace

(since we will remove end), and π = π[σ, X] contains π ′ as a prefix. We can then use the LTL f equivalence ¬ ϕ ≡ ¬ϕ and the fact that α is safe to derive π | = ¬α. If (ii) holds (and (i) does not), then it follows from the definition of σ that

For the other direction, let σ be a winning strategy for S. Define a strategy σ ′ for S ′ by setting σ

is a bad prefix for α, and

Basically, σ ′ mimics σ and outputs end as soon as a bad prefix is reached or σ terminates the execution due to satisfaction of ϕ, whichever situation occurs first. The construction of σ ′ is such that executions always terminate -which is not necessarily true for σ -and induce finite traces that satisfy the LTL f formula α ′ → ϕ.

To show that σ ′ is a winning strategy for S ′ , take some X ∈ (2 X ) ω . Consider the infinite induced trace π = π[σ, X], and let k X be the minimum k such that π(1) . . . π(k) is a bad prefix for α (k X = ∞ if π has no bad prefix). We examine these three cases separately: (i) n σ,X < ∞ and k X ≤ n σ,X , (ii) n σ,X < ∞ and k X > n σ,X , and (iii) n σ,X = ∞.

If (i) holds, then n σ ′ ,X = k X , and π ′ = π f [σ ′ , X] = π(1) . . . π(k X ). From the fact that π(1) . . . π(k X ) is a bad prefix for the safe formula α and the LTL f equivalence ¬ ϕ ≡ ¬ϕ, we obtain

If (iii) holds, then it must be the case that π ̸ | = α (because ϕ is a winning strategy). As α is a safe formula, π must contain a bad prefix for α, so k X < ∞. Using a similar argument as in case (i), we can show that π ′ | = ¬α ′ .

Theorem 5 The constrained LTL f specification S = ⟨X, Y, α, ϕ⟩ is realizable iff LTL specification S ∞ = ⟨X, Y ∪ {alive, end} , ψ α,ϕ ⟩ is realizable. Moreover, for every winning strategy σ for S ∞ , the strategy σ ′ defined by σ

Proof. For the first direction, suppose that S = ⟨X, Y, α, ϕ⟩ is realizable, and let σ be a winning strategy for S. By definition, for every X ∈ (2 X ) ω , the trace π[σ, X] satisfies one of the following: (i) it has a finite prefix of length n σ,X < ∞ that satisfies ϕ, or (ii) n σ,X = ∞ and π[σ, X] ̸ | = α. We define a strategy σ ∞ for S ∞ = ⟨X, Y ∪ {alive, end} , ψ α,ϕ ⟩ as follows: