{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:31Z","timestamp":1750306531524,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,10,20]],"date-time":"2014-10-20T00:00:00Z","timestamp":1413763200000},"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":["110020021"],"award-info":[{"award-number":["110020021"]}],"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":[[2014,10,20]]},"DOI":"10.1145\/2687357.2687366","type":"proceedings-article","created":{"date-parts":[[2015,1,5]],"date-time":"2015-01-05T13:32:15Z","timestamp":1420464735000},"page":"55-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Efficient TCTL Model Checking Algorithm for Timed Actors"],"prefix":"10.1145","author":[{"given":"Ehsan","family":"Khamespanah","sequence":"first","affiliation":[{"name":"University of Tehran, Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramtin","family":"Khosravi","sequence":"additional","affiliation":[{"name":"University of Tehran, Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[{"name":"Reykjavik University, Reykjavik, Iceland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,10,20]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Rebeca Home Page. http:\/\/www.rebeca-lang.org. Rebeca Home Page. http:\/\/www.rebeca-lang.org."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00022-X"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_4_1","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J.-P. Katoen . Principles of Model Checking . MIT Press , 2008 . ISBN 978-0--262-02649--9. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. ISBN 978-0--262-02649--9."},{"key":"e_1_3_2_1_5_1","series-title":"Lecture Notes in Computer Science","first-page":"232","volume-title":"Hybrid Systems","author":"Bengtsson J.","year":"1995","unstructured":"J. Bengtsson , K. G. Larsen , F. Larsson , P. Pettersson , and W. Yi . UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems . In R. Alur, T. A. Henzinger, and E. D. Sontag, editors, Hybrid Systems , volume 1066 of Lecture Notes in Computer Science , pages 232 -- 243 . Springer , 1995 . ISBN 3--540--61155-X. J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems. In R. Alur, T. A. Henzinger, and E. D. Sontag, editors, Hybrid Systems, volume 1066 of Lecture Notes in Computer Science, pages 232--243. Springer, 1995. ISBN 3--540--61155-X."},{"key":"e_1_3_2_1_6_1","first-page":"129","volume-title":"Theories and experiences for real-time system development","author":"Campos S. V.","year":"1994","unstructured":"S. V. Campos and E. M. Clarke . Theories and experiences for real-time system development . chapter Real-time Symbolic Model Checking for Discrete Time Models, pages 129 -- 145 . World Scientific Publishing Co., Inc. , River Edge, NJ, USA , 1994 . ISBN 981-02--1923--7. URL http:\/\/dl.acm.org\/citation.cfm?id=207907.207912. S. V. Campos and E. M. Clarke. Theories and experiences for real-time system development. chapter Real-time Symbolic Model Checking for Discrete Time Models, pages 129--145. World Scientific Publishing Co., Inc., River Edge, NJ, USA, 1994. ISBN 981-02--1923--7. URL http:\/\/dl.acm.org\/citation.cfm?id=207907.207912."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1994.342709"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_39"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00355298"},{"key":"e_1_3_2_1_10_1","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"Garey M. R.","year":"1979","unstructured":"M. R. Garey and D. S. Johnson . Computers and Intractability: A Guide to the Theory of NP-Completeness . W. H. Freeman , 1979 . ISBN 0--7167--1044--7. M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979. ISBN 0--7167--1044--7."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967707"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2414639.2414645"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00644-8"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.020"},{"key":"e_1_3_2_1_15_1","volume-title":"Simulation-Based Analysis of Timed Rebeca Using TeProp and SQL. Master's thesis","author":"Magnusson B.","year":"2012","unstructured":"B. Magnusson . Simulation-Based Analysis of Timed Rebeca Using TeProp and SQL. Master's thesis , Reykjavk University , School of Computer Science, Iceland, 2012 . http:\/\/rebeca.cs.ru.is\/files\/MasterThesisBrynjarMagnusson2012.pdf. B. Magnusson. Simulation-Based Analysis of Timed Rebeca Using TeProp and SQL. Master's thesis, Reykjavk University, School of Computer Science, Iceland, 2012. http:\/\/rebeca.cs.ru.is\/files\/MasterThesisBrynjarMagnusson2012.pdf."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1006\/jagm.2001.1201"},{"key":"e_1_3_2_1_17_1","series-title":"Communications in Computer and Information Science","first-page":"178","volume-title":"C. Artho and P. C. \u00d6lveczky","author":"Sabahi-Kaviani Z.","year":"2013","unstructured":"Z. Sabahi-Kaviani , R. Khosravi , M. Sirjani , P.C. \u00d6lveczky , and E. Khamespanah . Formal semantics and analysis of timed rebeca in real-time maude . In C. Artho and P. C. \u00d6lveczky , editors, FTSCS, volume 419 of Communications in Computer and Information Science , pages 178 -- 194 . Springer , 2013 . ISBN 978--3--319-05415--5. Z. Sabahi-Kaviani, R. Khosravi, M. Sirjani, P.C. \u00d6lveczky, and E. Khamespanah. Formal semantics and analysis of timed rebeca in real-time maude. In C. Artho and P. C. \u00d6lveczky, editors, FTSCS, volume 419 of Communications in Computer and Information Science, pages 178--194. Springer, 2013. ISBN 978--3--319-05415--5."},{"key":"e_1_3_2_1_18_1","first-page":"66","article-title":"Functional and performance analysis of network-onchips using actor-based modeling and formal verification","author":"Sharifi Z.","year":"2013","unstructured":"Z. Sharifi , M. Mosaffa , S. Mohammadi , and M. Sirjani . Functional and performance analysis of network-onchips using actor-based modeling and formal verification . ECEASST , 66 , 2013 . Z. Sharifi, M. Mosaffa, S. Mohammadi, and M. Sirjani. Functional and performance analysis of network-onchips using actor-based modeling and formal verification. ECEASST, 66, 2013.","journal-title":"ECEASST"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24933-4_3"},{"issue":"4","key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","first-page":"385","DOI":"10.3233\/FUN-2004-63405","volume":"63","author":"Sirjani M.","year":"2004","unstructured":"M. Sirjani , A. Movaghar , A. Shali , and F. S. de Boer . Modeling and Verification of Reactive Systems using Rebeca . Fundam. Inform. , 63 ( 4 ): 385 -- 410 , 2004 . M. Sirjani, A. Movaghar, A. Shali, and F. S. de Boer. Modeling and Verification of Reactive Systems using Rebeca. Fundam. Inform., 63(4):385--410, 2004.","journal-title":"Fundam. Inform."}],"event":{"name":"SPLASH '14: Conference on Systems, Programming, and Applications: Software for Humanity","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"],"location":"Portland Oregon USA","acronym":"SPLASH '14"},"container-title":["Proceedings of the 4th International Workshop on Programming based on Actors Agents & Decentralized Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2687357.2687366","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2687357.2687366","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:14Z","timestamp":1750227134000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2687357.2687366"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,20]]},"references-count":20,"alternative-id":["10.1145\/2687357.2687366","10.1145\/2687357"],"URL":"https:\/\/doi.org\/10.1145\/2687357.2687366","relation":{},"subject":[],"published":{"date-parts":[[2014,10,20]]},"assertion":[{"value":"2014-10-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}