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.

翻译：信号时序逻辑（STL）作为一种规约语言，已被广泛用于描述混合系统所需的行为特性。通过监测给定的STL规约，我们可以检测出违反该规约的执行轨迹，这些轨迹通常被称为反例。在实际应用中，这些反例可能源于不同的原因，因此与不同的系统缺陷相关联。为有效处理这一问题，我们需要一个适当的准则来对这些反例进行分类，从而理解可能的违反模式以及反例在这些模式上的分布。本文提出一种分类准则，该准则使用参数化信号时序逻辑（PSTL）来表示每个类别。基于这种形式化方法，识别反例所属类别需要为PSTL找到合适的参数值，使得该类别能够包含该反例。为提高类别识别的效率，我们进一步推导了不同类别之间的包含关系，并在此基础上提出一种类似二分搜索的方法，该方法能显著减少需要查询的类别数量。我们实现了一个原型工具，并在两个被广泛研究的系统上通过实验评估了其有效性。