{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T09:28:39Z","timestamp":1780565319936,"version":"3.54.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,3,19]],"date-time":"2015-03-19T00:00:00Z","timestamp":1426723200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s10703-015-0227-2","type":"journal-article","created":{"date-parts":[[2015,3,18]],"date-time":"2015-03-18T14:48:53Z","timestamp":1426690133000},"page":"286-316","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["The ins and outs of first-order runtime verification"],"prefix":"10.1007","volume":"46","author":[{"given":"Andreas","family":"Bauer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan-Christoph","family":"K\u00fcster","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gil","family":"Vegliach","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,3,19]]},"reference":[{"issue":"4","key":"227_CR1","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):14","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"227_CR2","doi-asserted-by":"crossref","unstructured":"Dong W, Leucker M, Schallhart C (2008) Impartial anticipation in runtime-verification. In: Proc. 6th Intl. Symp. on automated technology for verification and analysis (ATVA), vol 5311. LNCS, Springer, pp 386\u2013396","DOI":"10.1007\/978-3-540-88387-6_33"},{"key":"227_CR3","doi-asserted-by":"crossref","unstructured":"Halle S, Villemaire R (2008) Runtime monitoring of message-based workflows with data. In: Proc. 12th Enterprise Distr. Object Comp. Conf. (EDOC), pp 63\u201372, IEEE. doi: 10.1109\/EDOC.2008.32","DOI":"10.1109\/EDOC.2008.32"},{"issue":"2","key":"227_CR4","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund K, Rosu G (2004) Efficient monitoring of safety properties. Softw Tools Technol Transf 6(2):158\u2013173","journal-title":"Softw Tools Technol Transf"},{"key":"227_CR5","doi-asserted-by":"crossref","unstructured":"Basin D, Klaedtke F, M\u00fcller S (2010) Policy monitoring in first-order temporal logic. In: Proc. 22nd Intl. Conf. on computer aided verification (CAV), vol 6174. LNCS, Springer, pp 1\u201318","DOI":"10.1007\/978-3-642-14295-6_1"},{"key":"227_CR6","doi-asserted-by":"crossref","unstructured":"Bauer A, Gore R, Tiu A (2009) A first-order policy language for history-based transaction monitoring. In: Proc. 6th Intl. Colloq. on theoretical aspects of computing (ICTAC), vol 5684. LNCS, Springer, pp 96\u2013111","DOI":"10.1007\/978-3-642-03466-4_6"},{"issue":"2","key":"227_CR7","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1145\/210197.210200","volume":"20","author":"J Chomicki","year":"1995","unstructured":"Chomicki J (1995) Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans Database Syst 20(2):149\u2013186","journal-title":"ACM Trans Database Syst"},{"issue":"3","key":"227_CR8","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1006\/jcss.1995.1088","volume":"51","author":"J Chomicki","year":"1995","unstructured":"Chomicki J, Niwinski D (1995) On the feasibility of checking temporal integrity constraints. J Comput Syst Sci 51(3):523\u2013535","journal-title":"J Comput Syst Sci"},{"issue":"3","key":"227_CR9","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1109\/69.390251","volume":"7","author":"AP Sistla","year":"1995","unstructured":"Sistla AP, Wolfson O (1995) Temporal triggers in active databases. IEEE Trans Knowl Data Eng 7(3):471\u2013486","journal-title":"IEEE Trans Knowl Data Eng"},{"key":"227_CR10","doi-asserted-by":"crossref","unstructured":"Bauer A, K\u00fcster JC, Vegliach G (2012) Runtime verification meets android security. In: Proc. 4th NASA formal methods symp. (NFM), vol 7226. LNCS, Springer, pp 174\u2013180","DOI":"10.1007\/978-3-642-28891-3_18"},{"key":"227_CR11","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1987) A hierarchy of temporal properties. In: Proc. 6th Annual ACM Symp. on principles of distributed computing (PODC), ACM, pp 205\u2013205","DOI":"10.1145\/41840.41857"},{"key":"227_CR12","doi-asserted-by":"crossref","unstructured":"Bauer A, K\u00fcster JC, Vegliach G (2013) From propositional to first-order monitoring. In: Proc. 4th Intl. Conf. on runtime verification (RV), vol 8174. LNCS, Springer, pp 59\u201375","DOI":"10.1007\/978-3-642-40787-1_4"},{"key":"227_CR13","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"227_CR14","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. The MIT Press, Cambridge"},{"key":"227_CR15","doi-asserted-by":"crossref","unstructured":"Markey N, Schnoebelen P (2003) Model checking a path. In: Proc. 14th Int. Conf. on concurrency theory (CONCUR), vol 2761. LNCS, Springer, pp 248\u2013262 Springer","DOI":"10.1007\/978-3-540-45187-7_17"},{"issue":"3","key":"227_CR16","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla AP, Clarke EM (1985) The complexity of propositional linear temporal logics. J ACM 32(3):733\u2013749","journal-title":"J ACM"},{"key":"227_CR17","doi-asserted-by":"crossref","unstructured":"Genon A, Massart T, Meuter C (2006) Monitoring distributed controllers: When an efficient LTL algorithm on sequences is needed to model-check traces. In: Proc. 14th Intl. Symp. on formal methods (FM), vol 4085. LNCS, Springer, pp 557\u2013572","DOI":"10.1007\/11813040_37"},{"key":"227_CR18","doi-asserted-by":"crossref","unstructured":"Kuhtz L, Finkbeiner B (2012) Efficient parallel path checking for linear-time temporal logic with past and bounds. Log Methods Comput Sci 8(4)","DOI":"10.2168\/LMCS-8(4:10)2012"},{"key":"227_CR19","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: Proc. 15th Intl. Conf. on Computer Aided Verification (CAV), vol 2725. LNCS, Springer, pp 27\u201339","DOI":"10.1007\/978-3-540-45069-6_3"},{"key":"227_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07003-1","volume-title":"Elements of finite model theory","author":"L Libkin","year":"2004","unstructured":"Libkin L (2004) Elements of finite model theory. Springer, New York"},{"key":"227_CR21","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: Proc. 15th IFIP WG6.1 Intl. Symp. on protocol specification, testing and verification XV (IFIP). Chapman & Hall, pp 3\u201318","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"227_CR22","volume-title":"Introduction to automata theory, languages and computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages and computation, 1st edn. Addison-Wesley, Reading","edition":"1"},{"key":"227_CR23","doi-asserted-by":"crossref","unstructured":"Bacchus F, Kabanza F (1998) Planning for temporally extended goals. Ann Math Artif Intell 22:5\u201327. doi: 10.1023\/A:1018985923441 . http:\/\/portal.acm.org\/citation.cfm?id=590220.590230","DOI":"10.1023\/A:1018985923441"},{"key":"227_CR24","doi-asserted-by":"crossref","unstructured":"Dwyer M, Avrunin G, Corbett J (1999) Patterns in property specifications for finite-state verification. In: Proc. 21st Intl. Conf. on Softw. Eng. (ICSE), IEEE, pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"227_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: Proc. 14th Intl. Symp. on formal methods (FM), vol 4085. LNCS, Springer, pp 573\u2013586","DOI":"10.1007\/11813040_38"},{"key":"227_CR26","unstructured":"Bauer A (2010) Monitorability of $$\\omega $$ \u03c9 -regular languages. Comput Res Repos (CoRR\/arXive) abs\/1006.3638, ACM"},{"key":"227_CR27","doi-asserted-by":"crossref","unstructured":"Allan C, Avgustinov P, Christensen AS, Hendren L, Kuzins S, Lhot\u00e1k O, de Moor O, Sereni D, Sittampalam G, Tibble J (2005) Adding trace matching with free variables to aspect J. In: Proc. 20th ACM SIGPLAN Conf. on object-oriented programming, systems, languages, and applications (OOPSLA), ACM, pp 345\u2013364","DOI":"10.1145\/1094811.1094839"},{"key":"227_CR28","doi-asserted-by":"crossref","unstructured":"Chen F, Ro\u015fu G (2009) Parametric trace slicing and monitoring. In: Proc. 15th Intl. Conf. on tools and algorithms for the construction and analysis of systems (TACAS), vol 5505. LNCS, Springer, pp 246\u2013261","DOI":"10.1007\/978-3-642-00768-2_23"},{"issue":"3","key":"227_CR29","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1093\/logcom\/exn078","volume":"20","author":"V Stolz","year":"2010","unstructured":"Stolz V (2010) Temporal assertions with parametrized propositions. J. Log. Comp. 20(3):743\u2013757","journal-title":"J. Log. Comp."},{"key":"227_CR30","doi-asserted-by":"crossref","unstructured":"Jin D, Meredith PO, Lee C, Rosu G (2012) JavaMOP: efficient parametric runtime monitoring framework. In: Proc. 34th Intl. Conf. on Softw. Eng. (ICSE), IEEE, pp 1427\u20131430","DOI":"10.1109\/ICSE.2012.6227231"},{"key":"227_CR31","unstructured":"Medhat R, Joshi Y, Bonakdarpour B, Fischmeister S (2014) Parallelized runtime verification of first-order LTL specifications. Technical Report CS-2014-11, University of Waterloo"},{"issue":"1","key":"227_CR32","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1145\/1629175.1629198","volume":"53","author":"J Dean","year":"2010","unstructured":"Dean J, Ghemawat S (2010) Map reduce: a flexible data processing tool. Commun ACM 53(1):72\u201377","journal-title":"Commun ACM"},{"key":"227_CR33","doi-asserted-by":"crossref","unstructured":"Decker N, Leucker M, Thoma D (2014) Monitoring modulo theories. In: Proc. 20th Intl. Conf. on tools and algorithms for the construction and analysis of systems, vol 8413. Springer, LNCS, pp 341\u2013356","DOI":"10.1007\/978-3-642-54862-8_23"},{"issue":"6","key":"227_CR34","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract davis\u2013putnam\u2013logemann\u2013loveland procedure to dpll(T). J ACM 53(6):937\u2013977. doi: 10.1145\/1217856.1217859","journal-title":"J ACM"},{"key":"227_CR35","volume-title":"Computers and intractability: a guide to the theory of NP-completeness","author":"MR Garey","year":"1979","unstructured":"Garey MR, Johnson DS (1979) Computers and intractability: a guide to the theory of NP-completeness. W. H. Freeman & Co., New York"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0227-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0227-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0227-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T23:45:45Z","timestamp":1566431145000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0227-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,19]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["227"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0227-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,19]]}}}