Counterexample Classification for Signal Temporal Logic Specifications

Abstract

Signal Temporal Logic (STL) has been widely adopted as a specification language for specifying desirable behaviors of hybrid systems. One of the most common uses of STL is falsification, which attempts to generate counterexample signals that demonstrate how the system violates a given STL specification. A number of falsification methods and tools are available for efficient generation of counterexamples, which can be examined by the engineer to identify potential defects in the system. However, some of these counterexamples may be considered similar to each other in that they describe system behavior that stems from the same underlying causes or defects. Since examining counterexamples can be a labor-intensive task, a tool that presents a distinct set of counterexamples and avoids showing repetitive ones could reduce the amount of effort that the engineer spends in debugging. In this paper, we propose a counterexample classification method for STL specifications. Our approach is based on a novel criterion for classifying given counterexamples into a finite set of classes, each of which corresponds to a set of signals that share a common behavioral pattern. In particular, each class is represented by a formula in parametric signal temporal logic (PSTL), which provides a concise description of the signals in the class; then, the problem of checking whether a given signal belongs to a particular class can be formulated as finding parameter values for the corresponding PSTL such that the signal satisfies the formula. We propose an algorithm for automatically identifying classes from a given set of counterexamples and an efficient pruning method that leverages the concept of an inclusion relation between different classes. We demonstrate the efficiency of our algorithm and its utility on three hybrid systems, including automatic transmission, abstract fuel control, and robot navigation.