{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:22:07Z","timestamp":1750220527485,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,8,18]],"date-time":"2021-08-18T00:00:00Z","timestamp":1629244800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100017637","name":"Simons Institute for the Theory of Computing, University of California Berkeley","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100017637","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["PhD Fellowship"],"award-info":[{"award-number":["PhD Fellowship"]}],"id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,8,20]]},"DOI":"10.1145\/3468264.3468557","type":"proceedings-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T01:40:03Z","timestamp":1629337203000},"page":"131-143","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Checking LTL[F,G,X] on compressed traces in polynomial time"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5017-2228","authenticated-orcid":false,"given":"Minjian","family":"Zhang","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2021. JavaMOP. https:\/\/github.com\/runtimeverification\/javamop Accessed: 2021-02-24.  2021. JavaMOP. https:\/\/github.com\/runtimeverification\/javamop Accessed: 2021-02-24."},{"key":"e_1_3_2_1_2_1","unstructured":"2021. Rabinizer 4 - From LTL to Your Favourite Deterministic Automaton. https:\/\/www7.in.tum.de\/ kretinsk\/rabinizer4.html Accessed: 2021-02-24.  2021. Rabinizer 4 - From LTL to Your Favourite Deterministic Automaton. https:\/\/www7.in.tum.de\/ kretinsk\/rabinizer4.html Accessed: 2021-02-24."},{"volume-title":"Sequitur: Inferring Hierarchies From Sequences","key":"e_1_3_2_1_3_1","unstructured":"2021. Sequitur: Inferring Hierarchies From Sequences . http:\/\/www.sequitur.info\/ Accessed: 2021-02-24. 2021. Sequitur: Inferring Hierarchies From Sequences. http:\/\/www.sequitur.info\/ Accessed: 2021-02-24."},{"key":"e_1_3_2_1_4_1","unstructured":"2021. ZipMOP. https:\/\/github.com\/minjian233\/ZIPMOP Accessed: 2021-06-20.  2021. ZipMOP. https:\/\/github.com\/minjian233\/ZIPMOP Accessed: 2021-06-20."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/963927.963928"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3422-8_30"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(96)00014-8"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2372785"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297069"},{"volume-title":"Succinct Encodings of Graph Isomorphism","author":"Das Bireswar","key":"e_1_3_2_1_12_1","unstructured":"Bireswar Das , Patrick Scharpfenecker , and Jacobo Tor\u00e1n . 2014. Succinct Encodings of Graph Isomorphism . In Language and Automata Theory and Applications, Adrian-Horia Dediu, Carlos Mart\u00edn-Vide, Jos\u00e9-Luis Sierra-Rodr\u00edguez, and Bianca Truthe (Eds.). Springer International Publishing , Cham . 285\u2013296. isbn:978-3-319-04921-2 Bireswar Das, Patrick Scharpfenecker, and Jacobo Tor\u00e1n. 2014. Succinct Encodings of Graph Isomorphism. In Language and Automata Theory and Applications, Adrian-Horia Dediu, Carlos Mart\u00edn-Vide, Jos\u00e9-Luis Sierra-Rodr\u00edguez, and Bianca Truthe (Eds.). Springer International Publishing, Cham. 285\u2013296. isbn:978-3-319-04921-2"},{"volume-title":"Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI \u201913)","author":"Giacomo Giuseppe De","key":"e_1_3_2_1_13_1","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi . 2013. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces . In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI \u201913) . AAAI Press, 854\u2013860. isbn:9781577356332 Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI \u201913). AAAI Press, 854\u2013860. isbn:9781577356332"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"J. Feigenbaum S. Kannan M. Y. Vardi and M. Viswanathan. 1998. Complexity of problems on graphs represented as OBDDs. In STACS 98 Michel Morvan Christoph Meinel and Daniel Krob (Eds.). Springer Berlin Heidelberg Berlin Heidelberg. 216\u2013226. isbn:978-3-540-69705-3  J. Feigenbaum S. Kannan M. Y. Vardi and M. Viswanathan. 1998. Complexity of problems on graphs represented as OBDDs. In STACS 98 Michel Morvan Christoph Meinel and Daniel Krob (Eds.). Springer Berlin Heidelberg Berlin Heidelberg. 216\u2013226. isbn:978-3-540-69705-3","DOI":"10.1007\/BFb0028563"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80004-7"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/781498.781530"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_15"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/872023.872572"},{"volume-title":"A Retrospective Look at the Monitoring and Checking (MaC) Framework","author":"Kannan Sampath","key":"e_1_3_2_1_20_1","unstructured":"Sampath Kannan , Moonzoo Kim , Insup Lee , Oleg Sokolsky , and Mahesh Viswanathan . 2019. A Retrospective Look at the Monitoring and Checking (MaC) Framework . In Runtime Verification, Bernd Finkbeiner and Leonardo Mariani (Eds.). Springer International Publishing , Cham . 1\u201314. Sampath Kannan, Moonzoo Kim, Insup Lee, Oleg Sokolsky, and Mahesh Viswanathan. 2019. A Retrospective Look at the Monitoring and Checking (MaC) Framework. In Runtime Verification, Bernd Finkbeiner and Leonardo Mariani (Eds.). Springer International Publishing, Cham. 1\u201314."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.841160"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.850665"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236025"},{"volume-title":"Rabinizer 4: From LTL to Your Favourite Deterministic Automaton","author":"K\u0159et\u00ednsk\u00fd Jan","key":"e_1_3_2_1_24_1","unstructured":"Jan K\u0159et\u00ednsk\u00fd , Tobias Meggendorfer , Salomon Sickert , and Christopher Ziegler . 2018. Rabinizer 4: From LTL to Your Favourite Deterministic Automaton . In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing , Cham . 567\u2013577. isbn:978-3-319-96145-3 Jan K\u0159et\u00ednsk\u00fd, Tobias Meggendorfer, Salomon Sickert, and Christopher Ziegler. 2018. Rabinizer 4: From LTL to Your Favourite Deterministic Automaton. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham. 567\u2013577. isbn:978-3-319-96145-3"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.892708"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301678"},{"volume-title":"Runtime Assurance Based On Formal Specifications. In In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications.","author":"Lee I.","key":"e_1_3_2_1_27_1","unstructured":"I. Lee , S. Kannan , M. Kim , O. Sokolsky , and M. Viswanathan . 1999 . Runtime Assurance Based On Formal Specifications. In In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications. I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan. 1999. Runtime Assurance Based On Formal Specifications. In In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications."},{"volume-title":"2016 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE). 602\u2013613","author":"Legunsen O.","key":"e_1_3_2_1_28_1","unstructured":"O. Legunsen , W. U. Hassan , X. Xu , G. Ro\u015fu , and D. Marinov . 2016. How good are the specs? A study of the bug-finding effectiveness of existing Java API specifications . In 2016 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE). 602\u2013613 . O. Legunsen, W. U. Hassan, X. Xu, G. Ro\u015fu, and D. Marinov. 2016. How good are the specs? A study of the bug-finding effectiveness of existing Java API specifications. In 2016 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE). 602\u2013613."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1006209.1006227"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1515\/gcc-2012-0016"},{"key":"e_1_3_2_1_31_1","volume-title":"Balc\u00e1zar","author":"Lozano Antonio","year":"1990","unstructured":"Antonio Lozano and Jos\u00e9 L . Balc\u00e1zar . 1990 . The complexity of graph problems for succinctly represented graphs. In Graph-Theoretic Concepts in Computer Science, Manfred Nagl (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 277\u2013286. isbn:978-3-540-46950-6 Antonio Lozano and Jos\u00e9 L. Balc\u00e1zar. 1990. The complexity of graph problems for succinctly represented graphs. In Graph-Theoretic Concepts in Computer Science, Manfred Nagl (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 277\u2013286. isbn:978-3-540-46950-6"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41857"},{"volume-title":"CONCUR 2003 - Concurrency Theory, Roberto Amadio and Denis Lugiez (Eds.). Springer Berlin Heidelberg","author":"Markey N.","key":"e_1_3_2_1_33_1","unstructured":"N. Markey and P. Schnoebelen . 2003. Model Checking a Path . In CONCUR 2003 - Concurrency Theory, Roberto Amadio and Denis Lugiez (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 251\u2013265. isbn:978-3-540-45187-7 N. Markey and P. Schnoebelen. 2003. Model Checking a Path. In CONCUR 2003 - Concurrency Theory, Roberto Amadio and Denis Lugiez (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 251\u2013265. isbn:978-3-540-45187-7"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0198-6"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMRTS.1999.777457"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-SEIP52600.2021.00038"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80009-2"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397356"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377813.3381369"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081721"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1039834.1039864"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.42"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2004.1317473"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.1996.507675"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1330017.1330021"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1984.1659158"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.841161"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1977.1055714"}],"event":{"name":"ESEC\/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Athens Greece","acronym":"ESEC\/FSE '21"},"container-title":["Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468264.3468557","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3468264.3468557","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3468264.3468557","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:50Z","timestamp":1750195490000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468264.3468557"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,18]]},"references-count":49,"alternative-id":["10.1145\/3468264.3468557","10.1145\/3468264"],"URL":"https:\/\/doi.org\/10.1145\/3468264.3468557","relation":{},"subject":[],"published":{"date-parts":[[2021,8,18]]},"assertion":[{"value":"2021-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}