{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T14:55:17Z","timestamp":1791298517504,"version":"4.1.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2016,3,7]],"date-time":"2016-03-07T00:00:00Z","timestamp":1457308800000},"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":[[2016,10]]},"DOI":"10.1007\/s10703-016-0242-y","type":"journal-article","created":{"date-parts":[[2016,3,7]],"date-time":"2016-03-07T13:35:35Z","timestamp":1457357735000},"page":"75-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Scalable offline monitoring of temporal specifications"],"prefix":"10.1007","volume":"49","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Germano","family":"Caronni","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sarah","family":"Ereth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mat\u00fa\u0161","family":"Harvan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Heiko","family":"Mantel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,3,7]]},"reference":[{"key":"242_CR1","volume-title":"Foundations of databases: the logical level","author":"S Abiteboul","year":"1994","unstructured":"Abiteboul S, Hull R, Vianu V (1994) Foundations of databases: the logical level. Addison-Wesley, Reading"},{"key":"242_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger TA (1992) Logics and models of real time: a survey. In: Proceedings of the 1991 REX workshop on real time: theory in practice (Lecture notes in computer science), vol 600, pp 74\u2013106","DOI":"10.1007\/BFb0031988"},{"key":"242_CR3","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. The MIT Press, Cambridge"},{"key":"242_CR4","doi-asserted-by":"crossref","unstructured":"Barre B, Klein M, Soucy-Boivin M, Ollivier P-A, Hall\u00e9 S (2013) MapReduce for parallel trace validation of LTL properties. In: Proceedings of the 3rd international conference on runtime verification (Lecture notes in computer science), vol 7687, pp 184\u2013198","DOI":"10.1007\/978-3-642-35632-2_20"},{"key":"242_CR5","doi-asserted-by":"crossref","unstructured":"Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: Proceedings of the 5th international conference on verification, model checking and abstract interpretation (Lecture notes in computer science), vol 2937, pp 44\u201357","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"242_CR6","doi-asserted-by":"crossref","first-page":"365","DOI":"10.2514\/1.49356","volume":"7","author":"H Barringer","year":"2010","unstructured":"Barringer H, Groce A, Havelund K, Smith M (2010) Formal analysis of log files. J Aero Comput Inform Comm 7:365\u2013390","journal-title":"J Aero Comput Inform Comm"},{"key":"242_CR7","doi-asserted-by":"crossref","unstructured":"Barth A, Datta A, Mitchell JC, Nissenbaum H (2006) Privacy and contextual integrity: framework and applications. In: Proceedings of the 2006 IEEE symposium on security and privacy, pp 184\u2013198","DOI":"10.1109\/SP.2006.32"},{"key":"242_CR8","doi-asserted-by":"crossref","unstructured":"Basin D, Caronni G, Ereth S, Harvan M, Klaedtke F, Mantel H (2014) Scalable offline monitoring. In: Proceedings of the 14th international conference on runtime verification (Lecture notes in computer science), vol 8734, pp 31\u201347","DOI":"10.1007\/978-3-319-11164-3_4"},{"key":"242_CR9","doi-asserted-by":"crossref","unstructured":"Basin D, Harvan M, Klaedtke F, Z\u0103linescu E (2012) MONPOLY: Monitoring usage-control policies. In: Proceedings of the 2nd international conference on runtime verification (Lecture notes in computer science), vol 7186, pp 360\u2013364","DOI":"10.1007\/978-3-642-29860-8_27"},{"issue":"10","key":"242_CR10","doi-asserted-by":"crossref","first-page":"1403","DOI":"10.1109\/TSE.2013.18","volume":"39","author":"D Basin","year":"2013","unstructured":"Basin D, Harvan M, Klaedtke F, Z\u0103linescu E (2013) Monitoring data usage in distributed systems. IEEE Trans Softw Eng 39(10):1403\u20131426","journal-title":"IEEE Trans Softw Eng"},{"issue":"2","key":"242_CR11","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/2699444","volume":"62","author":"D Basin","year":"2015","unstructured":"Basin D, Klaedtke F, M\u00fcller S, Z\u0103linescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2):15","journal-title":"J ACM"},{"key":"242_CR12","doi-asserted-by":"crossref","unstructured":"Bauer A, Gor\u00e9 R, Tiu A (2009) A first-order policy language for history-based transaction monitoring. In: Proceedings of the 6th international colloquium on theoretical aspects of computing (Lecture notes in computer science), vol 5684, pp 96\u2013111","DOI":"10.1007\/978-3-642-03466-4_6"},{"key":"242_CR13","doi-asserted-by":"crossref","unstructured":"Bianculli D, Ghezzi C, Krsti\u0107 S (2014) Trace checking of metric temporal logic with aggregating modalities using MapReduce. In: Proceedings of the 12th international conference on software engineering and formal methods (Lecture notes in computer science), vol 8702, pp 144\u2013158","DOI":"10.1007\/978-3-319-10431-7_11"},{"issue":"2","key":"242_CR14","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"},{"key":"242_CR15","doi-asserted-by":"crossref","unstructured":"Chowdhury O, Jia L, Garg D, Datta A (2014) Temporal mode-checking for runtime monitoring of privacy policies. In: Proceedings of the 26th international conference on computer aided verification (Lecture notes in computer science), vol 8559, pp 131\u2013149","DOI":"10.1007\/978-3-319-08867-9_9"},{"issue":"1","key":"242_CR16","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1327452.1327492","volume":"51","author":"J Dean","year":"2008","unstructured":"Dean J, Ghemawat S (2008) MapReduce: simplified data processing on large clusters. Commun ACM 51(1):107\u2013113","journal-title":"Commun ACM"},{"key":"242_CR17","doi-asserted-by":"crossref","unstructured":"De Young H, Garg D, Jia L, Kaynar D, Datta A (2010) Experiences in the logical specification of the HIPAA and GLBA privacy laws. In: Proceedings of the 9th annual ACM workshop on privacy in the electronic society, pp 73\u201382","DOI":"10.1145\/1866919.1866930"},{"key":"242_CR18","doi-asserted-by":"crossref","unstructured":"Dinesh N, Joshi AK, Lee I, Sokolsky O (2008) Checking traces for regulatory conformance. In: Proceedings of the 8th international workshop on runtime verification (Lecture notes in computer science), vol 5289, pp 86\u2013103","DOI":"10.1007\/978-3-540-89247-2_6"},{"key":"242_CR19","volume-title":"A mathematical introduction to logic","author":"H Enderton","year":"2001","unstructured":"Enderton H (2001) A mathematical introduction to logic, 2nd edn. Academic Press, San Diego","edition":"2"},{"key":"242_CR20","doi-asserted-by":"crossref","unstructured":"Garg D, Jia L, Datta A (2011) Policy auditing over incomplete logs: theory, implementation and applications. In: Proceedings of the 18th ACM conference on computer and communications security, pp 151\u2013162","DOI":"10.1145\/2046707.2046726"},{"key":"242_CR21","unstructured":"Groce A, Havelund K, Smith M (2010) From scripts to specification: The evaluation of a flight testing effort. In: Proceedings of the 32nd ACM\/IEEE international conference on software engineering, vol 2, pp 129\u2013138"},{"issue":"2","key":"242_CR22","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1109\/TSC.2011.10","volume":"5","author":"S Hall\u00e9","year":"2012","unstructured":"Hall\u00e9 S, Villemaire R (2012) Runtime enforcement of web service message contracts with data. IEEE Trans Serv Comput 5(2):192\u2013206","journal-title":"IEEE Trans Serv Comput"},{"key":"242_CR23","doi-asserted-by":"crossref","unstructured":"Hilty M, Pretschner A, Basin DA, Schaefer C, Walter T (2007) A policy language for distributed usage control. In: Proceedings of the 12th european symposium on research in computer security (Lecture notes in computer science), vol 4734, pp 531\u2013546","DOI":"10.1007\/978-3-540-74835-9_35"},{"issue":"4","key":"242_CR24","doi-asserted-by":"crossref","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"},{"issue":"3","key":"242_CR25","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport L (1994) The temporal logic of actions. ACM Trans Program Lang Syst 16(3):872\u2013923","journal-title":"ACM Trans Program Lang Syst"},{"key":"242_CR26","doi-asserted-by":"crossref","unstructured":"Maggi FM, Montali M, Westergaard M, van der Aalst WMP (2011) Monitoring business constraints with linear temporal logic: an approach based on colored automata. In: Proceedings of the 9th international conference on business process management (Lecture notes in computer science), vol 6896, pp 132\u2013147","DOI":"10.1007\/978-3-642-23059-2_13"},{"key":"242_CR27","unstructured":"Medhat R, Joshi Y, Bonakdarpour B, Fischmeister S (2014) Accelerated runtime verification of LTL specifications with counting semantics. CoRR: Computing Research Repository - arXiv, http:\/\/arxiv.org\/abs\/1411.2239"},{"issue":"3","key":"242_CR28","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s00446-004-0117-0","volume":"17","author":"N Mittal","year":"2005","unstructured":"Mittal N, Garg VK (2005) Techniques and applications of computation slicing. Distrib Comput 17(3):251\u2013277","journal-title":"Distrib Comput"},{"key":"242_CR29","unstructured":"Wikipedia MurmurHash (2015) the free encyclopedia. Accessed 2 March 2015. https:\/\/en.wikipedia.org\/wiki\/MurmurHash"},{"key":"242_CR30","unstructured":"Neumeyer L, Robbins B, Nair A, Kesari A (2010) S4: Distributed stream computing. In: Proceedings of the 11th international conference on data mining workshops, pp 170\u2013177"},{"issue":"1","key":"242_CR31","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/984334.984339","volume":"7","author":"J Park","year":"2004","unstructured":"Park J, Sandhu R (2004) The $$\\text{ UCON }_{\\text{ ABC }}$$ UCON ABC usage control model. ACM Trans Inform Syst Secur 7(1):128\u2013174","journal-title":"ACM Trans Inform Syst Secur"},{"key":"242_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium on foundations of computer science, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"242_CR33","unstructured":"Protocol Buffers: Google\u2019s data interchange format. Accessed 2 March 2015. https:\/\/code.google.com\/p\/protobuf\/"},{"issue":"1","key":"242_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-8(1:9)2012","volume":"8","author":"G Ro\u015fu","year":"2012","unstructured":"Ro\u015fu G, Chen F (2012) Semantics and algorithms for parametric monitoring. Log Method Comput Sci 8(1):1\u201347","journal-title":"Log Method Comput Sci"},{"key":"242_CR35","doi-asserted-by":"crossref","unstructured":"Roger M, Goubault-Larrecq J (2001) Log auditing through model-checking. In: Proceedings of the 14th IEEE computer security foundations workshop, pp 220\u2013234","DOI":"10.1109\/CSFW.2001.930148"},{"issue":"3","key":"242_CR36","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":"242_CR37","unstructured":"STORM: Distributed and fault-tolerant realtime computation. Apache Storm. Accessed 2 March 2015. https:\/\/storm.apache.org"},{"issue":"7","key":"242_CR38","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1145\/358557.358577","volume":"25","author":"M Weiser","year":"1982","unstructured":"Weiser M (1982) Programmers use slices when debugging. Commun ACM 25(7):446\u2013452","journal-title":"Commun ACM"},{"issue":"4","key":"242_CR39","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/1108906.1108908","volume":"8","author":"X Zhang","year":"2005","unstructured":"Zhang X, Parisi-Presicce F, Sandhu R, Park J (2005) Formal model and policy specification of usage control. ACM Trans Inform Syst Secur 8(4):351\u2013387","journal-title":"ACM Trans Inform Syst Secur"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0242-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0242-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0242-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0242-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:55Z","timestamp":1559253955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0242-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,7]]},"references-count":39,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["242"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0242-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,7]]}}}