LTL Synthesis Under Environment Specifications (Short Paper)

Abstract

In this communication we present recent advances in the field of synthesis for agent goals specified in Linear Temporal Logic on finite traces under environment specifications. In synthesis, environment specifications are constraints on the environments that rule out certain environment behavior. To solve synthesis of LTL goals under environment specifications, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTL and in LTL have the same worst-case complexity (both are 2EXPTIME-complete), the algorithms available for LTL synthesis are much harder in practice than those for LTL synthesis. We report recent results showing that when the environment specifications are in form of fairness, stability, or GR(1) formulas, we can avoid such a detour to LTL and keep the simplicity of LTL synthesis. Furthermore, even when the environment specifications are specified in full LTL we can partially avoid this detour.

Keywords

• eol>Linear Temporal Logic on Finite Traces
• Synthesis
• Automata-Theoretic Approach

1. Introduction

Program synthesis is one of the most ambitious and challenging problem of CS and AI. Reactive synthesis is a class of program synthesis problems which aims at synthesizing a program for interactive/reactive ongoing computations [ 1, 2 ]. We have two sets of Boolean variables and , controlled by the environment and the agent, respectively, and a specification over ∪ in terms of Linear Temporal Logic (ltl) [ 3 ]. The synthesis has to generate a program, aka a strategy, for the agent such that for every environment strategy the simultaneous execution of the two strategies generate a trace that satisfies [ 2, 4, 5 ].

Recently, the problem of reactive synthesis has been studied in the case the specification is expressed in ltl over finite traces ( ltl ) and its variants [ 6 ]. This logic is particularly fitting for expressing temporally-extended goals in Planning since it retains the fact that ultimately the goal must be achieved and the plan terminated [ 7 ].

In the classical formulation of the problem of reactive synthesis the environment is free to choose an arbitrary move at each step, but in AI typically we have a model of world, i.e., of the environment behavior, e.g., encoded in a planning domain [ 8, 9, 10 ], or more generally directly in temporal logic [ 11, 12, 13, 14 ]. In other words, we are interested in synthesis under environment specifications [ 15, 16, 17, 18, 19, 20, 21 ], which can be reduced to standard synthesis of the implication: → where is the specification of the environment (the environment specification) and is the specification of the task of the agent [ 13, 16 ]. The agent has to realize its task only on those traces that satisfy the environment specification . Specifically, we focus on synthesis under environment specifications for ltl goals. However, while it is natural to consider the task specification as an ltl formula, requiring that also is an ltl formula is often too strong, since accomplishing the agent task may require an unbounded number of environment moves and such number is decided by the agent that determines when its task is finished. As a result typically needs to be expressed over ltl not ltl [ 17, 21 ]. So, even when focusing on ltl , what we need to study is the case where we have the task expressed in ltl and the environment specification expressed in ltl.

One way to handle this case is to translate into ltl [22] and then do ltl synthesis for → , see e.g. [ 17 ]. But, while synthesis in ltl and in ltl have the same worst-case complexity, being both 2exptime-complete [ 2, 6 ], the algorithms available for ltl synthesis are much harder in practice than those for ltl synthesis as experimentally shown [23, 24, 25].

For these reasons, several specific forms of ltl environment specifications have been considered. In this communication we reports recent results showing how to avoid the detour to LTL synthesis in cases where the environment specifications are in the form of fairness or stability [21], or gr(1) formulas [20], or specified in both ltl (e.g., for representing nodeterministic planning domains or other safety properties) and ltl (e.g., for liveness/fairness), but separating the contributions of the two by limiting the second one as much as possible [ 18 ]. 2. ltl and ltl ltl is one of the most popular logics for temporal properties [ 3 ]. Given a set of propositions , the formulas of ltl are generated by the following grammar:

::= | ( 1 ∧ 2) | (¬ ) | (○ ) | ( 1 2) where ∈ . We use common abbreviations for eventually ♢ ≡ true and always as □ ≡ ¬ ♢ ¬ .

ltl formulas are interpreted over infinite traces ∈ (2 ). A trace = 0 1 . . . is a sequence of propositional interpretations (sets), where for every ≥ 0, ∈ 2 is the -th interpretation of . Intuitively, is interpreted as the set of propositions that are at instant . Given , we define when an ltl formula holds at position , written as , |= , inductively on the structure of , as follows: • , |= if ∈ (for ∈ ); • , |= 1 ∧ 2 if , |= 1 and , |= 2; • , |= ¬ if , ̸|= ; • , |= ○ if , + 1 |= ; • , |= 1 2 if there exists ≤ such that , |= 2, and for all , ≤ < we have that , |= 1.

We say satisfies , written as |= , if , 0 |= .

ltl is a variant of ltl interpreted over finite traces instead of infinite traces [ 22]. The syntax of ltl is the same as the syntax of ltl. We define , |= , stating that holds at position , as for ltl, except that for the temporal operators we have: • , |= ○ if < last ( ) and , + 1 |= ; • , |= 1 2 if there exists such that ≤ ≤ last ( ) and , |= 2, and for all , ≤ < we have that , |= 1. where last ( ) denotes the last position (i.e., index) in the finite trace . In addition, we define the weak next operator ∙ as abbreviation of ∙ ≡ ¬ ○ ¬ . Note that, over finite traces, it does not holds that ¬○ ̸≡ ○ ¬ , but instead ¬○ ≡ ∙ ¬ . We say that a trace satisfies an ltl formula , written as |= , if , 0 |= . 3. ltl Synthesis Under Environment Specifications Let and Boolean variables, controlled by the environment and the agent, respectively. An agent strategy is a function : (2 )* → 2 , and an environment strategy is a function : (2 )+ → 2 . A trace is a sequence (0 ∪ 0)(1 ∪ 1) · · · ∈ (2 ∪ ). A trace ( ∪ ) is consistent with an agent strategy if ( ) = 0 and (01 · · · ) = +1 for every ≥ 0. A trace ( ∪ ) is consistent with and environment strategy if (01 · · · ) = for every ≥ 0. For an agent strategy and an environment strategy let play( , ) denote the unique trace induced by both and , and play( , ) = (0 ∪ 0), . . . , ( ∪ ) be the finite trace up to .

Let be an ltl formula over ∪ . An agent strategy realizes if for every environment strategy there exists ≥ 0, chosen by the agent, such that the finite trace play( , ) |= , i.e., is agent realizable.

In standard synthesis the environment is free to choose an arbitrary move at each step, but in AI typically the agent has some knowledge of how the environment works, which it can exploit in order to enforce the goal, specified as an ltl formula . Here, we specify the environment behaviour by an ltl formula Env and call it environment specification . In particular, Env specifies the set of environment strategies that enforce Env [ 16 ]. Moreover, we require that Env must be environment realizable, i.e., the set of environment strategies that enforce Env is not empty. Formally, given an ltl formula , we say that an environment strategy enforces , written ▷ , if for every agent strategy we have play( , ) |= .

The problem of ltl synthesis under environment specifications is to find an agent strategy such that

∀ ▷ Env : ∃.play( , ) |= .

As shown in [ 16 ], this can be reduced to solving the synthesis problem for the implication Env → () where () being a suitable ltl -to-ltl transformation [22], which is 2exptime-complete [ 2 ].

3.1. GR(1) Environment Specifications

There have been two success stories with ltl synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with ltl as the specification language. In [ 20] we take these two lines of work and bring them together, devising an approach to solve ltl synthesis under gr(1) environment specification. In more details, to solve the problem we observe that the agent’s goal is to satisfy ¬Env (1) ∨ , while the environment’s goal is to satisfy Env (1) ∧ ¬. Moreover, can be represented by a deterministic finite automata ( dfa) [ 6 ]. Then, focusing on the environment point of view, we show that the problem can be reduced into a gr(1) game in which the game arena is the complement of the dfa for and Env (1) is the gr(1) winning condition. Since we want a winning strategy for the agent, we need to deal with the complement of the gr(1) game to obtain a winning strategy for the antagonist.

This framework can be enriched by adding safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of ltl synthesis. These two kinds of safety conditions difer, since the environment needs to maintain its safety indefinitely (as usual for safety), while the agent has to maintain its safety conditions only until s/he fulfills its ltl goal, i.e., within a finite horizon. Again, the problem can be reduced to a gr(1) game in which the game arena is the product of the dfa for the environment safety condition and the complement of the dfa obtained by the product of deterministic automaton of the agent safety condition and the one for the agent task.

Tool. The two approaches were implemented in a so-called tool GFSynth which is based on two tools: Syft [25] for the the construction of the corresponding dfas and Slugs [26] to solve and compute a strategy in a gr(1) game.

3.2. Fairness and Stability Environment Specifications

We now consider two diferent basic forms of environment specifications: a basic form of fairness □♢ (always eventually ), and a basic form of stability ♢□ where in both cases the truth value of is under the control of the environment, and hence the environment specifications are trivially realizable by the environment. Note that due to the existence of ltl goals, synthesis under both kinds of environment specifications does not fall under known easy forms of synthesis, such as gr(1) formulas [27]. For these kinds of environment specifications, [ 18 ] develops a specific algorithm based on using the dfa for the ltl goal as the arena and then computing 2-nested fixpoint properties over such arena.

The algorithm proceeds as follows. First, translate the ltl into a dfa . Then, in case of fairness environment specifications, solve the fair dfa game , i.e., a game over the dfa , in which the environment (resp. the agent) winning condition is to remain in a region (resp., to avoid the region) where holds infinitely often, meanwhile the accepting states are forever avoidable, by applying a nested fixed-point computation on .

Likewise, for stability environment specifications, solve the stable dfa game , in which the environment (resp. the agent) winning condition is to reach a region (resp., to avoid the region) where holds forever, meanwhile the accepting states are forever avoidable, by applying a nested fixed-point computation on .

Tool. The fixpoint-based techniques for solving ltl synthesis under fainerss and stability environment specifications are implemented in two tools called FSyft and StSyft, both based on Syft, a tool for solving symbolic ltl synthesis.

3.3. General ltl Environment Specifications

We now consider the general case where the environment specifications are expressed in both ltl and ltl. For this case, in [ 18 ] we develop two-stage technique to efectively handle general ltl environment specifications. This technique takes advantage of the simpler way to handle ltl goals in the first stage and confines the dificulty of handling ltl environment specification to the bare minimum in stage 2. In particular, given an ltl environment specification and an ltl formula that specifies the agent goal, the problem is to find a strategy for the agent that realizes under ltl environment specification Env . The algorithm proceeds by taking the following stages.

• Stage 1: Build the corresponding deterministic finite automaton of and solve the reachability game for the agent over . If the agent has a winning strategy in , then return it. • Stage 2: If not, computes the following steps: 1. remove from the agent winning region, obtaining ′; 2. do the product of ′ with the corresponding deterministic parity automaton (dpa) of , obtaining ℬ = ′ × , and solve the parity game for the environment over it [28, 29, 30]; 3. if the agent has a winning strategy in ℬ then the synthesis problem is realizable and hence return the agent winning strategy as a combination of the agent winning strategies in the two stages.

An interesting observation in [ 18 ] is that when the part of the environment specifications are expressed in ltl , i.e., the environment specifications have the form = ∞ ∧ , where ∞ can be expressed as ltl formula and as an ltl formula. In this case the synthesis problem → becomes (∞ ∧ ) → which is equivalent to ∞ → ( → ) where ( → ) is expressible in ltl . In this way does not contribute the resulting dpa and can be handled during stage 1 instead of 2 of our technique. Specifically, it builds a dfa as the union of the dfa , i.e., the complement of the dfa for , and the dfa Goal for the goal.

Tool. The two-stage technique was implemented in the tool 2SLS which is based on two tools: Syft [25] for building the corresponding dfas and OWL [31] a tool for translating LTL into diferent types of automata, and thus dpas.

Acknowledgments

We thank our co-authors on the publications mentioned in this communication: Giuseppe De Giacomo, Lucas Tabajara, Moshe Y. Vardi and Shufang Zhu. This work is partially supported by the ERC Advanced Grant WhiteMech (No. 834228), by the EU ICT-48 2020 project TAILOR (No. 952215), by the PRIN project RIPER (No. 20203FFYLK), and by the JPMorgan AI Faculty Research Award "Resilience-based Generalized Planning and Strategic Reasoning”. [19] G. De Giacomo, A. Di Stasio, G. Perelli, S. Zhu, Synthesis with mandatory stop actions, in:

KR 2021, 2021, pp. 237–246. [20] G. D. Giacomo, A. D. Stasio, L. M. Tabajara, M. Y. Vardi, S. Zhu, Finite-trace and generalizedreactivity specifications in temporal synthesis, in: IJCAI 2021, 2021, pp. 1852–1858. [21] S. Zhu, G. De Giacomo, G. Pu, M. Vardi, LTL synthesis with fairness and stability assumptions, in: AAAI, 2020. [22] G. De Giacomo, M. Y. Vardi, Linear temporal logic and linear dynamic logic on finite traces, in: IJCAI, 2013, pp. 854–860. [23] S. Bansal, Y. Li, L. M. Tabajara, M. Y. Vardi, Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications, in: AAAI, 2020. [24] A. Camacho, J. A. Baier, C. J. Muise, S. A. McIlraith, Finite LTL synthesis as planning, in:

ICAPS, 2018, pp. 29–38. [25] S. Zhu, L. M. Tabajara, J. Li, G. Pu, M. Y. Vardi, Symbolic LTL synthesis, in: IJCAI, 2017, pp. 1362–1369. [26] R. Ehlers, V. Raman, Slugs: Extensible GR(1) synthesis, in: CAV, 2016, pp. 333–339. [27] R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, Y. Sa’ar, Synthesis of reactive(1) designs,

J. Comput. Syst. Sci. 78 (2012) 911–938. [28] A. Di Stasio, A. Murano, G. Perelli, M. Vardi, Solving parity games using an automata-based algorithm, in: CIAA 2016, 2016, pp. 64–76. [29] M. Jurdzinski, Small progress measures for solving parity games, in: STACS 2000, 2000, pp. 290–301. [30] A. D. Stasio, A. Murano, M. Y. Vardi, Solving parity games: Explicit vs symbolic, in: CIAA 2018, 2018, pp. 159–172. [31] J. Kretínský, T. Meggendorfer, S. Sickert, Owl: A library for -words, automata, and LTL, in: ATVA, 2018, pp. 543–550.

References

[1] A. Church , Logic, arithmetics, and automata, in: Proc. Int. Congress of Mathematicians , 1963 .

[2] A. Pnueli , R. Rosner , On the synthesis of a reactive module , in: POPL , 1989 .

[3] A. Pnueli , The temporal logic of programs , in: FOCS, 1977 , pp. 46 - 57 .

[4] R. Ehlers , S. Lafortune , S. Tripakis , M. Y. Vardi , Supervisory control and reactive synthesis: a comparative introduction , Discrete Event Dynamic Systems 27 ( 2017 ) 209 - 260 .

[5] B. Finkbeiner , Synthesis of Reactive Systems., Dependable Software Systems Eng . 45 ( 2016 ) 72 - 98 .

[6] G. De Giacomo , M. Y. Vardi , Synthesis for LTL and LDL on finite traces , in: IJCAI , 2015 .

[7] J. A. Baier , S. A. McIlraith , Planning with first-order temporally extended goals using heuristic search , in: AAAI, 2006 , pp. 788 - 795 .

[8] G. De Giacomo , S. Rubin , Automata-theoretic foundations of FOND planning for LTL and LDL goals , in: IJCAI, 2018 , pp. 4729 - 4735 .

[9] H. Gefner , B. Bonet , A Coincise Introduction to Models and Methods for Automated Planning , Morgan&Claypool, 2013 .

[10] C. Green , Theorem proving by resolution as basis for question-answering systems , in: Machine Intelligence , volume 4 , American Elsevier , 1969 , pp. 183 - 205 .

[11] R. Bloem , R. Ehlers , S. Jacobs , R. Könighofer , How to handle assumptions in synthesis , in: SYNT, 2014 .

[12] B. Bonet , G. De Giacomo, H. Gefner , S. Rubin , Generalized planning: Non-deterministic abstractions and trajectory constraints , in: IJCAI , 2017 , pp. 873 - 879 .

[13] K. Chatterjee , T. A. Henzinger , B. Jobstmann , Environment assumptions for synthesis , in: CONCUR , 2008 , pp. 147 - 161 .

[14] N. D'Ippolito , N. Rodríguez , S. Sardiña , Fully observable non-deterministic planning as assumption-based reactive synthesis , J. Artif. Intell. Res . 61 ( 2018 ) 593 - 621 .

[15] B. Aminof , G. De Giacomo, A. Murano , S. Rubin , Synthesis under assumptions , in: KR , 2018 , pp. 615 - 616 .

[16] B. Aminof , G. De Giacomo, A. Murano , S. Rubin , Planning under LTL environment specifications , in: ICAPS , 2019 , pp. 31 - 39 .

[17] A. Camacho , M. Bienvenu , S. A. McIlraith , Finite LTL synthesis with environment assumptions and quality measures , in: KR , 2018 , pp. 454 - 463 .

[18] G. De Giacomo , A. Di Stasio , M. Y. Vardi , S. Zhu , Two-stage technique for LTL synthesis under LTL assumptions , in: KR 2020 , 2020 , pp. 304 - 314 .