pith. sign in

arxiv: 2604.24540 · v1 · submitted 2026-04-27 · 💻 cs.LO

Counterexample-Guided Interval Weakening

Ben M. Andrew , Louise A. Dennis , Michael Fisher , Marie Farrell This is my paper

Pith reviewed 2026-05-08 01:16 UTC · model grok-4.3

classification 💻 cs.LO
keywords counterexample-guidedinterval weakeningMetric Temporal LogicMTLtiming specificationsformal verificationmodel checkingsystem degradation
0
0 comments X

The pith

A counterexample-guided algorithm automatically weakens timing intervals in timed logic specifications to ensure they hold for a given system while preserving logical structure.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces CEGIW, an algorithm that iteratively uses counterexamples from model checking to relax the numeric bounds on timing intervals in Metric Temporal Logic formulas. This addresses situations where systems degrade over time and original strict timing requirements no longer hold, but looser ones do. If the method works, it allows automatic adjustment of specifications without changing their core logic, keeping them useful for verification. The authors prove the algorithm is correct and finds the strongest possible such weakening, and test it on real-world examples.

Core claim

CEGIW is an iterative counterexample-guided algorithm for weakening timing intervals in MTL specifications. It preserves the logical structure and only adjusts interval bounds. Using a model checker to produce counterexamples, CEGIW either identifies the strongest interval weakening under which the specification holds, or determines that no such weakening exists. The algorithm is proven correct and optimal.

What carries the argument

CEGIW, the counterexample-guided interval weakening algorithm, which iteratively identifies intervals to relax based on counterexamples and searches for the minimal relaxation needed.

If this is right

  • The algorithm terminates with the strongest valid weakened specification or concludes none is possible.
  • It can be used on formalized requirements from real-world case studies.
  • Only numeric bounds are changed, keeping the formula's structure fixed.
  • Correctness ensures the output weakening satisfies the model if one exists.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This approach might apply to other temporal logics or specification languages beyond MTL.
  • Integration with automated system monitoring could allow ongoing adjustment of requirements.
  • Future work could explore weakening other parts of the specification if intervals alone are insufficient.

Load-bearing premise

The approach assumes a model checker can always provide suitable counterexamples for the MTL formulas and that adjusting only interval bounds is enough to make the specification hold.

What would settle it

Model checking the output of the algorithm against the system and finding either that it does not hold, or that a strictly stronger version with tighter intervals also holds.

Figures

Figures reproduced from arXiv: 2604.24540 by Ben M. Andrew, Louise A. Dennis, Marie Farrell, Michael Fisher.

Figure 1
Figure 1. Figure 1: Abstract state transition system for the robot’s foraging behaviour. The view at source ↗
Figure 2
Figure 2. Figure 2: Infinite lasso counterexample trace for the property in Eq. (16). view at source ↗
Figure 3
Figure 3. Figure 3: Abstract state transition system for the robot’s modified foraging be view at source ↗
Figure 4
Figure 4. Figure 4: Iterative interval weakening to generate optimal, valid intervals. view at source ↗
Figure 5
Figure 5. Figure 5: Example fretish requirements from the case studies. Both are taken from systems that are fully implemented and operational in real-world settings. ments that can be weakened using interval weakening per case study is shown in view at source ↗
read the original abstract

Systems deployed for long periods of time in dynamic environments may experience performance degradation that affects timing guarantees, even when their functional behaviour remains unchanged. In the design and verification of critical systems, such timing guarantees are often expressed using Metric Temporal Logic (MTL). Under degradation, these specifications may no longer hold as stated, although weaker variants that relax timing bounds may still be satisfied and remain meaningful. For example, while an elevator may initially be required to arrive within 30 seconds of a request, degradation of its motor may only allow us to guarantee arrival within 60 seconds. Although weaker, this guarantee is still useful and allows the system to maintain a reasonable level of operation. In this paper we present CEGIW, an iterative, counterexample-guided algorithm for automatically weakening timing intervals in MTL specifications so that they hold for a given system model. The algorithm preserves the logical structure of the original specification and weakens only interval bounds. We prove the correctness and optimality of CEGIW, and conduct an empirical evaluation to demonstrate the practicality of interval weakening using formalised requirements from a number of real-world case-studies. Using a model checker to produce counterexamples, CEGIW either identifies the strongest interval weakening under which the specification holds, or determines that no such weakening exists.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces CEGIW, an iterative counterexample-guided algorithm for automatically weakening timing intervals in Metric Temporal Logic (MTL) specifications so that they hold for a given system model, while preserving the original logical structure. It claims to prove the correctness and optimality of CEGIW and reports an empirical evaluation on formalised requirements from real-world case studies, using a model checker to produce counterexamples; the algorithm either returns the strongest valid interval weakening or determines that none exists.

Significance. If the stated proofs of correctness and optimality hold, the result is significant for formal verification of timed systems: it automates adaptation of timing bounds under degradation without changing logical structure, which is useful for long-running critical systems. The counterexample-guided approach, optimality guarantee, and evaluation on real-world cases provide a practical contribution to the MTL verification literature.

minor comments (2)
  1. [Abstract] Abstract: the high-level description of CEGIW would benefit from a one-sentence outline of the main loop (e.g., how counterexamples are used to tighten candidate weakenings) to improve immediate readability.
  2. [Introduction] The elevator example is introduced but not accompanied by an explicit MTL formula; adding one (e.g., □(request → ◇_[0,30] arrive)) would make the notion of interval weakening concrete for readers.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive review and recommendation for minor revision. We are pleased that the significance of CEGIW for formal verification of timed systems is recognized, particularly the counterexample-guided approach and optimality guarantee. No major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The CEGIW algorithm is defined as an independent iterative procedure that invokes an external model checker to obtain counterexamples and then weakens numeric interval bounds while preserving logical structure. Correctness and optimality are established via separate proofs that rely on standard MTL monotonicity properties under interval widening rather than on any fitted parameters, self-referential definitions, or load-bearing self-citations. The central claim therefore remains self-contained against external benchmarks and does not reduce to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard semantics of Metric Temporal Logic and the availability of a model checker capable of generating counterexamples. No free parameters or invented entities are introduced.

axioms (2)
  • standard math Standard semantics of Metric Temporal Logic (MTL) for satisfaction and counterexample generation
    The algorithm and its proofs rely on the established definition of MTL satisfaction over timed traces.
  • domain assumption Existence of a model checker that can produce counterexamples for MTL formulas over the given system model
    CEGIW is defined in terms of iterative calls to such a model checker.

pith-pipeline@v0.9.0 · 5525 in / 1426 out tokens · 51884 ms · 2026-05-08T01:16:26.643223+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages · 1 internal anchor

  1. [1]

    Au- tomata Learning through Counterexample Guided Abstraction Refine- ment

    F. Aarts, F. Heidarian, H. Kuppens, P. Olsen, and F. Vaandrager. “Au- tomata Learning through Counterexample Guided Abstraction Refine- ment”. In:Formal Methods. 2012

    work page 2012

  2. [2]

    Exploring Automatic Specification Repair in Dafny Programs

    A. Abreu, N. Macedo, and A. Mendes. “Exploring Automatic Specification Repair in Dafny Programs”. In:International Conference on Automated Software Engineering Workshops. 2023

    work page 2023

  3. [3]

    Akshay, P

    S. Akshay, P. Contractor, P. Gastin, R. Govind, and B. Srivathsan.Ef- ficient Verification of Metric Temporal Properties with Past in Pointwise Semantics. https://arxiv.org/abs/2510.14699v1. 2025

    work page internal anchor Pith review arXiv 2025

  4. [4]

    Syntax- Guided Synthesis

    R. Alur, R. Bodik, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. “Syntax- Guided Synthesis”. In:Formal Methods in Computer-Aided Design. 2013

    work page 2013

  5. [5]

    Real-Time Logics: Complexity and Expres- siveness

    R. Alur and T. A. Henzinger. “Real-Time Logics: Complexity and Expres- siveness”. In:Information and Computation104.1 (1993)

    work page 1993

  6. [6]

    Counter-Strategy Guided Refinement ofGR(1)TemporalLogicSpecifications

    R. Alur, S. Moarref, and U. Topcu. “Counter-Strategy Guided Refinement ofGR(1)TemporalLogicSpecifications”.In:Formal Methods in Computer- Aided Design. 2013

    work page 2013

  7. [7]

    Weakening Goals in Logical Specifications

    B. M. Andrew. “Weakening Goals in Logical Specifications”. In:Rigorous State-Based Methods. 2026

    work page 2026

  8. [8]

    Baier and J.-P

    C. Baier and J.-P. Katoen.Principles of Model Checking. 2008

    work page 2008

  9. [9]

    Integrating Formal Verification and Assurance: An Inspection Rover Case Study

    H. Bourbouh, M. Farrell, A. Mavridou, I. Sljivo, G. Brat, L. A. Dennis, and M. Fisher. “Integrating Formal Verification and Assurance: An Inspection Rover Case Study”. In:NASA Formal Methods. 2021

    work page 2021

  10. [10]

    Effi- cient Algorithms and Tools for MITL Model-Checking and Synthesis

    T. Brihaye, G. Geeraerts, H.-M. Ho, A. Milchior, and B. Monmege. “Effi- cient Algorithms and Tools for MITL Model-Checking and Synthesis”. In: International Conference on Engineering of Complex Computer Systems. 2018

    work page 2018

  11. [11]

    Automated Repair of Unrealisable LTL Specifications Guided by Model Counting

    M. Brizzio, M. Cordy, M. Papadakis, C. Sánchez, N. Aguirre, and R. De- giovanni. “Automated Repair of Unrealisable LTL Specifications Guided by Model Counting”. In:Genetic and Evolutionary Computation Confer- ence. 2023

    work page 2023

  12. [12]

    ThenuXmvSymbolic Model Checker

    R.Cavada,A.Cimatti,M.Dorigatti,A.Griggio,A.Mariotti,A.Micheli,S. Mover, M. Roveri, and S. Tonetta. “ThenuXmvSymbolic Model Checker”. In:Computer Aided Verification. 2014

    work page 2014

  13. [13]

    Timely Specification Repair for Alloy 6

    J. Cerqueira, A. Cunha, and N. Macedo. “Timely Specification Repair for Alloy 6”. In:Software Engineering and Formal Methods. 2022

    work page 2022

  14. [14]

    Counterexample- Guided Abstraction Refinement

    E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. “Counterexample- Guided Abstraction Refinement”. In:Computer Aided Verification. 2000

    work page 2000

  15. [15]

    Completeness andComplexityofBoundedModelChecking

    E. Clarke, D. Kroening, J. Ouaknine, and O. Strichman. “Completeness andComplexityofBoundedModelChecking”.In:Verification, Model Check- ing, and Abstract Interpretation. 2004

    work page 2004

  16. [16]

    Learning As- sumptions for Compositional Verification

    J. M. Cobleigh, D. Giannakopoulou, and C. S. Păsăreanu. “Learning As- sumptions for Compositional Verification”. In:Tools and Algorithms for the Construction and Analysis of Systems. 2003. 18 B.M. Andrew et al

    work page 2003

  17. [17]

    FRETting and Formal Modelling: A Mechanical Lung Ventilator

    M. Farrell, M. Luckcuck, R. Monahan, C. Reynolds, and O. Sheridan. “FRETting and Formal Modelling: A Mechanical Lung Ventilator”. In: Rigorous State-Based Methods. 2024

    work page 2024

  18. [18]

    FRETting About Requirements:FormalisedRequirementsforanAircraftEngineController

    M. Farrell, M. Luckcuck, O. Sheridan, and R. Monahan. “FRETting About Requirements:FormalisedRequirementsforanAircraftEngineController”. In:Requirements Engineering: Foundation for Software Quality. 2022

    work page 2022

  19. [19]

    Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal

    M. Farrell, N. Mavrakis, A. Ferrando, C. Dixon, and Y. Gao. “Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal”. In:Frontiers in Robotics and AI8 (2022)

    work page 2022

  20. [20]

    Automatic Software Repair: A Survey

    L. Gazzola, D. Micucci, and L. Mariani. “Automatic Software Repair: A Survey”. In:International Conference on Software Engineering. 2018

    work page 2018

  21. [21]

    Formal Requirements Elicitation with FRET

    D. Giannakopoulou, T. Pressburger, A. Mavridou, J. Rhein, J. Schumann, and N. Shi. “Formal Requirements Elicitation with FRET”. In:Interna- tional Working Conference on Requirements Engineering: Foundation for Software Quality(2020)

    work page 2020

  22. [22]

    Au- tomated Formalization of Structured Natural Language Requirements

    D. Giannakopoulou, T. Pressburger, A. Mavridou, and J. Schumann. “Au- tomated Formalization of Structured Natural Language Requirements”. In: Information and Software Technology137 (2021)

    work page 2021

  23. [23]

    The Model Checker SPIN

    G. J. Holzmann. “The Model Checker SPIN”. In:IEEE Transactions on Software Engineering23.5 (1997)

    work page 1997

  24. [24]

    Automata Learning with Auto- mated Alphabet Abstraction Refinement

    F. Howar, B. Steffen, and M. Merten. “Automata Learning with Auto- mated Alphabet Abstraction Refinement”. In:Verification, Model Check- ing, and Abstract Interpretation. 2011

    work page 2011

  25. [25]

    80601-2-12

    ISO.Particular Requirements for Basic Safety and Essential Performance of Critical Care Ventilators. 80601-2-12. 2023

    work page 2023

  26. [26]

    SpecifyingReal-TimePropertieswithMetricTemporalLogic

    R.Koymans.“SpecifyingReal-TimePropertieswithMetricTemporalLogic”. In:Real-Time Systems2.4 (1990)

    work page 1990

  27. [27]

    Modeling and Optimization of Adaptive Foraging in Swarm Robotic Systems

    W. Liu and A. F. T. Winfield. “Modeling and Optimization of Adaptive Foraging in Swarm Robotic Systems”. In:The International Journal of Robotics Research29.14 (2010)

    work page 2010

  28. [28]

    Symbolic Repairs for GR(1) Spec- ifications

    S. Maoz, J. O. Ringert, and R. Shalom. “Symbolic Repairs for GR(1) Spec- ifications”. In:International Conference on Software Engineering. 2019

    work page 2019

  29. [29]

    The Ten Lockheed Martin Cyber- Physical Challenges: Formalized, Analyzed, and Explained

    A. Mavridou, H. Bourbouh, D. Giannakopoulou, T. Pressburger, M. He- jase, P.-L. Garoche, and J. Schumann. “The Ten Lockheed Martin Cyber- Physical Challenges: Formalized, Analyzed, and Explained”. In:Interna- tional Requirements Engineering Conference. 2020

    work page 2020

  30. [30]

    Authoring, Ana- lyzing, and Monitoring Requirements for a Lift-Plus-Cruise Aircraft

    T. Pressburger, A. Katis, A. Dutle, and A. Mavridou. “Authoring, Ana- lyzing, and Monitoring Requirements for a Lift-Plus-Cruise Aircraft”. In: Requirements Engineering: Foundation for Software Quality. 2023

    work page 2023

  31. [31]

    SharperSpecsforSmarterDrones:FormalisingRequirementswithFRET

    O. Sheridan, L. B. Becker, M. Farrell, M. Luckcuck, and R. Monahan. “SharperSpecsforSmarterDrones:FormalisingRequirementswithFRET”. In:Requirements Engineering: Foundation for Software Quality. 2025

    work page 2025

  32. [32]

    Robotics: A New Mission for FRET Requirements

    G. Vázquez, A. Mavridou, M. Farrell, T. Pressburger, and R. Calinescu. “Robotics: A New Mission for FRET Requirements”. In:NASA Formal Methods. 2024

    work page 2024