{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:07:22Z","timestamp":1750306042163,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,7,13]],"date-time":"2017-07-13T00:00:00Z","timestamp":1499904000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001840","name":"Icelandic Centre for Research","doi-asserted-by":"publisher","award":["163205-051"],"award-info":[{"award-number":["163205-051"]}],"id":[{"id":"10.13039\/501100001840","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,7,13]]},"DOI":"10.1145\/3092282.3092294","type":"proceedings-article","created":{"date-parts":[[2017,7,13]],"date-time":"2017-07-13T13:45:49Z","timestamp":1499953549000},"page":"41-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["LeeTL: LTL with quantifications over model objects"],"prefix":"10.1145","author":[{"given":"Pouria","family":"Mellati","sequence":"first","affiliation":[{"name":"University of Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ehsan","family":"Khamespanah","sequence":"additional","affiliation":[{"name":"University of Tehran, Iran \/ Reykjavik University, Iceland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramtin","family":"Khosravi","sequence":"additional","affiliation":[{"name":"University of Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Joe Armstrong. 1997.  Joe Armstrong. 1997."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/258949.258967"},{"key":"e_1_3_2_1_3_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008.  Christel Baier and Joost-Pieter Katoen. 2008."},{"key":"e_1_3_2_1_4_1","unstructured":"Principles of Model Checking. MIT Press. I\u2013XVII 1\u2013975 pages.  Principles of Model Checking. MIT Press. I\u2013XVII 1\u2013975 pages."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090200075"},{"key":"e_1_3_2_1_6_1","unstructured":"Claudio Demartini Radu Iosif and Riccardo Sisto. 1999.  Claudio Demartini Radu Iosif and Riccardo Sisto. 1999."},{"volume-title":"5th and 6th International SPIN Workshops","year":"1999","key":"e_1_3_2_1_7_1","unstructured":"dSPIN : A Dynamic Extension of SPIN. In Theoretical and Practical Aspects of SPIN Model Checking , 5th and 6th International SPIN Workshops , Trento, Italy , July 5, 1999 , Toulouse, France, September 21 and 24 1999, Proceedings (Lecture Notes in Computer Science), Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink (Eds.), Vol. 1680. dSPIN: A Dynamic Extension of SPIN. In Theoretical and Practical Aspects of SPIN Model Checking, 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24 1999, Proceedings (Lecture Notes in Computer Science), Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink (Eds.), Vol. 1680."},{"key":"e_1_3_2_1_8_1","unstructured":"Springer 261\u2013276.  Springer 261\u2013276."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_21"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the Fifteenth IFIP WG6. 1 International Symposium on Protocol Specification, Testing and Verification. IFIP. LeeTL: LTL with Quantifications over Model Objects SPIN\u201917","author":"Gerth Rob","year":"1995","unstructured":"Rob Gerth , Doron Peled , Moshe Y Vardi , and Pierre Wolper . 1995 . Simple onthe-fly automatic verification of linear temporal logic . In Proceedings of the Fifteenth IFIP WG6. 1 International Symposium on Protocol Specification, Testing and Verification. IFIP. LeeTL: LTL with Quantifications over Model Objects SPIN\u201917 , July 2017, Santa Barbara, CA, USA Rob Gerth, Doron Peled, Moshe Y Vardi, and Pierre Wolper. 1995. Simple onthe-fly automatic verification of linear temporal logic. In Proceedings of the Fifteenth IFIP WG6. 1 International Symposium on Protocol Specification, Testing and Verification. IFIP. LeeTL: LTL with Quantifications over Model Objects SPIN\u201917, July 2017, Santa Barbara, CA, USA"},{"key":"e_1_3_2_1_11_1","unstructured":"Dimitra Giannakopoulou and Flavio Lerda. 2002.  Dimitra Giannakopoulou and Flavio Lerda. 2002."},{"key":"e_1_3_2_1_12_1","volume-title":"Formal Techniques for Networked and Distributed SytemsfiFORTE","author":"From","year":"2002","unstructured":"From states to transitions : Improving translation of LTL formulae to B \u00fcchi automata . In Formal Techniques for Networked and Distributed SytemsfiFORTE 2002 . Springer , 308\u2013326. From states to transitions: Improving translation of LTL formulae to B \u00fcchi automata. In Formal Techniques for Networked and Distributed SytemsfiFORTE 2002. Springer, 308\u2013326."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000017721.39909.4b"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000017721.39909.4b"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0164-1212(03)00062-1"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-009-0111-x"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of FACS","author":"Sabouri Hamideh","year":"2008","unstructured":"Hamideh Sabouri and Marjan Sirjani . 2008 . Slicing-Based Reductions for Rebeca . In Proceedings of FACS 2008. ENTCS. Hamideh Sabouri and Marjan Sirjani. 2008. Slicing-Based Reductions for Rebeca. In Proceedings of FACS 2008. ENTCS."},{"key":"e_1_3_2_1_19_1","volume-title":"Rebeca: Theory, applications, and tools. In Formal Methods for Components and Objects","author":"Sirjani Marjan","year":"2007","unstructured":"Marjan Sirjani . 2007 . Rebeca: Theory, applications, and tools. In Formal Methods for Components and Objects . Springer , 102\u2013126. Marjan Sirjani. 2007. Rebeca: Theory, applications, and tools. In Formal Methods for Components and Objects. Springer, 102\u2013126."},{"key":"e_1_3_2_1_20_1","first-page":"1695","article-title":"Modular Verification of a Component-Based Actor Language","volume":"11","author":"Sirjani Marjan","year":"2005","unstructured":"Marjan Sirjani , Frank S. de Boer , and Ali Movaghar-Rahimabadi . 2005 . Modular Verification of a Component-Based Actor Language . J. UCS 11 , 10 (2005), 1695 \u2013 1717 . Marjan Sirjani, Frank S. de Boer, and Ali Movaghar-Rahimabadi. 2005. Modular Verification of a Component-Based Actor Language. J. UCS 11, 10 (2005), 1695\u2013 1717.","journal-title":"J. UCS"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Marjan Sirjani and Mohammad Mahdi Jaghoori. 2011. Ten Years of Analyzing Actors: Rebeca Experience. In Formal Modeling: Actors Open Systems Biological Systems. 20\u201356.   Marjan Sirjani and Mohammad Mahdi Jaghoori. 2011. Ten Years of Analyzing Actors: Rebeca Experience. In Formal Modeling: Actors Open Systems Biological Systems. 20\u201356.","DOI":"10.1007\/978-3-642-24933-4_3"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.08.002"}],"event":{"name":"ISSTA '17: International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Santa Barbara CA USA","acronym":"ISSTA '17"},"container-title":["Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092282.3092294","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3092282.3092294","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:08Z","timestamp":1750215788000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092282.3092294"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,13]]},"references-count":22,"alternative-id":["10.1145\/3092282.3092294","10.1145\/3092282"],"URL":"https:\/\/doi.org\/10.1145\/3092282.3092294","relation":{},"subject":[],"published":{"date-parts":[[2017,7,13]]},"assertion":[{"value":"2017-07-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}