{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:03:27Z","timestamp":1781172207239,"version":"3.54.1"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T00:00:00Z","timestamp":1491955200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Max Planck Institute for Software Systems"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10703-016-0261-8","type":"journal-article","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T09:50:02Z","timestamp":1491990602000},"page":"168-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Quantifying conformance using the Skorokhod metric"],"prefix":"10.1007","volume":"50","author":[{"given":"Jyotirmoy V.","family":"Deshmukh","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vinayak S.","family":"Prabhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,4,12]]},"reference":[{"key":"261_CR1","doi-asserted-by":"publisher","unstructured":"Abbas H, Fainekos GE (2014) Formal property verification in a conformance testing framework. In: MEMOCODE, to appear","DOI":"10.1109\/MEMCOD.2014.6961854"},{"key":"261_CR2","unstructured":"Abbas H, Hoxha B, Fainekos GE, Deshmukh JV, Kapinski J, Ueda K (2014) Conformance testing as falsification for cyber-physical systems. CoRR, \n                        arXiv:1401.5200"},{"key":"261_CR3","doi-asserted-by":"publisher","unstructured":"Althoff M (2013) Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: HSCC 13, pp 173\u2013182","DOI":"10.1145\/2461328.2461358"},{"issue":"1","key":"261_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R Alur","year":"1994","unstructured":"Alur R, Henzinger TA (1994) A really temporal logic. J ACM 41(1):181\u2013204","journal-title":"J ACM"},{"key":"261_CR5","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: Proc TACAS, pp 254\u2013257","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"261_CR6","doi-asserted-by":"publisher","unstructured":"Bouyer P, Chevalier F, Markey N (2005) On the expressiveness of TPTL and MTL. In: FSTTCS 05, LNCS. vol 3821, pp 432\u2013443. Springer, Berlin","DOI":"10.1007\/11590156_35"},{"key":"261_CR7","unstructured":"Branicky MS (1995) Studies in hybrid systems: modeling, analysis, and control. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA"},{"key":"261_CR8","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) STL\n                        $$^*$$\n                        \n                            \n                                            \n                                \n                                    \n                                    \u2217\n                                \n                            \n                        \n                    : extending signal temporal logic with signal-value freezing operator. Inf Comput 236:52\u201367","journal-title":"Inf Comput"},{"key":"261_CR9","doi-asserted-by":"publisher","unstructured":"Brim L, Vejpustek T, Safr\u00e1nek D, Fabrikov\u00e1 J (2013) Robustness analysis for value-freezing signal temporal logic. In: Proceedings second international workshop on hybrid systems and biology, HSB 2013, EPTCS. vol 125, pp 20\u201336","DOI":"10.4204\/EPTCS.125.2"},{"key":"261_CR10","first-page":"4283","volume":"4","author":"M Broucke","year":"1998","unstructured":"Broucke M (1998) Regularity of solutions and homotopic equivalence for hybrid systems. IEEE Conf Decis Control 4:4283\u20134288","journal-title":"IEEE Conf Decis Control"},{"key":"261_CR11","doi-asserted-by":"publisher","unstructured":"Caspi P, Benveniste A (2002) Toward an approximation theory for computerised control. In: EMSOFT, pp 294\u2013304. Springer, Berlin","DOI":"10.1007\/3-540-45828-X_22"},{"key":"261_CR12","first-page":"258","volume":"13","author":"X Chen","year":"2013","unstructured":"Chen X, \u00c1brah\u00e1m E, Sankaranarayanan S (2013) Flow*: an analyzer for non-linear hybrid systems. CAV 13:258\u2013263","journal-title":"CAV"},{"key":"261_CR13","unstructured":"Crossley PR, Cook JA (1991) A nonlinear engine model for drivetrain system development. In: International conference on control, pp 921\u2013925. IET"},{"key":"261_CR14","doi-asserted-by":"publisher","unstructured":"Davoren JM (2009) Epsilon-tubes and generalized Skorokhod metrics for hybrid paths spaces. In: HSCC, LNCS. vol 5469, pp 135\u2013149. Springer, Berlin","DOI":"10.1007\/978-3-642-00602-9_10"},{"key":"261_CR15","doi-asserted-by":"publisher","unstructured":"Deshmukh JV, Majumdar R, Prabhu VS (2015) Quantifying conformance using the skorokhod metric. In: Computer aided verification, CAV 2015, Part II, LNCS. vol 9207, pp 234\u2013250. Springer, Berlin","DOI":"10.1007\/978-3-319-21668-3_14"},{"key":"261_CR16","doi-asserted-by":"publisher","unstructured":"Donz\u00e9 A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: FORMATS, LNCS. vol 6246, pp 92\u2013106. Springer, Berlin","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"261_CR17","unstructured":"Donz\u00e9 Alexandre (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: CAV, pp 167\u2013170"},{"key":"261_CR18","doi-asserted-by":"publisher","unstructured":"Duggirala PS, Mitra S, Viswanathan M (2013) Verification of annotated models from executions. In: EMSOFT 13, pp 26","DOI":"10.1109\/EMSOFT.2013.6658604"},{"issue":"1","key":"261_CR19","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TAC.2009.2034922","volume":"55","author":"A Girard","year":"2010","unstructured":"Girard A, Pola G, Tabuada P (2010) Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans Autom Control 55(1):116\u2013126","journal-title":"IEEE Trans Autom Control"},{"issue":"2\u20133","key":"261_CR20","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.tcs.2005.03.045","volume":"342","author":"E Haghverdi","year":"2005","unstructured":"Haghverdi E, Tabuada P, Pappas GJ (2005) Bisimulation relations for dynamical, control, and hybrid systems. Theor Comput Sci 342(2\u20133):229\u2013261","journal-title":"Theor Comput Sci"},{"issue":"1","key":"261_CR21","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J ACM 32(1):137\u2013161","journal-title":"J ACM"},{"key":"261_CR22","doi-asserted-by":"publisher","unstructured":"Henzinger MR, Henzinger TA, Kopke PW (1995) Computing simulations on finite and infinite graphs. In: FOCS: Foundations of Computer Science, pp 453\u2013462. IEEE Computer Society","DOI":"10.1109\/SFCS.1995.492576"},{"key":"261_CR23","doi-asserted-by":"publisher","unstructured":"Jin X, Deshmukh JV, Kapinski J, Ueda K, Butts K (2014) Powertrain control verification benchmark. In: HSCC 14, pp 253\u2013262","DOI":"10.1145\/2562059.2562140"},{"key":"261_CR24","doi-asserted-by":"publisher","unstructured":"Kapinski J, Deshmukh JV, Sankaranarayanan S, Arechiga N (2014) Simulation-guided lyapunov analysis for hybrid dynamical systems. In: HSCC 14, pp 133\u2013142. ACM, New York","DOI":"10.1145\/2562059.2562139"},{"issue":"4","key":"261_CR25","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255\u2013299","journal-title":"Real-Time Syst"},{"key":"261_CR26","unstructured":"Majumdar R, Prabhu VS (214) Computing the Skorokhod distance between polygonal traces (full paper). CoRR, \n                        arXiv:1410.6075"},{"key":"261_CR27","doi-asserted-by":"publisher","unstructured":"Majumdar R, Prabhu VS (2015) Computing the Skorokhod distance between polygonal traces. In: HSCC. ACM, New York","DOI":"10.1145\/2728606.2728618"},{"key":"261_CR28","unstructured":"The MathWorks. \n                        https:\/\/www.mathworks.com\/"},{"key":"261_CR29","unstructured":"The Mathworks. Engine timing model with closed loop control. \n                        https:\/\/www.mathworks.com\/help\/simulink\/examples\/engine-timing-model- with-closed-loop-control.html"},{"key":"261_CR30","unstructured":"Messner W, Tilbury D. Control tutorials for matlab and simulink. \n                        https:\/\/www.mathworks.com\/academia\/courseware\/control-tutorials.html"},{"key":"261_CR31","doi-asserted-by":"publisher","unstructured":"Milner R (1980) A calculus of communicating systems, LNCS. vol 92, Springer, Berlin","DOI":"10.1007\/3-540-10235-3"},{"key":"261_CR32","volume-title":"Advanced topics in bisimulation and coinduction","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi D, Rutten J (2011) Advanced topics in bisimulation and coinduction. cambridge University Press, Cambridge"},{"key":"261_CR33","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511801181","volume-title":"An introduction to numerical analysis","author":"E S\u00fcli","year":"2003","unstructured":"S\u00fcli E, Mayers DF (2003) An introduction to numerical analysis. Cambridge University Press, Cambridge"},{"key":"261_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and control of hybrid systems: a symbolic approach","author":"P Tabuada","year":"2009","unstructured":"Tabuada P (2009) Verification and control of hybrid systems: a symbolic approach. Springer, Berlin"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0261-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0261-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0261-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,4,20]],"date-time":"2017-04-20T07:37:55Z","timestamp":1492673875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0261-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,12]]},"references-count":34,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["261"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0261-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,12]]}}}