{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:03Z","timestamp":1776333423913,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642346903","type":"print"},{"value":"9783642346910","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34691-0_11","type":"book-chapter","created":{"date-parts":[[2012,11,14]],"date-time":"2012-11-14T09:10:35Z","timestamp":1352884235000},"page":"136-151","source":"Crossref","is-referenced-by-count":30,"title":["Querying Parametric Temporal Logic Properties on Embedded Systems"],"prefix":"10.1007","author":[{"given":"Hengyi","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bardh","family":"Hoxha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Lions, J.L., Lbeck, L., Fauquembergue, J.L., Kahn, G., Kubbat, W., Levedag, S., Mazzini, L., Merle, D., O\u2019Halloran, C.: Ariane 5, flight 501 failure, report by the inquiry board. Technical report, CNES (1996)"},{"key":"11_CR2","unstructured":"Hoffman, E.J., Ebert, W.L., Femiano, M.D., Freeman, H.R., Gay, C.J., Jones, C.P., Luers, P.J., Palmer, J.G.: The near rendezvous burn anomaly of december 1998. Technical report, Applied Physics Laboratory, Johns Hopkins University (1999)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Tripakis, S., Dang, T.: Modeling, Verification and Testing using Timed and Hybrid Automata. In: Model-Based Design for Embedded Systems, pp. 383\u2013436. CRC Press (2009)","DOI":"10.1201\/9781420067859-c13"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivancic, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 211\u2013220. ACM Press (2010)","DOI":"10.1145\/1755952.1755983"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R. Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems\u00a02, 255\u2013299 (1990)","journal-title":"Real-Time Systems"},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"G.E. Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science\u00a0410, 4262\u20134291 (2009)","journal-title":"Theoretical Computer Science"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: ACM International Conference on Hybrid Systems: Computation and Control (2012)","DOI":"10.1145\/2185632.2185653"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Annapureddy, Y.S.R., Fainekos, G.E.: Ant colonies for temporal logic falsification of hybrid systems. In: Proceedings of the 36th Annual Conference of IEEE Industrial Electronics, pp. 91\u201396 (2010)","DOI":"10.1109\/IECON.2010.5675195"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-29860-8_12","volume-title":"Runtime Verification","author":"E. Asarin","year":"2012","unstructured":"Asarin, E., Donz\u00e9, A., Maler, O., Nickovic, D.: Parametric Identification of Temporal Properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol.\u00a07186, pp. 147\u2013160. Springer, Heidelberg (2012)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.S.R. Annapureddy","year":"2011","unstructured":"Annapureddy, Y.S.R., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 254\u2013257. Springer, Heidelberg (2011)"},{"key":"11_CR11","unstructured":"Chutinan, A., Butts, K.R.: Dynamic analysis of hybrid system models for design validation. Technical report, Ford Motor Company (2002)"},{"key":"11_CR12","unstructured":"Abbas, H., Fainekos, G.E., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Transactions on Embedded Computing Systems (2011) (in press)"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1109\/LICS.1990.113764","volume-title":"Fifth Annual IEEE Symposium on Logic in Computer Science","author":"R. Alur","year":"1990","unstructured":"Alur, R., Henzinger, T.A.: Real-Time Logics: Complexity and Expressiveness. In: Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 390\u2013401. IEEE Computer Society Press, Washington, D.C (1990)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Zhao, Q., Krogh, B.H., Hubbard, P.: Generating test inputs for embedded control systems. IEEE Control Systems Magazine, 49\u201357 (August 2003)","DOI":"10.1109\/MCS.2003.1213603"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Fainekos, G., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using s-taliro. In: Proceedings of the American Control Conference (2012)","DOI":"10.1109\/ACC.2012.6315384"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A. Donze","year":"2010","unstructured":"Donze, A., Maler, O.: Robust Satisfaction of Temporal Logic over Real-Valued Signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol.\u00a06246, pp. 92\u2013106. Springer, Heidelberg (2010)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Silva, B.I., Krogh, B.H.: Formal verification of hybrid systems using CheckMate: a case study. In: Proceedings of the American Control Conference, vol.\u00a03, pp. 1679\u20131683 (2000)","DOI":"10.1109\/ACC.2000.879487"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Conrad, M., Fey, I.: Testing automotive control software. In: Automotive Embedded Systems Handbook. CRC Press (2008)","DOI":"10.1201\/9780849380273.ch11"},{"key":"11_CR19","unstructured":"Koopman, P.: Better Embedded System Software. Drumnadrochit Education LLC (2010)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-00768-2_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Plaku","year":"2009","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of LTL Safety Properties in Hybrid Systems. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 368\u2013382. Springer, Heidelberg (2009)"},{"key":"11_CR21","unstructured":"Tan, L., Kim, J., Sokolsky, O., Lee, I.: Model-based testing and monitoring for hybrid embedded systems. In: Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration, pp. 487\u2013492 (2004)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink\/stateflow verification. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 243\u2013252 (2010)","DOI":"10.1145\/1755952.1755987"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1145\/377978.377990","volume":"2","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for model measuring. ACM Trans. Comput. Logic\u00a02, 388\u2013407 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-13089-2_21","volume-title":"Language and Automata Theory and Applications","author":"B. Giampaolo Di","year":"2010","unstructured":"Di Giampaolo, B., La Torre, S., Napoli, M.: Parametric Metric Interval Temporal Logic. In: Dediu, A.-H., Fernau, H., Mart\u00edn-Vide, C. (eds.) LATA 2010. LNCS, vol.\u00a06031, pp. 249\u2013260. Springer, Heidelberg (2010)"},{"key":"11_CR25","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.tcs.2008.07.004","volume":"408","author":"F. Fages","year":"2008","unstructured":"Fages, F., Rizk, A.: On temporal logic constraint solving for analyzing numerical data time series. Theor. Comput. Sci.\u00a0408, 55\u201365 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR26","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-88562-7_19","volume-title":"Computational Methods in Systems Biology","author":"A. Rizk","year":"2008","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: On a Continuous Degree of Satisfaction of Temporal Logic Formulae with Applications to Systems Biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol.\u00a05307, pp. 251\u2013268. Springer, Heidelberg (2008)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Computer Aided Verification","author":"W. Chan","year":"2000","unstructured":"Chan, W.: Temporal-Logic Queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 450\u2013463. Springer, Heidelberg (2000)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-45069-6_21","volume-title":"Computer Aided Verification","author":"M. Chechik","year":"2003","unstructured":"Chechik, M., Gurfinkel, A.: TLQSolver: A Temporal Logic Query Checker. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 210\u2013214. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Testing Software and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34691-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T21:19:22Z","timestamp":1745183962000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34691-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642346903","9783642346910"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34691-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}