{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T11:06:32Z","timestamp":1781175992403,"version":"3.54.1"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,3,27]],"date-time":"2018-03-27T00:00:00Z","timestamp":1522108800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004955","name":"\u00d6sterreichische Forschungsf\u00f6rderungsgesellschaft","doi-asserted-by":"crossref","award":["845631"],"award-info":[{"award-number":["845631"]}],"id":[{"id":"10.13039\/501100004955","id-type":"DOI","asserted-by":"crossref"}]},{"name":"ICT COST Action ARVI","award":["IC1402"],"award-info":[{"award-number":["IC1402"]}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["11405-N23"],"award-info":[{"award-number":["11405-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S 11412-N23"],"award-info":[{"award-number":["S 11412-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Doctoral Program Logical Methods in Computer Science"],"award-info":[{"award-number":["Doctoral Program Logical Methods in Computer Science"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s10703-018-0319-x","type":"journal-article","created":{"date-parts":[[2018,3,27]],"date-time":"2018-03-27T04:28:02Z","timestamp":1522124882000},"page":"83-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":47,"title":["Quantitative monitoring of STL with edit distance"],"prefix":"10.1007","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3203-9415","authenticated-orcid":false,"given":"Stefan","family":"Jak\u0161i\u0107","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radu","family":"Grosu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thang","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dejan","family":"Ni\u010dkovi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,3,27]]},"reference":[{"key":"319_CR1","doi-asserted-by":"publisher","unstructured":"Abbas H, Mittelmann HD, Fainekos GE (2014) Formal property verification in a conformance testing framework. In: Proceedings of MEMOCODE 2014: the twelfth ACM\/IEEE international conference on formal methods and models for codesign, pp 155\u2013164. IEEE. \n                    https:\/\/doi.org\/10.1109\/MEMCOD.2014.6961854","DOI":"10.1109\/MEMCOD.2014.6961854"},{"key":"319_CR2","doi-asserted-by":"publisher","unstructured":"Akazaki T, Tasuo I (2015) Time robustness in MTL and expressivity in hybrid system falsification. In: Proceedings of CAV 2015: the 27th international conference on computer aided verification, LNCS, vol 9207. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-21668-3","DOI":"10.1007\/978-3-319-21668-3"},{"key":"319_CR3","unstructured":"Allauzen C, Mohri M (2009) Linear-space computation of the edit-distance between a string and a finite automaton. CoRR \n                    arXiv:0904.4686"},{"key":"319_CR4","doi-asserted-by":"publisher","unstructured":"Annpureddy Y, Liu C, Fainekos GE, Sankaranarayanan S (2011) S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Proceedings of TACAS 2011: the 17th international conference on tools and algorithms for the construction and analysis of systems, LNCS, vol 6605, pp 254\u2013257. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"319_CR5","unstructured":"Bardh Hoxha HA, Fainekos G (2015) Benchmarks for temporal logic requirements for automotive systems. In: Proceedings of ARCH@CPSWeek 2014 and ARCH@CPSWeek 2015: the 1st and 2nd international workshop on applied verification for continuous and hybrid systems, vol 34"},{"key":"319_CR6","doi-asserted-by":"publisher","unstructured":"Bartocci E, Bortolussi L, Sanguinetti G (2014) Data-driven statistical learning of temporal logic properties. In: Proceedings of FORMATS 2014: the 12th international conference on formal modeling and analysis of timed systems, LNCS, vol 8711, pp 23\u201337. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-10512-3_3","DOI":"10.1007\/978-3-319-10512-3_3"},{"key":"319_CR7","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.ic.2014.01.012","volume":"236","author":"L Brim","year":"2014","unstructured":"Brim L, Dluhos P, Safr\u00e1nek D, Vejpustek T (2014) \n                    \n                      \n                    \n                    $${STL}^*$$\n                    \n                      \n                        \n                          \n                            STL\n                          \n                          \u2217\n                        \n                      \n                    \n                  : extending signal temporal logic with signal-value freezing operator. Inf Comput 236:52\u201367. \n                    https:\/\/doi.org\/10.1016\/j.ic.2014.01.012","journal-title":"Inf Comput"},{"key":"319_CR8","doi-asserted-by":"publisher","unstructured":"Davoren JM (2009) Epsilon-tubes and generalized Skorokhod metrics for hybrid paths spaces. In: Proceedings of HSCC 2009: the 12th international conference on hybrid systems: computation and control, LNCS, vol 5469, pp 135\u2013149. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-00602-9_10","DOI":"10.1007\/978-3-642-00602-9_10"},{"issue":"1","key":"319_CR9","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-017-0286-7","volume":"51","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh JV, Donz\u00e9 A, Ghosh S, Jin X, Juniwal G, Seshia SA (2017) Robust online monitoring of signal temporal logic. Form Methods Syst Des 51(1):5\u201330. \n                    https:\/\/doi.org\/10.1007\/s10703-017-0286-7","journal-title":"Form Methods Syst Des"},{"key":"319_CR10","unstructured":"Deshmukh JV, Majumdar R, Prabhu VS (2015) Quantifying conformance using the Skorokhod metric (full version). CoRR \n                    arXiv:1505.05832"},{"issue":"2\u20133","key":"319_CR11","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/s10703-016-0261-8","volume":"50","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh JV, Majumdar R, Prabhu VS (2017) Quantifying conformance using the Skorokhod metric. Form Methods Syst Des 50(2\u20133):168\u2013206. \n                    https:\/\/doi.org\/10.1007\/s10703-016-0261-8","journal-title":"Form Methods Syst Des"},{"key":"319_CR12","doi-asserted-by":"publisher","unstructured":"Dokhanchi A, Hoxha B, Fainekos GE (2014) On-line monitoring for temporal logic robustness. In: Proceedings RV 2014: the 5th international conference on runtime verification, LNCS, vol 8734, pp 231\u2013246. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-11164-3_19","DOI":"10.1007\/978-3-319-11164-3_19"},{"key":"319_CR13","doi-asserted-by":"publisher","unstructured":"Donz\u00e9 A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proceedings of CAV 2010: the 22nd international conference on computer aided verification, LNCS, vol 6174, pp 167\u2013170. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-14295-6_17","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"319_CR14","doi-asserted-by":"publisher","unstructured":"Donz\u00e9 A, Ferr\u00e8re T, Maler O (2013) Efficient robust monitoring for STL. In: Proceedings of CAV 2013: the 25th international conference on computer aided verification, LNCS, vol 8044, pp 264\u2013279. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-39799-8","DOI":"10.1007\/978-3-642-39799-8"},{"key":"319_CR15","doi-asserted-by":"publisher","unstructured":"Donz\u00e9 A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: Proceedings of FORMATS 2010: the 8th international conference on formal modeling and analysis of timed systems, LNCS, vol 6246, pp 92\u2013106. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-15297-9","DOI":"10.1007\/978-3-642-15297-9"},{"key":"319_CR16","doi-asserted-by":"publisher","unstructured":"Droste M, Kuich W, Vogler H (2009) Handbook of weighted automata. Springer, Berlin (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-01492-5","DOI":"10.1007\/978-3-642-01492-5"},{"key":"319_CR17","doi-asserted-by":"crossref","unstructured":"Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: Proceedings of the computer aided verification, 15th international conference, CAV 2003, Boulder, CO, USA, July 8\u201312, 2003, pp 27\u201339","DOI":"10.1007\/978-3-540-45069-6_3"},{"issue":"42","key":"319_CR18","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos GE, Pappas GJ (2009) Robustness of temporal logic specifications for continuous-time signals. Theor Comput Sci 410(42):4262\u20134291. \n                    https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theor Comput Sci"},{"key":"319_CR19","doi-asserted-by":"publisher","unstructured":"Fainekos GE, Sankaranarayanan S, Ivancic F, Gupta A (2009) Robustness of model-based simulations. In: Proceedings of RTSS 2009: the 30th IEEE real-time systems symposium, pp 345\u2013354. IEEE Computer Society. \n                    https:\/\/doi.org\/10.1109\/RTSS.2009.26","DOI":"10.1109\/RTSS.2009.26"},{"key":"319_CR20","doi-asserted-by":"crossref","unstructured":"Gerth R, Peled D, Vardi MY, Wolper P (1996) Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the fifteenth IFIP WG6.1 international symposium on protocol specification, testing and verification, IFIP conference proceedings, vol 38, pp 3\u201318. Chapman & Hall","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"319_CR21","doi-asserted-by":"publisher","unstructured":"Herrmann L, Vogler H (2016) Weighted symbolic automata with data storage. In: Proceedings of DLT 2016: the 20th international conference on developments in language theory, LNCS, vol 9840, pp 203\u2013215. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-662-53132-7","DOI":"10.1007\/978-3-662-53132-7"},{"key":"319_CR22","unstructured":"http:\/\/jautomata.sourceforge.net\/\n                    \n                  . Accessed 28 March 2017"},{"key":"319_CR23","unstructured":"http:\/\/www.mathworks.com\/products\/demos\/stateflow\/fuelsys.html\n                    \n                  . Accessed 28 March 2017"},{"key":"319_CR24","unstructured":"International S (2016) SENT\u2014single edge nibble transmission for automotive applications, J2716, Standard. \n                    http:\/\/standards.sae.org\/j2716_201001\/\n                    \n                  . Accessed 21 Jan 2017"},{"key":"319_CR25","doi-asserted-by":"publisher","unstructured":"Jaksic S, Bartocci E, Grosu R, Nickovic D (2016) Quantitative monitoring of STL with edit distance. In: Proceedings of RV 2016: the 16th international conference on runtime verification, LNCS, vol 10012, pp 201\u2013218. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-46982-9_13","DOI":"10.1007\/978-3-319-46982-9_13"},{"issue":"9","key":"319_CR26","doi-asserted-by":"publisher","first-page":"1307","DOI":"10.1016\/j.ic.2007.06.001","volume":"205","author":"S Konstantinidis","year":"2007","unstructured":"Konstantinidis S (2007) Computing the edit distance of a regular language. Inf Comput 205(9):1307\u20131316. \n                    https:\/\/doi.org\/10.1016\/j.ic.2007.06.001","journal-title":"Inf Comput"},{"key":"319_CR27","volume-title":"Taxicab geometry: an adventure in non-Euclidean geometry","author":"EF Krause","year":"2012","unstructured":"Krause EF (2012) Taxicab geometry: an adventure in non-Euclidean geometry. Courier Corporation, North Chelmsford"},{"key":"319_CR28","first-page":"707","volume":"10","author":"VI Levenshtein","year":"1966","unstructured":"Levenshtein VI (1966) Binary codes capable of correcting deletions, insertions and reversals. Sov Phys Dokl 10:707","journal-title":"Sov Phys Dokl"},{"issue":"3","key":"319_CR29","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler O, Nickovic D (2013) Monitoring properties of analog and mixed-signal circuits. STTT 15(3):247\u2013268. \n                    https:\/\/doi.org\/10.1007\/s10009-012-0247-9","journal-title":"STTT"},{"issue":"6","key":"319_CR30","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1142\/S0129054103002114","volume":"14","author":"M Mohri","year":"2003","unstructured":"Mohri M (2003) Edit-distance of weighted automata: general definitions and algorithms. Int J Found Comput Sci 14(6):957\u2013982. \n                    https:\/\/doi.org\/10.1142\/S0129054103002114","journal-title":"Int J Found Comput Sci"},{"key":"319_CR31","doi-asserted-by":"publisher","unstructured":"Nguyen T, Nickovic D (2014) Assertion-based monitoring in practice\u2014checking correctness of an automotive sensor interface. In: Proceedings of FMICS 2014: the 19th international conference on formal methods for industrial critical systems, LNCS, vol 8718, pp 16\u201332. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-10702-8","DOI":"10.1007\/978-3-319-10702-8"},{"key":"319_CR32","volume-title":"The definitive ANTLR 4 reference","author":"T Parr","year":"2013","unstructured":"Parr T (2013) The definitive ANTLR 4 reference, 2nd edn. Pragmatic Bookshelf, Dallas","edition":"2"},{"key":"319_CR33","doi-asserted-by":"publisher","unstructured":"Pnueli A, Zaks A (2008) On the merits of temporal testers. In: 25 years of model checking\u2014history, achievements, perspectives, LNCS, vol 5000, pp 172\u2013195. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-540-69850-0","DOI":"10.1007\/978-3-540-69850-0"},{"key":"319_CR34","unstructured":"Quesel J (2013) Similarity, logic, and games\u2014bridging modeling layers of hybrid systems. Ph.D. thesis, Universit\u00e4t Oldenburg"},{"key":"319_CR35","doi-asserted-by":"publisher","unstructured":"Rizk A, Batt G, Fages F, Soliman S (2008) On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Proceedings of CMSB 2008: the 6th international conference on computational methods in systems biology, LNCS, vol 5307, pp 251\u2013268. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-540-88562-7","DOI":"10.1007\/978-3-540-88562-7"},{"key":"319_CR36","doi-asserted-by":"publisher","unstructured":"Samanta R, Deshmukh JV, Chaudhuri S (2013) Robustness analysis of string transducers. In: Proceedings of ATVA 2013: the 11th international symposium on automated technology for verification and analysis, LNCS, vol 8172, pp 427\u2013441. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-02444-8_30","DOI":"10.1007\/978-3-319-02444-8_30"},{"issue":"1","key":"319_CR37","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10032-002-0082-8","volume":"5","author":"UK Schulz","year":"2002","unstructured":"Schulz UK, Mihov S (2002) Fast string correction with Levenshtein automata. Int J Doc Anal Recognit 5(1):67\u201385. \n                    https:\/\/doi.org\/10.1007\/s10032-002-0082-8","journal-title":"Int J Doc Anal Recognit"},{"key":"319_CR38","doi-asserted-by":"publisher","unstructured":"Selyunin K, Jaksic S, Nguyen T, Reidl C, Hafner U, Bartocci E, Nickovic D, Grosu R (2017) Runtime monitoring with recovery of the SENT communication protocol. In: Proceedings of CAV 2017: the 29th international conference on computer aided verification, LNCS, vol 10426, pp 336\u2013355. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-319-63387-9","DOI":"10.1007\/978-3-319-63387-9"},{"issue":"3","key":"319_CR39","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1137\/1101022","volume":"1","author":"AV Skorokhod","year":"1956","unstructured":"Skorokhod AV (1956) Limit theorems for stochastic processes. Theory Probab Appl 1(3):261\u2013290","journal-title":"Theory Probab Appl"},{"issue":"4","key":"319_CR40","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1109\/5.843002","volume":"88","author":"M Unser","year":"2000","unstructured":"Unser M (2000) Sampling 50 years after Shannon. Proc IEEE 88(4):569\u2013587","journal-title":"Proc IEEE"},{"key":"319_CR41","doi-asserted-by":"publisher","unstructured":"Veanes M, Bj\u00f8rner N, de\u00a0Moura LM (2010) Symbolic automata constraint solving. In: Proceedings of LPAR-17: the 17th international conference on logic for programming, artificial intelligence, and reasoning, LNCS, vol 6397, pp 640\u2013654. Springer. \n                    https:\/\/doi.org\/10.1007\/978-3-642-16242-8","DOI":"10.1007\/978-3-642-16242-8"},{"issue":"5","key":"319_CR42","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/360980.360995","volume":"17","author":"RA Wagner","year":"1974","unstructured":"Wagner RA (1974) Order-n correction for regular languages. Commun ACM 17(5):265\u2013268. \n                    https:\/\/doi.org\/10.1145\/360980.360995","journal-title":"Commun ACM"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-0319-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0319-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0319-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,26]],"date-time":"2019-03-26T20:56:45Z","timestamp":1553633805000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-0319-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,27]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["319"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-0319-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3,27]]},"assertion":[{"value":"27 March 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}