Counterexample Classification against Signal Temporal Logic Specifications

TL;DR

The paper tackles how to interpret and exploit the diversity of counterexamples to $STL$ specifications in hybrid systems. The approach uses timing parameters in $PSTL$ to define a set of sufficient conditions for violation, represented as a valuation space $\boldsymbol{\Theta} \subseteq \mathbb{R}_{+}^m$, and for a given signal $\mathbf{w}$, searches for a valuation $\boldsymbol{\theta}$ that yields a violating instance to assign the signal to a class. A partial order over classes based on signal-set inclusion enables a binary-search-like algorithm that prunes checks, improving efficiency. A prototype tool is evaluated on two benchmark models (ARCHCOMP24Falsification), showing improved efficiency and the ability to differentiate violation patterns, enabling targeted debugging and reengineering.

Abstract

Signal Temporal Logic (STL) has been widely adopted as a specification language for specifying desirable behaviors of hybrid systems. By monitoring a given STL specification, we can detect the executions that violate it, which are often referred to as counterexamples. In practice, these counterexamples may arise from different causes and thus are relevant to different system defects. To effectively address this, we need a proper criterion for classifying these counterexamples, by which we can comprehend the possible violation patterns and the distributions of these counterexamples with respect to the patterns. In this paper, we propose a classification criterion by using parametric signal temporal logic (PSTL) to represent each class. Due to this formalism, identifying the classes of a counterexample requires finding proper parameter values of PSTL that enable a class to include the counterexample. To improve the efficiency of class identification, we further derive an inclusion relation between different classes, and then propose a binary search-like approach over it that significantly prunes the classes needed to query. We implement a prototype tool and experimentally evaluate its effectiveness on two widely-studied systems.

Figures (1)

• Figure 1: Proposed workflow of counterexample classification