Learning Specifications for Labelled Patterns

Learning Specifications for Labelled Patterns
复制标题

标记模式的学习规范

DOI:
--
复制
发表时间:
2020
期刊:
International Conference on Formal Modeling and Analysis of Timed Systems
影响因子:
--
通讯作者:
José
José
中科院分区:
--
文献类型:
--
作者:
Nicolas Basset;T. Dang;Akshay Mambakam;José

文献摘要

被引文献

相似文献

在这项工作中,我们引入了一种监督学习框架,用于从信号中的标记模式推断时间逻辑规范,以便使用公式来正确检测未标记样本中的相同模式。馈送到训练过程的输入模式由捕获其出现情况的布尔信号进行标记。为了表达具有定量特征的模式,我们使用递增的参数规范,我们将其称为递增参数模式预测器(IPPPP)。这意味着增加参数值可以使预测模式在更大的集合上成立。我们使用的一类特定的参数规范形式是参数信号时间逻辑(PSTL)。本文的主要贡献之一是定义了一种新度量,称为 -count,用于评估学习公式的质量。这种测量使我们能够比较两个布尔信号,从而量化公式引起的标记信号与真实标记信号(例如由专家给出的)的差异程度。因此,-count 可以在一定的容错范围内测量不匹配的数量(误报或漏报)。我们的监督学习框架可以用具有两个目标函数的多标准优化问题来表示:信号参数公式给出的误报和漏报最小化。我们提供了一种算法来解决这个多标准优化问题。我们的方法在涉及标记 ECG(心电图)数据的表征和分类的两个案例研究中得到了证明。
In this work, we introduce a supervised learning framework for inferring temporal logic specifications from labelled patterns in signals, so that the formulae can then be used to correctly detect the same patterns in unlabelled samples. The input patterns that are fed to the training process are labelled by a Boolean signal that captures their occurrences. To express the patterns with quantitative features, we use parametric specifications that are increasing, which we call Increasing Parametric Pattern Predictor (IPPP). This means that augmenting the value of the parameters makes the predicted pattern true on a larger set. A particular class of parametric specification formalisms that we use is Parametric Signal Temporal Logic (PSTL). One of the main contributions of this paper is the definition of a new measure, called -count, to assess the quality of the learned formula. This measure enables us to compare two Boolean signals and, hence, quantifies how much the labelling signal induced by the formula differs from the true labelling signal (e.g. given by an expert). Therefore, the -count can measure the number of mismatches (either false positives or false negatives) up to some error tolerance . Our supervised learning framework can be expressed by a multicriteria optimization problem with two objective functions: the minimization of false positives and false negatives given by the parametric formula on a signal. We provide an algorithm to solve this multi-criteria optimization problem. Our approach is demonstrated on two case studies involving characterization and classification of labeled ECG (electrocardiogram) data.