{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,26]],"date-time":"2025-09-26T13:21:39Z","timestamp":1758892899936,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995232"},{"type":"electronic","value":"9783030995249"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of a<jats:italic>kernel function<\/jats:italic>, well known in machine learning as a conceptually and computationally efficient tool. The corresponding<jats:italic>kernel trick<\/jats:italic>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<jats:italic>predicting (quantitative) satisfaction<\/jats:italic>of STL formulae on stochastic processes: Using our kernel and the kernel trick, we learn (i)\u00a0computationally efficiently (ii)\u00a0a practically precise predictor of satisfaction, (iii)\u00a0avoiding 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.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_15","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"281-300","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8874-4001","authenticated-orcid":false,"given":"Luca","family":"Bortolussi","sequence":"first","affiliation":[]},{"given":"Giuseppe Maria","family":"Gallo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2263-9342","authenticated-orcid":false,"given":"Laura","family":"Nenzi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"15_CR1","unstructured":"Amortila, P., Bellemare, M.G., Panangaden, P., Precup, D.: Temporally extended metrics for markov decision processes. In: SafeAI@AAAI. CEUR Workshop Proceedings, vol.\u00a02301. CEUR-WS.org (2019)"},{"key":"15_CR2","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: A complete quantitative deduction system for the bisimilarity distance on markov chains. Log. Methods Comput. Sci. 14(4) (2018)"},{"key":"15_CR3","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R., Tang, Q., van Breugel, F.: Computing probabilistic bisimilarity distances for probabilistic automata. In: CONCUR. LIPIcs, vol.\u00a0140, pp. 9:1\u20139:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"15_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587, 3\u201325 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.02.046","DOI":"10.1016\/j.tcs.2015.02.046"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Proc. of FORMATS. pp. 23\u201337 (2014)","DOI":"10.1007\/978-3-319-10512-3_3"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Deshmukh, J., Donz\u00e9, A., Fainekos, G., Maler, O., Ni\u010dkovi\u0107, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Lectures on Runtime Verification, pp. 135\u2013175. Springer (2018)","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"15_CR8","unstructured":"Billingsley, P.: Probability and measure. John Wiley & Sons (2008)"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A Decision Tree Approach to Data Classification using Signal Temporal Logic. In: Hybrid Systems: Computation and Control. pp. 1\u201310. ACM Press (2016). https:\/\/doi.org\/10.1145\/2883817.2883843","DOI":"10.1145\/2883817.2883843"},{"key":"15_CR10","unstructured":"Bortolussi, L., Gallo, G.M., K\u0159et\u00ednsk\u00fd, J., Nenzi, L.: Learning model checking and the kernel trick for signal temporal logic on stochastic processes. Tech. Rep. 2201.09928, arXiv (2022), https:\/\/arxiv.org\/abs\/2201.09928"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Brezis, H.: Functional analysis, Sobolev spaces and partial differential equations. Springer Science & Business Media (2010)","DOI":"10.1007\/978-0-387-70914-7"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Comaniciu, D., Meer, P.: Mean shift: A robust approach toward feature space analysis. IEEE Transactions on Pattern Analysis & Machine Intelligence 24(5), 603\u2013619 (2002)","DOI":"10.1109\/34.1000236"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Linear distances between markov chains. In: Desharnais, J., Jagadeesan, R. (eds.) CONCUR. LIPIcs, vol.\u00a059, pp. 20:1\u201320:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.20","DOI":"10.4230\/LIPIcs.CONCUR.2016.20"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Ferrere, T., Maler, O.: Efficient robust monitoring for stl. In: International Conference on Computer Aided Verification. pp. 264\u2013279. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"15_CR16","doi-asserted-by":"publisher","unstructured":"Ernst, G., Arcaini, P., Bennani, I., Donze, A., Fainekos, G., Frehse, G., Mathesen, L., Menghi, C., Pedrielli, G., Pouzet, M., Yaghoubi, S., Yamagata, Y., Zhang, Z.: Arch-comp 2020 category report: Falsification. In: Frehse, G., Althoff, M. (eds.) ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20). EPiC Series in Computing, vol.\u00a074, pp. 140\u2013152. EasyChair (2020). https:\/\/doi.org\/10.29007\/trr1, https:\/\/easychair.org\/publications\/paper\/ps5t","DOI":"10.29007\/trr1"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Fainekos, G., Hoxha, B., Sankaranarayanan, S.: Robustness of specifications and its applications to falsification, parameter mining, and runtime monitoring with s-taliro. In: Finkbeiner, B., Mariani, L. (eds.) Runtime Verification (RV). Lecture Notes in Computer Science, vol. 11757, pp. 27\u201347. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_3","DOI":"10.1007\/978-3-030-32079-9_3"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Haghighi, I., Mehdipour, N., Bartocci, E., Belta, C.: Control from signal temporal logic specifications with smooth cumulative quantitative semantics. In: 58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019. pp. 4361\u20134366. IEEE (2019). https:\/\/doi.org\/10.1109\/CDC40024.2019.9029429","DOI":"10.1109\/CDC40024.2019.9029429"},{"key":"15_CR19","unstructured":"Jacobs, S., Bloem, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, P.J., Michaud, T., Sakr, M., Sickert, S., Tentrup, L., Walker, A.: The 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, participants & results. CoRR abs\/1904.07736 (2019)"},{"key":"15_CR20","unstructured":"Kim, E.: Everything you wanted to know about the kernel trick (but were too afraid to ask). https:\/\/www.eric-kim.net\/eric-kim-net\/posts\/1\/kernel_trick.html, accessed on Jan 20, 2021"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Kret\u00ednsk\u00fd, J., Manta, A., Meggendorfer, T.: Semantic labelling and learning for parity game solving in LTL synthesis. In: ATVA. Lecture Notes in Computer Science, vol. 11781, pp. 404\u2013422. Springer (2019)","DOI":"10.1007\/978-3-030-31784-3_24"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Maarleveld, T.R., Olivier, B.G., Bruggeman, F.J.: Stochpy: a comprehensive, user-friendly tool for simulating stochastic biological processes. PloS one 8(11), e79345 (2013)","DOI":"10.1371\/journal.pone.0079345"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Madsen, C., Vaidyanathan, P., Sadraddini, S., Vasile, C.I., DeLateur, N.A., Weiss, R., Densmore, D., Belta, C.: Metrics for signal temporal logic formulae. In: 2018 IEEE Conference on Decision and Control (CDC). pp. 1542\u20131547. IEEE (2018)","DOI":"10.1109\/CDC.2018.8619541"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proc. FORMATS (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 578\u2013586. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"15_CR26","unstructured":"Mohri, M., Rostamizadeh, A., Talwalkar, A.: Foundations of machine learning. The MIT Press, Cambridge, Massachusetts, second edition edn. (2018)"},{"key":"15_CR27","unstructured":"Murphy, K.P.: Machine learning: a probabilistic perspective. MIT press (2012)"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Nenzi, L., Silvetti, S., Bartocci, E., Bortolussi, L.: A robust genetic algorithm for learning temporal specifications from data. In: McIver, A., Horv\u00e1th, A. (eds.) QEST. Lecture Notes in Computer Science, vol. 11024, pp. 323\u2013338. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_20","DOI":"10.1007\/978-3-319-99154-2_20"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Pallara, D\u00a0Ambrosio, L., Fusco, N.: Functions of bounded variation and free discontinuity problems. Oxford University Press, Oxford (2000)","DOI":"10.1093\/oso\/9780198502456.001.0001"},{"key":"15_CR30","unstructured":"Paszke, A., Gross, S., Chintala, S., Chanan, G., Yang, E., DeVito, Z., Lin, Z., Desmaison, A., Antiga, L., Lerer, A.: Automatic differentiation in pytorch. In: NIPS 2017 Workshop on Autodiff (2017), https:\/\/openreview.net\/forum?id=BJJsrmfCZ"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Rasmussen, C.E., Williams, C.K.I.: Gaussian Processes for Machine Learning. MIT Press (2006)","DOI":"10.7551\/mitpress\/3206.001.0001"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Shawe-Taylor, J., Cristianini, N.: Kernel methods for pattern analysis. Cambridge Univ Pr (2004)","DOI":"10.1017\/CBO9780511809682"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: CAV. Lecture Notes in Computer Science, vol.\u00a02404, pp. 223\u2013235. Springer (2002)","DOI":"10.1007\/3-540-45657-0_17"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,19]],"date-time":"2023-11-19T10:29:07Z","timestamp":1700389747000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}