Learning Model Checking and the Kernel Trick for Signal
Temporal Logic on Stochastic Processes

D 2022

Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes

BORTOLUSSI, Luca; Giuseppe Maria GALLO; Jan KŘETÍNSKÝ a Laura NENZI

Základní údaje

Originální název

Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes

Autoři

BORTOLUSSI, Luca; Giuseppe Maria GALLO; Jan KŘETÍNSKÝ a Laura NENZI

Vydání

Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, od s. 281-300, 20 s. 2022

Nakladatel

Springer

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Organizační jednotka

Fakulta informatiky

ISBN

9783030995232

ISSN

DOI

https://doi.org/10.1007/978-3-030-99524-9_15

Změněno: 17. 3. 2025 14:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of a kernel function, well known in machine learning as a conceptually and computationally efficient tool. The corresponding kernel trick allows us to circumvent the complicated process of feature extraction, i.e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task of predicting (quantitative) satisfaction of STL formulae on stochastic processes: Using our kernel and the kernel trick, we learn (i) computationally efficiently (ii) a practically precise predictor of satisfaction, (iii) avoiding the difficult task of finding a way to explicitly turn formulae into vectors of numbers in a sensible way. We back the high precision we have achieved in the experiments by a theoretically sound PAC guarantee, ensuring our procedure efficiently delivers a close-to-optimal predictor.

Citovat

BORTOLUSSI, Luca; Giuseppe Maria GALLO; Jan KŘETÍNSKÝ a Laura NENZI. Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Springer, 2022, s. 281-300. ISBN 9783030995232. Dostupné z: https://doi.org/10.1007/978-3-030-99524-9_15.

@inproceedings{2484778,
   author = {Bortolussi, Luca and Gallo, Giuseppe Maria and Křetínský, Jan and Nenzi, Laura},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I},
   doi = {https://doi.org/10.1007/978-3-030-99524-9_15},
   isbn = {9783030995232},
   pages = {281-300},
   publisher = {Springer},
   title = {Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes},
   year = {2022}
}

TY  - CONF
ID  - 2484778
AU  - Bortolussi, Luca - Gallo, Giuseppe Maria - Křetínský, Jan - Nenzi, Laura
PY  - 2022
TI  - Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes
PB  - Springer
SN  - 9783030995232
N2  - We introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of a kernel function, well known in machine learning as a conceptually and computationally efficient tool. The corresponding kernel trick allows us to circumvent the complicated process of feature extraction, i.e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task of predicting (quantitative) satisfaction of STL formulae on stochastic processes: Using our kernel and the kernel trick, we learn (i) computationally efficiently (ii) a practically precise predictor of satisfaction, (iii) avoiding the difficult task of finding a way to explicitly turn formulae into vectors of numbers in a sensible way. We back the high precision we have achieved in the experiments by a theoretically sound PAC guarantee, ensuring our procedure efficiently delivers a close-to-optimal predictor.
ER  -

BORTOLUSSI, Luca; Giuseppe Maria GALLO; Jan KŘETÍNSKÝ a Laura NENZI. Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes. In \textit{Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I}. Springer, 2022, s.~281-300. ISBN~9783030995232. Dostupné z: https://doi.org/10.1007/978-3-030-99524-9\_{}15.

Přehled o publikaci