PaperlayerView exact revision on arXiv

Source-linked AI summary

Learning to adapt GR(1) specifications through degradation

Tiberiu-Andrei Georgescu, Dalal Alrajeh, Sebastian Uchitel

arXiv:2609.12231v1cs.SEcs.AIcs.LO

TL;DR

When GR(1) controllers encounter environment behavior outside their assumptions, existing approaches generally lack precise control over guarantee degradation. This paper uses oracle-guided inductive synthesis and preference criteria to adapt specifications, reporting higher-preference solutions than trivial alternatives across case studies, sometimes without weakening guarantees.

  • Problem

    Under assumption violations, prior robustness techniques generally lack precise control over which guarantees degrade and by how much.

    Source: §1 · p. 1

  • Method

    The paper formalizes preferred adaptations and uses oracle-guided inductive synthesis to explore multiple realisable specification adaptations.

    Source: §1 · p. 2, §5.2.2 · p. 27

  • Results

    Across case studies, the learning-based solver finds more-preferred solutions than trivial alternatives; in Arbiter and Traffic Single, it avoids guarantee weakening.

    Source: §6.3 · p. 35

  • Takeaways & Limitations

    These case studies show that adaptation need not require guarantee weakening for the system to resume safe behavior.

    Source: §6.3 · p. 35

    The search may explore many candidate specifications, making the current methodology best suited to adaptations without hard computation-time constraints.

    Source: §6.3 · p. 35

Abstract

from arXiv · show

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

The paper formalizes adaptation of reactive specifications after assumption violations, incorporating observed environment behavior and modifying guarantees as needed to restore realisability. It develops criteria for preferring among alternative adaptations and introduces reduction- and learning-based algorithms.

1 Introduction

  • GR(1) enables polynomial-time synthesis, but when environmental assumptions are violated, controllers may behave arbitrarily and existing robustness methods offer limited control over guarantee degradation.Complex operational environments make accurate and complete assumptions difficult to construct, leaving controllers vulnerable to mismatches at runtime.Source: §1 · pp. 1–2
  • The paper formalizes adaptation under mismatches by incorporating newly observed environmental behavior into assumptions and modifying guarantees when needed to restore realisability.The approach considers a space of admissible adaptations rather than a single repaired specification.Source: §1 · p. 2
  • Across five literature case studies, the learning-based approach consistently outperforms specification reduction, with evaluation examining changes, tradeoffs, and preferences in adapted specifications.The reduction baseline drops violated assumptions and non-realisable guarantees.Source: §1 · pp. 2–3
  • The preference framework evaluates alternative realisable adaptations by specification preservation, retention of critical guarantees, and robustness to future assumption violations.Axioms guide heuristics in a learning-based algorithm that explores multiple candidate adaptations.Source: §1 · p. 2
  • The authors develop a specification-reduction algorithm and a formula-level inductive learning algorithm; both generate realisable specifications consistent with observed environment behavior.Formula-level degradation explores a richer space of candidate adaptations.Source: §1 · p. 2

2 Motivating Example

The arbiter example shows how an assumption violation can leave intended guarantees unenforced, while different realisable repairs preserve different amounts of the original specification. It motivates principled criteria for finding preferred adaptations that avoid unnecessary degradation.

2 Motivating Example

  • The arbiter must grant each requesting master access eventually, never grant both simultaneously, and withhold grants when the environment locks it; the model assumes it remains active.The case study considers two masters requesting access to an ARM Advanced High-Performance Bus.Source: §2 · p. 3
  • If the arbiter becomes inactive, violating the environment assumption, the controller is no longer obliged to satisfy its guarantees, even if its behavior remains operationally robust.The example trace has the environment deactivate the bus at the first time point.Source: §2 · p. 4
  • Prior repair weakens assumption_1 and guarantee_3 to ⊤, restoring realisability but preserving only a subset of the original guarantees.This repair also removes the influence of observable variable a from the specification, discarding meaningful behavior.Source: §2 · p. 4
  • Prematurely accepting the first feasible intermediate solution and restricting the solution space can prevent exploration of repairs that preserve more of the original specification.Addressing either limitation could increase the likelihood of finding such repairs.Source: §2 · p. 4
  • Weakening assumption_1 to □((g1 ∨ g2) → a) restores realisability without weakening guarantees, allowing deactivation only when neither requesting master has been granted access.This is an alternative repair available in the framework of.Source: §2 · p. 4
  • Replacing the invariant that the arbiter remains active with the justice property □♢a also restores realisability without degrading system guarantees [8].This allows the arbiter to become inactive temporarily, provided it eventually becomes active again; prior work did not explore this pattern.Source: §2 · p. 4
  • Because realisable adaptations can preserve the original specification unequally, the paper investigates repair preferences and methods for systematically discovering desirable candidates.The goal is to identify repairs that minimise unnecessary degradation, since prior approaches offer limited guidance when both assumptions and guarantees may change.Source: §2 · pp. 4–5

3 Background

This section introduces the formal foundations for the approach: LTL over traces, specification weakness, GR(1) specifications and synthesis games, and the notions of realisability, counter-strategies, and counter-plays.

3.1 Linear Temporal Logic over Infinite and Finite Traces

  • LTL evaluates temporal formulas on infinite traces of Boolean-variable states, while weak next, weak until, and weak eventually support finite-trace reasoning.Weak eventually allows a proposition to hold beyond a finite trace's horizon.Source: §3.1 · pp. 5–6
  • An LTL formula denotes its satisfying-trace language, and formulas are weaker when their languages admit more traces.Source: §3.1 · p. 6

3.2 Generalised Reactivity of Rank 1

  • GR(1) restricts attention to a tractable LTL fragment, organizing environment assumptions and system guarantees as initial conditions, transition constraints, and liveness goals.The paper notes that arbitrary LTL synthesis is doubly exponential, whereas GR(1) synthesis is polynomial in the game structure when the specification is realisable.Source: §3.2 · p. 7
  • The set representation treats assumptions and guarantees as individual formulas, enabling comparison and modification by removing or weakening specific constraints.A weaker assumption admits a larger set of traces.Source: §3.2 · pp. 8–9
  • GR(1) synthesis models interaction as a game in which the environment moves before the system, whose winning strategy must satisfy the specification against admissible environment behavior.Source: §3.2 · pp. 9–10
  • A GR(1) specification is realisable exactly when the system has a winning strategy; if it is unrealisable, the environment wins the corresponding game.The environment's strategy that forces a violation regardless of the system's behavior is called a counter-strategy.Source: §3.2 · p. 10
  • A counter-strategy forces every compliant play to violate the specification through an initial-condition, transition-relation, or liveness-guarantee failure.For the liveness case, the environment satisfies its assumptions infinitely often while the system fails at least one guarantee infinitely often.Source: §3.2 · pp. 10–11
  • Counter-strategies characterize sets of environment behaviors that force specification violations, and each infinite play compliant with one is a counter-play.A counter-play is defined as an infinite play compliant with the counter-strategy for an unrealisable GR(1) specification.Source: §3.2 · p. 11

4 Adaptation under Assumption Violations

This section develops adaptation of realisable specifications to admit observed environment violations while restoring realisability and preserving original intent. It defines criteria for comparing and combining candidate adaptations and presents a baseline degradation procedure, illustrated by examples where weakening a guarantee can preserve more intended behavior than removing formulas alone.

4 Adaptation under Assumption Violations

  • The baseline procedure based on specification-reduction operations is proved to produce valid adaptation solutions satisfying the section’s optimality criteria.Source: §4 · p. 11

4.1 Problem Definition

  • Adaptation must admit the observed violation trace, preserve previously allowed environment and system behaviours, and yield a realisable specification.The assumptions are weakened to admit the trace, while guarantees retain previously guaranteed behaviours; a solution that discards all guarantees is formally possible but uninformative.Source: §4.1 · pp. 11–12

4.2 Preference over Comparable Adaptations

  • Preference axioms provide principled comparisons of candidate adaptations and induce a partial order from which preferred solutions can be selected.Realisability alone does not determine which adaptation to choose.Source: §4.2 · p. 12

4.2.1 Reasoning about comparable specifications.

  • When comparing adaptations, stronger guarantees are preferred under equivalent assumptions, while stronger assumptions are preferred under equivalent guarantees to reduce overgeneralisation.If both assumptions and guarantees are stronger, the combined criterion also prefers that solution; aggressively weakening assumptions from limited observations can later force guarantee degradation.Source: §4.2.1 · pp. 13–15

4.2.2 Reasoning about Incomparable Adaptations.

  • Incomparable adaptations generally cannot be ordered without domain knowledge or external priorities, though a valid third solution may combine their assumptions while preserving their guarantees.The combined solution is preferred to both when it is realisable.Source: §4.2.2 · pp. 15–16

4.2.2 Reasoning about Incomparable Adaptations

  • When candidate assumption sets are incomparable but one guarantee set is stronger, combining the assumptions can yield a preferred adaptation preserving that stronger guarantee set.If guarantee sets are themselves incomparable, logical weakness alone cannot rank them; domain knowledge may distinguish them, so both candidates must remain available without it.Source: §4.2.2 · pp. 16–17

4.2.3 Extracting Preferred Specifications

  • Candidate adaptations may omit preferred solutions because combining their assumption sets can produce strictly preferred candidates.Taking the union of all candidate assumptions yields the most preferred assumption A∗; replacing each candidate’s assumptions with A∗ preserves validity and reduces preference comparisons to guarantee sets.Source: §4.2.3 · pp. 17–18

4.3 Baseline Adaptation Procedure

  • The baseline procedure removes assumptions violated by the trace and, if the resulting specification is unrealizable, removes a minimal hitting set of guarantees from its unrealisable cores.This computes optimal trivial degradations; multiple minimal hitting sets can produce multiple solutions.Source: §4.3 · pp. 19–20
  • The baseline degradation accepts the observed trace, restores realisability, and is minimal in the number of assumptions and guarantees removed.It removes trace-violated assumptions and, when needed, uses a minimal hitting set of unrealisable cores to select guarantees for removal.Source: §4.3 · pp. 19, 21

4.4 Case Study: Minepump

  • In the Minepump case study, simultaneous methane and dangerous water violates an assumption, leaving the synthesized controller’s correctness guarantees no longer assured.The case study uses this previously unmodelled behavior to motivate adapting the specification to observed environmental behavior.Source: §4.4 · p. 21

4.4.1 Baseline Adaptation Applied.

  • Removing assumption_1 after the violation trace makes the specification unrealizable and yields two optimal trivial adaptations, each dropping guarantee_1 or guarantee_2.The intermediate specification retains assumption_0 and assumption_2.Source: §4.4.1 · p. 22
  • The two removal-only solutions produce controllers that keep the pump continuously active or permanently inactive, illustrating the structural limits of formula removal.Removal cannot recover behaviors that remain compatible with the newly observed environment dynamics.Source: §4.4.1 · p. 22
  • Replacing □(highwater → pump) with □(highwater ∧ ¬methane → pump) remains realizable while preserving more intended behavior; an analogous weakening applies to φ1.The original guarantee cannot hold universally when highwater and methane can occur together, while the methane safety guarantee remains necessary.Source: §4.4.1 · p. 22

5 Learning Degradations

This section develops an OGIS-based approach to exploring formula-level specification degradations, using a preference criterion to find preferred realisable adaptations and degrading guarantees only when assumption adaptation does not restore realisability.

5.1 Syntactic Formula Weakening

  • Syntactic weakening modifies formula structure locally, extending the coarse-grained removal approach to express a wider range of behavioural degradations.The framework represents invariants as implications between DNF formulas and treats justice-goal degradation analogously, including response-style formulas.Source: §5.1 · p. 23

5.1.1 Types of Weakening.

  • Three operators weaken formulas by strengthening antecedents, adding consequent disjuncts, or converting invariants into response or justice properties.Antecedent weakening restricts when the consequent must hold; consequent weakening enlarges the satisfying behaviours; conversion relaxes an immediate obligation to eventual satisfaction.Source: §5.1.1 · pp. 24–25

5.1.2 Weakening Search Space.

  • The weakening search space comprises formulas obtainable through these operators, but the operators are neither exhaustive nor guaranteed to yield a globally optimal degradation.The procedure is intended to explore this space according to the preference framework.Source: §5.1.2 · p. 25

5.2 Specification Degradation via Formula Weakening

  • Formula-level weakening can retain more specification behaviour than removal by replacing formulas with weaker formulas rather than discarding them.The section frames this as a way to explore adaptations outside the restricted space reached by removal-based methods.Source: §5.2 · pp. 25–26
  • Adaptation composes assumption weakening to admit the observed violation trace with guarantee weakening to restore realisability.The implementation usually selects replacement formulas from the weakening search space.Source: §5.2 · p. 26

5.2.1 Learning Assumption Degradations.

  • Assumption adaptation weakens only assumptions violated by the trace; every such assumption admits a trace-satisfying weakening, though the resulting specification may remain unrealisable.The objective is to admit the observed trace while preserving as much of the original environment model as possible.Source: §5.2.1 · p. 26, §5.2 · p. 26, §5.2.2 · p. 27

5.2.2 Learning Guarantee Degradations.

  • Guarantee adaptation uses OGIS with counter-strategies and counter-plays as oracle feedback to iteratively weaken guarantees until the specification is realisable.Unlike classical monotonic learning, runtime adaptation may revisit earlier decisions as new traces arrive; counter-plays identify guarantees to weaken, and the loop may continue to the empty guarantee set in the worst case.Source: §5.2.2 · pp. 27–28

5.3 Synthesis of Preferred Degradations

  • Preferred degraded specifications preserve the strongest possible guarantees, with incomparable solutions allowed only when semantically unavoidable.Source: §5.3 · p. 29
  • Thorough exploration avoids missing preferred adaptations or converging on unnecessarily weak specifications, since different degradation paths can preserve different subsets of system behaviour.Source: §5.3 · p. 29
  • OGIS systematically explores syntactic weakenings under the preference ordering, returning preferred assumption adaptations when realisable and otherwise using counter-plays to guide iterative guarantee degradation.Source: §5.3 · p. 29
  • The queue empties after all relevant degradations are explored, every branch eventually reaches a realisable specification, and preferred solutions are then filtered and merged.Source: §5.3 · p. 29
  • Redundancy checks skip equivalent branches and intermediate specifications weaker than known solutions, reducing exploration while preserving completeness for preferred outputs.Source: §5.3 · p. 31

6 Evaluation

The evaluation compares learned and trivial degradations by their relative preference and usefulness, then assesses the learned method’s results and search cost across case studies.

6.1 Methodology

  • The evaluation tests whether each trivial solution has a preferred learned counterpart, using benchmark specifications paired with traces that violate their assumptions.The methods are guaranteed to produce satisfying degradations, so evaluation focuses on relative quality rather than correctness; the case studies are adapted from Buckworth et al.. Specifications are encoded in Spectra using SYNTECH tools, whose handling of response patterns permits the third syntactic degradation methodology despite the original realizability rules.Source: §6.1 · pp. 31–32

6.2 Experimental Results

  • In every case study, the learned degradation is preferred to the trivial solution(s); Arbiter and Traffic Single also avoid guarantee weakening entirely.Learned degradations retain stronger assumptions than trivial ones, reflecting targeted weakening of only the assumptions affected by the violation trace.Source: §6.2 · p. 32, Table 4 · p. 32
  • For Minepump, one learned solution is strictly preferable to both trivial solutions and has strictly stronger guarantees than either.Its assumptions are comparable to the trivial assumptions, while the learned assumptions are strictly stronger; this satisfies the preference criteria despite requiring guarantee degradation.Source: §6.2 · pp. 32–33, Figure 2 · p. 33

6.2.1 Discussion on scale.

  • Learning explores many realizable candidates before converging; preferred maxima number around 10 or fewer except in Minepump, and every case study yields one merged final specification.The discussion attributes the larger explored sets in complex cases to the traversal methodology, which can branch into several solutions and continuations from a discovered specification.Source: §6.2.1 · pp. 33–34

6.3 Summary

  • The learning method consistently produces more preferred solutions, but substantial candidate exploration makes it best suited to adaptations without hard time constraints.The authors identify heuristics that guide search more directly as a need for more time-constrained scenarios.Source: §6.3 · p. 35

7 Related Work

The work adapts specifications by syntactically degrading behaviour statements to handle environment violations while preserving as much of the original requirements as possible. It distinguishes this approach through a preference criterion for degraded specifications and highlights limitations in existing resilience and specification-weakness measures.

7 Related Work

  • The work extends syntactic degradation of GR(1) specifications by investigating which adapted specification is preferred, while focusing on behaviour statements rather than configuration changes [7].Its goal is to salvage as much of the original requirements as possible.Source: §7 · p. 35
  • Weakening environment assumptions can overfit observed behaviour and cause unnecessary guarantee degradation when the perceived and actual world models diverge.The paper relates this risk to learned or manually generated assumptions used to enable specific guarantees, illustrated in Section 4.2 and Figure 1.Source: §7 · p. 35
  • Cavezza et al.’s refinement work [11] informs the preference criterion and search strategy; this work makes the assumption preference symmetric and extends minimal BFS search to guarantee degradation when necessary.Their refinement algorithm searches for minimal refinements in breadth-first order to find strong solutions early.Source: §7 · pp. 35–36
  • Unlike k-robustness, which assigns costs to specification errors, this work uses failures to learn an explicit specification without permitting deviations from it; (k,b)-resilience instead bounds glitches in duration and frequency.Because this work addresses environment errors that may occur infinitely often, it cannot frame its solutions in terms of (k,b)-sanity.Source: §7 · p. 36
  • Cavezza et al.’s weakness measure orders assumptions using a triple of entropy and Hausdorff dimensions, but its lexicographic form cannot aggregate multiple solutions, and quantitative comparison of non-nested LTL formulas remains an open gap.More broadly, specification quality has no trivial numerical representation.Source: §7 · p. 36
  • Runtime adaptation is also studied in requirements engineering [10] [14], using quantitative model checking to verify models against PCTL or similar requirements.Source: §7 · p. 36

8 Conclusion

The paper proposes preference-guided adaptation of GR(1) specifications after assumption violations, with a learning-based method that finds higher-quality degradations than a formula-removal baseline. It argues that robustness should include salvaging the widest set of goal-related behaviours under any environment condition, and identifies open challenges for practical adaptation.

8 Conclusion

  • Syntactic, inductive degradation discovers higher-quality solutions than formula removal for adapting a specification to an observed assumption-violating trace.The baseline removes the smallest amount of formulas, while the finer-grained algorithm iteratively degrades violating formulas until the specification is realisable and consistent with the observed behaviour.Source: §8 · pp. 36–37
  • The paper defines robustness as salvaging the widest set of goal-related behaviours with the strongest possible guarantees under any environment condition.It argues that preferring the strongest degraded specification differs from the conventional robustness logic of weakest assumptions and strongest guarantees across the most scenarios.Source: §8 · p. 37
  • Future work should further analyse the robustness notion and develop realistic scenarios to assess adaptation and retention of operational guarantees.The favourable adapted results under the paper’s preference criteria only hint at broader desirability in adaptive systems.Source: §8 · p. 37
  • The preference criteria intentionally treat maximal system guarantees equally, leaving guarantee discrimination to stakeholder input or future methods.Guarantee criticality has been studied under uncertainty; where guarantees are equally critical, prioritisation or weighting could be used.Source: §8 · p. 37
  • Industrial-scale guarantee sets may overwhelm stakeholders’ ability to specify priorities, motivating semantic formula meanings grounded in stakeholder principles [25].The specification and violation trace could provide context for an adaptive system to derive priorities reflecting clients, manufacturers, and legal requirements.Source: §8 · p. 37
  • The learning-based search is too time-consuming for runtime use, so the current methodology is limited to proactive adaptation unless guided by priorities and search heuristics.Counter-traces and counter-strategies can steer which guarantees are degraded; heuristics and methods such as Monte-Carlo Tree Search may help find realisable solutions in fewer steps.Source: §8 · pp. 37–38

A Proofs · A.1 Counter Example Disjunction of Assumptions

This appendix refutes the claim that two adaptation solutions with equivalent guarantees always admit a solution whose assumptions are their disjunction. Its counterexample shows that the disjunction may violate GR(1) syntax, while a weaker GR(1)-compliant assumption can make the specification unrealizable.

A.1 Counter Example Disjunction of Assumptions

  • The counterexample refutes the claim that solutions with equivalent guarantees always yield a solution using the disjunction of their assumptions.The proof only needs a case where that disjunction cannot be expressed with the syntactic structure of GR(1) assumptions.Source: §A.1 · p. 40
  • The example starts from a realisable specification whose assumption a1 is violated by the trace.The specification’s realisability was verified with the SYNTECH toolbox.Source: Figure 4 · p. 40
  • The two proposed repairs avoid guarantee degradation and use assumptions G(a∨b) and GF(a), respectively.Both repaired specifications were verified as realisable with the SYNTECH toolbox.Source: Figure 6 · p. 41, Figure 5 · p. 41
  • The disjunction G(a∨b) ∨ GF(a) cannot be meaningfully rewritten to satisfy GR(1) syntax, contradicting the claim.Source: §A.1 · p. 40, Figure 6 · p. 41
  • GF(a∨b) is the strongest GR(1)-compliant assumption found that is weaker than both proposed assumptions.The relationship among the repair proposals is visualised in Figure 7.Source: Figure 6 · p. 41, Figure 7 · p. 42
  • The specification using GF(a∨b) is unrealizable, so complete repair requires weakening guarantees and cautions against excessive assumption degradation.Source: Figure 6 · p. 41, Figure 8 · p. 42

A.2 Proof of soundness of baseline algorithm · A.3 Finiteness of Semantic Equivalence Classes · A.3.1 Finiteness of Weaker Assertions.

The appendix proves that the baseline removes exactly the assumptions violated by a trace and a minimal set of guarantees to restore realisability. It also establishes that, over finite Boolean variables, semantic assertion classes and weaker GR(1) assumptions and guarantees are finite.

A.2 Proof of soundness of baseline algorithm

  • Removing the trace’s violation set makes the remaining assumptions satisfied by that trace, and no strict subset of the violation set has this property.The violation set is therefore the minimal set of assumptions to remove for trace satisfaction.Source: §A.2 · p. 43
  • Removing a minimal hitting set of unrealisable cores from the guarantees restores realisability, and no strict subset of that set suffices.The result applies after removing the assumptions violated by the trace.Source: §A.2 · p. 43

A.3 Finiteness of Semantic Equivalence Classes

  • The set of semantic equivalence classes of assertions over a finite set of Boolean variables is finite.The proof proceeds by representing formulas as Boolean functions; semantic equivalence means defining the same function.Source: §A.3 · pp. 43–44
  • With n Boolean variables there are 2^n possible truth assignments, which bounds the number of Boolean functions and hence semantic assertion classes.Formulas that define the same Boolean function are semantically equivalent.Source: §A.3 · p. 44

A.3.1 Finiteness of Weaker Assertions.

  • For a GR(1) specification over finite Boolean variables, the sets of semantically distinct weaker environment assumptions and weaker system guarantees are finite.The theorem concerns weakenings of both specification modules.Source: §A.3.1 · p. 44
  • These weaker specifications are finite because each module has finitely many formula slots, each drawn from finitely many semantically distinct propositional formulas.Assumptions and guarantees are weakened by replacing formulas in their respective modules.Source: §A.3.1 · p. 44

A.4 Soundness of Algorithm … C Case Studies

The adaptation algorithm terminates with a solution satisfying Definition 4.2, and its guarantee-weakening stage terminates because its finite solution space strictly shrinks across iterations. Helper functions filter minimal formulas and merge preferred specifications, falling back to trivial guarantee weakening when the merged specification is unrealisable.

A.4 Soundness of Algorithm

  • The adapt method always terminates on a realisable specification and violation trace with a solution conforming to Definition 4.2.The proof reduces the result to termination of the guarantee-weakening stage.Source: §A.4 · p. 44
  • Guarantee weakening always terminates when applied to the unrealisable assumption-adjusted specification and violation trace, returning a solution conforming to Definition 4.2.This lemma supplies the termination result needed for the full adaptation algorithm.Source: §A.4 · pp. 44–45
  • The guarantee-weakening search terminates because its solution space is finite and each intermediate problem has a strictly larger solution set than any future one.The finite space consists of specifications whose guarantees are strictly weaker than the current specification.Source: §A.4 · p. 45

B.1 Helper Functions

  • The minimal-formula filter retains formulas not dominated by a strictly weaker formula in the filtered set.It removes a filtered formula when the candidate formula is strictly weaker, and adds the candidate only if no such removal occurs.Source: §B.1 · p. 46
  • The merge helper forms a specification by taking the unions of assumptions and guarantees from the preferred specifications.It initializes both components to true before accumulating the unions.Source: §B.1 · p. 46
  • The merge helper returns the merged specification if it is realisable; otherwise, it applies trivial guarantee weakening.The two outcomes are the branches of the helper's final realisability check.Source: §B.1 · p. 46

C.1 Size of Specifications

The evaluation uses five realisable specifications, each paired with a violation trace, and reports their sizes across environment and system variables, invariants, and justice conditions.

C.1 Size of Specifications

  • Five realisable specifications, each paired with a violation trace, form the evaluation set.Their sizes are presented in Table 6.Source: §C.1 · p. 46, Table 6 · p. 47
  • Environment specification size is described by the number of environment variables, invariants, and justice assumptions.Source: §C.1 · p. 46
  • System specification size is described by the number of system variables, invariants, and justice guarantees.Source: §C.1 · p. 47

C.2 Specifications & Violation Traces … C.2.5 Traffic Updated.

The appendix pairs each case study’s Spectra GR(1) specification with a trace that violates one or more environment assumptions, using Dwyer patterns for equivalent patterns that Spectra cannot express syntactically. It presents Arbiter, Lift, Minepump, and two Traffic case studies.

C.2 Specifications & Violation Traces

  • Each case study pairs a Spectra GR(1) specification with a trace that intentionally violates one or more environment assumptions, using Dwyer patterns for syntactic equivalents.For example, the pattern G(a→F(b)) is represented in Spectra as pRespondsToS(a,b).Source: §C.2 · p. 47
  • The Arbiter case study is presented as a specification-and-violation-trace example.The supplied figure caption identifies it as the Arbiter case study.Source: Figure 9 · p. 48

C.2.2 Lift.

  • The Lift specification assumes all three buttons start off and that each button switches off in the next state when pressed while the lift is at its corresponding floor.For button 1, it also assumes the button remains on in the next state when it is on, not at floor 1, and the lift is not closing.Source: §C.2.2 · p. 48
  • The Lift assumptions require at least one floor to be occupied, prohibit multiple occupied floors, and prohibit all three buttons being on.These conditions are stated in the assumptions for one_floor, one_floor_only1–3, and not_all_buttons_on.Source: §C.2.2 · p. 48
  • The supplied figures identify Lift and Minepump as case studies.The captions label Fig. 10 as Lift and Fig. 11 as Minepump.Source: Figure 10 · p. 49, Figure 11 · p. 49

C.2.4 Traffic Single.

  • The Traffic Single section includes a case study figure.The supplied caption labels Fig. 12 as the Traffic single case study.Source: Figure 12 · p. 50

C.2.5 Traffic Updated.

  • The Traffic Updated section includes a case study figure.The supplied caption labels Fig. 13 as the Traffic updated case study.Source: Figure 13 · p. 51

C.3 Trivial Solutions · C.3.2 Minepump.

The appendix showcases trivial solutions for each case study, including an Arbiter module and a Minepump specification listing assumptions and guarantees.

C.3 Trivial Solutions

  • The appendix presents trivial solutions for each case study.Source: §C.3 · p. 51
  • The Arbiter trivial solution is presented as one module named Arbiter.Source: §C.3 · p. 51

C.3.2 Minepump.

  • Minepump assumptions include button3_off_at_floor3 and button1_stays_on, button2_stays_on, and button3_stays_on.Source: §C.3.2 · p. 53
  • Minepump's guarantees include initial_guarantees and move_one_max1, move_one_max2, and move_one_max3.Source: §C.3.2 · p. 53
  • Minepump also lists assumptions named one_floor, one_floor_only1, one_floor_only2, and one_floor_only3.Source: §C.3.2 · p. 53
  • The specification also lists button1_answered, button2_answered, and button3_answered as guarantees.Source: §C.3.2 · p. 53

C.4 Preferred Learned Solutions

The section presents preferred solutions discovered with Algorithm 4 for the case studies. The excerpts show response guarantees in Arbiter and Traffic Single, and both vehicle guarantees and a conditional persistence assumption in Traffic Updated.

C.4.1 Arbiter

  • Arbiter’s preferred solution includes response guarantees for r1 and r2, alongside assumptions named button2_stays_on and button3_stays_on.Source: §C.4 · pp. 55, 57

C.4.4 Traffic Single

  • Traffic Single lists green_often and no_car_often guarantees, with a response condition requiring a car to eventually move off when it is on and the light is green.Source: §C.4 · p. 58

C.4.5 Traffic Updated

  • Traffic Updated lists carA- and carB-to-green response guarantees, as well as a red_when_emergency guarantee.Source: §C.4 · p. 59
  • Traffic Updated also includes an assumption that carA eventually remains true when carA is true and greenA is false.Source: §C.4 · p. 59
Loading 2609.12231v1…