{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T03:10:02Z","timestamp":1748401802507,"version":"3.41.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192482"},{"type":"electronic","value":"9783319192499"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_15","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"231-247","source":"Crossref","is-referenced-by-count":10,"title":["Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL"],"prefix":"10.1007","author":[{"given":"Xiaoning","family":"Du","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Rageagainstthecage (2011), http:\/\/thesnkchrmr.wordpress.com\/2011\/03\/24\/rageagainstthecage"},{"key":"15_CR2","unstructured":"Tli monitoring of ltl extended with a counting quantifier (2015), http:\/\/pat.sce.ntu.edu.sg\/xndu\/fm2015"},{"key":"15_CR3","unstructured":"Arzt, S., Falzon, K., Follner, A., Rasthofer, S., Bodden, E., Stolz, V.: How useful are existing monitoring languages for securing android apps? In: ATPS, pp. 107\u2013122 (2013)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H. Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 44\u201357. Springer, Heidelberg (2004)"},{"issue":"3","key":"15_CR5","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H. Barringer","year":"2010","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from eagle to ruler. Journal of Logic and Computation\u00a020(3), 675\u2013706 (2010)","journal-title":"Journal of Logic and Computation"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-40787-1_3","volume-title":"Runtime Verification","author":"D. Basin","year":"2013","unstructured":"Basin, D., Klaedtke, F., Marinovic, S., Z\u0103linescu, E.: Monitoring of temporal first-order properties with aggregations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol.\u00a08174, pp. 40\u201358. Springer, Heidelberg (2013)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-03466-4_6","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","author":"A. Bauer","year":"2009","unstructured":"Bauer, A., Gor\u00e9, R., Tiu, A.: A first-order policy language for history-based transaction monitoring. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol.\u00a05684, pp. 96\u2013111. Springer, Heidelberg (2009)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-40787-1_4","volume-title":"Runtime Verification","author":"A. Bauer","year":"2013","unstructured":"Bauer, A., K\u00fcster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol.\u00a08174, pp. 59\u201375. Springer, Heidelberg (2013)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-54804-8_19","volume-title":"Fundamental Approaches to Software Engineering","author":"M.M. Bersani","year":"2014","unstructured":"Bersani, M.M., Bianculli, D., Ghezzi, C., Krsti\u0107, S., San Pietro, P.: SMT-based checking of SOLOIST over sparse traces. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol.\u00a08411, pp. 276\u2013290. Springer, Heidelberg (2014)"},{"issue":"4","key":"15_CR10","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1016\/j.jal.2014.07.005","volume":"12","author":"M.M. Bersani","year":"2014","unstructured":"Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., Pietro, P.S.: Constraint ltl satisfiability checking without automata. Journal of Applied Logic\u00a012(4), 522\u2013557 (2014)","journal-title":"Journal of Applied Logic"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-35861-6_4","volume-title":"Formal Aspects of Component Software","author":"D. Bianculli","year":"2013","unstructured":"Bianculli, D., Ghezzi, C., San Pietro, P.: The tale of SOLOIST: A specification language for service compositions interactions. In: P\u0103s\u0103reanu, C.S., Sala\u00fcn, G. (eds.) FACS 2012. LNCS, vol.\u00a07684, pp. 55\u201372. Springer, Heidelberg (2013)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Bianculli, D., Krstic, S., Ghezzi, C., San Pietro, P.: From soloist to cltlb (d): Checking quantitative properties of service-based applications (2013)","DOI":"10.1109\/SOCA.2014.14"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-16612-9_38","volume-title":"Runtime Verification","author":"C. Colombo","year":"2010","unstructured":"Colombo, C., Gauci, A., Pace, G.J.: LarvaStat: Monitoring of statistical properties. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 480\u2013484. Springer, Heidelberg (2010)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime monitoring of synchronous systems. In: TIME, pp. 166\u2013174 (2005)","DOI":"10.1109\/TIME.2005.26"},{"issue":"3","key":"15_CR15","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10703-005-3399-3","volume":"27","author":"B. Finkbeiner","year":"2005","unstructured":"Finkbeiner, B., Sankaranarayanan, S., Sipma, H.B.: Collecting statistics over runtime executions. Form. Methods Syst. Des.\u00a027(3), 253\u2013274 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer (1996)","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Gunadi, H., Tiu, A.: Efficient runtime monitoring with metric temporal logic: A case study in the android operating system. In: FM, pp. 296\u2013311 (2014)","DOI":"10.1007\/978-3-319-06410-9_21"},{"issue":"2","key":"15_CR18","first-page":"1","volume":"17","author":"K. Havelund","year":"2012","unstructured":"Havelund, K.: Rule-based runtime verification revisited. International Journal on Software Tools for Technology Transfer\u00a017(2), 1\u201328 (2012)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Meyer, A., Petonnet, E.: Counting ltl. In: TIME, pp. 51\u201358 (2010)","DOI":"10.1109\/TIME.2010.20"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Pieterse, H., Olivier, M.S.: Android botnets on the rise: Trends and characteristics. In: ISSA2, pp. 1\u20135 (2012)","DOI":"10.1109\/ISSA.2012.6320432"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Zhou, Y., Jiang, X.: Dissecting android malware: Characterization and evolution. In: SP, pp. 95\u2013109 (2012)","DOI":"10.1109\/SP.2012.16"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T02:42:55Z","timestamp":1748400175000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}