Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Weakening Goals in Logical Specifications

Ben M. Andrew

TL;DR

The paper presents a counterexample-guided framework to automatically weaken logical specifications when system degradation invalidates the original property. It formulates a triple $(A, P_D, P_C)$ and uses a SAT-based loop to incrementally derive a weaker property $P_I$ between $P_D$ and $P_C$, guaranteed to terminate for finite propositional variables. Demonstrated on a quadrotor example, the method yields a practical weakened property (e.g., $W_L → L$) that still captures safe behavior under fault conditions. The work outlines extensions to state-based representations via automata learning (e.g., $L^*$) and discusses connections to contract-based reasoning and interpolation, highlighting the approach's potential for robust compositional verification under uncertainty.

Abstract

Logical specifications are widely used to represent software systems and their desired properties. Under system degradation or environmental changes, commonly seen in complex real-world robotic systems, these properties may no longer hold and so traditional verification methods will simply fail to construct a proof. However, weaker versions of these properties do still hold and can be useful for understanding the system's behaviour in uncertain conditions, as well as aiding compositional verification. We present a counterexample-guided technique for iteratively weakening properties, apply it to propositional logic specifications, and discuss planned extensions to state-based representations.

Weakening Goals in Logical Specifications

TL;DR

The paper presents a counterexample-guided framework to automatically weaken logical specifications when system degradation invalidates the original property. It formulates a triple and uses a SAT-based loop to incrementally derive a weaker property between and , guaranteed to terminate for finite propositional variables. Demonstrated on a quadrotor example, the method yields a practical weakened property (e.g., ) that still captures safe behavior under fault conditions. The work outlines extensions to state-based representations via automata learning (e.g., ) and discusses connections to contract-based reasoning and interpolation, highlighting the approach's potential for robust compositional verification under uncertainty.

Abstract

Logical specifications are widely used to represent software systems and their desired properties. Under system degradation or environmental changes, commonly seen in complex real-world robotic systems, these properties may no longer hold and so traditional verification methods will simply fail to construct a proof. However, weaker versions of these properties do still hold and can be useful for understanding the system's behaviour in uncertain conditions, as well as aiding compositional verification. We present a counterexample-guided technique for iteratively weakening properties, apply it to propositional logic specifications, and discuss planned extensions to state-based representations.
Paper Structure (6 sections, 2 equations, 1 figure)

This paper contains 6 sections, 2 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Related Work.
  3. Counterexample-Guided Weakening
  4. Algorithm.
  5. Example.
  6. Future Work

Figures (1)

  • Figure 1: Overview of the algorithm, which iteratively weakens the candidate property $P^i_I$ until it is satisfied by the system representation $A$.