Model Checking of Optimal LTL and ASAP Properties

Abstract

Model checking has long been employed as a method for the formal verification of control systems, with a focus on ensuring correctness and safety. However, in practical scenarios (e.g., robotics, aviation and aerospace), simply verifying whether a control system satisfies a given property may not sufice. There is often the requisite to optimize system behavior with respect to certain criteria, such as response time. For instance, in verifying a reachability property, one may be interested in knowing if the controller reaches the goal as soon as possible (ASAP). Despite the simplicity of such requirement, its formalization has not yet been addressed in the literature and requires to reason about the strategy of the controller and the cost of the executions in closed-loop with the given environment. More in general, this paper proposes the formalization and verification of properties for controllers that must satisfy a temporal logic specification optimally, i.e., in the best way possible given the behavior on the plant to be controlled. This relies on and is parametrized by a quantitative semantics for temporal logic. We focus on linear-time temporal logic (LTL), for which various quantitative semantics have been defined. In order to characterize the fulfillment of LTL properties as soon as possible (ASAP), we introduce a new quantitative semantics related to the length of the shortest informative prefix. Finally, we focus on ASAP co-safety properties and reduce the optimal model checking to standard qualitative reactive synthesis. We provide a proof of concept demonstration of the reduction with nuXmv.

1. Introduction

Model checking has long been employed as a method for the formal verification of control systems, with a focus on ensuring correctness and safety. However, in practical scenarios (e.g., robotics, aviation and aerospace), simply verifying whether a control system satisfies a given property may not sufice. There is often a desire to optimize system behavior with respect to certain criteria, such as response time. For instance, in verifying a reachability property, one may be interested in knowing if the controller reaches the goal as soon as possible (ASAP). Despite the simplicity of such requirement, its formalization has not yet been addressed in the literature and requires to reason about the strategy of the controller and the cost of the executions in closed-loop with the given environment. More in general, this paper formalizes the problem of verifying that a control system not only satisfies a specified LTL property, but also it does it in the best way possible given the assumption on the environment. The problem is parametric with respect to a quantitative semantics that defines the value the controller should optimize. As second contribution, we propose a novel quantitative semantics for LTL tailored to capture the ASAP requirement for temporal reachability properties and, as third contribution, we focus on a co-safety fragment of LTL, namely negation of formulas expressed in LTLEBR [ 1 ], and reduce the optimal model checking problem with the ASAP semantics to a qualitative realizability problem. Finally, to demonstrate the eficacy of our approach, we have implemented our methodology and applied it to various examples using nuXmv [ 2 ], a state-of-the-art model checker. We tested the optimal model checking procedure on various co-safety properties and on some scalable benchmarks.

The rest of the paper is organized as follows: Section 2 describes a motivating example; Section 3

recalls the background definitions and results; Section 4 defines the optimal model checking problem;

Section 5 introduces the new ASAP semantics; Section 6 reduces the ASAP optimal model checking problem to reactive synthesis; in Section 7, we compare with related work; in Section 8, we report on the experimental results, and finally in Section 9, we draw some conclusions.

2. Example

We introduce the optimal model checking problem with a simple illustrative example of an agent that

must reach a goal position avoiding an opponent, for example a fox that must reach a chicken and it is hindered by a dog, as shown in Figure 1.

The fox and the dog move in a grid, while the chicken stays in the upper right corner. The possible movements are: move up, down, left, right, or stop. Suppose that the fox moves faster than the dog (i.e. the fox can move at each step while the dog moves every other step) and that the dog is not standing still. The strategy of the fox can be to go towards the chicken unless the dog is on the way and in that case, it just stops until the dog moves and then it goes ahead. However, such a strategy does Figure 1: The fox-dog-chicken example. not reach the goal as soon as possible. Since the fox is quicker than the dog, a better strategy is to pass around the dog.

The controller and the plant are specified as transition systems. The property is specified in

LTL as ¬bad_states U goal where bad_states are the states where the fox and the dog are in the same position, while goal is the state where the fox and the chicken are in the same cell of the grid. We formalize and solve the problem of checking whether satisfies the property ASAP with the given plant .

3. Notations and Preliminary Definitions

In the following, we consider Symbolic Transition Systems (STSs), also known as synchronous state machines, to represent the behavior of reactive systems, i.e. systems whose role is to maintain an ongoing interaction with their environment.

Given a set of propositional variables Σ , an STS over Σ is a tuple ⟨, Σ , , ⟩, where is a set of state variables disjoint from Σ , is a formula over , and is a formula over ∪ Σ ∪ ′. We assume the reader to be familiar with the standard notions of paths, traces, and products of STSs.

In order to specify properties, we consider Linear Temporal Logic with future and past operators, denoted by LTL and interpreted over infinite sequences of states. Two notable classes of properties that can be expressed in LTL are safety and co-safety properties. Safety properties are those properties which can be refuted by a bad-prefix, i.e., a finite computation than cannot be extended to an infinite computation that satisfies the formula. Conversely, co-safety properties are those properties which can be verified by identifying a good-prefix, i.e., a finite computation such that all infinite extensions satisfy the formula. In this paper we use the syntactic fragment LTLEBR [ 1 ] to express safety properties, and the dual fragment co-LTLEBR for co-safety ones.

Definition 3.1 (The logic co-LTLEBR). Let , ∈ N, a LTLEBR formula is inductively defined as follows: := | ¬ | 1 ∨ 2 | Y | 1S 2 := | ¬ | 1 ∨ 2 | X | 1U[,] 2 := | 1 ∧ 2 | X | F | U := | 1 ∨ 2 | 1 ∧ 2 (Pure Past Layer) (Bounded Future Layer)

(Future Layer) (Boolean Layer)

In the rest of the paper, we assume that Σ = ∪ is divided into two disjoint sets and of, respectively, controllable and uncontrollable variables.

Definition 3.2. An arena for a reachability game is given by a deterministic STS = ⟨, Σ , , ⟩ and a formula over , called winning condition. We say that a strategy for controller : (2 )+ → 2 wins the reachability game with arena and winning condition if for all sequences of choices made by environment = 1, 2, · · · ∈ (2 ), there exists such that the -th state of the unique path over the trace 1 · (1), 2 · (12), . . . satisfies .

Reactive synthesis is the problem of translating a logical specification into a reactive system that is guaranteed to satisfy the specification for all possible behaviors of its environment.

Definition 3.3 (Reactive Synthesis problem). Let be a temporal formula over the alphabet Σ = ∪ . We say that is realizable if and only if there exists a strategy : (2 )+ → 2 such that for all = (1, 2, . . .) ∈ (2 ), it holds that the sequence satisfies 1 · (1), 2 · (12), . . . |= . The synthesis problem is the decision problem to say whether is realizable or not. If is realizable, the corresponding strategy is computed.

For co-safety properties, reactive synthesis can be reduced to finding a winning strategy in a reachability game defined from the formula. In [ 1 ] is shown how reactive synthesis from LTLEBR formulas can be reduced to solving a safety game over a monitor built directly from the specifications. Such monitor accepts only those traces satisfying the formula from which is built, while it goes into error state whenever a trace not satisfying the formula is met. Thanks to the duality between safety and reachability games, it is possible to synthesize a co-LTLEBR formula exploiting the monitor built from the corresponding LTLEBR formula, i.e. the negation.

In [3], the synthesis problem is extended to variants of LTL with quantitative semantics such as

LTL[ℱ ] and LTLdisc[ ]. In general, quantitative semantics assign a real value , K ∈ [ 0, 1 ] to J a formula over a sequence . As in [ 3 ], we extend the evaluation of a formula to a system as J, K := inf {J, K | ∈ ℒ ()}, and thus to a strategy as J, K := inf {J(), K | ∈ (2 )}.

Definition 3.4 ([3] Quantitative Reactive Synthesis problem). Let be a temporal formula over Σ .

The realizability problem for is the problem to find a strategy such that J, K is maximal among all the strategies. We say that is realizable with value if and only if there exists a strategy such that J, K ≥ .

In order to distinguish the quantitative realizability from the standard one, we call the latter qualitative

realizability. Unsurprisingly, the decidability and complexity of the quantitative realizability problem depends on the actual quantitative semantics we consider. As shown in [ 4 ], the quantitative realizability problem for LTL[ℱ ] is 2EXPTIME-complete. The same paper gives only an approximate solution for the logic LTLdisc[ ], that allows to obtain a strategy that is optimal up to any desired accuracy > 0.

Later on in this paper, we propose a quantitative semantics to formalize ASAP properties, and we show that checking if a given strategy is optimal is 2EXPTIME for generic co-safety properties.

4. Optimal Model Checking

In this section, we formalize the problem of checking whether a controller satisfies optimally a temporal specification with respect to a given plant. To this purpose, we suppose to be given a quantitative semantics that assigns a real value J, K to a formula and a transition system . Moreover, we define formally some notations and assume that the system = × is the closed loop composition of a controller and a plant . Given a subset of propositions in Σ , we say that an STS = ⟨, Σ , , ⟩ is input-enabled with respect to if for all ∈ 2 and ∈ 2 , there exist ∈ 2Σ∖ and ′ ∈ 2 such that , · , ′ |= . Given a subset of propositions in Σ , we say has a functional dependency on the states for if for every , 1, 2 ∈ 2 , 1, 2 ∈ 2Σ, if , 1, 1 |= and , 2, 2 |= , then 1() = 2(). The plant model is an STS over Σ that is input-enabled with respect to and has a functional dependency on the states for , i.e. it is a symbolic representation of a set of strategies of the form : (2 )* → 2 . The controller model is an STS over Σ that is input-enabled with respect to , i.e. it is a symbolic representation of a set of strategies of the form : (2 )+ → 2 .

We are interested in proving that the closed loop ℒ ( × ) satisfies an LTL formula over Σ . This optimal model checking problem is formalized and adapted to our case as follows: Definition 4.1 (Optimal model checking). We say that satisfies in the context optimally, denoted by |=* , if there does not exist ′ such that J′ × , K > J × , K. traces.

Note that, in general, given two controllers and ′, their composition with the plant may lead

to completely diferent runs. Thus, it is not possible to compare the semantics of × and ′ × on single runs. This is why in Def. 4.1, we use J × , K, which takes the minimum value of over all if and only if there exists a controller such that J × , K ≥ .

Definition 4.2 (Quantitative Realiability Under Assumptions). Let be a temporal formula over the

alphabet Σ =

∪ and is a plant model. We say that is realizable under assumption with value Suppose we can compute the value =

J

K × , , then we can reduce the optimal model checking problem to quantitative realizability of under the assumption with a value ′ > . In the next sections, we will show how this reduction can rely on qualitative realizability in the particular case of the ASAP quantitative semantics.

5. ASAP LTL

In this section, we propose a new quantitative semantics that is suitable to formalize ASAP properties.

Our definition of ASAP semantics gives a value in

N ∪ {∞}. We then cast the semantics to [ 0, 1 ] ⊂ R that accepts exactly all informative prefixes of to be aligned with the standard definitions of quantitative semantics. Moreover, we introduce an alternative recursive definition of the ASAP semantics and show that the two definitions are equivalent.

The ASAP semantics is related to the notion of informative prefix introduced in [ 5 ] as the syntactical counterpart of the notion of “good prefix” for a co-safety formula: a finite computation that witnesses the satisfaction of the formula. While liveness, persistence, and reactivity LTL formulas do not necessarily have an informative prefix, if is a safety LTL formula then it is possible to build an automaton ¬ ¬ [ 5 ]. This “tightness” results on the monitor for a formula can be extended to LTLEBR by redefining the definition of informative prefix to include past operators as follows. and only if there exists a mapping : {0, . . . , } ↦→ 2() that respects the following conditions: We say that a finite computation = 0 1 . . . − 1 is an informative prefix for an LTL formula if 1. ∈ (0) 2. () is empty. 3. For all 0 ≤ ≤ − 1 and ∈ (): • if is ⊤, , or ¬, then it is satisfied by ; • if = 1 ∧ 2, then 1 ∈ () and 2 ∈ (); • if = 1 ∨ 2, then 1 ∈ () or 2 ∈ (); • if = X 1, then 1 ∈ ( + 1); • if = Y 1, then > 0 and 1 ∈ ( − 1); • if = Z 1, then = 0 or 1 ∈ ( − 1); • if = 1 U 2, then 2 ∈ () or [ 1 ∈ () and 1 U 2 ∈ ( + 1) ]; • if = 1R 2, then 2 ∈ () and [ 1 ∈ () or 1R 2 ∈ ( + 1) ]; • if = 1S 2, then 2 ∈ () or [ 1 ∈ () and 1S 2 ∈ ( − 1) ]; • if = 1T 2, then 2 ∈ () and [ 1 ∈ () or 1T 2 ∈ ( − 1) ].

The mapping is called the witness for in . Given an informative prefix of a formula on

an infinite trace , we say that is minimal if there does not exist any other informative prefix of shorter in length than . , , ⊤KASAP = 1 , , ⊥KASAP = +∞ , , ¬KASAP = if ∈ otherwise if ̸∈ otherwise J , , 1 ∧ 2KASAP = max {︀ , , 1KASAP J

J

}︀ , , , 2KASAP , , 1 ∨ 2KASAP = min {︀ , , 1KASAP J

J

}︀ , , , 2KASAP , , XKASAP = , + 1, KASAP + 1

J , , YKASAP = , , ZKASAP = {︃ , − 1, KASAP − 1 if > 0

J {︃ , − 1, KASAP − 1 if > 0

J otherwise otherwise Definition 5.1 (ASAP semantics). Let be an LTL formula and an infinite trace. The ASAP semantics shortest informative prefix of . of evaluated on , denoted by , KASAP, is defined as follows:

J

J, KASAP = ( ), where is the

The ASAP semantics can also be defined by recursion on the structure of the formula.

recursively as follows: Definition 5.2

(ASAP recursive semantics). Let be an LTL formula and be a trace. The ASAP semantics of evaluated on at position is a natural number , denoted by , , KASAP and defined J {︃1 {︃1 +∞ +∞ +∞ 1 ≥ 0 ≥ 0 ︂{ ︂{ J , , 1 U 2KASAP = min J , , 1R2KASAP = max J , , 1S2KASAP = min 0≤ ≤ , , 1T2KASAP = max 0≤ ≤ max min ︂{ ︂{ ︂{ ︂{ max min ︂{ ︂{ J , + , 2KASAP + , max {︀ , + , 1KASAP + }︀

J 0≤ < J , + , 2KASAP + , min {︀ , + , 1KASAP + }︀

J 0≤ < J , − , 2KASAP − , max {︀ , − , 1KASAP −

︀}

J 0<≤ J , − , 2KASAP − , min {︀ , − , 1KASAP −

︀}

J 0≤ < ︂} ︂} ︂} ︂} if and only if , 0, KASAP = .

J ∞ − = ∞, if ∈ N, 0 − = 0, if ∈ N ∪ {∞}, and − ∞

We now prove that the two quantitative semantics are equivalent.

where , , +, and − are defined on the extended natural numbers N ∪ {∞}. We recall that = 0, if ∈ N. We say that J, KASAP = the prefix of of length . If is a minimal informative prefix for , then , KASAP = , KASAP. J J Theorem 5.1. Let be an LTL formula, = 0 1 . . . be an infinite trace, and = 0 1 . . . − 1 be

Finally, we define the normalized version of the ASAP semantics as follows:

Definition 5.3 (Normalized ASAP Semantics). For any formula and trace ,

J, KASAP = {︃0 1/( , KASAP) otherwise

J if , KASAP = +∞

J Thus, , KASAP tends to 0 while J, KASAP tends to +∞.

J

6. Reduction of ASAP LTL Model Checking to Reactive Synthesis

We now show that, in the case of co-safety formulas, the optimal model checking problem with ASAP

LTL semantics can be reduced to a reachability game. The key step is to build an arena with a parametrized winning condition () so that there exists a winning strategy if there exists a controller such that J × , KASAP < . With such a construction, we can reduce the optimal model checking problem to a qualitative synthesis problem. This is achieved by 1) computing = J × , KASAP and 2) checking if there exists a winning strategy for the game with winning condition ().

We first define an STS counting the transitions from the initial state. It has a new state variable steps so that initially steps has value 0 and at each step it is increased by 1. Formally, we define the STS steps as follows: steps := ⟨{steps}, ∅, steps = 0, steps′ ↔ ite(steps < max , steps + 1, steps)⟩, where ite is the Boolean encoding of an if-then-else term and max is a suficiently large constant. Let be a deterministic STS with a boolean condition on the STS variables that is reached by any informative prefix of and built starting from an LTLEBR formula, as given by [ 1 ]. Recall that a boolean condition is reached by a STS if there exists a finite path 0 . . . in such that |= . Step 1, i.e. computing , can be solved by looking for a minimal such that × × × steps |= F( ∧ steps ≤ ).

This can be achieved with an incremental number of model checking problems or with parametric model checking.

Let be the deterministic STS accepting the same language of with error state that is reached

wherever the trace is not accepted by . Then we define the arena as the product × × with the winning condition () defined as ∨ ( ∧ step < ).

A winning strategy for the reachability game with winning condition () and arena guarantees that in every play of the game the controller can reach a state where either the plant monitor is in (the play is not a valid trace of the plant), or the monitor for is in the accepting state and the value of is less than the bound (formula is true in less than steps). We can prove that existence of a winning strategy corresponds to existence of a controller that can enforce with cost less than . Theorem 6.1. There exists a winning strategy for the reachability game with winning condition () and arena if there exists a controller such that J × , KASAP < .

The next theorem states the complexity of the procedure.

Theorem 6.2. The ASAP LTL model checking problem for co-LTLEBR is 2EXPTIME-complete. Remark. It is not possible to synthesize a controller winning the game enforcing the monitor plant into error state, since the plant is assumed to be input-enabled and so the built monitor accepts any possible combination of controllable variables. Therefore, it is up to the environment to choose whether it goes into error state or not.

7. Related work

The problem of optimizing winning strategies has been studied since the early 2000 [6]. Earlier works

addressed optimization of the memory size of the controller (i.e., number of states of the automaton) [ 7 ] and minimization of waiting times for request-response conditions [ 8 ]. In this paper, we relate the problem of model checking open systems, also studied in [ 9 ], to the problem of optimal synthesis, using a quantitative semantics for LTL to define the problem of optimal model checking in terms of synthesis of a better strategy.

Several formalisms for quantitative semantics for temporal logic exist in the literature [10, 11, 12, 13, 14, 15, 16]. While these formalisms can be used to define optimality criteria, most of the current works concentrate on the model checking problem and do not consider the synthesis problem. Notable exceptions are the logics LTL[ℱ ] and LTLdisc[ ], introduced in [ 4 ], which extend LTL, the first, with propositional quality operators to prioritize and weight diferent satisfaction possibilities and, the second, with discounting operators, to take into account the delay incurred in the satisfaction of eventualities. The logic LTL[ℱ ] has been subsequently used to develop algorithms for quantitative assume-guarantee synthesis of GR(1) properties [ 3 ], for compositional assume-guarantee synthesis [17], and for the synthesis of finite-memory controllers of discrete event systems [ 18]. In particular, the ASAP quantitative semantics is very related to the logic LTLdisc[ ], which extends LTL with a “discounted until” U operator that takes into consideration the length of the prefix needed to satisfy the eventualities. It is parametrized by a function over the natural numbers. Indeed, with discounting function () = +11 , if and are propositional, the semantics of U is the same as the ASAP semantics of U . In [ 4 ], it is also remarked that a discounted next can be expressed using the normal X and the discounted until: one has to define () such that () = ( + 1) and then define the discounted next X ( ) as X(⊥ U ). However, in this case, the semantics of the discounted next and the discounted until use diferent discount functions. Moreover, the recursive definition of the temporal operators are not valid for LTLdisc[ ]. Thus, although the motivations are the same, the quantitative semantics that we propose difer from LTL disc[ ] and is more natural to express ASAP requirements in the sense that it is directly connected to the length of informative prefixes that satisfy the formula.

A line of research related to this paper is the study of “good enough/best efort synthesis”, a variant of synthesis in which the system is required to satisfy the specification only as long and as much as allowed by the environment, and it is allowed to fail when a satisfying computation does not exist [19, 20, 21, 22, 23]. While the formalisms and the algorithms are related to our work, the setting is quite diferent, as they aim to synthesize a controller that is “good enough” to at least partially respect the desired properties when they cannot be enforced, and not to synthesize the “best controller” under some optimality criteria.

8. Proof of Concept Evaluation

We implemented the optimal model checking procedure with a toolchain called optimal-strategy that uses the nuXmv model checker [ 2 ] to build the monitor for the formula, solve the parametric model checking, and build the arena for the reachability game. The game is solved by the symbolic safety game solver simple-synth we developed from scratch. The game arena is produced in AIGER format [24], to allow using any tool for reactive synthesis for solving the game. All code, examples and benchmarks to replicate the experiments are available in the artifact 1. The toolchain can either solve the parameterized model checking defined in Section 5 to compute the upper-bound for the reachability game, or start with a user-defined upper bound.

As a first benchmark, we tested the fox, dog and chicken example introduced in Section 2 and we

have proved that the given controller is not optimal, since it enforces the specification in 15 steps, while the toolchain synthesized a controller which satisfies the specification in 7 steps.

To test the tool, we considered scalable formulas of increasing size. Since there are no other tools solving the optimal model checking problems for ASAP LTL, there are no comparisons with other software. The first formula considers a scenario where a car moves on a × square grid. The initial controller can only move the car up, down, left and right. The optimal controller synthesized by the tool is allowed also to move diagonally. We require the controller to reach points along the diagonal of the grid, avoiding a set of bad states, as formalized by: ¬ U (− 1 ∧ O(− 2 ∧ O(− 3 ∧ O(. . . ∧ O0)))), (1) where is the set of bad states defined as follows: = ⋁︀⌊− 1⌋( = ∧ = + 1). =0

The other 6 categories consist of synthetic formulas which are conjunctions and disjunctions of next, bounded finally, bounded globally, and unbounded finally and until operators. The plant consists of controllable variables , uncontrollable variables and is defined to flip the values of uncontrollable variables at each step, forcing mutual exclusion between odd and even uncontrollable variable. The formulas 1https://drive.google.com/file/d/1qbs6FvfcFeUQitwFWGImfuQcjgOkzQ7I/view?usp=sharing are aimed to test the toolchain by increasing the number of variables and the nesting of next operators: ⋀︁− 1 X(F[ 0,6 ]( = )) (2)

=0 ⋀︁− 1(XG[ 0,3 ]F[ 0,3 ]( = )) (3) =0

9. Conclusions and Future Work

In this paper, we formalized the requirements of fulfilling some temporal reachability properties ASAP

for a controller assuming some constraints on the environment. In order to do that, we formalized the optimal model checking problem w.r.t. LTL with a quantitative semantics able to capture the time needed to fulfill a property and so that its optimal model checking problem corresponds to check the

ASAP requirement. Finally, we provided a reduction to standard co-safety synthesis. A proof-of-concept

evaluation shows that the approach is indeed feasible. The paper opens various problems left for future work, e.g., how to solve the optimal model checking with other semantics, how to generalize the reduction to synthesis to support larger fragments of ASAP LTL, and how to scale up the verification for example exploiting incremental approaches.

Acknowledgments: The authors want to thank all the anonymous reviewers of OVERLAY 2024 for

the insightful comments on a preliminary version of this paper. [10] T. Anevlavis, M. Philippe, D. Neider, P. Tabuada, Being correct is not enough: Eficient verification using robust linear temporal logic, ACM Trans. Comput. Logic 23 (2022). doi:10.1145/3491216. [11] P. Bouyer, N. Markey, R. M. Matteplackel, Averaging in LTL, in: CONCUR, volume 8704 of LNCS,

Springer, 2014, pp. 266–280. [12] K. Chatterjee, L. Doyen, T. A. Henzinger, Quantitative languages, ACM Trans. Comput. Log. 11 (2010) 23:1–23:38. doi:10.1145/1805950.1805953. [13] M. Droste, G. Grabolle, G. Rahonis, Weighted Linear Dynamic Logic, Int. J. Found. Comput. Sci.

35 (2024) 145–177. doi:10.1142/S0129054123480088. [14] M. Faella, A. Legay, M. Stoelinga, Model Checking Quantitative Linear Time Logic, in: QAPL, number 3 in Electronic Notes in Theoretical Computer Science, Elsevier, 2008, pp. 61–77. [15] P. Gastin, B. Monmege, A unifying survey on weighted logics and weighted automata, Soft

Comput. 22 (2018) 1047–1065. doi:10.1007/S00500-015-1952-6. [16] Y. Li, M. Droste, L. Lei, Model checking of linear-time properties in multi-valued systems, Inf. Sci.

377 (2017) 51–74. doi:10.1016/J.INS.2016.10.030. [17] R. Dewes, R. Dimitrova, Compositional high-quality synthesis, in: Automated Technology for

Verification and Analysis, Springer Nature Switzerland, 2023, pp. 334–354.

[18] A. Sakakibara, N. Urabe, T. Ushio, Finite-Memory Supervisory Control of Discrete Event Systems for LTL[ℱ ] Specifications, IEEE Transactions on Automatic Control 67 (2022) 6896–6903. doi: 10. 1109/TAC.2021.3139221. [19] S. Almagor, O. Kupferman, Good-enough synthesis, in: CAV, 2020, pp. 541–563. [20] B. Aminof, G. D. Giacomo, S. Rubin, Best-Efort Synthesis: Doing Your Best Is Not Harder Than

Giving Up, in: IJCAI, 2021, pp. 1766–1772. doi:10.24963/IJCAI.2021/243. [21] B. Aminof, G. D. Giacomo, S. Rubin, Reactive Synthesis of Dominant Strategies, in: AAAI, 2023, pp. 6228–6235. doi:10.1609/AAAI.V37I5.25767. [22] B. Aminof, G. D. Giacomo, A. Lomuscio, A. Murano, S. Rubin, Synthesizing Best-efort Strategies under Multiple Environment Specifications, in: KR, 2021, pp. 42–51. doi: 10.24963/KR.2021/5. [23] M. Lahijanian, S. Almagor, D. Fried, L. E. Kavraki, M. Y. Vardi, This Time the Robot Settles for a

Cost: A Quantitative Approach to Temporal Logic Planning with Partial Satisfaction, in: AAAI,

2015, pp. 3664–3671. doi:10.1609/AAAI.V29I1.9670. [24] A. Biere, K. Heljanko, S. Wieringa, AIGER 1.9 And Beyond, Technical Report 11/2, Institute for

Formal Models and Verification, Johannes Kepler University, 2011.

References

[1] A. Cimatti , L. Geatti , N. Gigante , A. Montanari , S. Tonetta , Extended bounded response LTL: a new safety fragment for eficient reactive synthesis , Form Methods Syst Des ( 2021 ). doi: 10.1007/ s10703-021-00383-3.

[2] R. Cavada , A. Cimatti , M. Dorigatti , A. Griggio , A. Mariotti , A. Micheli , S. Mover , M. Roveri , S. Tonetta , The nuXmv Symbolic Model Checker , in: CAV, volume 8559 of LNCS , Springer, 2014 , pp. 334 - 342 .

[3] S. Almagor , O. Kupferman , J. O. Ringert , Y. Velner , Quantitative Assume Guarantee Synthesis, in: CAV, volume 10427 , 2017 , pp. 353 - 374 . doi: 10 .1007/978-3- 319 -63390-9\_ 19 .

[4] S. Almagor , U. Boker , O. Kupferman , Formally reasoning about quality , J. ACM 63 ( 2016 ). doi: 10 .1145/2875421.

[5] O. Kupferman , M. Vardi , Model checking of safety properties , Formal Methods in System Design 19 ( 1999 ). doi: 10 .1023/A: 1011254632723 .

[6] W. Thomas , Optimizing winning strategies in regular infinite games , in: SOFSEM , volume 4910 of LNCS , Springer, 2008 , pp. 118 - 123 . doi: 10 .1007/978-3- 540 -77566-9\_ 10 .

[7] M. Holtmann , C. Löding , Memory Reduction for Strategies in Infinite Games , in: CIAA, volume 4783 of LNCS , Springer, 2007 , pp. 253 - 264 . doi: 10 .1007/978-3- 540 -76336-9\_ 24 .

[8] F. Horn , W. Thomas, N. Wallmeier , M. Zimmermann , Optimal strategy synthesis for requestresponse games , RAIRO Theor. Informatics Appl . 49 ( 2015 ) 179 - 203 . doi: 10 .1051/ITA/2015005.

[9] O. Kupferman , M. Y. Vardi , P. Wolper , Module Checking, Inf. Comput. 164 ( 2001 ) 322 - 344 .