Counterexample Classification against Signal Temporal Logic Specifications

TL;DR

This paper introduces a method for classifying counterexamples to Signal Temporal Logic specifications using parametric STL, improving understanding of violation patterns and system defects.

Contribution

It proposes a novel classification criterion based on PSTL, along with an efficient binary search approach to identify counterexample classes.

Findings

Effective classification of counterexamples achieved

Binary search approach significantly reduces class querying

Prototype tool demonstrates practical applicability

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.