Counterexample-Guided Interval Weakening

TL;DR

CEGIW is an iterative algorithm that automatically weakens timing intervals in Metric Temporal Logic specifications to ensure they hold in degraded system models, maintaining logical structure and optimal bounds.

Contribution

This paper introduces CEGIW, a novel counterexample-guided method for automatically weakening MTL timing intervals while preserving specification structure and proving correctness.

Findings

CEGIW successfully weakens timing bounds in real-world case studies.

The algorithm guarantees the weakest interval bounds that satisfy the system model.

Empirical results demonstrate CEGIW's practicality and effectiveness.

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.