{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T19:27:52Z","timestamp":1780342072498,"version":"3.54.1"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,5,6]],"date-time":"2015-05-06T00:00:00Z","timestamp":1430870400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Nokia Research Center, Switzerland"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2015,5,6]]},"abstract":"<jats:p>Runtime monitoring is a general approach to verifying system properties at runtime by comparing system events against a specification formalizing which event sequences are allowed. We present a runtime monitoring algorithm for a safety fragment of metric first-order temporal logic that overcomes the limitations of prior monitoring algorithms with respect to the expressiveness of their property specification languages. Our approach, based on automatic structures, allows the unrestricted use of negation, universal and existential quantification over infinite domains, and the arbitrary nesting of both past and bounded future operators. Furthermore, we show how to use and optimize our approach for the common case where structures consist of only finite relations, over possibly infinite domains. We also report on case studies from the domain of security and compliance in which we empirically evaluate the presented algorithms. Taken together, our results show that metric first-order temporal logic can serve as an effective specification language for expressing and monitoring a wide variety of practically relevant system properties.<\/jats:p>","DOI":"10.1145\/2699444","type":"journal-article","created":{"date-parts":[[2015,5,11]],"date-time":"2015-05-11T16:30:57Z","timestamp":1431361857000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":142,"title":["Monitoring Metric First-Order Temporal Properties"],"prefix":"10.1145","volume":"62","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[{"name":"ETH Zurich and NEC Europe Ltd., Heidelberg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samuel","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich and Scandit AG, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eugen","family":"Z\u0103linescu","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,5,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Congress. 2001","year":"2001","unstructured":"107th Congress. 2001 . Uniting and strengthening America by Providing Appropriate Tools Required to Intercept and Obstruct Terrorism Act of 2001 (USA PATRIOT ACT). Public Law 107-56. 107th Congress. 2001. Uniting and strengthening America by Providing Appropriate Tools Required to Intercept and Obstruct Terrorism Act of 2001 (USA PATRIOT ACT). Public Law 107-56."},{"key":"e_1_2_1_2_1","volume-title":"Foundations of Databases","author":"Abiteboul Serge","unstructured":"Serge Abiteboul , Richard Hull , and Victor Vianu . 1995. Foundations of Databases . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA . Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of Databases. Addison-Wesley Longman Publishing Co., Inc., Boston, MA."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_4_1","volume-title":"Henzinger","author":"Alur Rajeev","year":"1992","unstructured":"Rajeev Alur and Thomas A . Henzinger . 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 . Springer , Heidelberg, Germany, 74--106. Rajeev Alur and Thomas A. Henzinger. 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. Springer, Heidelberg, Germany, 74--106."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-004-0147-z"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 7th International Symposium on Frontiers of Combining Systems","author":"Baader Franz","unstructured":"Franz Baader , Andreas Bauer , and Marcel Lippmann . 2009. Runtime verification using a temporal description logic . In Proceedings of the 7th International Symposium on Frontiers of Combining Systems . Lecture Notes in Computer Science , vol. 5749 . Springer , Heidelberg, Germany , 149--164. Franz Baader, Andreas Bauer, and Marcel Lippmann. 2009. Runtime verification using a temporal description logic. In Proceedings of the 7th International Symposium on Frontiers of Combining Systems. Lecture Notes in Computer Science, vol. 5749. Springer, Heidelberg, Germany, 149--164."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02138-1_2"},{"key":"e_1_2_1_9_1","volume-title":"Rydeheard","author":"Barringer Howard","year":"2012","unstructured":"Howard Barringer , Yli\u00e9s Falcone , Klaus Havelund , Giles Reger , and David E . Rydeheard . 2012 . Quantified event automata: Towards expressive and efficient runtime monitors. In Proceedings of the 18th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 7436 . Springer , Heidelberg, Germany, 68--84. Howard Barringer, Yli\u00e9s Falcone, Klaus Havelund, Giles Reger, and David E. Rydeheard. 2012. Quantified event automata: Towards expressive and efficient runtime monitors. In Proceedings of the 18th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 7436. Springer, Heidelberg, Germany, 68--84."},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation","author":"Barringer Howard","unstructured":"Howard Barringer , Allen Goldberg , Klaus Havelund , and Koushik Sen . 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 . Springer , Heidelberg, Germany , 44--57. Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. 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. Springer, Heidelberg, Germany, 44--57."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2514\/1.49356"},{"key":"e_1_2_1_12_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 18th International Symposium on Formal Methods","author":"Barringer Howard","unstructured":"Howard Barringer and Klaus Havelund . 2011. TraceContract: A scala DSL for trace analysis . In Proceedings of the 18th International Symposium on Formal Methods . Lecture Notes in Computer Science , vol. 6664 . Springer , Heidelberg, Germany , 57--72. Howard Barringer and Klaus Havelund. 2011. TraceContract: A scala DSL for trace analysis. In Proceedings of the 18th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 6664. Springer, Heidelberg, Germany, 57--72."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn076"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.32"},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computing Science","volume-title":"Proceedings of the 5th International Conference on Runtime Verification","author":"Basin David","unstructured":"David Basin , Germano Caronni , Sarah Ereth , Mat\u00fa\u0161 Harvan , Felix Klaedtke , and Heiko Mantel . 2014. Scalable offline monitoring . In Proceedings of the 5th International Conference on Runtime Verification . Lecture Notes in Computing Science , vol. 8734 . Springer , Heidelberg, Germany , 31--47. David Basin, Germano Caronni, Sarah Ereth, Mat\u00fa\u0161 Harvan, Felix Klaedtke, and Heiko Mantel. 2014. Scalable offline monitoring. In Proceedings of the 5th International Conference on Runtime Verification. Lecture Notes in Computing Science, vol. 8734. Springer, Heidelberg, Germany, 31--47."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_27"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.18"},{"key":"e_1_2_1_18_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 3rd International Conference on Runtime Verification","author":"Basin David","unstructured":"David Basin , Felix Klaedtke , Srdjan Marinovic , and Eugen Z\u0103linescu . 2013b. Monitoring compliance policies over incomplete and disagreeing logs . In Proceedings of the 3rd International Conference on Runtime Verification . Lecture Notes in Computer Science , vol. 7687 , Springer , Heidelberg, Germany , 151--167. David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Z\u0103linescu. 2013b. Monitoring compliance policies over incomplete and disagreeing logs. In Proceedings of the 3rd International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 7687, Springer, Heidelberg, Germany, 151--167."},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 4th International Conference on Runtime Verification","author":"Basin David","unstructured":"David Basin , Felix Klaedtke , Srdjan Marinovic , and Eugen Z\u0103linescu . 2013c. Monitoring of temporal first-order properties with aggregations . In Proceedings of the 4th International Conference on Runtime Verification . Lecture Notes in Computer Science , vol. 8174 . Springer , Heidelberg, Germany , 40--58. David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Z\u0103linescu. 2013c. Monitoring of temporal first-order properties with aggregations. In Proceedings of the 4th International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 8174. Springer, Heidelberg, Germany, 40--58."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1809842.1809849"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_1"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs). LIPIcs","volume":"2","author":"Basin David","year":"2008","unstructured":"David Basin , Felix Klaedtke , Samuel M\u00fcller , and Birgit Pfitzmann . 2008 . Runtime monitoring of metric first-order temporal properties . In Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs). LIPIcs , vol. 2 . Schloss Dagstuhl - Leibniz Center for Informatics, 49--60. David Basin, Felix Klaedtke, Samuel M\u00fcller, and Birgit Pfitzmann. 2008. Runtime monitoring of metric first-order temporal properties. In Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs). LIPIcs, vol. 2. Schloss Dagstuhl - Leibniz Center for Informatics, 49--60."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_20"},{"key":"e_1_2_1_24_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 18th International Symposium on Formal Methods","author":"Bauer Andreas","unstructured":"Andreas Bauer and Yli\u00e9s Falcone . 2012. Decentralised LTL monitoring . In Proceedings of the 18th International Symposium on Formal Methods . Lecture Notes in Computer Science , vol. 7436 . Springer , Heidelberg, Germany , 85--100. Andreas Bauer and Yli\u00e9s Falcone. 2012. Decentralised LTL monitoring. In Proceedings of the 18th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 7436. Springer, Heidelberg, Germany, 85--100."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_6"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-004-1133-y"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/210197.210200"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1995.1088"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.404030"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/383891.383892"},{"key":"e_1_2_1_32_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedinggs of the 1981 Workshop on Logics of Programs","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke and E. Allen Emerson . 1982. Design and synthesis of synchronization skeletons using branching-time temporal logic . In Proceedinggs of the 1981 Workshop on Logics of Programs . Lecture Notes in Computer Science , vol. 131 . Springer , Heidelberg, Germany , 52--71. Edmund M. Clarke and E. Allen Emerson. 1982. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedinggs of the 1981 Workshop on Logics of Programs. Lecture Notes in Computer Science, vol. 131. Springer, Heidelberg, Germany, 52--71."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187677"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2005.26"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1327452.1327492"},{"key":"e_1_2_1_36_1","unstructured":"Department of the Treasury. 1970. Bank Secrecy Act of 1970 (BSA). 31 USC 5311-5332 and 31 CFR 103.  Department of the Treasury. 1970. Bank Secrecy Act of 1970 (BSA). 31 USC 5311-5332 and 31 CFR 103."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/321510.321524"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89247-2_6"},{"key":"e_1_2_1_39_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 12th European Symposium on Research in Computer Security","author":"Dougherty Daniel J.","unstructured":"Daniel J. Dougherty , Kathi Fisler , and Shriram Krishnamurthi . 2007. Obligations and their interaction with programs . In Proceedings of the 12th European Symposium on Research in Computer Security . Lecture Notes in Computer Science , vol. 4734 . Springer , Heidelberg, Germany , 375--289. Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. 2007. Obligations and their interaction with programs. In Proceedings of the 12th European Symposium on Research in Computer Security. Lecture Notes in Computer Science, vol. 4734. Springer, Heidelberg, Germany, 375--289."},{"key":"e_1_2_1_40_1","volume-title":"A Mathematical Introduction to Logic","author":"Enderton Herbert B.","unstructured":"Herbert B. Enderton . 1972. A Mathematical Introduction to Logic . Academic Press, San Diego , CA. Herbert B. Enderton. 1972. A Mathematical Introduction to Logic. Academic Press, San Diego, CA."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/501978.501980"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000017718.28096.48"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046726"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/872023.872506"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 18th Annual Conference on Legal Knowledge and Information Systems (Frontiers Artificial Intelligence Appl.). Frontiers in Artificial Intelligence and Applications","volume":"134","author":"Giblin Christopher","year":"2005","unstructured":"Christopher Giblin , Alice Y. Liu , Samuel M\u00fcller , Birgit Pfitzmann , and Xin Zhou . 2005 . Regulations expressed as logical models (REALM) . In Proceedings of the 18th Annual Conference on Legal Knowledge and Information Systems (Frontiers Artificial Intelligence Appl.). Frontiers in Artificial Intelligence and Applications , vol. 134 . IOS Press, Amsterdam, The Netherlands, 37--48. Christopher Giblin, Alice Y. Liu, Samuel M\u00fcller, Birgit Pfitzmann, and Xin Zhou. 2005. Regulations expressed as logical models (REALM). In Proceedings of the 18th Annual Conference on Legal Knowledge and Information Systems (Frontiers Artificial Intelligence Appl.). Frontiers in Artificial Intelligence and Applications, vol. 134. IOS Press, Amsterdam, The Netherlands, 37--48."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2011.10"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0117-6"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0080-7"},{"key":"e_1_2_1_49_1","series-title":"Lecture Notes in Computer Science","volume-title":"Mona: Monadic second-order logic in practice. In Proceedings of the 1st International Workshop on Tools and Algorithms for Contruction and Analysis of Systems","author":"Henriksen Jesper G.","year":"1995","unstructured":"Jesper G. Henriksen , Jakob L. Jensen , Michael E. J\u00f8rgensen , Nils Klarlund , Robert Paige , Theis Rauhe , and Anders Sandholm . 1995 . Mona: Monadic second-order logic in practice. In Proceedings of the 1st International Workshop on Tools and Algorithms for Contruction and Analysis of Systems . Lecture Notes in Computer Science , vol. 1019 . Springer, Heidelberg , Germany , 89--110. Jesper G. Henriksen, Jakob L. Jensen, Michael E. J\u00f8rgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. 1995. Mona: Monadic second-order logic in practice. In Proceedings of the 1st International Workshop on Tools and Algorithms for Contruction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1019. Springer, Heidelberg, Germany, 89--110."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/93385.93429"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90005-G"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/11555827_7"},{"key":"e_1_2_1_53_1","volume-title":"Standard for SystemVerilog--Unified Hardware Design, Specification, and Verification Language. (December","author":"IEEE","year":"2009","unstructured":"IEEE Std 1800-2009 2009. Standard for SystemVerilog--Unified Hardware Design, Specification, and Verification Language. (December 2009 ). http:\/\/ieeexplore.ieee.org\/xpls\/abs&lowbar;all.jsp&quest;arnumber&equals;5354441&tag&equals;&equals;1. IEEE Std 1800-2009 2009. Standard for SystemVerilog--Unified Hardware Design, Specification, and Verification Language. (December 2009). http:\/\/ieeexplore.ieee.org\/xpls\/abs&lowbar;all.jsp&quest;arnumber&equals;5354441&tag&equals;&equals;1."},{"key":"e_1_2_1_54_1","volume-title":"Standard for Property Specification Language (PSL). (June","author":"IEEE","year":"2012","unstructured":"IEEE Std 1850-2010 2012. Standard for Property Specification Language (PSL). (June 2012 ).http:\/\/ieeexplore.ieee.org\/xpl\/articleDetails.jsp&quest;arnumber&equals;6228486. IEEE Std 1850-2010 2012. Standard for Property Specification Language (PSL). (June 2012).http:\/\/ieeexplore.ieee.org\/xpl\/articleDetails.jsp&quest;arnumber&equals;6228486."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00103-1"},{"key":"e_1_2_1_56_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Workshop on Logical and Computational Complexity","author":"Khoussainov Bakhadyr","unstructured":"Bakhadyr Khoussainov and Anil Nerode . 1995. Automatic presentations of structures . In Proceedings of the International Workshop on Logical and Computational Complexity . Lecture Notes in Computer Science , vol. 960 . Springer, Heidelberg , Germany , 367--392. Bakhadyr Khoussainov and Anil Nerode. 1995. Automatic presentations of structures. In Proceedings of the International Workshop on Logical and Computational Complexity. Lecture Notes in Computer Science, vol. 960. Springer, Heidelberg, Germany, 367--392."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200128X"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_59_1","volume-title":"Zuck","author":"Lichtenstein Orna","year":"1985","unstructured":"Orna Lichtenstein , Amir Pnueli , and Lenore D . Zuck . 1985 . The glory of the past. In Proceedings of the Conference on Logic of Programs. Lecture Notes in Computer Science, vol. 193 . Springer , Heidelberg, Germany, 196--218. Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. 1985. The glory of the past. In Proceedings of the Conference on Logic of Programs. Lecture Notes in Computer Science, vol. 193. Springer, Heidelberg, Germany, 196--218."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/0306-4379(87)90004-4"},{"key":"e_1_2_1_61_1","volume-title":"van der Aalst","author":"Maggi Fabrizio Maria","year":"2011","unstructured":"Fabrizio Maria Maggi , Marco Montali , Michael Westergaard , and Wil M. P . van der Aalst . 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 . Springer , Heidelberg, Germany, 132--147. Fabrizio Maria Maggi, Marco Montali, Michael Westergaard, and Wil M. P. van der Aalst. 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. Springer, Heidelberg, Germany, 132--147."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0247-9"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0198-6"},{"key":"e_1_2_1_64_1","unstructured":"MonPoly. 2013. MonPoly source code and examples. http:\/\/sourceforge.net\/projects\/monpoly.  MonPoly. 2013. MonPoly source code and examples. http:\/\/sourceforge.net\/projects\/monpoly."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_38"},{"issue":"1","key":"e_1_2_1_67_1","first-page":"4","article-title":"PostgreSQL","volume":"9","author":"PostgreSQL Global Development Group","year":"2012","unstructured":"PostgreSQL Global Development Group . 2012 . PostgreSQL , Version 9 . 1 . 4 . http:\/\/www.postgresql.org\/. PostgreSQL Global Development Group. 2012. PostgreSQL, Version 9.1.4. http:\/\/www.postgresql.org\/.","journal-title":"Version"},{"key":"e_1_2_1_68_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 3rd International Conference on Runtime Verification","author":"Reinbacher Thomas","unstructured":"Thomas Reinbacher , Matthias Fuegger , and J\u00f6rg Brauer . 2013. Real-time runtime verification on chip . In Proceedings of the 3rd International Conference on Runtime Verification . Lecture Notes in Computer Science , vol. 7687 . Springer , Heidelberg, Germany , 110--125. Thomas Reinbacher, Matthias Fuegger, and J\u00f6rg Brauer. 2013. Real-time runtime verification on chip. In Proceedings of the 3rd International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 7687. Springer, Heidelberg, Germany, 110--125."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873518"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:9)2012"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-6205-y"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.390251"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.007"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.5555\/2773579.2773774"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/114325.103712"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92701-3_7"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108906.1108908"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699444","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2699444","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:58Z","timestamp":1750227418000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699444"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,6]]},"references-count":77,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,5,6]]}},"alternative-id":["10.1145\/2699444"],"URL":"https:\/\/doi.org\/10.1145\/2699444","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,6]]},"assertion":[{"value":"2013-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-05-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}