{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:22:08Z","timestamp":1760016128316,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":24,"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"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,7,13]]},"DOI":"10.1145\/3092282.3092303","type":"proceedings-article","created":{"date-parts":[[2017,7,13]],"date-time":"2017-07-13T13:45:49Z","timestamp":1499953549000},"page":"102-111","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Practical controller synthesis for MTL\n            <sub>0,\u221e<\/sub>"],"prefix":"10.1145","author":[{"given":"Guangyuan","family":"Li","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University at Chinese Academy of Sciences, China"}]},{"given":"Peter Gj\u00f8l","family":"Jensen","sequence":"additional","affiliation":[{"name":"Aalborg University, Denmark"}]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[{"name":"Aalborg University, Denmark"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Danny B\u00f8gsted","family":"Poulsen","sequence":"additional","affiliation":[{"name":"University of Kiel, Germany"}]}],"member":"320","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038685"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_3_2_1_4_1","volume-title":"Springer","author":"Behrmann G.","year":"2007","unstructured":"G. Behrmann , A. Cougnard , A. David , E. Fleury , K. G. Larsen , and D. Lime . Uppaal-tiga: Time for playing games! In Proceedings of the 19th International Conference on Computer Aided Verification, number 4590 in LNCS, pages 121\u2013125 . Springer , 2007 . G. Behrmann, A. Cougnard, A. David, E. Fleury, K. G. Larsen, and D. Lime. Uppaal-tiga: Time for playing games! In Proceedings of the 19th International Conference on Computer Aided Verification, number 4590 in LNCS, pages 121\u2013125. Springer, 2007."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_30"},{"key":"e_1_3_2_1_6_1","first-page":"84","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"Brihaye T.","unstructured":"T. Brihaye , M. Esti\u00e9venart , and G. Geeraerts . On mitl and alternating timed automata over infinite words . In Formal Modeling and Analysis of Timed Systems , pages 69\u2013 84 . Springer, 2014. T. Brihaye, M. Esti\u00e9venart, and G. Geeraerts. On mitl and alternating timed automata over infinite words. In Formal Modeling and Analysis of Timed Systems, pages 69\u201384. Springer, 2014."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1969-0280205-0"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_15"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-013-0189-z"},{"key":"e_1_3_2_1_10_1","volume-title":"Automata. In Proc. International Mathematical Congress","author":"Church A.","year":"1962","unstructured":"A. Church . Logic, Arithmetic , Automata. In Proc. International Mathematical Congress , 1962 . A. Church. Logic, Arithmetic, Automata. In Proc. International Mathematical Congress, 1962."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04368-0_12"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04368-0_12"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_3_2_1_14_1","first-page":"290","volume-title":"In International Conference on Computer Aided Verification","author":"Geilen M.","unstructured":"M. Geilen . An improved on-the-fly tableau construction for a real-time temporal logic . In In International Conference on Computer Aided Verification , pages 276\u2013 290 . Springer, 2003. M. Geilen. An improved on-the-fly tableau construction for a real-time temporal logic. In In International Conference on Computer Aided Verification, pages 276\u2013 290. Springer, 2003."},{"key":"e_1_3_2_1_15_1","first-page":"326","volume-title":"Formal Techniques for Networked and SPIN\u201917","author":"Giannakopoulou D.","year":"2017","unstructured":"D. Giannakopoulou and F. Lerda . From states to transitions: Improving translation of ltl formulae to b\u00fcchi automata . In Formal Techniques for Networked and SPIN\u201917 , July 2017 , Santa Barbara, CA, USA G. Li, P. G. Jensen, K.G. Larsen, A. Legay, and D.B. Poulsen Distributed Sytems\u2014FORTE 2002, pages 308\u2013 326 . Springer, 2002. D. Giannakopoulou and F. Lerda. From states to transitions: Improving translation of ltl formulae to b\u00fcchi automata. In Formal Techniques for Networked and SPIN\u201917, July 2017, Santa Barbara, CA, USA G. Li, P. G. Jensen, K.G. Larsen, A. Legay, and D.B. Poulsen Distributed Sytems\u2014FORTE 2002, pages 308\u2013326. Springer, 2002."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_6"},{"key":"e_1_3_2_1_17_1","first-page":"507","volume-title":"MFCS","author":"Kupferman O.","year":"2000","unstructured":"O. Kupferman and M. Y. Vardi . \u00b5-calculus synthesis . In MFCS , pages 497\u2013 507 , 2000 . O. Kupferman and M. Y. Vardi. \u00b5-calculus synthesis. In MFCS, pages 497\u2013507, 2000."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11867340_20"},{"key":"e_1_3_2_1_19_1","first-page":"107","volume-title":"CAV","author":"Maler O.","year":"2007","unstructured":"O. Maler , D. Nickovic , and A. Pnueli . On synthesizing controllers from boundedresponse properties . In CAV , pages 95\u2013 107 , 2007 . O. Maler, D. Nickovic, and A. Pnueli. On synthesizing controllers from boundedresponse properties. In CAV, pages 95\u2013107, 2007."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59042-0_76"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/357233.357237"},{"key":"e_1_3_2_1_22_1","first-page":"128","volume-title":"MBMV","author":"Morgenstern A.","year":"2008","unstructured":"A. Morgenstern , K. Schneider , and S. Lamberti . Generating deterministic \u03c9automata for most ltl formulas by the breakpoint construction . In MBMV , pages 119\u2013 128 , 2008 . A. Morgenstern, K. Schneider, and S. Lamberti. Generating deterministic \u03c9automata for most ltl formulas by the breakpoint construction. In MBMV, pages 119\u2013128, 2008."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"}],"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.3092303","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3092282.3092303","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.3092303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,13]]},"references-count":24,"alternative-id":["10.1145\/3092282.3092303","10.1145\/3092282"],"URL":"https:\/\/doi.org\/10.1145\/3092282.3092303","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"}}]}}