{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:20:28Z","timestamp":1779074428066,"version":"3.51.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,1,23]],"date-time":"2019-01-23T00:00:00Z","timestamp":1548201600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,1,23]],"date-time":"2019-01-23T00:00:00Z","timestamp":1548201600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["CNS-1740079"],"award-info":[{"award-number":["CNS-1740079"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["1750009"],"award-info":[{"award-number":["1750009"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006754","name":"Army Research Laboratory","doi-asserted-by":"publisher","award":["US ARL Cooperative Agreement W911NF-17- 2-0196"],"award-info":[{"award-number":["US ARL Cooperative Agreement W911NF-17- 2-0196"]}],"id":[{"id":"10.13039\/100006754","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":[[2019,11]]},"DOI":"10.1007\/s10703-019-00332-1","type":"journal-article","created":{"date-parts":[[2019,1,24]],"date-time":"2019-01-24T18:01:25Z","timestamp":1548352885000},"page":"364-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":35,"title":["TeLEx: learning signal temporal logic from positive examples using tightness metric"],"prefix":"10.1007","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5983-9095","authenticated-orcid":false,"given":"Susmit","family":"Jha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tuhin","family":"Sahai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,23]]},"reference":[{"key":"332_CR1","doi-asserted-by":"crossref","unstructured":"Abbas H, Hoxha B, Fainekos G, Ueda K (2014) Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems. In: IEEE 4th annual international conference on cyber technology in automation, control, and intelligent systems (CYBER). IEEE, pp 1\u20136","DOI":"10.1109\/CYBER.2014.6917426"},{"key":"332_CR2","doi-asserted-by":"crossref","unstructured":"Abbas H, Winn A, Fainekos G, Julius AA (2014) Functional gradient descent method for metric temporal logic specifications. In: American control conference (ACC). IEEE, pp 2312\u20132317","DOI":"10.1109\/ACC.2014.6859453"},{"key":"332_CR3","doi-asserted-by":"crossref","unstructured":"Akazaki T (2016) Falsification of conditional safety properties for cyber-physical systems with gaussian process regression. In: International conference on runtime verification. Springer, pp 439\u2013446","DOI":"10.1007\/978-3-319-46982-9_27"},{"key":"332_CR4","doi-asserted-by":"crossref","unstructured":"Aksaray D, Jones A, Kong Z, Schwager M, Belta C (2016) Q-learning for robust satisfaction of signal temporal logic specifications. In: IEEE 55th conference on decision and control (CDC). IEEE, pp 6565\u20136570","DOI":"10.1109\/CDC.2016.7799279"},{"key":"332_CR5","unstructured":"Angluin D (1988) Identifying languages from stochastic examples. Technical report, YALEU\/DCS\/RR-614, Yale University. Department of Computer Science"},{"key":"332_CR6","doi-asserted-by":"crossref","unstructured":"Annpureddy Y, Liu C, Fainekos G, Sankaranarayanan S (2011) S-taliro: a tool for temporal logic falsification for hybrid systems. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 254\u2013257","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"332_CR7","doi-asserted-by":"crossref","unstructured":"Bartocci E, Bortolussi L, Sanguinetti G (2014) Data-driven statistical learning of temporal logic properties. In: International conference on formal modeling and analysis of timed systems. Springer, pp 23\u201337","DOI":"10.1007\/978-3-319-10512-3_3"},{"key":"332_CR8","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-662-45231-8_30","volume-title":"Leveraging applications of formal methods, verification and validation. Specialized techniques and applications","author":"S Bufo","year":"2014","unstructured":"Bufo S, Bartocci E, Sanguinetti G, Borelli M, Lucangelo U, Bortolussi L (2014) Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation. Specialized techniques and applications. Springer, Berlin, pp 391\u2013403"},{"issue":"1\u20132","key":"332_CR9","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1023\/A:1010826628977","volume":"44","author":"F Denis","year":"2001","unstructured":"Denis F (2001) Learning regular languages from simple positive examples. Mach Learn 44(1\u20132):37\u201366","journal-title":"Mach Learn"},{"key":"332_CR10","doi-asserted-by":"crossref","unstructured":"Deshmukh JV, Majumdar R, Prabhu VS (2015) Quantifying conformance using the Skorokhod metric. In: International conference on computer aided verification. Springer, pp 234\u2013250","DOI":"10.1007\/978-3-319-21668-3_14"},{"key":"332_CR11","doi-asserted-by":"crossref","unstructured":"Donz\u00e9 A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: International conference on computer aided verification. Springer, pp 167\u2013170","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"332_CR12","doi-asserted-by":"crossref","unstructured":"Donz\u00e9 A (2013) On signal temporal logic. In: International conference on runtime verification. Springer, pp 382\u2013383","DOI":"10.1007\/978-3-642-40787-1_27"},{"key":"332_CR13","doi-asserted-by":"crossref","unstructured":"Donz\u00e9 A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: International conference on formal modeling and analysis of timed systems. Springer, pp 92\u2013106","DOI":"10.1007\/978-3-642-15297-9_9"},{"issue":"4","key":"332_CR14","doi-asserted-by":"publisher","first-page":"1100","DOI":"10.1137\/S1052623499359890","volume":"12","author":"F Facchinei","year":"2002","unstructured":"Facchinei F, Lucidi S, Palagi L (2002) A truncated Newton algorithm for large scale box constrained optimization. SIAM J Optim 12(4):1100\u20131125","journal-title":"SIAM J Optim"},{"key":"332_CR15","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/11940197_12","volume-title":"Formal approaches to software testing and runtime verification","author":"GE Fainekos","year":"2006","unstructured":"Fainekos GE, Pappas GJ (2006) Robustness of temporal logic specifications. In: Havelund K, N\u00fa\u00f1ez M, Ro\u015fu G, Wolff B (eds) Formal approaches to software testing and runtime verification. Springer, Berlin, pp 178\u2013192"},{"issue":"11","key":"332_CR16","doi-asserted-by":"publisher","first-page":"3464","DOI":"10.1109\/TAC.2016.2518639","volume":"61","author":"J Fu","year":"2016","unstructured":"Fu J, Topcu U (2016) Synthesis of joint control and active sensing strategies under temporal logic constraints. IEEE Trans Autom Control 61(11):3464\u20133476. \nhttps:\/\/doi.org\/10.1109\/TAC.2016.2518639","journal-title":"IEEE Trans Autom Control"},{"key":"332_CR17","unstructured":"Giuseppe B, Cristian Ioan V, Francisco PA, Hirotoshi Y, Calin B (2016) A decision tree approach to data classification using signal temporal logic. In: Hybrid systems: computation and control (HSCC), Vienna, Austria, pp 1\u201310"},{"issue":"5","key":"332_CR18","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1016\/S0019-9958(67)91165-5","volume":"10","author":"EM Gold","year":"1967","unstructured":"Gold EM (1967) Language identification in the limit. Inf Control 10(5):447\u2013474","journal-title":"Inf Control"},{"key":"332_CR19","unstructured":"Horning JJ (1969) A study of grammatical inference. Technical report, DTIC document"},{"key":"332_CR20","unstructured":"Hoxha B, Dokhanchi A, Fainekos G (2015) Mining parametric temporal logic properties in model based design for cyber-physical systems. arXiv preprint \narXiv:1512.07956"},{"key":"332_CR21","doi-asserted-by":"crossref","unstructured":"Jak\u0161i\u0107 S, Bartocci E, Grosu R, Ni\u010dkovi\u0107 D (2016) Quantitative monitoring of STL with edit distance. In: International conference on runtime verification. Springer, pp 201\u2013218","DOI":"10.1007\/978-3-319-46982-9_13"},{"key":"332_CR22","doi-asserted-by":"crossref","unstructured":"Jha S, Raman V (2016) Automated synthesis of safe autonomous vehicle control under perception uncertainty. In: Rayadurgam S, Tkachuk O (eds) NASA formal methods: 8th international symposium, NFM, pp 117\u2013132","DOI":"10.1007\/978-3-319-40648-0_10"},{"key":"332_CR23","doi-asserted-by":"crossref","unstructured":"Jha S, Raman V (2016) On optimal control of stochastic linear hybrid systems. In: Fr\u00e4nzle M, Markey N (eds) Formal modeling and analysis of timed systems: 14th international conference. Springer, pp 69\u201384. \nhttp:\/\/dx.doi.org\/10.1007\/978-3-319-44878-7_5","DOI":"10.1007\/978-3-319-44878-7_5"},{"issue":"7","key":"332_CR24","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/s00236-017-0294-5","volume":"54","author":"Susmit Jha","year":"2017","unstructured":"Jha S, Seshia SA (2017) A theory of formal synthesis via inductive learning. Acta Inf. \nhttps:\/\/doi.org\/10.1007\/s00236-017-0294-5","journal-title":"Acta Informatica"},{"key":"332_CR25","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-319-67531-2_13","volume-title":"Runtime Verification","author":"Susmit Jha","year":"2017","unstructured":"Jha S, Tiwari A, Seshia SA, Sahai T, Shankar N (2017) Telex: passive STL learning using only positive examples. In: 17th international conference on runtime verification (RV), pp 208\u2013224"},{"issue":"11","key":"332_CR26","doi-asserted-by":"publisher","first-page":"1704","DOI":"10.1109\/TCAD.2015.2421907","volume":"34","author":"X Jin","year":"2015","unstructured":"Jin X, Donz\u00e9 A, Deshmukh JV, Seshia SA (2015) Mining requirements from closed-loop control models. IEEE Trans Comput Aided Des Integr Circuits Syst 34(11):1704\u20131717","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"332_CR27","doi-asserted-by":"crossref","unstructured":"Kong Z, Jones A, Medina Ayala A, Aydin Gol E, Belta C (2014) Temporal logic inference for classification and prediction from data. In: Proceedings of the 17th international conference on Hybrid systems: computation and control. ACM, pp 273\u2013282","DOI":"10.1145\/2562059.2562146"},{"issue":"1","key":"332_CR28","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(97)00016-9","volume":"185","author":"T Koshiba","year":"1997","unstructured":"Koshiba T, M\u00e4kinen E, Takada Y (1997) Learning deterministic even linear languages from positive examples. Theor Comput Sci 185(1):63\u201379","journal-title":"Theor Comput Sci"},{"key":"332_CR29","unstructured":"Lindemann L, Dimarogonas DV (2016) Robust control for signal temporal logic specifications using average space robustness. arXiv preprint \narXiv:1607.07019"},{"key":"332_CR30","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal techniques, modelling and analysis of timed and fault-tolerant systems","author":"O Maler","year":"2004","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Lakhnech Y, Yovine S (eds) Formal techniques, modelling and analysis of timed and fault-tolerant systems. Springer, Berlin, pp 152\u2013166"},{"key":"332_CR31","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-78127-1_26","volume-title":"Pillars of computer science","author":"O Maler","year":"2008","unstructured":"Maler O, Nickovic D, Pnueli A (2008) Checking temporal properties of discrete, timed and continuous behaviors. In: Avron A, Dershowitz N, Rabinovich A (eds) Pillars of computer science. Springer, Berlin, pp 475\u2013505"},{"key":"332_CR32","unstructured":"Muggleton S (1996) Learning from positive data. In: International conference on inductive logic programming. Springer, pp 358\u2013376"},{"key":"332_CR33","first-page":"358","volume-title":"Learning from positive data","author":"S Muggleton","year":"1997","unstructured":"Muggleton S (1997) Learning from positive data. Springer, Berlin, pp 358\u2013376"},{"key":"332_CR34","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1016\/0743-1066(94)90035-3","volume":"19","author":"S Muggleton","year":"1994","unstructured":"Muggleton S, De Raedt L (1994) Inductive logic programming: theory and methods. J Log Program 19:629\u2013679","journal-title":"J Log Program"},{"key":"332_CR35","doi-asserted-by":"crossref","unstructured":"Pant VY, Abbas H, Mangharam R (2017) Smooth operator: control using the smooth robustness of temporal logic. In: CCTA, pp 1235\u20131240","DOI":"10.1109\/CCTA.2017.8062628"},{"key":"332_CR36","volume-title":"Differential evolution: a practical approach to global optimization","author":"K Price","year":"2006","unstructured":"Price K, Storn RM, Lampinen JA (2006) Differential evolution: a practical approach to global optimization. Springer, Berlin"},{"key":"332_CR37","doi-asserted-by":"crossref","unstructured":"Raman V, Donz\u00e9 A, Maasoumy M, Murray RM, Sangiovanni-Vincentelli AL, Seshia SA (2014) Model predictive control with signal temporal logic specifications. In: CDC, pp 81\u201387","DOI":"10.1109\/CDC.2014.7039363"},{"key":"332_CR38","doi-asserted-by":"crossref","unstructured":"Sadraddini S, Belta C (2015) Robust temporal logic model predictive control. In: 53rd Annual Allerton conference on communication, control, and computing (Allerton). IEEE, pp 772\u2013779","DOI":"10.1109\/ALLERTON.2015.7447084"},{"key":"332_CR39","unstructured":"Silvetti S, Nenzi L, Bortolussi L, Bartocci E (2017) A robust genetic algorithm for learning temporal specifications from data. CoRR abs\/1711.06202. \nhttp:\/\/arxiv.org\/abs\/1711.06202"},{"issue":"11","key":"332_CR40","doi-asserted-by":"publisher","first-page":"1134","DOI":"10.1145\/1968.1972","volume":"27","author":"LG Valiant","year":"1984","unstructured":"Valiant LG (1984) A theory of the learnable. Commun ACM 27(11):1134\u20131142","journal-title":"Commun ACM"},{"key":"332_CR41","doi-asserted-by":"crossref","unstructured":"Yang H, Hoxha B, Fainekos G (2012) Querying parametric temporal logic properties on embedded systems. In: IFIP international conference on testing software and systems. Springer, pp 136\u2013151","DOI":"10.1007\/978-3-642-34691-0_11"},{"key":"332_CR42","doi-asserted-by":"crossref","unstructured":"Zhang B, Zuo W (2008) Learning from positive and unlabeled examples: a survey. In: International symposiums on information processing, pp 650\u2013654","DOI":"10.1109\/ISIP.2008.79"},{"issue":"4","key":"332_CR43","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1145\/279232.279236","volume":"23","author":"C Zhu","year":"1997","unstructured":"Zhu C, Byrd RH, Lu P, Nocedal J (1997) Algorithm 778: fortran subroutines for large-scale bound-constrained optimization. ACM Trans Math Softw (TOMS) 23(4):550\u2013560","journal-title":"ACM Trans Math Softw (TOMS)"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00332-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-019-00332-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00332-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:46:50Z","timestamp":1589730410000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-019-00332-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,23]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["332"],"URL":"https:\/\/doi.org\/10.1007\/s10703-019-00332-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,23]]},"assertion":[{"value":"23 January 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}