Paper deep dive
Learning to adapt GR(1) specifications through degradation
Tiberiu-Andrei Georgescu, Dalal Alrajeh, Sebastian Uchitel
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 9/16/2026, 8:18:28 AM
Summary
This paper addresses the limitation of GR(1) reactive synthesis where controllers fail when environment assumptions are violated. The authors propose an oracle-guided inductive synthesis approach to adapt specifications by degrading them minimally to restore realisability. Unlike prior work that may converge prematurely to suboptimal repairs, this method explores a broader space of adaptations using preference criteria based on robustness and guarantee preservation. Case studies demonstrate that the learning-based approach finds superior adaptations compared to simple specification reduction.
Entities (7)
Relation Signals (5)
Arbiter → isusedin → Learning to adapt GR(1) specifications through degradation
confidence 97% · for our case studies we successfully discover degradations... Arbiter case study... discussed in (Piterman et al., 2006)
GR(1) → isafragmentof → Linear Temporal Logic (LTL)
confidence 95% · Piterman et al. (Piterman et al., 2006) introduced a restricted fragment of LTL known as Generalised Reactivity of rank 1 (GR(1) for short)
Oracle-Guided Inductive Synthesis (OGIS) → isusedby → Learning to adapt GR(1) specifications through degradation
confidence 95% · Our work proposes an approach based on oracle-guided inductive synthesis to adapt the specification
Assumption Violation → causesfailureof → GR(1) Controllers
confidence 92% · should they encounter environment behaviour unspecified in the assumptions of the specification, the specified system guarantees are no longer ensured
Buckworth et al. → proposedpriorworkon → Specification Adaptation
confidence 90% · Recent work by Buckworth et al. (Buckworth et al., 2023) addresses this challenge through the adaptation of environmental assumptions
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Reactive synthesis is a powerful tool for generating correct-by-construction controllers from formal specifications. GR(1) is an assume-guarantee specification framework that enables efficient synthesis, allowing synthesised controllers to be used in a wide array of applications. The limitation of such controllers is that, should they encounter environment behaviour unspecified in the assumptions of the specification, the specified system guarantees are no longer ensured. Our work proposes an approach based on oracle-guided inductive synthesis to adapt the specification to be consistent with the observed assumption violation, while degrading system guarantees as little as possible to maintain realisability. Our methodology discovers multiple potential solutions, so we propose a preference criteria, based on the ability of the specification to enable robustness under adaptation. Although our approach is capable of degrading the entire specification, for our case studies we successfully discover degradations that preserve the entire set of original guarantees.
Tags
Links
- Source: https://arxiv.org/abs/2609.12231v1
- Canonical: https://arxiv.org/abs/2609.12231v1
Trouble viewing inline? Open PDF directly →
Full Text
200,324 characters extracted from source content.
Expand or collapse full text
Learning to adapt GR(1) specifications through degradationNote: This is a preprint of a manuscript under review at ACM Transactions on Software Engineering and Methodology. Tiberiu-Andrei Georgescu email: tibi.geo@ic.ac.uk Affiliation: Imperial College London, London, United Kingdom , Dalal Alrajeh Affiliation: Imperial College London, London, United Kingdom email: dalal.alrajeh04@ic.ac.uk and Sebastian Uchitel Affiliation: Imperial College London, London, United Kingdom Affiliation: Universidad de Buenos Aires, CONICET, Universidad de San Andrés, Argentina email: s.uchitel@ic.ac.uk Abstract. Reactive synthesis is a powerful tool for generating correct-by-construction controllers from formal specifications. GR(1) is an assume-guarantee specification framework that enables efficient synthesis, allowing synthesised controllers to be used in a wide array of applications. The limitation of such controllers is that, should they encounter environment behaviour unspecified in the assumptions of the specification, the specified system guarantees are no longer ensured. Our work proposes an approach based on oracle-guided inductive synthesis to adapt the specification to be consistent with the observed assumption violation, while degrading system guarantees as little as possible to maintain realisability. Our methodology discovers multiple potential solutions, so we propose a preference criteria, based on the ability of the specification to enable robustness under adaptation. Although our approach is capable of degrading the entire specification, for our case studies we successfully discover degradations that preserve the entire set of original guarantees. 1. Introduction Formal synthesis from temporal-logic specifications provides a rigorous approach for constructing reactive systems that are correct by construction with respect to their formally specified requirements. Consequently, stakeholders obtain stronger assurance that the generated controller satisfies the intended behavioural properties encoded within the specification (Pnueli and Rosner, 1989). However, synthesising controllers from unrestricted Linear Temporal Logic (LTL) specifications is doubly exponential in complexity, limiting practicality for many real-world applications. Piterman et al. (Piterman et al., 2006) introduced a restricted fragment of LTL known as Generalised Reactivity of rank 1 (GR(1) for short), enabling polynomial-time synthesis of reactive controllers and substantially improving the practical applicability of synthesis techniques. In GR(1) specifications, system behaviour is decomposed into two components: assumptions, which characterize the expected behaviour of the environment, and guarantees, which characterize the required behaviour of the system. GR(1) therefore follows an assume–guarantee structure, where realisability holds if and only if there exists a controller that can guarantee satisfaction of its specified properties whenever the environmental assumptions remain satisfied. The implication above exposes a fundamental limitation of assume–guarantee specifications: once an environmental assumption is violated at runtime, the controller may produce arbitrary behaviour, as the correctness criterion the controller was synthesised for only applies when assumptions hold. Although techniques exist for improving the robustness of synthesized controllers under assumption violations (Bloem et al., 2011), such approaches do not generally provide precise control over which guarantees may degrade, nor the extent to which system behaviour may diverge from the intended specification. Classical work in reactive synthesis has emphasized that the validity of assume–guarantee reasoning fundamentally depends on the correctness and adequacy of the environmental assumptions themselves (Zave and Jackson, 1997). In practice, however, constructing sufficiently accurate and complete models of complex operational environments remains a significant challenge. Consequently, much of the existing literature focuses on specifying only those aspects of environmental behaviour deemed necessary for system synthesis or verification (Ma’Ayan and Maoz, 2023). While practically motivated, this approach introduces the risk that assumptions are engineered primarily to support controller realisability rather than to faithfully characterize the true operational environment. As a result, synthesized controllers may exhibit formally correct behaviour with respect to the specification while remaining vulnerable to mismatches between assumed and actual runtime conditions. In this work, we consider the problem of adapting reactive specifications under assumption violations, a setting commonly addressed in the literature through forms of specification degradation or repair. Intuitively, this problem captures how a reactive system should evolve when behaviours observed during deployment reveal environmental conditions that were not captured by the original specification. Rather than viewing adaptation as the synthesis of a single repaired specification, we instead consider the broader space of admissible adaptations obtained by integrating newly observed environmental behaviours into the environment assumptions and, where necessary, weakening or modifying the corresponding system guarantees to restore realisability. Recent work by Buckworth et al. (Buckworth et al., 2023) addresses this challenge through the adaptation of environmental assumptions based on observed runtime behaviour. Starting from a controller synthesized from a GR(1) specification, they were able to successfully leverage inductive learning to weaken the original set of assumptions to make it consistent with an environment violation, and use an oracle-guided inductive synthesis (OGIS) like loop (Jha and Seshia, 2017) to converge to a realisable set of guarantees. However, the approach proposed by Buckworth et al. (Buckworth et al., 2023) produces a single adapted specification without explicitly considering the broader space of alternative adaptations that may also restore realisability. Moreover, the selected adaptation may not necessarily correspond to the solution that is closest to the original specification, nor the one that is most robust to future assumption violations. This limitation is closely related to challenges previously identified in robustness-oriented synthesis approaches (Bloem et al., 2011). A central contribution of this paper is the formal characterization of the adaptation space and the development of principled criteria for evaluating alternative solutions. In particular, we investigate which adaptations should be preferred when multiple realisable solutions exist, including considerations such as preservation of the original specification intent, retention of critical guarantees, and robustness to future assumption violations. From this perspective, we develop a set of axioms defining preferred adaptations and use them to develop a learning-based algorithm capable of exploring a rich space of candidate adaptations. The proposed approach supports the discovery and comparison of multiple realisable alternatives while incorporating heuristics designed to prioritize preferred solutions. Experimental evaluation across multiple case studies demonstrates that the learning-based approach consistently outperforms an adaptation that operates by specification reduction, dropping violated assumptions and non-realisable guarantees. We summarize the contributions of this work as follows: (1) We formalize the problem of adapting reactive specifications under observed mismatches between assumed and actual environmental behaviour. (2) We introduce a formal preference framework for reasoning about alternative adaptation solutions, including criteria related to specification preservation and guarantee retention. (3) We develop an adaptation algorithm based on specification reduction, and formally show that it generates realisable specifications consistent with observed environment behaviour. (4) We develop an inductive learning-based adaptation algorithm that weakens specification formulas to explore a richer space of realisable adaptations, and formally show that the generated specifications are consistent with environment observations. (5) We evaluate and analyze the proposed approaches across five case studies from the literature, examining the changes, tradeoffs, and preference of the resulting adapted specifications. Section 2 introduces a motivating example based on the Arbiter case study (Piterman et al., 2006). Section 3 presents the formal background necessary for the remainder of the paper. In Section 4, we formally define the adaptation problem, introduce a preference framework for reasoning about alternative adaptations, and present a baseline algorithm based on specification-reduction operations for discovering realisable solutions. Section 5 then considers formula-level degradation as a mechanism for solving the adaptation problem and presents an inductive learning-based adaptation algorithm for generating candidate specifications. Section 6 evaluates the proposed learning-based approach against a baseline adaptation algorithm, including comparative analysis of the resulting specifications and their logical relationships. Section 7 reviews related work and situates our work on adaptation within the broader literature on reactive synthesis, specification adaptation, and robustness. Finally, Section 8 concludes with a discussion of current limitations, broader implications, and directions for future work. 2. Motivating Example We motivate the problem of specification adaptation under assumption violations using the Arbiter case study, discussed in (Piterman et al., 2006), and further leveraged by subsequent literature on adaptation (Alur et al., 2013; Cavezza et al., 2020; Buckworth et al., 2023). The arbiter constitutes the system to be synthesized, and controls access to an ARM Advanced High-Performance Bus (AHB), an on-chip communication protocol. The environment consists of multiple masters together with a third party (e.g. a user), although we simplify the case study to two masters only. Each master may request access to the resource by flipping the environment variable r1r1 or r2r2, representing their respective request switch. In response to this behaviour, the arbiter needs to eventually grant access to each requesting master by flipping the system variable g1g1 or g2g2, representing their respective grant switch. The arbiter is bound to never grant access to this shared resource to both masters at the same time, even if they make their requests concurrently. Finally, the third party has the power to lock the arbiter by flipping the environment variable a off, which disallows the arbiter from granting access to the bus. We model the Arbiter behaviour as a GR(1) specification, shown in Table 1. In addition to the behaviour described earlier, we consider the addition of a further assumption to ensure realisability of the specification: the arbiter is always active. Consequently, the resulting system is realisable according to the realisability condition of GR(1) presented in (Bloem et al., 2012). Therefore, an implementation can be synthesized that satisfies the specified guarantees. Type & ID Informal requirement GR(1) formalization guarantee_1 If master 1 requests to start communicating with the bus, access is eventually granted to master 1 □(r1→◊g1) (r1→ 1) guarantee_2 If master 2 requests to start communicating with the bus, access is eventually granted to master 2 □(r2→◊g2) (r2→ 2) guarantee_3 If inactive, the arbiter cannot give access to the bus to any master □(¬a→(¬g1∧¬g2)) ( →( 1 2)) guarantee_4 At most one master may be granted access to the bus at a time □(¬g1∨¬g2) ( 1 2) assumption_1 The bus is never locked □(a) (a) Table 1. GR(1) specification for the arbiter example Suppose, however, that during deployment, the system exhibits an unexpected behaviour, in which the arbiter becomes inactive. A trace demonstrating a violation to the introduced environment assumption is one in which the environment deactivates the bus in the first time point. Consequently, the synthesized controller is no longer obliged to satisfy the specified guarantees. Although the controller may continue to exhibit operationally robust behaviour (Bloem et al., 2014), there is no guarantee that the guarantees it preserves correspond to the intended or safety-critical system behaviour. Prior work on specification repair (Buckworth et al., 2023) demonstrated that assumption-violating behaviours can be incorporated into a realisable specification through automated adaptation techniques. In particular, the arbiter specification in Table 1 was used as one of their case studies. Applying their repair method to this specification yields a repaired solution in which assumption_1assumption\_1 and guarantee_3guarantee\_3 are both weakened to ⊤ . The resulting specification is realisable while preserving a subset of the system’s original guarantees. We note, however, that this adaptation comes at a cost. Most notably, the repaired specification completely disregards the environment variable a. Although this variable remains observable to the controller, it no longer influences the specification and is therefore ignored during synthesis. One might argue that the original assumption requiring the arbiter to remain continuously active was overly restrictive and ultimately responsible for the assumption violation. However, as we demonstrate shortly, this does not justify eliminating all dependence on a, as doing so discards behaviour that remains both meaningful and exploitable. The problem above has two main causes: (1) Premature convergence to the first feasible intermediate solution encountered; and (2) An insufficiently expressive solution space, which restricts the exploration of alternative repairs. Addressing either of these limitations would increase the likelihood of identifying repairs that preserve a greater portion of the original specification. For example, the repair framework of (Buckworth et al., 2023) admits an alternative repair in which assumption_1assumption\_1 is weakened to □((g1∨g2)→a) ((g1 g2)→ a). Under this assumption, the arbiter may be deactivated only when neither requesting master has been granted access to the shared resource. Consequently, the specification remains realisable without weakening any of the system guarantees. However, if this repair, or one with similar properties, is not explored, the subsequent guarantee degradation procedure may unnecessarily weaken the specification despite the existence of repairs that preserve all original guarantees. Alternatively, prior work does not consider degrading assumptions to weaker temporal patterns, such as justice or response properties. In the arbiter example, observing that the arbiter may become inactive need not imply that it can remain inactive indefinitely. Instead, assumption_1assumption\_1 could be weakened from an invariant to the justice property □◊a a, requiring only that the arbiter eventually becomes active again. Although this repair lies outside the search space explored by prior work, it likewise restores realisability without requiring any degradation of the system guarantees. The discussion above suggests that some repairs are inherently more desirable than others. While the preference is straightforward when comparing a repair that preserves all system guarantees with one that preserves only a subset, the duality of assume–guarantee specifications makes such comparisons considerably less clear in the general case. Existing repair approaches (Buckworth et al., 2023; Zhang, 2025) provide limited guidance on how alternative adaptations should be evaluated when both assumptions and guarantees may be modified. We therefore investigate the structure of the adaptation space to identify the properties that characterize desirable specification repairs. Building on these properties, we develop methods for systematically discovering preferred realisable adaptations from a broader space of candidate specifications. More fundamentally, the observed violation exposes the need to reason about the quality of specification repairs, rather than merely their existence. Although multiple realisable adaptations may satisfy the observed environmental behaviour, they need not preserve the original specification equally well. This motivates the need for principled criteria for comparing candidate repairs and identifying those that minimise unnecessary degradation of the specification. 3. Background We present the theoretical background necessary for the remainder of this work. The preliminaries focus on the temporal-logic and reactive-synthesis foundations underlying our approach, including Linear Temporal Logic, GR(1) specifications, and notions of specification weakness, covered in Sections 3.1 and 3.2. 3.1. Linear Temporal Logic over Infinite and Finite Traces Temporal logics model system evolution over time using Boolean variables. Let V denote a finite set of propositional variables capturing relevant abstractions of the system at a given instant in time. Using this set of variables, we define a state as follows: Definition 3.1 (State). Given a finite set of Boolean variables V, a state is a valuation of the variables in V at a particular instant in time. Equivalently, a state can be represented as a subset p⊆p containing exactly those variables assigned the value true. We denote the set of all states over V by S=2S=2^V. This representation captures the system state at a particular instant in time. In discrete-time settings, system behavior can then be modeled as a sequence of consecutive states, referred to as a trace: Definition 3.2 (Trace). Given a set of Boolean variables V, a trace is an ordered sequence of states over V. A finite trace is an element of (2)∗(2^V)^*, while an infinite trace is an element of (2)ω(2^V)^ω. Infinite traces correspond equivalently to ω-words in the ω-language literature. Throughout this work, we use the terms trace and word interchangeably. The notion is also equivalent to the concept of a run in automata theory. Linear Temporal Logic (LTL), introduced in (Pnueli, 1977), provides a formal language for specifying and reasoning about temporal properties of execution traces. Definition 3.3 (Linear Temporal Logic). Linear Temporal Logic (LTL) is a formal language for specifying temporal properties over reactive systems. Given a finite set of Boolean variables V, LTL formulas are inductively generated by the following grammar: φ::=⊤∣⊥∣p∣¬φ∣(φ∧φ)∣○φ∣(φUφ) ::= p ( ) \, ( \ U\ ) where p∈p is a propositional variable, ⊤ and ⊥ denote the Boolean constants true and false, respectively, ¬ and ∧ denote negation and conjunction, ○ denotes the next temporal operator, and U denotes the strong until temporal operator. Additional operators can be derived from this grammar, including φ∨ψ≡¬(¬φ∧¬ψ) ψ≡ ( ψ), φ→ψ≡¬φ∨ψ →ψ≡ ψ, eventually: ◊φ≡⊤Uφ, \, ≡ \ U\ , and globally: □φ≡¬◊¬φ. \, ≡ \, . LTL formulas specify temporal properties over execution traces and are interpreted over infinite sequences of states. Let τ=s0s1s2…τ=s_0s_1s_2… denote an infinite trace over 22^V, and let (τ,i)⊧φ(τ,i) denote that the formula φ is satisfied at position i≥0i≥ 0 of the trace. The semantics of LTL formulas are defined inductively as follows: (τ,i) (τ,i) ⊧p p iff p∈sifor p∈ p∈ s_i p (τ,i) (τ,i) ⊧¬φ iff (τ,i)⊧̸φ (τ,i) (τ,i) (τ,i) ⊧φ∧ψ ψ iff (τ,i)⊧φ∧(τ,i)⊧ψ (τ,i) \ \ (τ,i) ψ (τ,i) (τ,i) ⊧○φ \, iff (τ,i+1)⊧φ (τ,i+1) (τ,i) (τ,i) ⊧φUψ \ U\ ψ iff ∃k≥i.(τ,k)⊧ψ∧∀j∈[i,k).(τ,j)⊧φ ∃ k≥ i.\;(τ,k) ψ\ \ ∀ j∈[i,k).\;(τ,j) For notational convenience, we additionally consider the past-time temporal operators yesterday (Y) and historically (H). The operator YφY\, specifies that φ held at the previous position in the trace, while HφH\, specifies that φ has held at all preceding positions. Their semantics are defined as follows: (τ,i)⊧Yφ (τ,i) Y\, ⇔(i>0)∧(τ,i−1)⊧φ (i>0) (τ,i-1) (τ,i)⊧Hφ (τ,i) H\, ⇔∀j<i.(τ,j)⊧φ ∀ j<i.\;(τ,j) Finally, our setting additionally requires reasoning over finite traces. To this end, we use the following weak temporal operators from (De Giacomo et al., 2014). The weak next operator is defined as Xφ≡¬X¬φ,X^W ≡ X , and specifies that φ holds at the next position in the trace, or vacuously when no successor position exists. Similarly, the weak until operator is defined as φ1Wφ2≡(φ1Uφ2)∨Gφ1, _1\ W\ _2≡( _1\ U\ _2) G\, _1, allowing φ1 _1 to hold indefinitely in the event that φ2 _2 never becomes true. Using weak until, we further define the weak eventually operator: Fφ≡⊤Wφ,F^W ≡ \ W\ , which expresses that φ may eventually hold, including beyond the finite horizon of a trace. An LTL formula induces a set of satisfying traces, commonly referred to as its language. Definition 3.4 (ω-Language of an LTL Formula). Let φ be an LTL formula over a finite set of Boolean variables V. The ω-language induced by φ is ℒ(φ)=τ∈(2)ω∣τ⊧φ.L( )=\τ∈(2^V)^ω τ \. That is, ℒ(φ)L( ) contains exactly the infinite traces that satisfy φ . Throughout this work, we use the term language to refer to ω-languages whenever no ambiguity arises. The language induced by an LTL formula captures the set of behaviours permitted by the specification. This naturally induces a notion of relative permissiveness between formulas: a formula is considered weaker if it admits a larger set of traces. Definition 3.5 (Weakness Relation over LTL Formulas). Let φ1 _1 and φ2 _2 be LTL formulas over the same set of Boolean variables V. • φ1≡φ2 _1≡ _2 iff ℒ(φ1)=ℒ(φ2)L( _1)=L( _2). • φ1⪰φ2 _1 _2 iff ℒ(φ1)⊇ℒ(φ2)L( _1) ( _2). In this case, φ1 _1 is said to be weaker than or equivalent to φ2 _2. • φ1≻φ2 _1 _2 iff ℒ(φ1)⊃ℒ(φ2)L( _1) ( _2). In this case, φ1 _1 is said to be strictly weaker than φ2 _2. • φ1⪯φ2 _1 _2 iff ℒ(φ1)⊆ℒ(φ2)L( _1) ( _2). In this case, φ1 _1 is said to be stronger than or equivalent to φ2 _2. • φ1≺φ2 _1 _2 iff ℒ(φ1)⊂ℒ(φ2)L( _1) ( _2). In this case, φ1 _1 is said to be strictly stronger than φ2 _2. The relation ⪯ is reflexive, antisymmetric, and transitive, and therefore defines a partial order over equivalence classes of LTL formulas under ≡. Given a partially ordered set, one may identify elements that are minimal or maximal with respect to the underlying order relation. Definition 3.6 (Minimal and Maximal Elements). Let (S,⪯)(S, ) be a partially ordered set. • An element e∈Se∈ S is maximal if there does not exist an element e′∈Se ∈ S such that e≺e′e e . • An element e∈Se∈ S is minimal if there does not exist an element e′∈Se ∈ S such that e′≺e e. In the remainder of this paper, the terms minimal and maximal are used with respect to the partial order over LTL formulas introduced in Definition 3.5, restricted to a given set of formulas under consideration. 3.2. Generalised Reactivity of Rank 1 Although LTL is highly expressive and can capture a broad range of temporal properties, including safety and liveness requirements, reactive synthesis from arbitrary LTL specifications is doubly exponential in the size of the formula (Pnueli and Rosner, 1989). Consequently, practical synthesis approaches often restrict attention to computationally tractable fragments of LTL. One of the most widely adopted fragments is Generalised Reactivity of rank 1 (Bloem et al., 2012), for which symbolic synthesis can be performed in polynomial time with respect to the size of the underlying game structure. In the remainder of this work, we restrict our attention to GR(1) specifications. We present the definition of GR(1) specifications following (Bloem et al., 2012), while adopting the modular environment–system decomposition style of (Maoz and Shalom, 2020). Definition 3.7 (GR(1) Specification). Let V be a finite set of Boolean variables partitioned into environment variables X and system variables Y, such that ∩=∅X = and ∪=X =V. A GR(1) specification is a tuple ⟨ℰ,⟩, ,S , where ℰ=⟨θe,ρe,J1e,…,Jme⟩E= θ^e,ρ^e,\J_1^e,…,J_m^e\ and =⟨θs,ρs,J1s,…,Jns⟩S= θ^s,ρ^s,\J_1^s,…,J_n^s\ denote the environment assumptions and system guarantees, respectively. The components of the specification are defined as follows: • θeθ^e and θsθ^s are Boolean formulas representing the initial conditions of the environment and system, respectively. The formula θeθ^e is defined over X, while θsθ^s is defined over Y. • ρeρ^e and ρsρ^s are the transition relations of the environment and system, respectively. The environment transition relation ρeρ^e constrains transitions over current-state variables in V and next-state environment variables in ′X . The system transition relation ρsρ^s constrains transitions over current-state variables in V and next-state variables in ′∪′X . These formulas specify the admissible evolution of the environment and system at each time step and are commonly referred to as safety constraints or invariants. • JieJ_i^e and JjsJ_j^s are liveness conditions over V. The environment assumptions JieJ_i^e specify properties that the environment is required to satisfy infinitely often, while the system guarantees JjsJ_j^s specify properties that the system must ensure infinitely often. A key advantage of the GR(1) fragment is that reactive synthesis can be performed in polynomial time whenever the specification is realisable. In this work, we adopt the notion of strict realisability, defined below. Definition 3.8 (GR(1) Strict Realisability (Bloem et al., 2012)). A GR(1) specification ⟨ℰ,⟩ ,S is said to be strictly realisable if the following LTL formula is realisable: ϕ:= φ:=\; (θe→θs)∧ (θ^e→θ^s )\ (θe→□(ρe→ρs))∧ (θ^e→ (Hρ^e→ρ^s ) )\ (θe∧□ρe→(⋀i=1m□◊Jie→⋀j=1n□◊Jjs)). (θ^e ρ^e→ ( _i=1^m J_i^e→ _j=1^n J_j^s ) ). Intuitively, the three conjuncts capture the following requirements: • If the environment satisfies its initial condition θeθ^e, then the system must satisfy its initial condition θsθ^s. • Assuming the environment satisfies its transition relation ρeρ^e up to the current time step, the system must satisfy its transition relation ρsρ^s at the current step. • If the environment satisfies its initial condition, continuously respects its transition relation, and satisfies all liveness assumptions JieJ_i^e infinitely often, then the system must satisfy all liveness guarantees JjsJ_j^s infinitely often. Throughout this work, and in particular in the context of the Spectra synthesiser, we frequently reason about individual formulas that constitute a GR(1) specification. In Spectra, the environment assumptions and system guarantees are typically represented as collections of separate constraints rather than as monolithic formulas. For example, the system guarantees may contain multiple invariant constraints, such as φ1=ρ1s _1=G _1^s and φ2=ρ2s _2=G _2^s, which together define the transition relation of the system specification S in a GR(1) specification ⟨ℰ,⟩ ,S . Analogously, the environment assumptions can be represented as collections of individual formulas. This representation naturally induces the interpretation that transition relations, such as ρeρ^e and ρsρ^s, are conjunctions over sets of invariant constraints. The same observation applies to initial conditions θeθ^e and θsθ^s, which may likewise be represented as conjunctions over sets of Boolean assertions. To facilitate reasoning about individual assumptions and guarantees, we introduce the following syntactic extension of GR(1) specifications, referred to as the set representation. Definition 3.9 (Set Representation of a GR(1) Specification). Let ⟨ℰ,⟩ ,S be a GR(1) specification. The set representation of the specification is the tuple ⟨,⟩ ,G , where A and G denote the sets of assumption and guarantee formulas, respectively. • A is the set of assumption formulas derived from the environment specification ℰ=⟨θe,ρe,J1e,…,Jme⟩.E= θ^e,ρ^e,\J_1^e,…,J_m^e\ . Formally, =Ie∪te∣te∈Te∪je∣je∈Le,A=I^e∪\Gt^e t^e∈ T^e\∪\GFj^e j^e∈ L^e\, where: – IeI^e is the set of conjuncts of the initial condition θeθ^e; – TeT^e is the set of conjuncts of the transition relation ρeρ^e; – Le=J1e,…,JmeL^e=\J_1^e,…,J_m^e\ is the set of environment liveness assumptions. • G is the set of guarantee formulas derived from the system specification =⟨θs,ρs,J1s,…,Jns⟩.S= θ^s,ρ^s,\J_1^s,…,J_n^s\ . Formally, =Is∪ts∣ts∈Ts∪js∣js∈Ls,G=I^s∪\Gt^s t^s∈ T^s\∪\GFj^s j^s∈ L^s\, where IsI^s, TsT^s, and LsL^s are defined analogously to IeI^e, TeT^e, and LeL^e. The partition into sets of initial conditions, transition constraints, and liveness goals is inspired by the abstract syntax representation proposed in (Maoz and Shalom, 2020). However, the broader framework introduced therein is not required for the purposes of this work. Intuitively, the assumption set A captures the expected behaviour of the environment, whereas the guarantee set G captures the required behaviour of the system. This distinction reflects the asymmetric nature of reactive synthesis: system guarantees correspond to behaviours enforceable by the controller, while environment assumptions characterise expected behaviours of the external environment. The set representation enables reasoning about GR(1) specifications at the level of individual assumptions and guarantees. In particular, it allows us to compare related specifications obtained through the removal or weakening of specific formulas. For example, given a specification ⟨,⟩ ,G , one may derive a weaker specification by removing an assumption φ∈ , yielding ′=∖φ.A =A \ \. Similarly, one may replace φ with a weaker formula φ′ such that φ′⪰φ , obtaining ′=(∖φ)∪φ′.A =(A \ \)∪\ \. Throughout this work, we primarily use the set representation ⟨,⟩ ,G when reasoning about GR(1) specifications, since it facilitates discussion of individual constraints and specification modifications. The tuple representation ⟨ℰ,⟩ ,S is retained only in situations where the structured decomposition into initial conditions, transition relations, and liveness goals improves clarity or precision. This style of representation has also been employed in prior work on specification analysis and realisability debugging (Cimatti et al., 2008). Moving back to the original representation of GR(1), we present the formal background required to understand the GR(1) controller. Reactive synthesis for GR(1) specifications is commonly formulated as a two-player game between the environment and the system, where the objective of the system is to satisfy its guarantees under the assumptions imposed on the environment. The corresponding game structure is defined as follows. Definition 3.10 (GR(1) Game (Bloem et al., 2012)). A GR(1) game is a tuple ⟨,,θe,θs,ρe,ρs,Win⟩, ,Y,θ^e,θ^s,ρ^e,ρ^s,Win , where X and Y are the environment and system variables, θeθ^e and θsθ^s are the initial conditions, and ρeρ^e and ρsρ^s are the transition relations, as defined in Definition 3.7. The winning condition of the game is given by the LTL formula Win=(⋀i=1mJie)→(⋀j=1nJjs),Win= ( _i=1^mGFJ_i^e )→ ( _j=1^nGFJ_j^s ), which states that if the environment satisfies all of its liveness assumptions infinitely often, then the system must satisfy all of its liveness guarantees infinitely often. Definition 3.11 (Game State and Projection). The state of a game is any valuation σ∈2σ∈ 2^V of the union of input and output variables =∪V=X . For any subset ′⊆V , we call σ|′=σ∩′σ|_V =σ the projection of σ onto set ′V . To reason about executions of a GR(1) game, we define game states as valuations over the environment and system variables, together with the standard notion of variable projection. Definition 3.12 (Game State and Projection). A game state is a valuation σ∈2σ∈ 2^V over the set of variables =∪.V=X . For any subset of variables ′⊆V , the projection of a state σ onto ′V is defined as σ|′=σ∩′.σ|_V =σ . That is, the projection retains only the variables in ′V that are assigned the value true in σ. Strategies provide a formal representation of how a player selects actions during the execution of a game. In the GR(1) setting, synthesis produces a finite-state strategy for the system player. Definition 3.13 (Finite-State Strategy). A finite-state strategy is a tuple ⟨Γ,γ0,f⟩, , _0,f , where: • Γ is a finite set of memory states; • γ0∈Γ _0∈ is the initial memory state; • f is a partial transition function f:Γ×Q⇀Γ×Σ,f: × Q × , where Q is the set of game states and Σ is the set of actions or outputs available to the player. Given a memory state γ∈Γγ∈ and a game state q∈Qq∈ Q, the function f returns an updated memory state γ′∈Γγ ∈ together with an output action o∈Σo∈ . When the memory structure Γ and initial memory state γ0 _0 are clear from context, we refer to a finite-state strategy ⟨Γ,γ0,f⟩ , _0,f simply by its transition function f. To relate strategies to executions of a GR(1) game, we next define when an infinite play is consistent with the choices prescribed by a strategy. Definition 3.14 (Play–Strategy Compliance (Bloem et al., 2012)). Let ⟨,,θe,θs,ρe,ρs,Win⟩ ,Y,θ^e,θ^s,ρ^e,ρ^s,Win be a GR(1) game, and let w=σ0σ1σ2⋯∈(2)ωw= _0 _1 _2…∈(2^V)^ω be an infinite play. • The play w is said to be compliant with an environment strategy ⟨Γe,γ0e,fe⟩ ^e, _0^e,f^e with fe:Γe×2⇀Γe×2,f^e: ^e× 2^V ^e× 2^X, iff there exists a sequence of memory states γ0e,γ1e,γ2e,… _0^e, _1^e, _2^e,… such that, for every i≥0i≥ 0, fe(γie,σi)=(γi+1e,σi+1|).f^e( _i^e, _i)=( _i+1^e, _i+1|_X). • Similarly, the play w is said to be compliant with a system strategy ⟨Γs,γ0s,fs⟩ ^s, _0^s,f^s with fs:Γs×2×2⇀Γs×2,f^s: ^s× 2^V× 2^X ^s× 2^Y, iff there exists a sequence of memory states γ0s,γ1s,γ2s,… _0^s, _1^s, _2^s,… such that, for every i≥0i≥ 0, fs(γis,σi,σi+1|)=(γi+1s,σi+1|).f^s( _i^s, _i, _i+1|_X)=( _i+1^s, _i+1|_Y). In the GR(1) setting, the environment and the system induce distinct classes of strategies corresponding to their respective roles in the game. Definition 3.15 (Environment and System Strategies). Let ⟨,,θe,θs,ρe,ρs,Win⟩ ,Y,θ^e,θ^s,ρ^e,ρ^s,Win be a GR(1) game. An environment strategy is a finite-state strategy whose transition function is of the form fe:Γe×2⇀Γe×2,f^e: ^e× 2^V ^e× 2^X, where the strategy selects the next valuation of the environment variables. A system strategy is a finite-state strategy whose transition function is of the form fs:Γs×2×2⇀Γs×2,f^s: ^s× 2^V× 2^X ^s× 2^Y, where the strategy selects the next valuation of the system variables after observing the next environment move. The asymmetry between the two definitions reflects the reactive nature of the game: the environment acts first at each step, while the system responds by choosing a compatible system action. The objective of reactive synthesis is to construct a system strategy that guarantees satisfaction of the specification against all admissible behaviours of the environment. Such strategies are referred to as winning strategies. Definition 3.16 (Winning Strategy). Let ⟨ℰ,⟩ ,S be a GR(1) specification. A system strategy fsf^s is said to be winning iff every play compliant with fsf^s satisfies the specification ⟨ℰ,⟩ ,S . A GR(1) specification is said to be realisable iff there exists a winning strategy for the system. Equivalently, the corresponding GR(1) game is said to be winning for the system. When a GR(1) specification is unrealisable, the environment can enforce a violation of the specification regardless of the behaviour of the system. The corresponding environment strategy is referred to as a counter-strategy. Definition 3.17 (Counter-Strategy). Let ⟨ℰ,⟩ ,S be a GR(1) specification. If the specification is unrealisable, then the corresponding GR(1) game is said to be winning for the environment. An environment strategy c is called a counter-strategy iff, for every system strategy fsf^s, every play w compliant with both c and fsf^s violates the specification. Equivalently, every such play satisfies at least one of the following conditions: • The environment satisfies its initial condition, but the system violates its initial condition: w[0]⊧θew[0] θ^e and w[0]⊧̸θs.w[0] θ^s. • The environment satisfies its transition relation at every step, but the system violates its transition relation at some step: ∀i≥0.(w[i],w[i+1])⊧ρe∀ i≥ 0.\;(w[i],w[i+1]) ρ^e and ∃i≥0.(w[i],w[i+1])⊧̸ρs.∃ i≥ 0.\;(w[i],w[i+1]) ρ^s. • The environment satisfies all of its liveness assumptions infinitely often, but the system fails to satisfy at least one of its liveness guarantees infinitely often: ∀i∈1,…,m.w⊧Jie∀ i∈\1,…,m\.\;w _i^e and ∃j∈1,…,n.w⊧̸Jjs.∃ j∈\1,…,n\.\;w _j^s. Counter-strategies characterise sets of environment behaviours that force the system to violate the specification. Individual executions induced by such strategies are referred to as counter-plays. Definition 3.18 (Counter-Play). Let c be a counter-strategy for an unrealisable GR(1) specification ⟨ℰ,⟩ ,S . A counter-play of c is an infinite play that is compliant with the counter-strategy c. 4. Adaptation under Assumption Violations In this section, we formally define the adaptation problem considered throughout the paper. Section 4.1 introduces the problem setting in which behaviours observed during deployment violate the assumptions of the original specification, requiring the synthesis of an adapted realisable specification that incorporates the newly observed environment behaviour while preserving as much of the original specification intent as possible. Section 4.2 then investigates the problem of comparing alternative adaptations. In particular, we identify desirable properties of adaptation solutions, analyse trade-offs between competing objectives, and derive a set of axiomatic criteria characterising preferred adaptations. We additionally discuss circumstances under which different solutions cannot be meaningfully ordered without additional contextual information or design priorities. Finally, Section 4.3 presents a baseline adaptation procedure based on specification-reduction operations. We formally prove that the proposed algorithm always produces valid solutions to the adaptation problem and satisfies the optimality criteria established earlier in the section. 4.1. Problem Definition Reactive synthesis under assumption violations has previously been studied through approaches based on specification degradation and repair (Buckworth et al., 2023). In this setting, the deployed system encounters behaviours of the environment that are not captured by the assumptions of the original specification, causing the theoretical guarantees of the synthesised controller to no longer apply. The objective of adaptation is therefore to recover a realisable specification that accounts for the newly observed behaviour while preserving as much of the original system intent as possible. We model such unexpected observations using the notion of a violation trace. Definition 4.1 (Violation Trace). Let A be a set of environment assumptions over a set of environment variables X. A finite trace τ∈(2)∗τ∈(2^X)^* is called a violation trace iff τ⊧̸.τ . When a violation trace is obtained from the execution of a deployed system, we may also refer to it as an observed behaviour or newly observed behaviour. Given a violation trace, the goal of adaptation is to revise the original specification so that the newly observed behaviour becomes admissible while maintaining as much of the original specification structure and system behaviour as possible. This leads to the following problem definition. Definition 4.2 (Adaptation Problem). Let φ=⟨,⟩ = ,G be a realisable specification, and let τ∈(2)∗τ∈(2^X)^* be a violation trace such that τ⊧̸.τ . An adaptation of the tuple (φ,τ)( ,τ) is a specification φ′=⟨′,′⟩ = ,G such that: (1) τ⊧′τ ; (2) ≺′A ; (3) ⪯′G ; (4) φ′ is realisable. We denote by AllSolutions(φ,τ)AllSolutions( ,τ) the set of all specifications satisfying the conditions above. If φ′∈AllSolutions(φ,τ), ∈ AllSolutions( ,τ), we say that φ′ is a solution to the adaptation problem induced by (φ,τ)( ,τ). Intuitively, Property 1 ensures that the newly observed behaviour is incorporated into the adapted environment model. Property 2 requires the adapted assumptions to be weaker than the original assumptions, thereby preserving all previously admissible environment behaviours while additionally admitting the observed violation trace. Property 3 requires the adapted guarantees to preserve as much of the original system behaviour as possible by ensuring that all previously guaranteed behaviours remain permitted by the adapted specification. Finally, Property 4 ensures that the resulting specification remains realisable and therefore admits a correct-by-construction implementation. A trivial solution to the adaptation problem is obtained by replacing both the assumptions and guarantees with ⊤ , thereby allowing all environment and system behaviours. Although such a specification satisfies the formal conditions above, it discards all meaningful behavioural guarantees and is therefore uninformative in practice. Consequently, the central challenge of adaptation lies not merely in recovering realisability, but in identifying preferred solutions that preserve as much of the original specification intent as possible. 4.2. Preference over Comparable Adaptations The adaptation problem introduced in Section 4.1 admits, in general, multiple valid solutions. Consequently, realisability alone is insufficient for determining which adapted specification should be preferred in practice. In this subsection, we investigate how alternative adaptations may be compared and ordered according to desirable behavioural properties. Our objective is to derive principled criteria for selecting preferred adaptations while preserving as much of the original specification intent as possible. To this end, we first analyse pairwise comparisons between candidate solutions and study how differences in assumptions and guarantees influence adaptation quality. Building upon this analysis, we derive a collection of preference axioms that induce a partial order over the space of valid adaptations. We refer to the ordering induced between two adaptation solutions as preference, formalised below. Definition 4.3 (Specification Preference). Let (φ,τ)( ,τ) be an adaptation problem, and let φ1,φ2∈AllSolutions(φ,τ) _1, _2∈ AllSolutions( ,τ) be two valid adaptation solutions. We use the following notation: • φ1⊏φ2 _1 _2 to denote that φ1 _1 is preferred to φ2 _2; • φ1⊐φ2 _1 _2 to denote that φ2 _2 is preferred to φ1 _1. The preference criteria developed in this subsection induce a partial order over the space of adaptation solutions, allowing the extraction of preferred solutions from a candidate solution set. 4.2.1. Reasoning about comparable specifications Consider an adaptation problem (φ,τ)( ,τ) together with two semantically distinct adaptation solutions φ1′=⟨1′,1′⟩ _1 = _1 ,G_1 and φ2′=⟨2′,2′⟩. _2 = _2 ,G_2 . To compare alternative adaptations, we use the logical weakness relation introduced in Definition 3.5. We begin by considering the following representative cases involving logically comparable assumptions and guarantees (incomparable cases are considered in Section 4.2.2): (1) 1′≡2′A_1 _2 and 1′≺2′G_1 _2 ; (2) 1′≺2′A_1 _2 and 1′≡2′G_1 _2 ; (3) 1′≺2′A_1 _2 and 1′≺2′G_1 _2 ; (4) 1′≻2′A_1 _2 and 1′≺2′G_1 _2 . When two adaptation solutions differ only in their guarantees, existing work on specification repair and degradation favours the stronger guarantee (Cavezza and Alrajeh, 2017; Maoz et al., 2019; Buckworth et al., 2023). This preference follows naturally from the fact that ≺1′≺2′.G _1 _2 . Consequently, φ1′ _1 preserves more of the original system behaviour encoded in G and introduces fewer additional behaviours beyond those intended by the original specification. Since stronger guarantees correspond to smaller deviations from the original specification intent, we adopt the following preference axiom. Axiom 4.4. Let (φ,τ)( ,τ) be an adaptation problem, and let φ1′=⟨1′,1′⟩ _1 = _1 ,G_1 and φ2′=⟨2′,2′⟩ _2 = _2 ,G_2 be two adaptation solutions. If the assumptions are equivalent and the guarantees of φ1′ _1 are stronger than those of φ2′ _2 , i.e., 1′≡2′A_1 _2 and 1′≺2′,G_1 _2 , then φ1′ _1 is preferred to φ2′ _2 . Existing work on assumption refinement typically favours the weakest assumptions capable of preserving a fixed set of guarantees (Cavezza and Alrajeh, 2017; Gaaloul et al., 2020; Shalom and Maoz, 2023; Maoz et al., 2019). Under this interpretation, the preferred adaptation would, therefore, be the one with the weakest assumption set. However, the preference criteria used in classical assumption refinement do not directly transfer to the adaptation setting considered in this work. Assumption refinement typically seeks to maximise the set of admissible environment behaviours while preserving a fixed set of guarantees. In contrast, our setting begins from an already deployed specification whose assumptions have been violated by newly observed behaviour. The objective is therefore not unrestricted weakening of the environment model, but rather controlled adaptation that incorporates the observed behaviour while preserving as much of the original specification intent as possible. To illustrate the implications of this distinction, consider extending the comparison setting from two adaptation solutions to three solutions. Let φ1′=⟨1′,1′⟩, _1 = _1 ,G_1 , φ2′=⟨2′,2′⟩, _2 = _2 ,G_2 , and φ3′=⟨3′,3′⟩ _3 = _3 ,G_3 be three adaptation solutions satisfying the following properties: (1) 2′≻1′A_2 _1 and 3′≻1′A_3 _1 ; (2) 3′A_3 and 2′A_2 are incomparable under the weakness relation; (3) 3′≡1′≡2′≡G_3 _1 _2 . The implication relations between the assumptions are visualised in Figure 1. Consider a deployed reactive system whose controller has been synthesised from a specification φ=⟨,⟩. = ,G . Suppose that, during execution, the system observes a trace τ such that τ⊧̸,τ , i.e., the observed behaviour violates the assumptions of the original specification. In this setting, two important sources of uncertainty arise: • the true dynamics of the environment are generally unknown and may not be fully characterisable; • the observed violation trace τ does not necessarily characterise the complete set of environment behaviours excluded by A. Existing work on specification learning and repair typically seeks to identify the weakest set of assumptions under which a fixed set of guarantees remains realisable. The underlying objective is to maximise the robustness of the synthesised system by enlarging the set of admissible environment behaviours while preserving the intended guarantees. Intuitively, if the same guarantees can be enforced under weaker assumptions, then the resulting specification is considered more robust, since the system can operate correctly under a broader range of environmental conditions. While this perspective is well-motivated, it becomes less clear in the adaptation setting considered here. In particular, temporal logic specifications characterise infinite sets of behaviours, and logical weakness induces only a partial order over these sets. Consequently, multiple incomparable assumption sets may exist that are each minimal or maximally permissive with respect to a given guarantee set. In such cases, selecting between incomparable weakenings based solely on permissiveness may admit behaviours unsupported by the observed violation trace. We refer to this phenomenon as overgeneralisation. A1′A_1 2′A_2 3′A_3 ′A G′G unrealisable Figure 1. Illustration of successive specification weakenings during adaptation. A and G denote the original assumption and guarantee sets, respectively. The sets 1′A_1 , 2′A_2 , 3′A_3 , and ′A represent weakened assumption sets derived from A, while ′G denotes a weakened guarantee set derived from G. Directed edges represent the strict weakness relation ≺ . Nodes with no directed path between them are incomparable under the weakness relation. To illustrate the risks of overgeneralisation in the adaptation setting, we return to Figure 1. Suppose the adaptation problem (φ,τ)( ,τ) admits multiple solutions requiring only assumption weakening to recover realisability. Formally, AllSolutions(φ,τ)⊇φ1′,φ2′,φ3′,AllSolutions( ,τ) \ _1 , _2 , _3 \, where φ1′=⟨1′,⟩, _1 = _1 ,G , φ2′=⟨2′,⟩, _2 = _2 ,G , and φ3′=⟨3′,⟩. _3 = _3 ,G . The logical relationships between the assumption sets 1′A_1 , 2′A_2 , and 3′A_3 are illustrated in Figure 1. Suppose that, guided solely by the preference for weaker assumptions under equivalent guarantees, the adaptation process selects φ3′ _3 (the same argument applies symmetrically to φ2′ _2 ). Consider now the later observation of a second violation trace τ2 _2 such that τ2⊧2′ _2 _2 but τ2⊧̸3′. _2 _3 . In this setting, the previously selected adaptation φ3′ _3 no longer accommodates the newly observed behaviour. Consequently, the adaptation process must further weaken the assumptions to some set ′≻3′A _3 such that τ2⊧′. _2 . Since 2′A_2 already admits τ2 _2, it follows that the new assumption set must additionally satisfy ′≻2′.A _2 . The difficulty is that the resulting specification ⟨′,⟩ ,G may no longer remain realisable. Recovering realisability may therefore require an additional weakening of the guarantees to some ′≻,G , yielding a realisable specification φ′=⟨′,′⟩. = ,G . Intuitively, this sequence of adaptations illustrates the risk of prematurely selecting overly permissive assumptions based on limited observations. Although φ3′ _3 initially appeared preferable under a weakest-assumption criterion, it may ultimately force stronger degradation of guarantees during subsequent adaptations. In contrast, the alternative solution φ2′=⟨2′,⟩ _2 = _2 ,G would already accommodate the second violation trace without requiring any degradation of the guarantees. Consequently, adaptation procedures that prioritise aggressively weak assumptions based on limited observations are susceptible to overgeneralisation, potentially leading to poorer long-term preservation of system behaviour. Two alternative adaptation strategies are worth discussing. First, one could attempt to refine assumptions after additional violations are observed, rather than continuing assumption weakening. Existing approaches to specification refinement achieve this either through reasoning over the current guarantee set (Cavezza and Alrajeh, 2017; Gaaloul et al., 2020) or through the incorporation of additional behavioural data (Keegan et al., 2020). However, the former risks overfitting assumptions to the current guarantees, while the latter may require substantially more observational data than is realistically available during deployment. Second, in the setting of Figure 1, one may consider the disjunctive assumption set 2′∨3′A_2 _3 together with the original guarantees G. Although such a construction may preserve realisability in some cases, the resulting specification does not, in general, remain within the GR(1) fragment. A counterexample is provided in Appendix A.1. These observations further motivate a conservative adaptation strategy based on gradual weakening of assumptions while preserving stronger guarantees whenever possible. We therefore obtain the following preference axiom. Axiom 4.5. Let (φ,τ)( ,τ) be an adaptation problem, and let φ1′=⟨1′,1′⟩ _1 = _1 ,G_1 and φ2′=⟨2′,2′⟩ _2 = _2 ,G_2 be two adaptation solutions. If the guarantees are equivalent and the assumptions of φ1′ _1 are stronger than those of φ2′ _2 , i.e., 1′≡2′G_1 _2 and 1′≺2′,A_1 _2 , then φ1′ _1 is preferred to φ2′ _2 . Formally, (1′≺2′)∧(1′≡2′)⇒φ1′⊏φ2′.(A_1 _2 ) (G_1 _2 ) _1 _2 . Axioms 4.4 and 4.5 immediately yield the following combined preference criterion. Axiom 4.6. Let (φ,τ)( ,τ) be an adaptation problem, and let φ1′=⟨1′,1′⟩ _1 = _1 ,G_1 and φ2′=⟨2′,2′⟩ _2 = _2 ,G_2 be two adaptation solutions. If both the assumptions and guarantees of φ1′ _1 are stronger than those of φ2′ _2 , i.e., 1′≺2′A_1 _2 and 1′≺2′,G_1 _2 , then φ1′ _1 is preferred to φ2′ _2 . Formally, (1′≺2′)∧(1′≺2′)⇒φ1′⊏φ2′.(A_1 _2 ) (G_1 _2 ) _1 _2 . Finally, the remaining comparison case can be reduced to the previous preference criteria through the following lemma. Lemma 4.7. Let (φ,τ)( ,τ) be an adaptation problem. Suppose φ1′=⟨1′,1′⟩ _1 = _1 ,G_1 and φ2′=⟨2′,2′⟩ _2 = _2 ,G_2 are adaptation solutions satisfying 1′≻2′A_1 _2 and 1′≺2′.G_1 _2 . Then φ3′=⟨2′,1′⟩ _3 = _2 ,G_1 is also a valid adaptation solution. Proof. Since φ2′ _2 is a valid adaptation solution, τ⊧2′τ _2 and ≺2′.A _2 . Moreover, since 2′≺1′A_2 _1 and φ1′ _1 is realisable, monotonicity of realisability under strengthening of assumptions implies that ⟨2′,1′⟩ _2 ,G_1 is also realisable. Finally, because φ1′ _1 is a valid adaptation solution, ⪯1′.G _1 . Therefore, φ3′=⟨2′,1′⟩ _3 = _2 ,G_1 satisfies all conditions of the adaptation problem and is consequently a valid adaptation solution. ∎ Lemma 4.7 reduces the remaining comparison case to Axiom 4.4, since φ3′ _3 and φ2′ _2 differ only in their guarantees. 4.2.2. Reasoning about Incomparable Adaptations Logical weakness induces only a partial order over specifications. Consequently, not all adaptation solutions can be compared directly using implication-based preference criteria. In particular, distinct adaptations may permit different, non-overlapping classes of behaviours while remaining equally valid solutions to the adaptation problem. In such cases, preference cannot generally be established without introducing additional domain knowledge, engineering priorities, or external optimisation criteria. We therefore analyse the following representative cases involving incomparable assumptions and guarantees. Let φ1=⟨1,1⟩ _1= _1,G_1 and φ2=⟨2,2⟩ _2= _2,G_2 be two solutions to the adaptation problem (φ,τ)( ,τ). We consider the following cases: (1) 1A_1 and 2A_2 are incomparable, and 1≡2G_1 _2; (2) 1A_1 and 2A_2 are incomparable, and 1≺2G_1 _2; (3) 1≡2A_1 _2, and 1G_1 and 2G_2 are incomparable; (4) 1≺2A_1 _2, and 1G_1 and 2G_2 are incomparable; (5) 1A_1 and 2A_2 are incomparable, and 1G_1 and 2G_2 are incomparable. Reasoning about incomparable adaptations may require considering additional candidate solutions beyond the original pair under comparison. This is already evident in the first case above, where the existence of a third adaptation directly influences the preference ordering. To analyse Case 1, recall that solutions to the adaptation problem satisfy ≺1A _1 and ≺2A _2. Since logical weakness corresponds to language inclusion, it follows that ⪯(1∪2)A (A_1 _2), where the union operator denotes conjunction over the combined assumption sets. Furthermore, because τ⊧1τ _1 and τ⊧2τ _2, the violation trace τ also satisfies the combined assumption set 1∪2A_1 _2. Since τ⊧̸τ , we obtain ≺(1∪2)A (A_1 _2). Consequently, the specification φ′=⟨1∪2,⟩ = _1 _2,G may itself constitute a valid adaptation solution. If realisable, Axiom 4.5 implies that φ′ is preferred to both φ1 _1 and φ2 _2, since it preserves strictly stronger assumptions while maintaining the same guarantees. This observation yields the following lemma. Lemma 4.8. Let (φ,τ)( ,τ) be an adaptation problem. Suppose φ1′=⟨1′,′⟩ _1 = _1 ,G and φ2′=⟨2′,′⟩ _2 = _2 ,G are specification adaptations whose assumption sets are incomparable under the weakness relation. Then φ3′=⟨1′∪2′,′⟩ _3 = _1 _2 ,G is also a valid specification adaptation. Lemma 4.8 shows that the first incomparable case reduces to the comparable setting addressed by Axiom 4.4. In particular, the construction of the specification adaptation φ3′ _3 yields a specification with strictly stronger assumptions while preserving the same guarantees. The second incomparable case admits a similar analysis. Lemma 4.9. Let (φ,τ)( ,τ) be an adaptation problem. Suppose φ1′=⟨1′,1′⟩ _1 = _1 ,G_1 and φ2′=⟨2′,2′⟩ _2 = _2 ,G_2 are specification adaptations such that the assumption sets 1′A_1 and 2′A_2 are incomparable under the weakness relation, and 1′≺2′G_1 _2 . Then φ3′=⟨1′∪2′,1′⟩ _3 = _1 _2 ,G_1 is also a valid specification adaptation. Lemma 4.9 combines the constructions of Lemmas 4.7 and 4.8. Consequently, the second incomparable case also reduces to the comparable setting addressed by Axiom 4.4. In particular, the construction of φ3′ _3 yields a specification adaptation with strictly stronger assumptions than both φ1′ _1 and φ2′ _2 , while preserving the stronger guarantee set 1′G_1 . Finally, we argue that the remaining cases involving incomparable guarantee sets cannot, in general, be resolved through logical weakness alone. Distinguishing between such specification adaptations requires extending the problem setting with additional information, such as behavioural preferences, domain-specific priorities, or constraints identifying undesirable behaviours. In the absence of such information, no principled basis exists for preferring one incomparable guarantee set over another, and both adaptations must therefore be retained as valid candidate solutions. This observation motivates the following final axiom. Axiom 4.10. Let (φ,τ)( ,τ) be an adaptation problem, and let φ1′=⟨1′,1′⟩ _1 = _1 ,G_1 and φ2′=⟨2′,2′⟩ _2 = _2 ,G_2 be two specification adaptations. If the guarantee sets 1′G_1 and 2′G_2 are incomparable under the weakness relation, then neither solution is preferred to the other. Formally, 1′ and 2′ incomparable⇒(φ1′⊏̸φ2′)∧(φ1′⋣φ2′).G_1 and G_2 incomparable ( _1 _2 ) ( _1 _2 ). Example 4.11. Consider the following two solutions for an adaptation problem: φ1′=⟨′,1′⟩ _1 = ,G_1 and φ2′=⟨′,2′⟩ _2 = ,G_2 , where ′=∅A = , 1′=□(a→○c)G_1 =\ (a→ c)\, and 2′=□(b→○¬c)G_2 =\ (b→ c)\. Suppose these adaptations originate from the adaptation problem generated by the specification φ=⟨,⟩ = ,G , where the violation trace is τ=[(a,b,c)]τ=[(a,b,c)], the assumptions are =□(¬a∨¬b)A=\ ( a b)\, and the original guarantees satisfy =1′∪2′G=G_1 _2 . Assume further that a and b are environment variables, while c is a system variable. At the purely symbolic level, there is insufficient information to determine whether φ1′ _1 or φ2′ _2 should be preferred. Both adaptations preserve different subsets of the original guarantees, and neither dominates the other under the logical preference criteria introduced previously. Now consider the following semantic interpretation: a=highwatera=highwater, b=methaneb=methane, and c=pumpc=pump. This corresponds to the Minepump specification introduced in Section 2, where highwater indicates dangerous water levels, methane indicates the presence of explosive gas, and pump denotes activation of the mine pump. Under this interpretation, a clear preference emerges. Specifically, φ2′ _2 becomes preferable because it preserves the safety property preventing pump activation during methane leaks, thereby avoiding a potentially catastrophic explosion. Crucially, however, this preference depends entirely on semantic knowledge external to the formal specification itself. An adaptation algorithm operating purely at the logical level has no access to such contextual information and therefore cannot soundly discard either solution. Consequently, both candidate adaptations should be preserved for subsequent analysis by a domain-aware stakeholder. We conclude that Axioms 4.4–4.10 collectively induce a preference ordering over specification adaptations. We summarise these criteria in the following definition. Definition 4.12 (Preference between Specification Adaptations). Let (φ,τ)( ,τ) be an adaptation problem, and let φ1=⟨1,1⟩ _1= _1,G_1 and φ2=⟨2,2⟩ _2= _2,G_2 be two semantically distinct specification adaptations in AllSolutions((φ,τ))AllSolutions(( ,τ)). We say that φ1 _1 is preferred to φ2 _2, denoted φ1⊏φ2 _1 _2, iff one of the following conditions holds: • (1≡2)∧(1≺2)(A_1 _2) (G_1 _2); • (1≺2)∧(1≡2)(A_1 _2) (G_1 _2); • (1≺2)∧(1≺2)(A_1 _2) (G_1 _2). Under all other circumstances, φ1 _1 and φ2 _2 are considered incomparable with respect to preference. 4.2.3. Extracting Preferred Specifications An adaptation procedure may discover multiple candidate specification adaptations for a given adaptation problem (φ,τ)( ,τ). Let Φ⊆AllSolutions((φ,τ)) AllSolutions(( ,τ)) denote the set of adaptations generated by such a procedure. Using the preference relation from Definition 4.12, the corresponding preference structure can be represented as the partially ordered set (Φ,⊏).( , ). Preferred adaptations can then be obtained by extracting the minimal elements of this partial order, corresponding to adaptations for which no strictly preferred alternative exists within Φ . However, Lemmas 4.7, 4.8, and 4.9 reveal an important limitation of this approach: the set Φ may not yet contain all relevant preferred adaptations. In particular, the previous lemmas show that combining assumptions from multiple solutions can yield new solutions that are strictly preferred according to the preference relation. This observation leads to the following theorem. Theorem 4.13 (Most Preferred Assumption). Let Φ⊆AllSolutions((φ,τ)) AllSolutions(( ,τ)) be a set of specification adaptations for an adaptation problem (φ,τ)( ,τ), where each solution φi′=⟨i′,i′⟩ _i = _i ,G_i belongs to Φ . Define ∗=⋃i∈|Φ|i′A^*= _i∈| |A_i to be the union of all assumption sets appearing in Φ . We call ∗A^* the most preferred assumption. Then the following properties hold: (1) ∗A^* is stronger than or equivalent to every assumption set appearing in Φ . Formally, ∀i∈|Φ|.∗⪯i′∀ i∈| |.\;A^* _i ; (2) For every adaptation in Φ , replacing its assumption set with ∗A^* yields another valid specification adaptation. Formally, ∀i∈|Φ|.⟨∗,i′⟩∈AllSolutions((φ,τ))∀ i∈| |.\; ^*,G_i ∈ AllSolutions(( ,τ)); (3) For every adaptation in Φ , the specification obtained using ∗A^* is preferred to or equivalent to the original adaptation. Formally, ∀i∈|Φ|.⟨∗,i′⟩⊑φi′∀ i∈| |.\; ^*,G_i _i . This theorem allows every adaptation in Φ to be rewritten using the most preferred assumption ∗A^*, yielding a new set of solutions Φ′⊆AllSolutions((φ,τ)) AllSolutions(( ,τ)). Consequently, preference reasoning can be reduced to comparisons between guarantee sets alone, for which Axioms 4.4 and 4.10 are sufficient to identify the preferred adaptations. Algorithm 1 Filter Preferred Specifications 1: function filterPreferred(specsspecs) 2: asms←[]asms←[] 3: gars←[]gars←[] 4: for spec∈specsspec∈ specs do 5: add(asms,spec.) add(asms,spec.A) 6: add(gars,spec.) add(gars,spec.G) 7: end for 8: minAsms←findMinimal(asms)minAsms← findMinimal(asms) 9: minGars←findMinimal(gars)minGars← findMinimal(gars) 10: ∗←setUnion(minAsms)A^*← setUnion(minAsms) 11: filteredSpecs←[]filteredSpecs←[] 12: for ′∈minGarsG ∈ minGars do 13: add(filteredSpecs,⟨∗,′⟩) add(filteredSpecs, ^*,G ) 14: end for 15: return filteredSpecsfilteredSpecs 16: end function We therefore propose Algorithm 1 for extracting the preferred specification adaptations from a candidate set Φ . Lines 2–7 separate the assumption and guarantee sets of each solution into the collections asms and gars, respectively. The minimal elements of these collections are then extracted in Lines 8 and 9 using the findMinimal procedure. In Line 10, the most preferred assumption ∗A^* is constructed through the union of the minimal assumption sets contained in minAsmsminAsms. Subsequently, Lines 11–14 generate the preferred specification adaptations by combining ∗A^* with each minimal guarantee set in minGarsminGars, yielding solutions of the form ⟨∗,′⟩ ^*,G . Each generated solution is added to the set filteredSpecsfilteredSpecs, which is returned in Line 15. The procedure setUnion corresponds to the standard set-union operator ⋃ , while findMinimal() findMinimal(), defined in Algorithm 5, returns the minimal elements of the partial order (formulas,≺)(formulas, ). Additional implementation details and pseudocode are provided in Appendix B.1. 4.3. Baseline Adaptation Procedure The previous section established the preference criteria governing specification degradations for adaptation problems. Intuitively, preferred adaptations preserve assumptions and guarantees as strongly as possible while still incorporating the observed violation behaviour and maintaining realisability. To construct specification adaptations satisfying the requirements, we consider a baseline procedure based on removal of formulas responsible for the observed violation or for subsequent unrealisability. The approach is inspired by techniques for computing minimal unsatisfiable subsets of constraints (Liffiton and Sakallah, 2008), and by related work on synthesis under unrealizability (Yang et al., 2024). If removing the assumptions violated by the observed trace immediately yields a realisable specification, then adaptation is straightforward. We therefore focus on the more interesting setting in which the original assumptions are already minimally sufficient with respect to the guarantees (i.e. any assumption removed would make the specification unrealisable). Such assumption sets may, for example, be obtained using techniques such as those proposed in (Shalom and Maoz, 2023). Under this assumption, removing any violated assumption necessarily produces an unrealisable specification, requiring subsequent degradation of the guarantees to restore realisability. The first step in adapting a specification is to identify the assumptions violated by the observed trace. These assumptions must be removed or weakened in order for the adapted specification to admit the newly observed behaviour. Definition 4.14 (Violation Set). Given a set of assumptions A and a violation trace τ, the violation set Aτ⊆A_τ is the subset of assumptions violated by τ. Formally, Aτ=a∈∣τ⊧̸a.A_τ=\a τ a\. After removing the violation set from the assumptions, the resulting specification becomes ⟨∖Aτ,⟩ A_τ,G . Since the original assumptions are assumed to be minimally sufficient, this specification is necessarily unrealisable. Consequently, restoring realisability requires degrading the guarantee set. Following the intuition of (Yang et al., 2024), we seek adaptations that remove as few guarantees as possible. To identify such adaptations, we first characterise the minimally unfulfillable subsets of guarantees, commonly referred to as unrealisable cores. Definition 4.15 (Unrealisable Core). Let φ=⟨,⟩ = ,G be an unrealisable specification. A set of guarantees uc⊆G^uc is an unrealisable core iff: (1) the specification ⟨,uc⟩ ,G^uc is unrealisable; and (2) removing any guarantee from ucG^uc restores realisability. Formally, ∀gi∈uc.⟨,uc∖gi⟩ is realisable.∀ g_i ^uc.\; ,G^uc \g_i\ is realisable. To minimise the number of guarantees removed during degradation, we require the notion of a minimal hitting set over the unrealisable cores. Definition 4.16 (Hitting Set (Liffiton and Sakallah, 2008)). Given a collection of sets F=S1,S2,…,SnF=\S_1,S_2,…,S_n\, a set ℋ(F)H(F) is called a hitting set of F iff ∀Si∈F.ℋ(F)∩Si≠∅∀ S_i∈ F.\;H(F)∩ S_i≠ . That is, ℋ(F)H(F) contains at least one element from every set in F. A hitting set ℋmin(F)H_min(F) is called minimal iff no strict subset H⊂ℋmin(F)H _min(F) is itself a hitting set. In our setting, we compute the set of unrealisable cores =1uc,2uc,…,kuc⊆()C=\G^uc_1,G^uc_2,…,G^uc_k\ (G) using the Punch algorithm 11 1 Experimental results show the implementation of the Punch algorithm may return non-minimal sets of guarantees as unrealisable cores. We contacted the SYNTECH team with respect to this matter, and will treat their implementation as sound for the rest of the paper. proposed in (Maoz and Shalom, 2021). From this collection, we compute a minimal hitting set and remove it from the guarantee set, yielding the degraded guarantees ′=∖ℋmin()G =G _min(C). The resulting specification ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) is then realisable. Definition 4.17 (Optimal Trivial Degradation). Given the adaptation problem (⟨,⟩,τ)( ,G ,τ), an optimal trivial degradation is the specification ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) , where: • Aτ⊆A_τ is the violation set induced by τ; • =1uc,2uc,…,kuc⊆()C=\G^uc_1,G^uc_2,…,G^uc_k\ (G) is the set of unrealisable cores of the specification ⟨∖Aτ,⟩ A_τ,G ; • ℋmin()H_min(C) is a minimal hitting set of C. Note that multiple minimal hitting sets may exist for a given collection of unrealisable cores. Consequently, the adaptation problem may admit multiple optimal trivial solutions. Algorithm 2 Trivial Degradation 1: ⟨,⟩ ,G (realisable GR(1) specification), τ (violation trace) 2: trivialSolutions, set of optimal trivial degradations 3: function trivialDegradation(⟨,⟩,τ ,G ,τ) 4: Aτ←∅A_τ← 5: for asm∈asm do 6: if τ⊧̸asmτ then 7: Aτ←Aτ∪asmA_τ← A_τ∪\asm\ 8: end if 9: end for 10: ′←∖AτA A_τ 11: if isRealisable(⟨′,⟩) isRealisable( ,G ) then 12: return [⟨′,⟩][ ,G ] 13: else 14: return trivialGD(⟨′,⟩) trivialGD( ,G ) 15: end if 16: end function Algorithm 3 Trivial Guarantee Degradation 1: ⟨,⟩ ,G (unrealisable GR(1) specification) 2: trivialSolutions, set of optimal trivial degradations 3: function trivialGD(⟨,⟩ ,G ) 4: trivialSolutions←[]trivialSolutions←[\ ] 5: ucsSet←getUnrealisableCores(⟨,⟩)ucsSet← getUnrealisableCores( ,G ) 6: minCorrectionSets←getMinimalHittingSets(ucsSet)minCorrectionSets← getMinimalHittingSets(ucsSet) 7: for uc∈minCorrectionSetsG^uc do 8: ′←∖ucG ^uc 9: append(trivialSolutions,⟨,′⟩) append(trivialSolutions,\ ,G ) 10: end for 11: return trivialSolutions 12: end function Algorithm 2 implements the baseline adaptation procedure described above and computes all optimal trivial solutions. Lines 4–10 identify the assumptions violated by the trace and remove them from the original assumption set. At the end of the loop in Line 9, the set vAsmsvAsms corresponds to the violation set AτA_τ, and the assignment in Line 10 constructs the degraded assumption set ′=∖AτA =A A_τ. Lines 11–12 then check whether the resulting specification is realisable. If so, the unique optimal trivial solution is returned directly. Otherwise, Algorithm 3 is invoked in Line 14 to compute the set of optimal trivial adaptations obtained through guarantee degradation. Algorithm 3 assumes that the degraded assumption set no longer violates the observed trace, but that the resulting specification remains unrealisable. In line 5, an external procedure such as the Punch algorithm from the Spectra toolbox (Maoz and Ringert, 2021) is used to compute all unrealisable cores of the specification. Subsequently, line 6 computes the corresponding minimal correction sets through a minimal hitting-set procedure. Lines 7–10 then construct a realisable specification adaptation for each discovered correction set by removing the associated guarantees. The resulting set of optimal trivial solutions is returned in line 11. From the discussion above, together with the construction implemented in Algorithm 2, we obtain the following result. Theorem 4.18 (Soundness and Minimality of the Optimal Trivial Degradation). Let ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) be an optimal trivial solution to the adaptation problem (⟨,⟩,τ)( ,G ,τ) as defined in Definition 4.17. Then: (i) the violation trace τ satisfies the degraded assumptions, i.e. τ⊧∖Aτ A_τ; (i) the specification ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) is realisable; (i) the pair ⟨Aτ,ℋmin()⟩ A_τ,H_min(C) is minimal with respect to the number of assumptions and guarantees removed. Properties (i) and (i) are sufficient to show that the resulting specification is a valid solution for the adaptation problem, since the degraded assumptions and guarantees are trivially weaker than their original counterparts. We prove property (i) of Theorem 4.18 in Appendix A.2. 4.4. Case Study: Minepump We now illustrate the behaviour and limitations of the baseline adaptation procedure presented in Algorithm 2 using the Minepump case study (Kramer et al., 1983), a canonical benchmark in the reactive-systems and formal-methods literature. Although comparatively simple, the Minepump specification captures the core interaction between environmental assumptions, safety-critical guarantees, and unexpected runtime behaviours, making it well suited for studying adaptation under assumption violations. The Minepump system models a coal mine in which water may accumulate over time and must be removed using a pump. The pump constitutes the system to be synthesized; the environment is characterized by the water and methane sensor readings, highwater and methane. However, methane may also accumulate inside the mine, and activating the pump in the presence of methane introduces a risk of explosion. The controller must therefore balance competing safety requirements under changing environmental conditions. The corresponding GR(1) specification is shown in Table 2. Under the stated assumptions, the specification is realisable according to the standard GR(1) realisability criteria (Bloem et al., 2012), and a correct-by-construction controller can therefore be synthesized. Type & ID Informal requirement GR(1) formalization assumption_0 Start with low water and no methane ¬highwater∧¬methane assumption_1 There can never be both high levels of water and dangerous levels of methane □(¬highwater∨¬methane) ( ) assumption_2 If pump is turned on for two time steps, water levels lower □(Ypump∧pump→○¬highwater) (Ypump → ) guarantee_0 Start with pump off ¬pump guarantee_1 Whenever water exceeds threshold, turn pump on □(highwater→pump) (highwater ) guarantee_2 Whenever methane levels are dangerous, turn pump off □(methane→¬pump) (methane→ ) Table 2. GR(1) specification for the mine pump example Suppose now that, during deployment, the system observes a previously unmodelled behaviour in which both methane and dangerous water levels occur simultaneously. Such a trace violates assumption_1assumption\_1, which explicitly excludes this configuration. As a consequence, the correctness guarantees established for the synthesized controller no longer necessarily hold. More fundamentally, the observation motivates the problem of how the specification itself should be adapted in response to newly observed environmental behaviour. 4.4.1. Baseline Adaptation Applied Consider the specification φ=⟨,⟩ = ,G encoded in Table 2, where =¬highwater∧¬methane,□(¬highwater∨¬methane),□(pump∧pump→○¬highwater)A=\ , ( ), (Ypump → )\ and =¬pump,□(highwater→pump),□(methane→¬pump)G=\ , (highwater ), (methane→ )\. For readability, we abbreviate these formulas as =assumption_0,assumption_1,assumption_2A=\assumption\_0,assumption\_1,assumption\_2\ and =guarantee_0,guarantee_1,guarantee_2G=\guarantee\_0,guarantee\_1,guarantee\_2\. Assume the system observes the violation trace τ=[highwater,methane,pump]τ=[\highwater,methane,pump\], which violates assumption_1. Algorithm 2 therefore removes this assumption, producing the intermediate specification φ′=⟨′,⟩ = ,G , where ′=assumption_0,assumption_2A =\assumption\_0,assumption\_2\. The resulting specification is unrealisable. Computing the unrealisable cores yields two minimal correction sets: guarantee_1\guarantee\_1\ and guarantee_2\guarantee\_2\. Consequently, the baseline adaptation procedure produces two optimal trivial solutions: φ1=⟨′,guarantee_0,guarantee_1⟩ _1= ,\guarantee\_0,guarantee\_1\ and φ2=⟨′,guarantee_0,guarantee_2⟩ _2= ,\guarantee\_0,guarantee\_2\ . Neither solution is entirely satisfactory after synthesis: (1) φ1 _1 yields a controller that keeps the pump continuously active; (2) φ2 _2 yields a controller that keeps the pump permanently inactive. The issue is not merely practical, but structural. Since the baseline procedure operates solely through formula removal, it cannot recover behaviours that remain compatible with the newly observed environment dynamics. As a result, important behavioural structure encoded in the original specification is lost unnecessarily. Consider φ2 _2 as an example. The guarantee □(methane→¬pump) (methane→ ) must be preserved, since activating the pump in the presence of methane remains unsafe. At the same time, the original guarantee □(highwater→pump) (highwater ) can no longer be maintained universally, because the newly admitted environment behaviour allows both highwater and methane to hold simultaneously. However, the original intent of the guarantee can still be partially preserved by strengthening its antecedent, and therefore weakening the overall formula. In particular, the specification φ2′=⟨′,guarantee_0,guarantee_2,□(highwater∧¬methane→pump)⟩ _2 = ,\guarantee\_0,guarantee\_2, (highwater )\ remains realisable while preserving substantially more of the intended controller behaviour. An analogous weakening can similarly be applied to φ1 _1. These alternative adaptations preserve much more of the behavioural structure of the original specification while modifying behaviour only in the previously unmodelled edge case introduced by the violation trace. More generally, they illustrate an important limitation of purely removal-based adaptation procedures: optimal solutions may require weakening formulas rather than discarding them entirely. This observation motivates the richer adaptation methodology developed in Section 5, where we consider formula-level weakening as a mechanism for exploring a substantially broader space of specification adaptations. 5. Learning Degradations Section 4 introduced the adaptation problem, formally characterised the space of admissible adaptations, and established preference criteria for comparing alternative solutions. We additionally presented a baseline degradation procedure based on formula removal and showed that it produces sound minimal adaptations restoring realisability after assumption violations. The removal-based methodology, however, explores only a restricted portion of the degradation space. In many cases, stronger degradations can be avoided by weakening formulas rather than discarding them entirely, thereby preserving substantially more of the original specification behaviour. In this section, we therefore investigate finer-grained degradation procedures based on formula-level weakening. Section 5.1 introduces syntactic weakening operators for generating degraded formulas and presents a collection of degradation strategies. Section 5.2 then shows how formula-level degradation can be incorporated into a degradation procedure based on the OGIS framework. Finally, Section 5.3 presents an implementation capable of systematically exploring the resulting degradation space and generating multiple candidate specification adaptations. Proofs of correctness and termination are deferred to Appendix A. 5.1. Syntactic Formula Weakening The baseline adaptation procedure presented earlier operates exclusively through formula removal. While effective for restoring realisability, such an approach may discard substantially more behavioural structure than necessary. Prior work on specification weakening (Zhang, 2025; Buckworth et al., 2023) has, therefore, considered finer-grained transformations capable of generating weaker formulas through modifications to their syntactic structure. This process is commonly referred to as syntactic degradation. Definition 5.1 (Syntactic Degradation). Given a formula φ , the process of transforming its syntactic structure to obtain a weaker formula φ′ such that φ′≻φ is called syntactic formula weakening. To some extent, the baseline degradation procedure introduced in Section 4.3 already constitutes a form of syntactic formula weakening. Removing formulas from the assumption or guarantee sets is equivalent to deleting conjuncts from the strict realisability formula represented by the GR(1) specification in set form (cf. Definition 3.8). However, simple formula removal provides only a coarse-grained degradation mechanism. While conjunct deletion can also be applied within invariant and justice formulas, such transformations remain limited in the range of behavioural degradations they can express. Consequently, we instead focus on adaptation procedures based on weakening formulas through local syntactic modifications rather than removed entirely. We begin by focusing on the degradation of invariants. The corresponding treatment for justice goals is analogous, and we highlight the relevant differences where appropriate. To enable syntactic weakening, we represent invariants as implications between formulas in disjunctive normal form (DNF) under the scope of the globally operator: φinv=□(⋁i∈m⋀j∈niαij→⋁k∈p⋀l∈qkβkl) ^inv= ( _i∈ m _j∈ n_i _ij→ _k∈ p _l∈ q_k _kl ) where each α is a literal that may optionally be preceded by the previous operator Y, and each β is a literal that may optionally be preceded by the next operator X. This representation forms the basis of the syntactic augmentation procedures used for invariant degradation. For justice goals, the structure is similar. However, since GR(1) synthesis tools such as Spectra support response-style justice specifications (Maoz and Ringert, 2021; Maoz and Ringert, 2015; Dwyer et al., 1999), we additionally consider response formulas of the form: φres=□(⋁i∈m⋀j∈niαij→◊⋁k∈p⋀l∈qkβkl) ^res= ( _i∈ m _j∈ n_i _ij→ [rgb]1,0,0 _k∈ p _l∈ q_k _kl ) The only structural difference between φinv ^inv and φres ^res is the presence of the eventuality operator ◊ in the consequent of the response formula. 5.1.1. Types of Weakening Given a formula φ , we consider three classes of syntactic degradation: antecedent weakening, consequent weakening, and conversion to response or justice formulas. For each degradation operator introduced below, it follows directly from the rules of LTL entailment that the resulting formula is weaker than the original specification. Antecedent Weakening Consider an invariant of the form □(A→B) (A→ B). Such a formula becomes weaker whenever the antecedent A becomes stronger, since the implication is then required to hold in fewer situations. Because the antecedent is represented in disjunctive normal form (DNF), we preserve the syntactic structure of the formula by strengthening individual disjuncts through conjunction with additional literals. Intuitively, this restricts the set of behaviours under which the consequent must hold. We therefore define the following degradation operator. Definition 5.2 (Antecedent Weakening). Formula φ¯inv=AW(φinv,x,γ) ^inv=AW( ^inv,x,γ) is the antecedent weakening of φinv ^inv obtained by conjoining the unary temporal literal γ to the xxth disjunct of the antecedent of φinv ^inv, where x∈[1..m]x∈[1..m]. The resulting formula has the form: φ¯inv⩴□[(γ∧⋀j∈nxαxj)∨(⋁i∈m,i≠x⋀j∈niαij)→⋁k∈p⋀l∈qkβkl] ^inv [ [rgb]1,0,0(γ _j∈ n_x _xj) ( _i∈ m,i =x _j∈ n_i _ij )→ _k∈ p _l∈ q_k _kl ] This methodology extends naturally to response formulas. For justice goals, we observe that every justice formula of the form □◊φ can equivalently be rewritten as the response formula □(⊤→◊φ) ( → ). Antecedent weakening can then be applied by conjoining a unary temporal literal γ to the antecedent ⊤ introduced by this transformation. Consequent Weakening An alternative mechanism for weakening φinv ^inv is to relax its consequent. Intuitively, adding additional disjuncts to the consequent enlarges the set of behaviours satisfying the implication, thereby weakening the overall specification. We formalise this transformation below. Definition 5.3 (Consequent Weakening). Formula φ¯inv=CW(φinv,Γ) ^inv=CW( ^inv, ) is the consequent weakening of φinv ^inv obtained by introducing the conjunction of unary temporal literals Γ as an additional disjunct in the consequent of φinv ^inv. The resulting formula has the following form: φ¯inv⩴□(⋁i∈m⋀j∈niαij→(⋁k∈p⋀l∈qkβkl)∨Γ) ^inv ( _i∈ m _j∈ n_i _ij→ ( _k∈ p _l∈ q_k _kl ) [rgb]1,0,0\; \; ) The same transformation applies analogously to response and justice formulas, with the additional disjunct introduced within the scope of the eventuality operator ◊ . Conversion to Response or Justice During the development of our degradation framework, and in particular while analysing the Arbiter case study, we identified the need for a third class of weakening operator. Unlike antecedent and consequent weakening, this transformation applies specifically to invariants and captures situations in which behaviour originally specified as an immediate obligation is more appropriately interpreted as an eventual response. Intuitively, some invariants may be overly restrictive because they require the consequent to hold immediately after the antecedent becomes true. In practice, however, the intended behaviour may only require eventual satisfaction. This motivates a degradation operator that relaxes invariants into response-style properties by introducing an eventuality operator in the consequent. Definition 5.4 (Conversion to Response or Justice). We define the formula φ¯inv=EV(φinv) ^inv=EV( ^inv) as the conversion of the invariant φinv ^inv into a response formula by prepending the consequent of φinv ^inv with the eventuality operator ◊ . The resulting formula has the form: φ¯inv⩴□(⋁i∈m⋀j∈niαij→◊⋁k∈p⋀l∈qkβkl) ^inv ( _i∈ m _j∈ n_i _ij→ [rgb]1,0,0 _k∈ p _l∈ q_k _kl ) We refer to this transformation as conversion to justice in the special case where the invariant φinv ^inv has no antecedent. In such cases, the resulting formula has the form: φ¯inv⩴□◊⋁k∈p⋀l∈qkβkl ^inv [rgb]1,0,0 _k∈ p _l∈ q_k _kl 5.1.2. Weakening Search Space The degradation operators introduced in Definitions 5.2, 5.3, and 5.4 collectively induce a search space of weaker formulas for a given GR(1) specification component. Definition 5.5 (Weakening Search Space). Let φ be a formula following one of the syntactic structures introduced in Section 5.1 (that is, either φinv ^inv or φres ^res). We define the weakening search space of φ , denoted Space(φ)Space( ), as the set of formulas φ′≻φ obtainable through applications of the weakening operators AW()AW(), CW()CW(), and EV()EV(). Formally: Space(φ)= Space( )= φ′∣∀γ,∀x∈[1..m].φ′=AW(φ,x,γ)∪ \ ∀γ,∀ x∈[1..m].\ =AW( ,x,γ)\\ ∪ φ′∣∀Γ.φ′=CW(φ,Γ)∪ \ ∀ .\ =CW( , )\\ ∪ EV(φ) \EV( )\ The search space Space(φ)Space( ) provides the foundation for exploring alternative specification adaptations beyond simple formula removal. Importantly, however, the degradation operators defined above are neither unique nor exhaustive. They represent only one possible family of weakening transformations and do not guarantee discovery of the globally optimal degradation for a given adaptation problem. Consequently, the challenge is not merely to generate weaker formulas, but rather to systematically explore the resulting degradation space in a manner that prioritises preferred adaptations according to the preference framework introduced in Section 4. The following sections develop a degradation procedure capable of leveraging these operators to discover higher-quality solutions than those produced by the baseline removal-based approach. 5.2. Specification Degradation via Formula Weakening Recall that a solution for an adaptation problem (⟨,⟩,τ)( ,G ,τ) is a realisable specification ⟨′,′⟩ ,G such that τ⊧′τ , where the degraded assumptions and guarantees are weaker than, or equivalent to, the original specification components. The baseline procedure in Algorithm 2 exploited these properties by constructing adaptations through formula removal from the sets A and G. As illustrated in the Minepump case study, however, purely removal-based adaptations explore only a restricted portion of the degradation space. In many situations, substantially better adaptations can be obtained by weakening formulas directly rather than discarding them entirely. This motivates the introduction of formula-level degradation operators within specifications. We therefore introduce the following notation. Definition 5.6 (Formula-level Degradation). Let A be a set of formulas. Suppose a∈a and let a′a be a degradation of a such that a≺a′a a . We define the weakening operation weaken(,a,a′)=∖a∪a′=′. weaken(A,a,a )=A \a\∪\a \=A . Intuitively, the operation replaces the original formula a with a weaker formula a′a , thereby generating a degraded specification component ′A . In our implementation, we usually select a′a from the space of weaker formulas from Definition 5.5, so a′∈Space(a)a ∈ Space(a). The introduction of formula-level weakening reveals that the baseline procedure in Algorithm 2 implicitly solves two distinct adaptation tasks: assumption adaptation and guarantee adaptation. We formalise these tasks separately below. Definition 5.7 (Assumption Adaptation). Let φ=⟨,⟩ = ,G be a specification and let τ be a violation trace. The assumption adaptation task consists of constructing a weakened assumption set ′A such that: (1) τ⊧′τ ; (2) ≺′A . The resulting specification ⟨′,⟩ ,G may still be unrealisable. However, the weakened assumptions at least incorporate the observed violation trace into the environment model. The remaining task is therefore to construct a suitable weakened guarantee set restoring realisability, which motivates the complementary adaptation task below. Definition 5.8 (Guarantee Adaptation). Let φ=⟨,⟩ = ,G be a specification, let τ be a violation trace, and let ′A be a solution to the assumption adaptation task. The guarantee adaptation task consists of constructing a weakened guarantee set ′G such that: (1) ⪯′G ; (2) the specification ⟨′,′⟩ ,G is realisable. This decomposition highlights that the adaptation problem can be viewed as the sequential composition of assumption adaptation followed by guarantee adaptation. 5.2.1. Learning Assumption Degradations The objective of assumption adaptation is to construct a weakened assumption set ′A that admits the observed violation trace while preserving as much of the original environment model as possible. To construct a weakened assumption set using only degradation operations, we first identify the assumptions violated by the trace, exactly as in Section 4.3. Weakening assumptions already satisfied by the violation trace would be unnecessary, since they already admit the observed behaviour. Consequently, the adaptation procedure focuses exclusively on formulas belonging to the violation set τA_τ from Definition 4.14. The viability of this approach follows from the observation below. Lemma 5.9 (Existence of Assumption Degradations). Given a violation set τ⊆A_τ for a violation trace τ, every violated assumption admits a weaker formula satisfied by the trace. Formally, ∀a∈τ.∃a′≻a.τ⊧a′.∀ a _τ.\ ∃ a a.\ τ a . The lemma follows immediately from the observation that every assumption admits a trivial weakening to ⊤ , which is satisfied by any trace, including τ. This observation further extends to the assumption set as a whole, leading to the theorem below. Theorem 5.10 (Existence of Violating-Assumption Degradations). Given a set of assumptions A, a violation trace τ⊧̸τ , and the corresponding violation set τA_τ, there exists a set of degraded assumptions τ′=a1′,…,an′A_τ =\a_1 ,…,a_n \ such that: (1) for every violated assumption ai∈τa_i _τ, the corresponding degraded assumption satisfies ai≺ai′a_i a_i ; (2) the degraded assumption set satisfies the violation trace, i.e., τ⊧τ′τ _τ . Lemma 5.9 shows that every violated assumption admits at least one satisfying degradation. Consequently, assumption adaptation can be formulated as the task of discovering an appropriate degraded replacement for each formula in the violation set τA_τ, thereby constructing a weakened assumption set satisfying the observed trace. More specifically, the objective is to construct a degraded assumption set of the form ′=∖τ∪τ′A =A _τ _τ , where every formula in τ′A_τ is a degradation of a corresponding violated assumption in τA_τ, and the resulting assumption set satisfies the violation trace, that is, τ⊧′τ . 5.2.2. Learning Guarantee Degradations Unlike assumption adaptation, guarantee adaptation cannot be guided directly by trace satisfaction alone. While assumption degradations can be validated locally against the observed violating traces, guarantee degradations must additionally preserve realisability of the resulting specification, introducing a substantially more difficult global synthesis problem. Oracle-Guided Inductive Synthesis (OGIS) (Jha and Seshia, 2017) is a synthesis framework in which a learner proposes candidate solutions from a hypothesis space, and an oracle checks whether each candidate satisfies the desired correctness condition. If a candidate fails, the oracle returns information, typically in the form of a counterexample (Alur et al., 2013), that guides the next synthesis step. In this work, we employ OGIS as the underlying framework for solving the assumption adaptation problem. It is particularly well suited to our setting because it separates candidate generation from formal verification, allowing degradation candidates to be refined iteratively through interaction with correctness oracles. Our setting, however, differs from the classical OGIS formulation in an important respect. Traditional OGIS approaches typically assume a monotonic learning process, in which newly acquired examples progressively reduce the admissible synthesis space. In contrast, adaptation under runtime assumption violations is inherently non-monotonic: newly observed traces may invalidate previously preferred degradations, requiring the adaptation procedure to revisit and revise earlier weakening decisions. Consequently, rather than learning degradations from a fixed set of examples in a single step, our methodology incrementally accumulates violating traces and counterexamples throughout execution. The guarantee adaptation task can therefore be viewed as an OGIS loop over the degradation search space introduced in Section 5.1. The inductive component generates weakened guarantees through applications of the syntactic degradation operators and the weaken transformation, while the oracle component verifies whether the resulting guarantees satisfy the accumulated violation traces and preserve the structural requirements of the specification. Counterexamples returned by the oracle are then incorporated into subsequent OGIS iterations, progressively refining the degradation search process. Consider a specification φ′=⟨′,⟩ = ,G obtained after adapting the assumptions of some specification φ in response to a violation trace τ. Suppose further that φ′ is unrealisable. From the discussion in Section 4.3, unrealisability implies the existence of at least one unrealisable core within the guarantee set. Each unrealisable core corresponds to one or more counter-strategies demonstrating how the environment can force the system to violate the specification. Intuitively, a counter-strategy identifies behaviours under which the current guarantees cannot all be enforced simultaneously. Guided by the OGIS paradigm, we therefore use counter-strategies as oracle feedback: given a counter-strategy cs, the OGIS loop searches for guarantee degradations that eliminate the ability of cs to force a guarantee violation. We therefore focus on degrading guarantees so that the behaviours enforced by a counter-strategy are no longer considered violating behaviours. To achieve this, we extract a finite counter-play ρ∈Σ∗ρ∈ ^* compliant with the selected counter-strategy cs, such that ρ⊧̸ρ , and search for a degraded guarantee set ′≻G satisfying ρ⊧′ρ . This leads to the following learning problem. Definition 5.11 (Counter-Play-Guided Guarantee Adaptation). Let G be the guarantee set of an unrealisable specification φ=⟨′,⟩ = ,G . Furthermore, let C⊂Σ∗C⊂ ^* be a finite set of counter-plays representing behaviours that the adapted specification should permit. The counter-play-guided guarantee adaptation task consists of constructing a degraded guarantee set ′G such that: (1) ≺′G ; (2) ∀ρ∈C.ρ⊧′∀ρ∈ C.\ ρ . We allocate the task of discovering one or more counter-plays to the oracle component of the OGIS loop. Once extracted, these counter-plays guide the guarantee adaptation process in a manner closely analogous to the role of violation traces during assumption adaptation. In particular, counter-plays identify guarantees whose current behaviour prevents the specification from admitting the behaviours enforced by the environment counter-strategy. This observation allows us to derive the following dual of Lemma 5.9. Lemma 5.12 (Existence of Guarantee Degradations). Given a counter-play violation set C⊆G_C for a set of counter-plays C, every violating guarantee admits a weaker formula satisfied by all counter-plays in C. Formally, ∀g∈C.∃g′≻g.∀ρ∈C.ρ⊧g′.∀ g _C.\ ∃ g g.\ ∀ρ∈ C.\ ρ g . The lemma follows immediately from the observation that every guarantee admits a trivial weakening to ⊤ , which is satisfied by every counter-play. This observation extends naturally to the entire guarantee set, leading to the theorem below. Theorem 5.13 (Existence of Violating-Guarantee Degradations). Given a set of guarantees G, a set of counter-plays C such that ∀ρ∈C.ρ⊧̸∀ρ∈ C.\ ρ , and the corresponding counter-play violation set CG_C, there exists a set of degraded guarantees C′G_C such that: (1) for every violating guarantee gi∈Cg_i _C, the corresponding degraded guarantee satisfies gi≺gi′g_i g_i ; (2) the degraded guarantee set satisfies every counter-play in C, that is, ∀ρ∈C.ρ⊧C′.∀ρ∈ C.\ ρ _C . Note that the construction above does not necessarily imply that the resulting specification φ′=⟨′,′⟩ = ,G is realisable. If φ′ remains unrealisable, the guarantee adaptation procedure can be applied iteratively over the degraded guarantee set ′G , using a newly generated set of counter-plays C′C returned by the oracle component. More specifically, the OGIS loop searches for a further degradation ′≻′G such that the specification φ′=⟨′,′⟩ = ,G becomes realisable. If realisability is achieved, the OGIS loop terminates. Otherwise, the process continues iteratively until a sufficiently weak guarantee set is discovered that restores realisability, potentially including the empty guarantee set in the worst case. A proof of soundness and termination for this iterative OGIS loop is provided in Appendix A.4. 5.3. Synthesis of Preferred Degradations Recall Definition 4.12, which characterises preference between degraded specifications. In particular, preferred solutions correspond to specifications preserving the strongest possible guarantees while remaining incomparable only when semantically unavoidable. Consequently, the OGIS loop must explore the degradation space sufficiently thoroughly to identify the strongest incomparable guarantee degradations obtainable through syntactic weakening. Since different degradation paths may preserve different subsets of system behaviour, restricting the search prematurely risks overlooking preferred adaptations and converging toward unnecessarily weak specifications. The objective of the OGIS loop presented in this section is therefore not merely to restore realisability, but to systematically explore the degradation space generated by the syntactic weakening operators introduced earlier, while using the preference ordering to guide the extraction of the most desirable degraded specifications. Algorithm 4 OGIS-Based Synthesis of Preferred Degradations 1: ⟨,⟩ ,G (realisable GR(1) specification), τ (violation trace), AWAW and CWCW (syntactic degradation operators) 2: preferredDegradations=⟨′,′⟩preferredDegradations=\ ,G \, a set of preferred realisable degraded specifications 3: function synthesisePreferredDegradations(⟨,⟩,τ ,G ,τ) 4: learnedSpecs←learnAssumptionDegradations(⟨,⟩,τ)learnedSpecs← learnAssumptionDegradations( ,G ,τ) 5: learnedSolutions←[]learnedSolutions←[\ ] 6: unrealisableSpecifications←[]unrealisableSpecifications←[\ ] 7: for spec∈learnedSpecsspec do 8: if isRealisable(spec) isRealisable(spec) then 9: append(learnedSolutions,speclearnedSolutions,\ spec) 10: else 11: append(unrealisableSpecifications,specunrealisableSpecifications,\ spec) 12: end if 13: end for 14: if learnedSolutions≠∅learnedSolutions≠ then 15: return merge(filterPreferred(learnedSolutions)) merge ( filterPreferred(learnedSolutions) ) 16: end if 17: spec←filterPreferred(unrealisableSpecifications)[0]spec← filterPreferred(unrealisableSpecifications)[0] 18: newCounterPlaySets←extractCounterPlays(spec)newCounterPlaySets← extractCounterPlays(spec) 19: candidateQueue←[]candidateQueue←[\ ] 20: for C∈newCounterPlaySetsC do 21: append(candidateQueue,(spec,C)candidateQueue,\ (spec,C)) 22: end for 23: while candidateQueue≠∅candidateQueue≠ do 24: (iSpec,C)←pop(candidateQueue)(iSpec,C)← pop(candidateQueue) 25: learnedSpecs←learnGuaranteeDegradations(iSpec,C)learnedSpecs← learnGuaranteeDegradations(iSpec,C) 26: for spec∈learnedSpecsspec do 27: if isRealisable(spec) isRealisable(spec) then 28: append(learnedSolutions,speclearnedSolutions,\ spec) 29: else 30: newCounterPlaySets←extractCounterPlays(spec)newCounterPlaySets← extractCounterPlays(spec) 31: for C∈newCounterPlaySetsC do 32: if ¬isRedundantCandidate(candidateQueue,learnedSolutions,spec,C) isRedundantCandidate(candidateQueue,learnedSolutions,spec,C) then 33: append(candidateQueue,(spec,C)candidateQueue,\ (spec,C)) 34: end if 35: end for 36: end if 37: end for 38: end while 39: return merge(filterPreferred(learnedSolutions)) merge ( filterPreferred(learnedSolutions) ) 40: end function We now introduce Algorithm 4, which employs a breadth-first OGIS-based degradation loop to compute preferred degraded specifications. In line 4, the learner generates candidate assumption degradations satisfying the assumption adaptation conditions from Definition 5.7. Lines 5–13 then partition the generated specifications into two sets: the set learnedSolutions, containing specifications that are already realisable after assumption adaptation, and the set unrealisableSpecifications, containing the remaining unrealisable candidates. In line 14, the algorithm checks whether any realisable specifications were discovered. If so, further guarantee adaptation is unnecessary. The algorithm therefore returns, in line 15, the merged preferred realisable degraded specifications extracted using the merge procedure in Appendix B.1 in Algorithm 6 and the filterPreferred procedure introduced in Algorithm 1. If no such specifications are discovered, the algorithm extracts the strongest intermediate specification in line 17. Observe that, at this stage, a call to filterPreferred returns only a single specification, since all candidates still preserve the original guarantee set G. Because this intermediate specification is unrealisable, the oracle component then extracts multiple sets of counter-plays in line 18, following the optimisation strategy discussed in Section 5.2. In lines 19–22, the algorithm constructs the initial synthesis frontier by inserting tuples composed of an unrealisable specification specspec together with an associated set of counter-plays C into the candidateQueuecandidateQueue. Starting from line 23, the algorithm enters the counter-play-guided guarantee adaptation loop. While there is some candidate tuple, we extract it on line 24 from the queue, then apply on line 25 a counter-play guided guarantee degradation step over the intermediate specification iSpeciSpec and the set of counter-plays C, as per Definition 5.11, to learn a new set of possible solutions to the adaptation problem. Lines 26–37 then evaluate each specification in the resulting set learnedSpecs. If a specification is realisable, it is added to the set learnedSolutions in line 28. Otherwise, the oracle component extracts new counter-play sets for the unrealisable specification in line 30. Finally, lines 31–35 extend the synthesis frontier by inserting newly generated specification/counter-play tuples back into the queue, allowing the OGIS loop to continue refining guarantee degradations iteratively. Eventually, the OGIS loop terminates once all relevant degradations have been explored, at which point the queue becomes empty after line 38. As proved in Appendix A.4, every exploration branch eventually converges to a realisable specification. Finally, line 39 applies the filterPreferred and merge procedures in succession to the accumulated set learnedSolutions, returning the merged preferred degraded specifications. The OGIS loop can be further optimised by exploiting the preference ordering introduced earlier. Since the objective is to discover specifications preserving the strongest distinct guarantee sets, the exploration queue need not retain candidates that cannot contribute to preferred adaptations. More specifically, the candidateQueuecandidateQueue can be extended with a redundancy check in line 32, preventing reinsertion of candidate tuples composed of equivalent intermediate specifications together with identical, or sufficiently similar, counter-play sets. In such cases, the resulting OGIS branches are expected to explore equivalent degradation regions, making repeated exploration unnecessary. Additionally, if an intermediate specification is already weaker than some specification contained in learnedSolutionslearnedSolutions, then it need not be inserted into the queue in line 33. Any adaptations generated from that specification would eventually be discarded by the filterPreferred procedure, since stronger preferred adaptations have already been discovered. These optimisations substantially reduce redundant exploration while preserving completeness with respect to the preferred degraded specifications returned by the OGIS loop. 6. Evaluation In Sections 4 and 5, we introduced the adaptation problem for GR(1) specifications together with two adaptation methodologies: a removal-based degradation approach, referred to as the trivial degradation algorithm, and a finer-grained syntactic degradation approach based on OGIS loops, and post-processing of the results. Both approaches were shown to compute at least one satisfying degraded specification for the adaptation problem. In this section, we evaluate the practical benefits and trade-offs of the proposed methodologies. Section 6.1 presents the evaluation methodology, including the preference criteria used to assess the proposed approach. Section 6.2 introduces the case studies, describes the experimental setup, and discusses the results obtained. Finally, Section 6.3 summarises the findings and discusses their implications. 6.1. Methodology We refer to the degraded specifications computed by the trivial degradation procedure from Section 4.3 as trivial degradations. Similarly, we refer to the degraded specifications computed by the OGIS-based syntactic degradation approach from Section 5 as learned degradations. The methodologies introduced in Sections 4 and 5 are guaranteed to produce satisfying degradations for the adaptation problem. Consequently, the evaluation focuses not on correctness, but on assessing the relative quality and usefulness of the degraded specifications produced by each approach. Specifically, we investigate whether the learned degradations are preferable, according to Definition 4.12, to trivial degradations. To this end, we evaluate the proposed approaches on a collection of case studies adapted from the degradation benchmarks of Buckworth et al. (Buckworth et al., 2023). Each case study consists of: (1) a specification φ=⟨,⟩ = ,G ; (2) a violation trace τ such that τ⊧̸τ . For each benchmark, we compute two sets of degraded specifications: (1) Φt=trivialDegradation(φ,τ) _t= trivialDegradation( ,τ), the set of trivial degradations; (2) Φl=learnPreferredDegradations(φ,τ) _l= learnPreferredDegradations( ,τ), the set of learned degradations. We are interested in determining whether, for every element in the set of trivial solutions, there exists a preferred specification in the set of learned solutions. Formally, we seek to establish the validity of the following property: ∀φt∈Φt.∃φl∈Φl.φl⊏φt(preference criteria) ∀ _t∈ _t.∃ _l∈ _l. _l _t (preference criteria) where ⊏ denotes preference between two specifications, and is defined in Definition 4.3. If the formula above is not true in any case study, then we are looking at some form of failure of our learning-based algorithm in Section 5, which we will investigate on a case-by-case basis. We encode the specifications in the GR(1) language Spectra, and leverage the tools and code base of the SYNTECH lab for synthesis and diagnosis (Maoz and Ringert, 2021). This choice infers an implementation detail of note, with respect to the formulation of response patterns □(p→◊s) (p→ s). When discussing pure GR(1) syntax, this behaviour is unsupported by the original rules of realisability (Bloem et al., 2012), which would disallow our third syntactic degradation methodology from Definition 5.4. 6.2. Experimental Results The results of the evaluation are presented in Tables 4 and 4. In Table 4, the columns NumT and NumL report the number of degradations returned by the trivial and learning-based adaptation algorithms, respectively. Across all case studies, the learning-based algorithm identifies a single preferred degradation. Table 4 provides a qualitative comparison between the trivial and learned degradations. The learned adaptations avoid guarantee weakening entirely for the Arbiter and Traffic Single case studies, demonstrating that fine-grained assumption weakening can preserve the complete set of system guarantees. Furthermore, the Assumptions Order column of Table 4 shows that the learned degradations consistently retain stronger assumptions than their trivial counterparts. This reflects the locality of the observed assumption violations: since the violation trace affects only a subset of the behaviour captured by the original assumptions, the learning-based approach weakens only the affected portion rather than discarding the assumption altogether. The Preference column of Table 4 reports the ordering between the trivial and learned degradations. In every case study, the learned degradation is preferred according to Definition 4.12, thereby satisfying the preference criteria. The complete degraded specifications are provided in Appendices C.3 and C.4. Case Study NumT NumL Outcome Arbiter 1 1 Success Lift 1 1 Success Minepump 2 1 Success Traffic Single 1 1 Success Traffic Updated 1 1 Success Table 3. Adaptation counts and preference-criteria outcome per case study. Case study Assumptions order Guarantees order Preference Arbiter o≺l≺tA_o _l _t o≡l≺tG_o _l _t φl⊏φt _l _t Lift o≺l≺tA_o _l _t o≡l≡tG_o _l _t φl⊏φt _l _t Traffic Single o≺l≺tA_o _l _t o≡l≺tG_o _l _t φl⊏φt _l _t Traffic Updated o≺l≺tA_o _l _t o≡l≡tG_o _l _t φl⊏φt _l _t Minepump o≺l≺tA_o _l _t o≡l≺t1G_o _l _t1 φl⊏φt _l _t o≡l≺t2G_o _l _t2 φl⊏φt _l _t Table 4. Relative weakness ordering between original, learned and trivial specification components, alongside preference between learned and trivial solution(s). We have to note separately on the fact that the minepump example returns a single solution that, semantically, yields stronger guarantees than both trivial solutions we discover. We illustrate the relationship between the trivial specifications and the learned specification in Figure 2. We identify the two trivial solutions as φt1=⟨t1,t1⟩ _t1= _t1,G_t1 and φt2=⟨t2,t2⟩ _t2= _t2,G_t2 , and similarly identify the learned solution as φl=⟨l,l⟩ _l= _l,G_l . The interested reader may find the raw solutions in Appendix C.3.2 and C.4.2 for the trivial and learned solutions respectively. We see that the sets of assumptions are comparable to each other, that the assumptions are equivalent between φt1 _t1 and φt2 _t2. Finally, we see that the learned assumptions are strictly stronger for the learned solutions, and the learned guarantees are strictly stronger than either of the trivial guarantees. This satisfies the preference criteria, since we needed to show there is a stronger (or equivalent) set of guarantees in the learned solutions for each trivial set of guarantees. Since the learned solution is strictly preferable to every specification in the set of trivial solutions, then we consider the minepump case study a success for the preference criteria, and report it in Table 4. lA_llG_lt1G_t1t1A_t1t2A_t2t2G_t2≡≺ ≺ ≺ ≺ specification φl _lTrivial specification φt1 _t1Trivial specification φt2 _t2 Figure 2. Comparison between learned and trivial solutions of the minepump case study. Solid arrows denote weakness-based ordering (≺ ), vertical solid lines denote semantic equivalence (≡), and lack of any line denotes incomparability. 6.2.1. Discussion on scale The procedure we developed in Algorithm 4 identifies, over the course of the run, five types of specifications: (1) Unrealisable specifications, during the BFS exploration phase, when the algorithm considers a degradation that yields a new syntactically unique specification that is not realisable; (2) Realisable specifications, during the BFS exploration, when a degradation step modifies either the original specification, or an unrealisable intermediate specification, into a realisable specification. We also call this the set of solutions; (3) Unique specifications, filtered after the exploration phase. Any group of semantically equivalent specifications is trimmed down to one. This procedure returns a set of pair-wise semantically distinct specifications; (4) Preferred specifications, when non-preferred solutions (as per Definition 4.12) are being filtered out of the pool of semantically unique solutions; (5) Final specifications, when the assumptions and guarantees of the preferred solutions are merged and manipulated to return the best set of solutions. For each case study, we report the number of specifications encountered of each category in Table 5. Every column coincides with a category above. The last column, "Trivial", reports on the amount of specifications our baseline adaptation procedure discovers, for the sake of comparing. Case Study Explored Unique Preferred Final Trivial Unrealisable Realisable Lift 0 21 17 11 1 1 Traffic Updated 0 21 17 10 1 1 Traffic Single 9 3 2 2 1 1 Arbiter 285 546 308 6 1 1 Minepump 809 3762 1218 17 1 2 Table 5. Amount of specifications discovered at each stage in the algorithm. We observe the learning procedure, for each case study, starts with a large set of explored solutions (i.e. realisable specifications), only to converge onto one or a few final solutions. The Explored Unrealisable column highlights the potential of the algorithm to discover a set of satisfiable solutions immediately, through the innate filtering that the ILP backbone of the algorithm does in order to degrade the set of assumptions in a way that the violation trace is satisfied. This fact is shown in the Lift and Traffic Updated rows, where the set of explored unrealisable specifications is 00. Other than the simple case study of Traffic Single, we see an increase on the realisable specifications side compared to the unrealisable side, with a significant increase for the complex case studies of Arbiter and Minepump. This is likely caused by the traversal methodology: for each syntactically distinct unrealisable specification discovered, there could be several solutions discovered, and several continuations from that point. We produce a snippet of our visualisation program highlighting this fact in Figure 3, where at least 3 realisable specifications and at least 3 unrealisable specifications are discovered from node 81 during traversal. Figure 3. A snippet of the exploration phase during learning for the Minepump case study. Every green node represents a new unrealisable specification discovered, every blue node represents a new realisable specification discovered. An arrow between two nodes represents a learning step. Out of the set of realisable specifications explored, we find a relatively small drop is followed when filtering out all extraneous specifications, those being any syntactically distinct, but semantically equivalent specification. We see the number reported in the "Unique" column. Although we see a smaller drop in the simpler case studies, for the complex studies, we see a sharper drop between the unique specifications, and the preferred maximal specifications. For all case studies, this number is around 1010 or lower, with the exception of Minepump, which is the only case study containing preferred specifications which require guarantee degradation. Finally, we observe that all case studies can be merged into a single final most preferred specification. 6.3. Summary We observe that, for each case study, the solutions produced by the learning-based solver yield solutions of higher preference compared to the trivial solutions that can be found. By prioritising solutions using the preference definition from Section 4.2, the learning method always produces a solution preferred to the trivial solution(s) discovered. There are two highlights in our results. The first one is the behaviour observed in the Arbiter and Traffic Single case studies, where the baseline trivial solution would require guarantee weakening, yet due to the fine grained learning-based repair method we employ, we discovered guarantee weakening can be skipped, allowing the system to resume its behaviour safely. The second highlight is the final solution in Minepump, which surpasses both trivial solutions in terms of preference, bypassing the necessity of stakeholder involvement by avoiding the need for making a choice. Although the learning-based algorithm reliably discovers a more preferred solution compared to the trivial solution(s) for every case study, this comes at the cost of exploring a large space of candidate specifications, as shown in Table 5. For the more complex case studies in particular, the number of realisable specifications explored before converging to a final solution is substantial. The current methodology is best suited to scenarios where there are no hard time constraints for computing an adaptation. More constraining scenarios motivate the need for heuristics capable of guiding the search towards preferred solutions more directly. 7. Related Work Our work is rooted in behaviour-based adaptation as opposed to configuration-based (Braberman et al., 2015) since we focus on modifying statements that refer to the intended behaviour of the system or the assumed behaviour of the environment, in terms of safety and liveness properties, in order to salvage as much of the original requirements as possible. We continue in the line of work of syntactic degradation-based adaptations of specifications, earlier explored in (Buckworth et al., 2023; Zhang, 2025). Both of their works enable controllers synthesised from a GR(1) specification to function in the context of encountering an environment violation. However, to the best of our knowledge, we are the first to investigate what makes a specification preferred in the context of this problem. Although the quality of assume-guarantee specifications has been analysed from a robustness-during-deployment perspective (Shalom and Maoz, 2023; Zhang, 2025), which correctly suggests that weakest environment assumptions are always preferred (Cobleigh et al., 2003; Lomuscio et al., 2013; Nam and Alur, 2006) with respect to the logic that the specified system may operate in as broad a set of environment dynamics as possible, the adaptation community seems to have overlooked the potential for over-fitting (too weak) environmental assumptions, and how online adaptation can lead to robustness vulnerabilities. In the avenue where formal methods literature has started learning environment model dynamics from data (Keegan et al., 2020; Gaaloul et al., 2020), and generating assumptions (through learning (Cobleigh et al., 2003), or by hand (Ma’Ayan and Maoz, 2023)) to enable specific guarantees (rather than the ideal methodology, where guarantees of the system/machine are based on assumptions of the environment/world (Jackson, 1995)), the chances of faults are increased. And as we illustrated in Section 4.2 and Figure 1, such faults lead to divergences in the perceived model of the world and the actual. These divergences can cascade towards a representation that, although it becomes inclusive of (most) observed environment behaviour, may lead to degrading the system guarantees unnecessarily. Other than Buckworth’s work built on the OGIS framework (Jha and Seshia, 2017), Cavezza et al.’s work on assumption refinement has been a strong influence for the specification preference criteria (Cavezza and Alrajeh, 2017), as well as their methodology of search space exploration (Cavezza et al., 2020). The refinement algorithm they propose also searches for the minimal refinements, explored in a BFS manner to discover the best solutions early during the run of the algorithm. We observe that our preference criteria for degraded assumptions is the symmetric of their work, and extend the minimal BFS exploration to cascade to guarantee degradation (when necessary). Work in the evaluation of the strength of a solution for refinement and degradation problem has always dealt with the following context-related issue: there is no trivial way of representing the quality of a specification numerically. There have been several avenues and angles for the fair and complete analysis of such approaches. One such avenue is the analysis of robustness under assumption violations. Bloem et al. (Bloem et al., 2014) have developed the notion of k-robustness, that attempts to minimise the cost of failure of the guarantees of the system by transforming the specification into an error specification, where each formula is given a cost function, and the overall cost of system errors needs to be smaller than k times the cost of environment errors. This design has the potential of generating resilient controllers in the face of failures, that are able to rebound should failures occur. Our work differs from this method, in the sense that we use the failures to learn an explicit new specification, never allowing or expecting deviations from the written specification to occur. Future work could look into leveraging the controller encoding in situations where learning takes longer, and potentially using the cost automata formulation for our own formulas, in order to only weaken behaviour that yields higher error cost. We believe cost automata has the potential to relay deeper meaning during the process of learning a weakening, as opposed to providing a rank to each individual requirement (Alur et al., 2008). An alternative controller resilience problem in the face of assumption violations has been proposed in Ehlers et al. (Ehlers and Topcu, 2014), where (k,b)(k,b)-resilience defines the concept that a controller of a GR(1) specification is resilient to glitches (environment failures) for at most k steps, separated by periods of at least b steps of no glitches, and the amount of glitches is finite. Since we address environment errors that may occur infinitely often, we cannot define our solutions in terms of (k,b)(k,b)-sanity. The closest approach to the quantitative measurement angle we consider is the weakness measurement of Cavezza et al. (Cavezza et al., 2021). They express a specification’s set of assumptions as a triple of elements: the entropy of the invariants, the Hausdorff dimension of the invariants, and the Hausdorff dimension of the fairness complement of the assumptions. This measurement has the quality that it preserves the ordering between two (or more) specifications, in terms of which formula is weaker/stronger than the other. The problem with this measurement comes in its structure and practicality. Unfortunately, the format of a lexicographical ordering on a triple makes it impossible to accurately aggregate information on multiple solutions at once. Furthermore, it has not been shown that the valuation would have any correlation to an order of magnitude of the weakness between solutions, although a case could be made that the usage of entropy and/or Hausdorff dimensions can be used as a metric over nested LTL formulas (i.e. φ→ψ →ψ or ψ→φψ→ ). Nonetheless, a meaningful quantitative metric to represent and compare non-nested LTL formulas is still a literature gap, which consequently, prevents the creation of a quantitative metric for assume-guarantee specifications based on LTL, like GR(1). The field of runtime adaptation of systems is well explored in the space of requirement engineering (Calinescu et al., 2012; Calinescu et al., 2017; Chu et al., 2024), where quantitative model checking techniques (Filieri et al., 2011; Kwiatkowska, 2007) are employed to verify models that satisfy a set of requirements written in probabilistic computational-tree logic (PCTL) or similar. 8. Conclusion Reactive systems synthesised from GR(1) specifications depend on the behaviour of the environment to hold. During deployment, a failure in environment behaviour has the potential to silently break most guaranteed behaviour of the system. We highlight the tuple consisting of an assume/guarantee specification and a behaviour trace violating the assumptions of the specification as an important adaptation problem. We propose a preference-based ordering with respect to what makes a good solution to this problem, then propose two algorithms for the discovery of solutions. The first algorithm represents a simple baseline methodology, where each individual formula is treated like a component in a set-theoretical problem, and a solution can be found through the removal of formulas from the specification. We show this algorithm removes the smallest amount of formulas from the original specification. The second algorithm is a finer grained solution, that leverages syntactic manipulation and inductive learning to iteratively degrade the violating formulas until they reach a realisable specification that no longer violates the observed environment behaviour. We show the second algorithm discovers solutions of higher quality than the baseline algorithm. This work has made a case in Section 4.2 for the desirability of the strongest degraded specification as the result of adaptation. To the best of our knowledge, the suggestion that the strongest possible set of assumptions would be preferred has not been previously proposed. Moreover, it appears to contradict the logic of robustness: that a system that is able to achieve its goals (strongest system guarantees) in the highest amount of scenarios (weakest environment assumptions) is more robust. We propose a finer grained definition to robustness, that considers partial failure as a certainty that a system needs to be ready for: an adaptive system that is able to salvage the widest set of goal-related behaviours (strongest possible system guarantees) in any scenario (any environment condition) is more robust. Future work should further analyse the notion of robustness considered in this work. This work showcased adapted results as being favourable under the preference criteria, therefore merely hinting at an extended desirability in the wider context of adaptive systems. Further study should focus on the development of realistic scenarios that systems can leverage to validate their ability to adapt, and their ability to retain their operational guarantees. One thing to note regarding the preference criteria is how maximal system guarantees are equally preferred. This was intentional, since discriminating between equally preferred guarantees requires additional information beyond the logical formalism alone. Future work will consider ways for a stakeholder to provide discrimination methods for system guarantees when adaptation is necessary. Criticality of guarantees has been explored in the context of synthesis under uncertainty (Yang et al., 2024), and in the context where all guarantees are equally critical, a prioritisation or weighting method could be employed. The problem with priorities and weights when applied to guarantees is that, in more complex scenarios, specifically industrial ones, the space of guarantees is vast, and the stakeholders involved in the process may not be sufficiently aware of the low level details of the adaptation process to propose a satisfying weighting or ordering of the guarantees. A relatively novel branch of work has the potential to circumvent that by introducing semantic meaning to the formulas within the specification (Bolt et al., 2019) with respect to a set of principles that can be translated from the natural language of the stakeholders (Kaushik et al., 2025) (i.e. the client of the system, the manufacturer’s priorities, the laws of the country etc.). This aggregated knowledge, including the current specification and the violation trace, creates a complete context for an adaptive system to generate its own set of priorities, ground in the priorities of the relevant stakeholders. Once a priority between system guarantees is in place, the next step will be to use it to guide the search towards only such solutions that follow the priority system. The learning-based algorithm, in its current state, generates and explores a vast space of potential adaptation candidates, which takes a significant amount of time. This inhibits the application of our methodology at runtime, meaning it can only be used proactively in practical scenarios, by estimating future failures, and pre-computing suitable adapted specifications before there is a need to adapt. To allow this level of controlled adaptation to occur reactively, rules and heuristics need to be developed, with the purpose of salvaging the most important guarantees, and finding a realisable solution in the least amount of steps. We have already discovered that the choice of counter-trace and counter-strategy allows us to manipulate in advance what system behaviour we want to salvage, and therefore, which guarantee is considered for degradation by the learner during OGIS. This methodology, alongside others from classical graph traversal theory (e.g. Monte-Carlo Tree Search), may be used to enable our adaptation methodology to function in reactive contexts, and therefore, enable systems to act in a principled manner under any circumstance. Acknowledgements. This work was supported by the UK Research and Innovation [grant number EP/S023356/1] in the UKRI Centre for Doctoral Training in Safe and Trusted Artificial Intelligence (w.safeandtrustedai.org). References Alur et al. (2008) Rajeev Alur, Aditya Kanade, and Gera Weiss. 2008. Ranking automata and games for prioritized requirements. In International Conference on Computer Aided Verification. Springer, 240–253. Alur et al. (2013) Rajeev Alur, Salar Moarref, and Ufuk Topcu. 2013. Counter-strategy guided refinement of GR (1) temporal logic specifications. In 2013 Formal Methods in Computer-Aided Design. IEEE, 26–33. Bloem et al. (2014) Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, and Robert Könighofer. 2014. Synthesizing robust systems. Acta Informatica 51, 3 (2014), 193–220. Bloem et al. (2011) Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. 2011. Specification-centered robustness. In 2011 6th IEEE International Symposium on Industrial and Embedded Systems. IEEE, 176–185. Bloem et al. (2012) Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. 2012. Synthesis of reactive (1) designs. J. Comput. System Sci. 78, 3 (2012), 911–938. Bolt et al. (2019) Joe Bolt, Bob Coecke, Fabrizio Genovese, Martha Lewis, Dan Marsden, and Robin Piedeleu. 2019. Interacting conceptual spaces I: Grammatical composition of concepts. In Conceptual spaces: Elaborations and applications. Springer, 151–181. Braberman et al. (2015) Victor Braberman, Nicolas D’Ippolito, Jeff Kramer, Daniel Sykes, and Sebastian Uchitel. 2015. Morph: A reference architecture for configuration and behaviour self-adaptation. In Proceedings of the 1st international workshop on control theory for software engineering. 9–16. Buckworth et al. (2023) Titus Buckworth, Dalal Alrajeh, Jeff Kramer, and Sebastian Uchitel. 2023. Adapting specifications for reactive controllers. In 2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS). IEEE, 1–12. Calinescu et al. (2012) Radu Calinescu, Carlo Ghezzi, Marta Kwiatkowska, and Raffaela Mirandola. 2012. Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55, 9 (2012), 69–77. Calinescu et al. (2017) Radu Calinescu, Danny Weyns, Simos Gerasimou, Muhammad Usman Iftikhar, Ibrahim Habli, and Tim Kelly. 2017. Engineering trustworthy self-adaptive software with dynamic assurance cases. IEEE Transactions on Software Engineering 44, 11 (2017), 1039–1069. Cavezza and Alrajeh (2017) Davide G Cavezza and Dalal Alrajeh. 2017. Interpolation-based GR (1) assumptions refinement. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 281–297. Cavezza et al. (2020) Davide G Cavezza, Dalal Alrajeh, and András György. 2020. Minimal assumptions refinement for realizable specifications. In Proceedings of the 8th International Conference on Formal Methods in Software Engineering. 66–76. Cavezza et al. (2021) Davide G Cavezza, Dalal Alrajeh, and András György. 2021. A weakness measure for GR (1) formulae. Formal Aspects of Computing 33, 1 (2021), 27–63. Chu et al. (2024) Simon Chu, Justin Koe, David Garlan, and Eunsuk Kang. 2024. Integrating graceful degradation and recovery through requirement-driven adaptation. In Proceedings of the 19th international symposium on software engineering for adaptive and self-managing systems. 122–132. Cimatti et al. (2008) Alessandro Cimatti, Marco Roveri, Viktor Schuppan, and Andrei Tchaltsev. 2008. Diagnostic information for realizability. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 52–67. Cobleigh et al. (2003) Jamieson M Cobleigh, Dimitra Giannakopoulou, and Corina S Păsăreanu. 2003. Learning assumptions for compositional verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 331–346. De Giacomo et al. (2014) Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali. 2014. Reasoning on LTL on finite traces: Insensitivity to infiniteness. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 28. Dwyer et al. (1999) Matthew B Dwyer, George S Avrunin, and James C Corbett. 1999. Patterns in property specifications for finite-state verification. In Proceedings of the 21st international conference on Software engineering. 411–420. Ehlers and Topcu (2014) Rüdiger Ehlers and Ufuk Topcu. 2014. Resilience to intermittent assumption violations in reactive synthesis. In Proceedings of the 17th international conference on Hybrid systems: computation and control. 203–212. Filieri et al. (2011) Antonio Filieri, Carlo Ghezzi, and Giordano Tamburrelli. 2011. Run-time efficient probabilistic model checking. In Proceedings of the 33rd international conference on software engineering. 341–350. Firman et al. (2020) Elizabeth Firman, Shahar Maoz, and Jan Oliver Ringert. 2020. Performance heuristics for GR (1) synthesis and related algorithms. Acta informatica 57, 1 (2020), 37–79. Gaaloul et al. (2020) Khouloud Gaaloul, Claudio Menghi, Shiva Nejati, Lionel C Briand, and David Wolfe. 2020. Mining assumptions for software components using machine learning. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 159–171. Jackson (1995) Michael Jackson. 1995. The world and the machine. In Proceedings of the 17th international conference on Software engineering. 283–292. Jha and Seshia (2017) Susmit Jha and Sanjit A Seshia. 2017. A theory of formal synthesis via inductive learning. Acta Informatica 54, 7 (2017), 693–726. Kaushik et al. (2025) Prakhar Kaushik, Shravan Chaudhari, Ankit Vaidya, Rama Chellappa, and Alan Yuille. 2025. The universal weight subspace hypothesis. arXiv preprint arXiv:2512.05117 (2025). Keegan et al. (2020) Maureen Keegan, Victor Braberman, Nicolás D’Ippolito, Nir Piterman, and Sebastian Uchitel. 2020. Control and discovery of environment behaviour. IEEE Transactions on Software Engineering 48, 6 (2020), 1965–1978. Kramer et al. (1983) Jeff Kramer, Jeff Magee, Morris Sloman, and Andrew Lister. 1983. Conic: an integrated approach to distributed computer control systems. IEE Proceedings E (Computers and Digital Techniques) 130, 1 (1983), 1–10. Kwiatkowska (2007) Marta Kwiatkowska. 2007. Quantitative verification: models techniques and tools. In Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering. 449–458. Liffiton and Sakallah (2008) Mark H Liffiton and Karem A Sakallah. 2008. Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning 40, 1 (2008), 1–33. Lomuscio et al. (2013) Alessio Lomuscio, Ben Strulo, Nigel Walker, and Peng Wu. 2013. Assume-guarantee reasoning with local specifications. International Journal of Foundations of Computer Science 24, 04 (2013), 419–444. Ma’Ayan and Maoz (2023) Dor Ma’Ayan and Shahar Maoz. 2023. Using reactive synthesis: An end-to-end exploratory case study. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 742–754. Maoz and Ringert (2015) Shahar Maoz and Jan Oliver Ringert. 2015. GR (1) synthesis for LTL specification patterns. In Proceedings of the 2015 10th joint meeting on foundations of software engineering. 96–106. Maoz and Ringert (2021) Shahar Maoz and Jan Oliver Ringert. 2021. Spectra: a specification language for reactive systems. Software and Systems Modeling 20, 5 (2021), 1553–1586. Maoz et al. (2019) Shahar Maoz, Jan Oliver Ringert, and Rafi Shalom. 2019. Symbolic repairs for GR (1) specifications. In 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE). IEEE, 1016–1026. Maoz and Shalom (2020) Shahar Maoz and Rafi Shalom. 2020. Inherent vacuity for GR (1) specifications. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 99–110. Maoz and Shalom (2021) Shahar Maoz and Rafi Shalom. 2021. Unrealizable cores for reactive systems specifications. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). IEEE, 25–36. Nam and Alur (2006) Wonhong Nam and Rajeev Alur. 2006. Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In International Symposium on Automated Technology for Verification and Analysis. Springer, 170–185. Piterman et al. (2006) Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. 2006. Synthesis of reactive (1) designs. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 364–380. Pnueli (1977) Amir Pnueli. 1977. The temporal logic of programs. In 18th annual symposium on foundations of computer science (sfcs 1977). ieee, 46–57. Pnueli and Rosner (1989) Amir Pnueli and Roni Rosner. 1989. On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 179–190. Shalom and Maoz (2023) Rafi Shalom and Shahar Maoz. 2023. Which of my assumptions are unnecessary for realizability and why should i care?. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 221–232. Yang et al. (2024) Dong Yang, Hao Shi, Wei Dong, Yanqi Dong, and Yong Zhang. 2024. Synthesizing Controller for Unsynthesizable Specification Based on Criticality Levels. In Proceedings of the 15th Asia-Pacific Symposium on Internetware. 199–208. Zave and Jackson (1997) Pamela Zave and Michael Jackson. 1997. Four dark corners of requirements engineering. ACM transactions on Software Engineering and Methodology (TOSEM) 6, 1 (1997), 1–30. Zhang (2025) Changjian Zhang. 2025. Behavioral robustness of software system designs. Ph. D. Dissertation. Carnegie Mellon University. Appendix A Proofs A.1. Counter Example Disjunction of Assumptions We present below a counter-example to the following claim. For any two solutions to an adaptation problem (φ,τ)( ,τ), φ1=⟨1,⟩ _1= _1,G and φ2=⟨2,⟩ _2= _2,G , if their guarantees are equivalent, then there exists a third solution φ′=⟨′,⟩ = ,G such that ′≡1∨2A _1 _2, and φ′ is also a solution to the same adaptation problem. Formally, the claim can be stated as follows: φ1,φ2∈AllSolutions(Adapt(φ,τ))⇒φ′∈AllSolutions(Adapt(φ,τ)), _1, _2 (Adapt( ,τ))\; \; (Adapt( ,τ)), where φ′=⟨1∨2,⟩ = _1 _2,G . Proof. We take note that we only need to show that there is such a case where 1∨2A_1 _2 does not have an equivalent for the syntactical structure of the set of assumptions of a GR(1) specification. We propose the following specification trace pair as our φ and τ respectively: ⬇ 1 module CounterExample_v0 2 3 env boolean a; 4 env boolean b; 5 sys boolean c; 6 7 assumption -- a1 8 G(a); 9 guarantee -- g1.1 10 G((!a&!b)|(!a&PREV(!b))->!c); 11 guarantee -- g1.2 12 G(a->c); 13 guarantee -- g2 14 G(PREV(b)&b->c); 15 guarantee -- g3 16 GF(c); Spectra τ=[(¬a,¬b,c)]τ=[( [rgb]1,0,0 a, b, [rgb]0,0.6,0c)] Figure 4. Counter example specification and trace We do highlight that, naturally, this spec by itself has very little practicality, but it would not be outside of the real of possibility for this spec to belong to a more complex specification, handling a larger amount of reactive interactions. This is the smallest self contained example we envisioned at the time of writing this paper. We note the specification above is realisable, a fact that has been verified with the usage of the SYNTECH toolbox plugins within the Eclipse development environment. We further note that assumption a1 obviously violates the trace τ. There are two immediate solutions that may be proposed without relying on guarantee degradation. φ1 _1 is presented below: ⬇ 1 module CounterExample_v1 2 3 env boolean a; 4 env boolean b; 5 sys boolean c; 6 7 assumption -- a1 8 G(a|b); 9 guarantee -- g1.1 10 G((!a&!b)|(!a&PREV(!b))->!c); 11 guarantee -- g1.2 12 G(a->c); 13 guarantee -- g2 14 G(PREV(b)&b->c); 15 guarantee -- g3 16 GF(c); Spectra Figure 5. Counter example specification repair 1 And φ2 _2 is presented below: ⬇ 1 module CounterExample_v2 2 3 env boolean a; 4 env boolean b; 5 sys boolean c; 6 7 assumption -- a1 8 GF(a); 9 guarantee -- g1.1 10 G((!a&!b)|(!a&PREV(!b))->!c); 11 guarantee -- g1.2 12 G(a->c); 13 guarantee -- g2 14 G(PREV(b)&b->c); 15 guarantee -- g3 16 GF(c); Spectra Figure 6. Counter example specification repair 2 We have verified again realisability using the SYNTECH toolbox. We identify the two proposed assumption degradations are G(a∨b)G(a b) and GF(a)GF(a) respectively, which can be visualised in Figure 7, where we highlight the relationship between the different repair proposals. We now return to the claim we started this section with, that there is always a disjunction between the assumptions. We clearly see though that G(a∨b)∨GF(a)G(a b) GF(a) cannot be meaningfully decomposed or rewritten to satisfy the GR(1) syntactic structure. Therefore, we have a contradiction to the claim, invalidating it. G(a)G(a)G(a∨b)G(a b)GF(a)GF(a)G(a∨b)∨GF(a)G(a b) GF(a)GF(a∨b)GF(a b)G′G realisableunrealisablerealisableφ φ1 _1φ2 _2not GR(1)φ′ Figure 7. Implication-based ordering of the counter-example specifications. As a bonus, let us try to find some formula weaker than both 1A_1 and 2A_2. The strongest one we may find that is still GR(1) compliant is GF(a∨b)GF(a b). The relationship is visualised in Figure 7, and the resulting specification φ′ is illustrated below: ⬇ 1 module CounterExample_v3_unrealisable 2 3 env boolean a; 4 env boolean b; 5 sys boolean c; 6 7 assumption -- a1 8 GF(a|b); 9 guarantee -- g1.1 10 G((!a&!b)|(!a&PREV(!b))->!c); 11 guarantee -- g1.2 12 G(a->c); 13 guarantee -- g2 14 G(PREV(b)&b->c); 15 guarantee -- g3 16 GF(c); Spectra Figure 8. Counter example specification repair 3 - UNREALISABLE We find, through verification, that this specification is no longer realisable, therefore requiring guarantee weakening for a complete repair. Therefore, we highlight using a clear example the danger of attempting to degrade our assumption set prematurely and excessively. ∎ A.2. Proof of soundness of baseline algorithm We prove Theorem 4.18 through the intermediate results stated in Lemmas A.1 and A.2 below. Lemma A.1 (Minimal Correction of Assumptions). Let Aτ⊆A_τ be the violation set induced by τ. Then: (i) τ⊧∖Aτ A_τ; (i) AτA_τ is minimal with respect to this property. Proof. Let A be a set of assumptions and let τ be a violation trace such that τ⊧̸τ . We show that the violation set Aτ⊆A_τ is the minimal set of assumptions whose removal yields a specification satisfied by τ. (i) Show that τ⊧∖Aτ A_τ. Assume, for contradiction, that τ⊧̸∖Aτ A_τ. Then there exists some assumption ai∈∖Aτa_i A_τ such that τ⊧̸aiτ a_i. By definition of the violation set, ai∈Aτa_i∈ A_τ, which contradicts the assumption that ai∈∖Aτa_i A_τ. Therefore, τ⊧∖Aτ A_τ. (i) Show that AτA_τ is minimal. Let A′⊂AτA ⊂ A_τ. Then there exists some assumption ai∈Aτa_i∈ A_τ such that ai∉A′a_i∉ A . Since ai∈Aτa_i∈ A_τ, by definition of the violation set we have τ⊧̸aiτ a_i. Consequently, τ⊧̸∖A′τ A , since aia_i remains in the degraded assumption set. Hence no strict subset of AτA_τ satisfies the required property, proving minimality. ∎ Lemma A.2 (Minimal Correction of Guarantees). Let =1uc,…,kucC=\G^uc_1,…,G^uc_k\ be the set of unrealisable cores of ⟨∖Aτ,⟩ A_τ,G , and let ℋmin()H_min(C) be a minimal hitting set of C. Then: (i) the specification ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) is realisable; (i) ℋmin()H_min(C) is minimal with respect to this property. Proof. (i) Show that ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) is realisable. Assume, for contradiction, that ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) is unrealisable. Then there exists some unrealisable subset ′⊆∖ℋmin()G _min(C) such that ⟨∖Aτ,′⟩ A_τ,G is unrealisable. Since ′G is unrealisable, it must contain some unrealisable core iuc∈G^uc_i . However, by definition of a hitting set, ℋmin()∩iuc≠∅H_min(C) ^uc_i≠ . Therefore, iuc⊈∖ℋmin()G^uc_i _min(C), contradicting the assumption that ′⊆∖ℋmin()G _min(C). Hence, ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) must be realisable. (i) Show that ℋmin()H_min(C) is minimal. Let ℋ′⊂ℋmin()H _min(C). Since ℋmin()H_min(C) is a minimal hitting set, there exists some unrealisable core iuc∈G^uc_i such that iuc∩ℋ′=∅G^uc_i = . Consequently, iuc⊆∖ℋ′G^uc_i . Since ⟨∖Aτ,iuc⟩ A_τ,G^uc_i is unrealisable, it follows that ⟨∖Aτ,∖ℋ′⟩ A_τ,G is also unrealisable. Therefore, no strict subset of ℋmin()H_min(C) is sufficient to restore realisability, proving minimality. Together, Properties (i) and (i) establish that ℋmin()H_min(C) is the minimal set of guarantees whose removal restores realisability of ⟨∖Aτ,∖ℋmin()⟩ A_τ,G _min(C) . ∎ From Lemmas A.1 and A.2, Theorem 4.18 follows directly. A.3. Finiteness of Semantic Equivalence Classes As part of our proof that the adaptation procedure in Algorithm 4 terminates, we propose the following theorem: Theorem A.3. The set ℱF of semantic equivalence classes of assertions over a finite set of Boolean variables X is finite. Proof. A formula φ over X defines a Boolean function: fφ:2→0,1.f_ :2^X→\0,1\. Since ||=n|X|=n, there are 2n2^n possible truth assignments, so there are: |f:2→0,1|=22n|\f:2^X→\0,1\\|=2^2^n Boolean functions. Two formulas φ,ψ ,ψ are semantically equivalent if and only if they define the same Boolean function, so: |ℱ|=22n,|F|=2^2^n, which is finite. ∎ A.3.1. Finiteness of Weaker Assertions Theorem A.4 (Finiteness of Weaker Assertions). Given a GR(1) specification ⟨A,G⟩ A,G over a finite set of Boolean variables X, the sets of semantically distinct weaker environment assumptions than A and weaker system guarantees than G are finite. Proof. A GR(1) assumption module A and guarantee module G each consist of: • Initial conditions: φinit\ ^init_i\ • Safety constraints: φjsafe\G ^safe_j\ • Liveness constraints: φklive\GF ^live_k\ where each φ is a propositional formula over the finite variable set X. By Theorem A.3, the set of semantically distinct propositional formulas over X is finite. Weaker assumptions correspond to replacements: ∀σ∈Σω:σ⊧A⟹σ⊧A′,∀σ∈ ^ω:σ A σ A , and weaker guarantees correspond to: ∀σ∈Σω:σ⊧G′⟹σ⊧G.∀σ∈ ^ω:σ G σ G. These correspond to semantic weakening of each φ . Since: • There are finitely many semantically distinct propositional formulas. • Each GR(1) module has a finite number of formula slots. The total number of semantically distinct weakenings of A and G is finite. ∎ A.4. Soundness of Algorithm To show our algorithm is sound, we prove the following theorem: Theorem A.5 (Termination of Algorithm 4). Given the tuple (φ,τ)( ,τ), where φ=⟨,⟩ = ,G is a realisable specification, and τ∈Σ∗τ∈ ^* is a violation trace of the specification, the adapt(φ,τ) adapt( ,τ) method will always terminate, with the solution φ′=⟨′,′⟩ = ,G , conforming to the properties at Definition 4.2. We show in Section 5 that an immediate solution exists for the discovery of a specification φ′=⟨′,⟩ = ,G as a solution to the assumption-only reality integration problem. Therefore, to prove Theorem A.5, we only need to prove the following lemma: Lemma A.6 (Termination for the second half of Algorithm 4 using Guarantee Weakening). Given the tuple (φ′,τ)( ,τ), where φ′=⟨′,⟩ = ,G is an unrealisable specification, and τ∈Σ∗τ∈ ^* is a violation trace of specification φ , the Guarantee Weakening task of the adapt(φ,τ) adapt( ,τ) method will always terminate, with the solution φ′=⟨′,′⟩ = ,G , conforming to the properties at Definition 4.2. Proof. We consider, without loss of generality, an intermediary step within the Guarantee Weakening problem, and use the structure of the Counter-Play Guided GW problem at 5.11: (φ′,τ,cts)( ,τ,cts) Since our solution space is composed of specifications whose guarantees are strictly weaker than φ′ , we know that our solution space is always finite, as proven for Theorem A.4. Therefore, in order to show termination, we will prove the following lemma: Lemma A.7. the set of solutions of the intermediate problem is always strictly larger than the set of solutions for any future intermediate problem: ∀φ′∈AdaptGW(φ,τ,cts).∀ct′∈Σ∗ s.t. ct′⊧′ and ct′⊧̸′ ∀ ∈ Adapt_GW( ,τ,cts).∀ ct ∈ ^* s.t. ct and ct AdaptGW(φ′,τ,cts++ct′)⊂AdaptGW(φ,τ,cts) Adapt_GW( ,τ,cts+ -5.59721pt+ 3.44444ptct )⊂ Adapt_GW( ,τ,cts) Proof. Take an arbitrary φ′=⟨′,′⟩ = ,G such that: φ′∈AdaptGW(φ′,τ,cts++ct′) ∈ Adapt_GW( ,τ,cts+ -5.59721pt+ 3.44444ptct ) If φ′ is realisable, the solution is found and there is no need for further iteration, so without loss of generality, let us assume φ′ is unrealisable. Then, since it is a solution of a CTGW problem, the following properties hold, as per Definition 5.11: (1) τ⊧′τ (2) ∀σ∈Σω∀σ∈ ^ω, σ⊧′→σ⊧′σ →σ (3) ∀τc∈cts++ct∀τ^c∈ cts+ -5.59721pt+ 3.44444ptct, τc⊧′τ^c Due to property 3, it also holds that ∀τc∈cts,τc⊧′∀τ^c∈ cts,τ^c Furthermore, due to property 2, and the equivalent property of φ′∈AdaptGW(φ′,τ,cts++ct′) ∈ Adapt_GW( ,τ,cts+ -5.59721pt+ 3.44444ptct ), we can extract the following property: ∀σ∈Σω, σ⊧→σ⊧′∀σ∈ ^ω, σ →σ Therefore, alongside property 1, we have shown that φ′∈AdaptGW(φ,τ,cts) ∈ Adapt_GW( ,τ,cts) Which proves that AdaptGW(φ′,τ,cts++ct′)⊆AdaptGW(φ,τ,cts).Adapt_GW( ,τ,cts+ -5.59721pt+ 3.44444ptct ) Adapt_GW( ,τ,cts). However, since we know ct′⊧̸′ct , but ct′⊧′ct , we conclude that φ′∉AdaptGW(φ′,τ,cts++ct′), ∈ Adapt_GW( ,τ,cts+ -5.59721pt+ 3.44444ptct ), which proves Lemma A.7 ∎ The proof above, in turn, proves Lemma A.6. ∎ Appendix B Code B.1. Helper Functions Algorithm 5 Filter Minimal Formulas 1: function filterMinimal(formulasformulas) 2: filteredFormulas←formulas[0]filteredFormulas← formulas[0] 3: for formula∈formulas[1:]formula∈ formulas[1:] do 4: isMinimal←⊤isMinimal← 5: for filteredFormula∈filteredFormulasfilteredFormula∈ filteredFormulas do 6: if formula≺filteredFormulaformula filteredFormula then 7: remove(filteredFormulas,filteredFormula) remove(filteredFormulas,filteredFormula) 8: isMinimal←⊥isMinimal← 9: break; 10: end if 11: end for 12: if isMinimalisMinimal then 13: add(filteredFormulas,formula) add(filteredFormulas,formula) 14: end if 15: end for 16: return filteredFormulasfilteredFormulas 17: end function Algorithm 6 Merging Preferred Specifications 1: function merge(specsspecs) 2: mergedSpec←⟨⊤,⊤⟩mergedSpec← , 3: for spec∈specsspec∈ specs do 4: mergedSpec.←mergedSpec.∪spec.mergedSpec.A← mergedSpec.A∪ spec.A 5: mergedSpec.←mergedSpec.∪spec.mergedSpec.G← mergedSpec.G∪ spec.G 6: end for 7: if isRealisable(mergedSpec) isRealisable(mergedSpec) then 8: return [mergedSpec][mergedSpec] 9: else 10: return trivialGW(mergedSpec) trivialGW(mergedSpec) 11: end if 12: end function Appendix C Case Studies C.1. Size of Specifications There are 5 specifications we use in our evaluation, each specification is realisable, and has a pairing of a violation trace. We present in Table 6 the sizes of the specifications in a similar way to (Firman et al., 2020). The sizes are given as follows: • |||X| - the number of environment variables • |Ie||I^e| - the number of environment invariants • |Le||L^e| - the number of justice assumptions • |||Y| - the number of system variables • |Is||I^s| - the number of system invariants • |Ls||L^s| - the number of justice guarantees Case Study Assumptions Guarantees |||X| |Ie||I^e| |Le||L^e| |||Y| |Is||I^s| |Ls||L^s| arbiter 3 1 0 2 4 0 lift 4 11 0 3 6 0 minepump 2 2 0 1 2 0 traffic single 3 2 1 1 1 1 traffic updated 3 4 1 2 4 0 Table 6. Specification sizes C.2. Specifications & Violation Traces We showcase below the exact case studies evaluated in this work in pairs of: (1) The GR(1) specification, written in Spectra, using Dwyer patterns to represent GR(1) equivalent patterns that are not syntactically allowed by Spectra (e.g. G(a→F(b))G(a→ F(b)) will be represented in Spectra as pRespondsToS(a,b)pRespondsToS(a,b)); (2) The violation trace that intentionally violates one (or multiple) environment assumptions. C.2.1. Arbiter ⬇ 1 module Arbiter 2 3 env boolean a; 4 env boolean r1; 5 env boolean r2; 6 sys boolean g1; 7 sys boolean g2; 8 9 assumption -- a_always 10 alw(a); 11 guarantee -- guarantee1 12 pRespondsToS(r1,g1); -- equiv to G(r1->F(g1)); 13 guarantee -- guarantee2 14 pRespondsToS(r2,g2); -- equiv to G(r2->F(g2)); 15 guarantee -- guarantee3 16 alw(!a->!g1&!g2); 17 guarantee -- guarantee4 18 alw(!g1 | !g2); 19 20 pattern pRespondsToS(s, p) 21 var S0, S1 state; 22 23 // initial assignments: initial state 24 ini state=S0; 25 26 // safety this and next state 27 alw ((state=S0 & ((!s) | (s & p)) & next(state=S0)) | 28 (state=S0 & (s & !p) & next(state=S1)) | 29 (state=S1 & (p) & next(state=S0)) | 30 (state=S1 & (!p) & next(state=S1))); 31 32 // equivalence of satisfaction 33 alwEv (state=S0); 34 Spectra τ=[(¬a,¬r1,¬r2,¬g1,¬g2)]τ=[( [rgb]1,0,0 a, r1, r2, [rgb]0,0.6,0 g1, g2)] Figure 9. Arbiter case study C.2.2. Lift ⬇ 1 module Lift 2 3 env boolean b1; 4 env boolean b2; 5 env boolean b3; 6 env boolean c; 7 sys boolean f1; 8 sys boolean f2; 9 sys boolean f3; 10 11 assumption -- initial_assumptions 12 !b1 & !b2 & !b3; 13 assumption -- button1_off_at_floor1 14 alw(b1 & f1 -> next(!b1)); 15 assumption -- button2_off_at_floor2 16 alw(b2 & f2 -> next(!b2)); 17 assumption -- button3_off_at_floor3 18 alw(b3 & f3 -> next(!b3)); 19 assumption -- button1_stays_on 20 alw(b1 & !f1 & !c -> next(b1)); 21 assumption -- button2_stays_on 22 alw(b2 & !f2 & !c -> next(b2)); 23 assumption -- button3_stays_on 24 alw(b3 & !f3 & !c -> next(b3)); 25 assumption -- one_floor 26 alw(f1 | f2 | f3); 27 assumption -- one_floor_only1 28 alw(f1 -> !f2 & !f3); 29 assumption -- one_floor_only2 30 alw(f2 -> !f1 & !f3); 31 assumption -- one_floor_only3 32 alw(f3 -> !f1 & !f2); 33 assumption -- not_all_buttons_on 34 alw(!b1 | !b2 | !b3); 35 36 guarantee -- initial_guarantees 37 f1 & !f2 & !f3; 38 guarantee -- move_one_max1 39 alw(f1 -> (next(f1) & !b2 & !b3) | (next(f2) & b2) | (next(f2) & b3) | next(f1) & c); 40 guarantee -- move_one_max2 41 alw(f2 -> (next(f1) & b1) | (next(f2) & !b1 & !b3) | (next(f3) & b3) | next(f2) & c); 42 guarantee -- move_one_max3 43 alw(f3 -> (next(f3) & !b1 & !b2) | (next(f2) & b1) | (next(f2) & b2) | next(f3) & c); 44 guarantee -- button1_answered 45 pRepondsToS(b1, (f1 | c)); -- equivalent to G(b1 -> F(f1 | c)); 46 guarantee -- button2_answered 47 pRepondsToS(b2, (f2 | c)); -- equivalent to G(b2 -> F(f2 | c)); 48 guarantee -- button3_answered 49 pRepondsToS(b3, (f3 | c)); -- equivalent to G(b3 -> F(f3 | c)); 50 51 -- pattern omitted Spectra τ=[(¬b1,¬b2,¬b3,c,f1,¬f2,¬f3),(b1,b2,b3,¬c,f1,¬f2,¬f3)]τ=[( [rgb]1,0,0 b1, b2, b3,c, [rgb]0,0.6,0f1, f2, f3),( [rgb]1,0,0b1,b2,b3, c, [rgb]0,0.6,0f1, f2, f3)] Figure 10. Lift case study C.2.3. Minepump ⬇ 1 module Minepump 2 3 env boolean highwater; 4 env boolean methane; 5 sys boolean pump; 6 7 assumption -- initial_assumption 8 !highwater & !methane; 9 assumption -- assumption1 10 alw(PREV(pump)&pump->next(!highwater)); 11 assumption -- assumption2 12 alw(!highwater|!methane); 13 guarantee -- initial_guarantee 14 !pump; 15 guarantee -- guarantee1 16 alw(highwater->next(pump)); 17 guarantee -- guarantee2 18 alw(methane->next(!pump)); Spectra τ=[(¬highwater,¬methane,¬pump),(highwater,methane,¬pump)]τ=[( [rgb]1,0,0 highwater, methane, [rgb]0,0.6,0 pump),( [rgb]1,0,0highwater,methane, [rgb]0,0.6,0 pump)] Figure 11. Minepump case study C.2.4. Traffic Single ⬇ 1 module TrafficE2 2 3 env boolean car; 4 env boolean emergency; 5 env boolean police; 6 sys boolean green; 7 8 assumption -- car_idle_when_red 9 alw(car & !green -> next(car)); 10 assumption -- car_moves_when_green 11 alw(car & green -> next(!car)); 12 assumption -- not_police_often 13 alwEv(!police); 14 guarantee -- green_often 15 pRepondsToS(car,green); -- equivalent to G(car -> F(green)); 16 guarantee -- no_car_often 17 alwEv(!car); 18 19 -- pattern omitted Spectra τ=[(car,¬emergency,police,green),(car,¬emergency,¬police,¬green)]τ=[( [rgb]1,0,0car, emergency,police, [rgb]0,0.6,0green),( [rgb]1,0,0car, emergency, police, [rgb]0,0.6,0 green)] Figure 12. Traffic single case study C.2.5. Traffic Updated ⬇ 1 module TrafficE2 2 3 env boolean carA; 4 env boolean carB; 5 env boolean emergency; 6 sys boolean greenA; 7 sys boolean greenB; 8 9 assumption -- carA_idle_when_red 10 alw(carA & !greenA -> next(carA)); 11 assumption -- carB_idle_when_red 12 alw(carB & !greenB -> next(carB)); 13 assumption -- carA_moves_when_green 14 alw(carA & greenA -> next(!carA)); 15 assumption -- carB_moves_when_green 16 alw(carB & greenB -> next(!carB)); 17 assumption -- no_emergency_often 18 alwEv(!emergency); 19 20 guarantee -- lights_not_both_red 21 alw(!greenA | !greenB); 22 guarantee -- carA_leads_to_greenA 23 pRespondsToS(carA,greenA); -- equiv to G(carA -> F(greenA)); 24 guarantee -- carB_lead_to_greenB 25 pRespondsToS(carB,greenB); -- equiv to G(carB -> F(greenB)); 26 guarantee -- red_when_emergency 27 alw(emergency -> !greenA & !greenB); 28 29 -- pattern omitted Spectra τ=[ τ=[ (carA,carB,emergency,¬greenA,¬greenB), ( [rgb]1,0,0carA,carB,emergency, [rgb]0,0.6,0 greenA, greenB), (¬carA,¬carB,¬emergency,¬greenA,¬greenB)] ( [rgb]1,0,0 carA, carB, emergency, [rgb]0,0.6,0 greenA, greenB)] Figure 13. Traffic updated case study C.3. Trivial Solutions We showcase below the trivial solutions for each case study. C.3.1. Arbiter ⬇ 1 module Arbiter 2 3 env boolean a; 4 sys boolean g1; 5 sys boolean g2; 6 env boolean r1; 7 env boolean r2; 8 9 guarantee -- guarantee1_1 10 pRespondsToS(r1=true,g1=true); -- equivalent to G((r1->F(g1))); 11 12 guarantee -- guarantee2_1 13 pRespondsToS(r2=true,g2=true); -- equivalent to G((r2->F(g2))); 14 15 guarantee -- guarantee4 16 alw((g1=false|g2=false)); 17 18 -- pattern omitted Spectra C.3.2. Minepump ⬇ 1 module Minepump 2 3 env boolean highwater; 4 env boolean methane; 5 sys boolean pump; 6 7 8 assumption -- initial_assumption 9 (highwater=false&methane=false); 10 11 guarantee -- initial_guarantee 12 pump=false; 13 14 guarantee -- guarantee1_1 15 alw((highwater=true->next(pump=true))); 16 17 assumption -- assumption1_1 18 alw(((PREV(pump=true)&pump=true)->next(highwater=false))); Spectra ⬇ 1 module Minepump 2 3 env boolean highwater; 4 env boolean methane; 5 sys boolean pump; 6 7 8 assumption -- initial_assumption 9 (highwater=false&methane=false); 10 11 guarantee -- initial_guarantee 12 pump=false; 13 14 guarantee -- guarantee2_1 15 alw((methane=true->next(pump=false))); 16 17 assumption -- assumption1_1 18 alw(((PREV(pump=true)&pump=true)->next(highwater=false))); Spectra C.3.3. Lift ⬇ 1 module Lift 2 3 env boolean b1; 4 env boolean b2; 5 env boolean b3; 6 env boolean c; 7 sys boolean f1; 8 sys boolean f2; 9 sys boolean f3; 10 11 12 assumption -- initial_assumptions 13 ((b1=false&b2=false)&b3=false); 14 15 assumption -- button1_off_at_floor1 16 alw(((b1=true&f1=true)->next(b1=false))); 17 18 assumption -- button2_off_at_floor2 19 alw(((b2=true&f2=true)->next(b2=false))); 20 21 assumption -- button3_off_at_floor3 22 alw(((b3=true&f3=true)->next(b3=false))); 23 24 assumption -- button1_stays_on 25 alw((((b1=true&f1=false)&c=false)->next(b1=true))); 26 27 assumption -- button2_stays_on 28 alw((((b2=true&f2=false)&c=false)->next(b2=true))); 29 30 assumption -- button3_stays_on 31 alw((((b3=true&f3=false)&c=false)->next(b3=true))); 32 33 guarantee -- initial_guarantees 34 ((f1=true&f2=false)&f3=false); 35 36 assumption -- one_floor 37 alw(((f1=true|f2=true)|f3=true)); 38 39 assumption -- one_floor_only1 40 alw((f1=true->(f2=false&f3=false))); 41 42 assumption -- one_floor_only2 43 alw((f2=true->(f1=false&f3=false))); 44 45 assumption -- one_floor_only3 46 alw((f3=true->(f1=false&f2=false))); 47 48 guarantee -- move_one_max1 49 alw((f1=true->(((((next(f1=true)&b2=false)&b3=false)|(next(f2=true)&b2=true))|(next(f2=true)&b3=true))|(next(f1=true)&c=true)))); 50 51 guarantee -- move_one_max2 52 alw((f2=true->((((next(f1=true)&b1=true)|((next(f2=true)&b1=false)&b3=false))|(next(f3=true)&b3=true))|(next(f2=true)&c=true)))); 53 54 guarantee -- move_one_max3 55 alw((f3=true->(((((next(f3=true)&b1=false)&b2=false)|(next(f2=true)&b1=true))|(next(f2=true)&b2=true))|(next(f3=true)&c=true)))); 56 57 guarantee -- button1_answered 58 pRespondsToS(b1=true,(f1=true|c=true)); -- equivalent to G((b1->F((f1|c)))); 59 60 guarantee -- button2_answered 61 pRespondsToS(b2=true,(f2=true|c=true)); -- equivalent to G((b2->F((f2|c)))); 62 63 guarantee -- button3_answered 64 pRespondsToS(b3=true,(f3=true|c=true)); -- equivalent to G((b3->F((f3|c)))); 65 66 -- pattern omitted Spectra C.3.4. Traffic Single ⬇ 1 module TrafficE2 2 3 env boolean car; 4 env boolean emergency; 5 sys boolean green; 6 env boolean police; 7 8 9 guarantee -- green_often 10 pRespondsToS(car=true,green=true); -- equivalent to G((car->F(green))); 11 12 assumption -- not_police_often 13 alwEv(police=false); 14 15 assumption -- car_idle_when_red 16 alw(((car=true&green=false)->next(car=true))); 17 18 -- pattern omitted Spectra C.3.5. Traffic Updated ⬇ 1 module TrafficE2 2 3 env boolean carA; 4 env boolean carB; 5 env boolean emergency; 6 sys boolean greenA; 7 sys boolean greenB; 8 9 10 assumption -- no_emergency_often 11 alwEv(emergency=false); 12 13 guarantee -- lights_not_both_red 14 alw((greenA=false|greenB=false)); 15 16 guarantee -- carA_leads_to_greenA 17 pRespondsToS(carA=true,greenA=true); -- equivalent to G((carA->F(greenA))); 18 19 guarantee -- carB_lead_to_greenB 20 pRespondsToS(carB=true,greenB=true); -- equivalent to G((carB->F(greenB))); 21 22 guarantee -- red_when_emergency 23 alw((emergency=true->(greenA=false&greenB=false))); 24 25 assumption -- carA_moves_when_green 26 alw(((carA=true&greenA=true)->next(carA=false))); 27 28 assumption -- carB_moves_when_green 29 alw(((carB=true&greenB=true)->next(carB=false))); 30 31 -- pattern omitted Spectra C.4. Preferred Learned Solutions We showcase below the solutions discovered when using Algorithm 4 for each case study. C.4.1. Arbiter ⬇ 1 module Arbiter 2 3 env boolean a; 4 sys boolean g1; 5 sys boolean g2; 6 env boolean r1; 7 env boolean r2; 8 9 10 guarantee -- guarantee1 11 pRespondsToS(r1=true,g1=true); -- equivalent to G((r1->F(g1))) 12 13 guarantee -- guarantee2 14 pRespondsToS(r2=true,g2=true); -- equivalent to G((r2->F(g2))) 15 16 guarantee -- guarantee3 17 alw((a=false->(g1=false&g2=false))); 18 19 guarantee -- guarantee4 20 alw((g1=false|g2=false)); 21 22 assumption -- a_always_0 23 alwEv(a=true); 24 25 assumption -- a_always_1 26 alw((a=true|(g1=false&g2=false&r1=false&r2=false))); Spectra C.4.2. Minepump ⬇ 1 module Minepump 2 3 env boolean highwater; 4 env boolean methane; 5 sys boolean pump; 6 7 8 assumption -- initial_assumption 9 (highwater=false&methane=false); 10 11 assumption -- assumption1_1 12 alw(((PREV(pump=true)&pump=true)->next(highwater=false))); 13 14 assumption -- assumption2_1 15 alw((pump=true->(highwater=false|methane=false))); 16 17 guarantee -- initial_guarantee 18 pump=false; 19 20 guarantee -- guarantee1_1_0 21 alw((highwater=true->next(pump=true))); 22 23 guarantee -- guarantee2_1_0 24 alw((methane=true->(next(pump=false)|next(methane=true)&next(highwater=true)))); 25 26 guarantee -- guarantee2_1_8 27 pRespondsToS(methane=true,next(pump=false)); --equivalent to G(methane->X(!pump)) 28 29 -- pattern omitted Spectra C.4.3. Lift ⬇ 1 module Lift 2 3 env boolean b1; 4 env boolean b2; 5 env boolean b3; 6 env boolean c; 7 sys boolean f1; 8 sys boolean f2; 9 sys boolean f3; 10 11 12 assumption -- initial_assumptions 13 ((b1=false&b2=false)&b3=false); 14 15 assumption -- button1_off_at_floor1 16 alw(((b1=true&f1=true)->next(b1=false))); 17 18 assumption -- button2_off_at_floor2 19 alw(((b2=true&f2=true)->next(b2=false))); 20 21 assumption -- button3_off_at_floor3 22 alw(((b3=true&f3=true)->next(b3=false))); 23 24 assumption -- button1_stays_on 25 alw((((b1=true&f1=false)&c=false)->next(b1=true))); 26 27 assumption -- button2_stays_on 28 alw((((b2=true&f2=false)&c=false)->next(b2=true))); 29 30 assumption -- button3_stays_on 31 alw((((b3=true&f3=false)&c=false)->next(b3=true))); 32 33 guarantee -- initial_guarantees 34 ((f1=true&f2=false)&f3=false); 35 36 assumption -- one_floor 37 alw(((f1=true|f2=true)|f3=true)); 38 39 assumption -- one_floor_only1 40 alw((f1=true->(f2=false&f3=false))); 41 42 assumption -- one_floor_only2 43 alw((f2=true->(f1=false&f3=false))); 44 45 assumption -- one_floor_only3 46 alw((f3=true->(f1=false&f2=false))); 47 48 guarantee -- move_one_max1 49 alw((f1=true->(((((next(f1=true)&b2=false)&b3=false)|(next(f2=true)&b2=true))|(next(f2=true)&b3=true))|(next(f1=true)&c=true)))); 50 51 guarantee -- move_one_max2 52 alw((f2=true->((((next(f1=true)&b1=true)|((next(f2=true)&b1=false)&b3=false))|(next(f3=true)&b3=true))|(next(f2=true)&c=true)))); 53 54 guarantee -- move_one_max3 55 alw((f3=true->(((((next(f3=true)&b1=false)&b2=false)|(next(f2=true)&b1=true))|(next(f2=true)&b2=true))|(next(f3=true)&c=true)))); 56 57 guarantee -- button1_answered 58 pRespondsToS(b1=true, (f1=true|c=true)); -- equivalent to G((b1->F((f1|c)))); 59 60 guarantee -- button2_answered 61 pRespondsToS(b2=true, (f2=true|c=true)); -- equivalent to G((b2->F((f2|c)))); 62 63 guarantee -- button3_answered 64 pRespondsToS(b3=true, (f3=true|c=true)); -- equivalent to G((b3->F((f3|c)))); 65 66 assumption -- not_all_buttons_on_0 67 alw((c=true->((b1=false|b2=false)|b3=false))); 68 69 assumption -- not_all_buttons_on_1 70 alw((f1=false->((b1=false|b2=false)|b3=false))); 71 72 -- pattern omitted Spectra C.4.4. Traffic Single ⬇ 1 module TrafficE2 2 3 env boolean car; 4 env boolean emergency; 5 sys boolean green; 6 env boolean police; 7 8 9 guarantee -- green_often 10 alw((car=true->F(green=true))); 11 12 guarantee -- no_car_often 13 alwEv(car=false); 14 15 assumption -- not_police_often 16 alwEv(police=false); 17 18 assumption -- car_idle_when_red 19 alw(((car=true&green=false)->next(car=true))); 20 21 assumption -- car_moves_when_green_0 22 alw((((car=true&green=true)&police=false)->next(car=false))); 23 24 assumption -- car_moves_when_green_1 25 pRespondsToS(car=true&green=true,next(car=false)); -- equivalent to G(((car&green)->F(next(!car)))); 26 27 -- pattern omitted Spectra C.4.5. Traffic Updated ⬇ 1 module TrafficE2 2 3 env boolean carA; 4 env boolean carB; 5 env boolean emergency; 6 sys boolean greenA; 7 sys boolean greenB; 8 9 assumption -- no_emergency_often 10 alwEv(emergency=false); 11 12 guarantee -- lights_not_both_red 13 alw((greenA=false|greenB=false)); 14 15 guarantee -- carA_leads_to_greenA 16 pRespondsToS(carA=true,greenA=true); -- equivalent to G((carA->F(greenA))); 17 18 guarantee -- carB_lead_to_greenB 19 pRespondsToS(carB=true,greenB=true); -- equivalent to G((carB->F(greenB))); 20 21 guarantee -- red_when_emergency 22 alw((emergency=true->(greenA=false&greenB=false))); 23 24 assumption -- carA_idle_when_red_0 25 alw((((carA=true&greenA=false)&carB=false)->next(carA=true))); 26 27 assumption -- carB_idle_when_red_1 28 alw((((carB=true&greenB=false)&carA=false)->next(carB=true))); 29 30 assumption -- carA_moves_when_green 31 alw(((carA=true&greenA=true)->next(carA=false))); 32 33 assumption -- carB_moves_when_green 34 alw(((carB=true&greenB=true)->next(carB=false))); 35 36 assumption -- carB_idle_when_red_3 37 alw(((carB=true&greenB=false)->(next(carB=true)|next(carA=false)))); 38 39 assumption -- carA_idle_when_red_2 40 alw(((carA=true&greenA=false)->(next(carA=true)|greenB=false))); 41 42 assumption -- carA_idle_when_red_3 43 alw(((carA=true&greenA=false)->(next(carA=true)|next(emergency=false)))); 44 45 assumption -- carB_idle_when_red_4 46 alw(((carB=true&greenB=false)->(next(carB=true)|greenA=false))); 47 48 assumption -- carB_idle_when_red_5 49 pRespondsToS(carB=true&greenB=false,next(carB=true)); -- equivalent to G(((carB&!greenB)->F(next(carB)))); 50 51 assumption -- carA_idle_when_red_4 52 alw(((carA=true&greenA=false)->(next(carA=true)|next(carB=false)))); 53 54 assumption -- carA_idle_when_red_5 55 pRespondsToS(carA=true&greenA=false,next(carA=true)); -- equivalent to G(((carA&!greenA)->F(next(carA)))); 56 57 assumption -- carA_idle_when_red 58 alw((((carA=true&greenA=false)&emergency=false)->next(carA=true))); 59 60 -- pattern omitted Spectra