Virtual seminar (the link will be sent later)
6 November 2020 - 10h30
Learning Specifications for Labelled Patterns
by Akshay Mambakam from VERIMAG
Abstract: We present 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). We introduce a measure called epsilon-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 epsilon-count can measure the number of mismatches (either false positives or false negatives) up to some error tolerance epsilon. 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.
The solution to the parametric identification problem for PSTL is not easily representable as union of boxes which the algorithm uses. In addition, the algorithm faces difficulties in handling parameters in timing constraints. This led us to study introduction of parameters in Timed Regular Expressions (TRE) which have efficient zone representations. They can also better express properties regarding time periods. We describe what we call a parametric zone, which is a special and simpler version of a convex polyhedron. Finally, we discuss the parametric identification and matching problem for Timed Regular Expressions.
