{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T06:10:02Z","timestamp":1746079802233,"version":"3.40.4"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2013,12,17]],"date-time":"2013-12-17T00:00:00Z","timestamp":1387238400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s00236-013-0189-z","type":"journal-article","created":{"date-parts":[[2013,12,16]],"date-time":"2013-12-16T01:47:55Z","timestamp":1387158475000},"page":"165-192","source":"Crossref","is-referenced-by-count":5,"title":["Efficient controller synthesis for a fragment of $$\\hbox {MTL}_{0, \\infty }$$ MTL 0 , \u221e"],"prefix":"10.1007","volume":"51","author":[{"given":"Peter","family":"Bulychev","sequence":"first","affiliation":[]},{"given":"Alexandre","family":"David","sequence":"additional","affiliation":[]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Guangyuan","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,17]]},"reference":[{"key":"189_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R: Formal verification of hybrid systems. In: Proceedings of the\u00a0 Ninth ACM International Conference on Embedded Software (EMSOFT \u201911), pap. 273\u2013278. ACM, New York, NY, USA (2011)","DOI":"10.1145\/2038642.2038685"},{"key":"189_CR2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"189_CR3","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"189_CR4","doi-asserted-by":"crossref","unstructured":"Babiak, T., Kret\u00ednsk\u00fd, M., Reh\u00e1k, V., Strejcek, J.: LTL to B\u00fcchi Automata Translation: Fast and More Deterministic. CoRR, abs\/1201.0682 (2012)","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"189_CR5","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: time for playing games! In: Proceedings of the 19th International Conference on Computer Aided Verification, Number 4590 in LNCS, pp. 121\u2013125. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"189_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"A Tutorial on Uppaal","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, Re, Larsen, K.G.: A Tutorial on Uppaal. Springer, Berlin (2004)"},{"key":"189_CR7","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification (2007)","DOI":"10.1016\/j.entcs.2007.09.004"},{"issue":"3","key":"189_CR8","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"189_CR9","doi-asserted-by":"crossref","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Proceedings of the 24th International Conference on Computer Aided Verification, CAV\u201912, pp. 652\u2013657. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"189_CR10","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Bozzelli, L., Chevalier, F.: Controller synthesis for MTL specifications. In: Proceedings of the 17th International Conference on Concurrency Theory (CONCUR\u201906) (2006)","DOI":"10.1007\/11817949_30"},{"key":"189_CR11","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"JR Buchi","year":"1969","unstructured":"Buchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295\u2013311 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"189_CR12","doi-asserted-by":"crossref","unstructured":"Bulychev, P., David, A., Larsen, K.\u00a0G., Legay, A., Li, G., Poulsen, D.\u00a0B., Stainer, A.: Monitor-based statistical model checking for weighted metric temporal logic. In: LPAR (2012)","DOI":"10.1007\/978-3-642-28717-6_15"},{"key":"189_CR13","doi-asserted-by":"crossref","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.\u00a0G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: CONCUR\u201905, volume 3653 of LNCS, pp. 66\u201380. Springer, Berlin (August 2005)","DOI":"10.1007\/11539452_9"},{"key":"189_CR14","unstructured":"Church, A.: Logic, Arithmetic. Automata. In: Proceedings of the International Mathematical Congress (1962)"},{"key":"189_CR15","doi-asserted-by":"crossref","unstructured":"David, A., Behrmann, G., Bulychev, P., Byg, J., Chatain, T., Larsen, T.G., Pettersson, P., Rasmussen, J., Srba, J., Yi, W., Joergensen, K.Y., Lime, D., Magnin, M., Roux, O.H., Traonouez, L.-M.: Tools for model-checking timed systems. In: Roux O.H., Claude, J. (eds.) Communicating Embedded Systems\u2014Software and Design, pp. 165\u2013225. ISTE Publishing, Wiley, New York (2009)","DOI":"10.1002\/9781118558188.ch6"},{"key":"189_CR16","unstructured":"Di Giampaolo, B., Geeraerts, G, Raskin, J.F., Sznajder, N.: Safraless procedures for timed specifications. In: Springer (ed.) Proceedings of FORMATS 2010, 8th International Conference on Formal Modelling and Analysis of Timed Systems, volume 6246 of, Lecture Notes in Computer Science, pp. 2\u201322, (2010)"},{"key":"189_CR17","doi-asserted-by":"crossref","unstructured":"Doyen, L., Geeraerts, G., Raskin, J.F., Reicher, J.: Realizability of real-time logics. In: Proceedings of FORMATS 2009, 7th International Conference on Formal Modeling and Analysis of Timed Systems, volume 5813 of Lecture Notes in Computer Science, pp. 133\u2013148. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04368-0_12"},{"key":"189_CR18","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: Touili, T., Cook, B., Jackson, P. (ed.) 22nd International Conference on Computer Aided Verification, volume 6174 of LNCS, pp. 365\u2013379. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_33"},{"issue":"3","key":"189_CR19","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"key":"189_CR20","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: CAV, pp. 263\u2013277 (2009)","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"189_CR21","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: Exploiting structure in LTL synthesis. Int. J. Softw. Tools Technol. Transf. (STTT) 541\u2013561 (2013). doi: 10.1007\/s10009-012-0222-5","DOI":"10.1007\/s10009-012-0222-5"},{"key":"189_CR22","doi-asserted-by":"crossref","unstructured":"G\u00f3mez, R., Bowman, H.: Efficient detection of zeno runs in timed automata. In: Proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS\u201907, pp. 195\u2013210. Springer, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-75454-1_15"},{"key":"189_CR23","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: 18th Conference on Computer Aided Verification, pp. 31\u201344 (2006)","DOI":"10.1007\/11817963_6"},{"key":"189_CR24","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: $$\\mu $$ \u03bc -Calculus synthesis. In: MFCS, pp. 497\u2013507 (2000)","DOI":"10.1007\/3-540-44612-5_45"},{"key":"189_CR25","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: Real time temporal logic: past, present, future. In: FORMATS, pp. 2\u201316 (2005)","DOI":"10.1007\/11603009_2"},{"key":"189_CR26","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: On synthesizing controllers from bounded-response properties. In: CAV, pp. 95\u2013107 (2007)","DOI":"10.1007\/978-3-540-73368-3_12"},{"key":"189_CR27","doi-asserted-by":"crossref","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) Proceedings of the STACS\u201995, LNCS 900, pp. 229\u2013242. Springer, Berlin (1995)","DOI":"10.1007\/3-540-59042-0_76"},{"issue":"1","key":"189_CR28","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6(1), 68\u201393 (1984)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"189_CR29","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS \u201905, pp. 188\u2013197. IEEE Computer Society, Washington, DC, USA (2005)","DOI":"10.1109\/LICS.2005.33"},{"key":"189_CR30","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Proceedings of the Verification, Model Checking, and Abstract Interpretation (VMCAI 06), pp. 364\u2013380. Springer, Berlin (2006)","DOI":"10.1007\/11609773_24"},{"key":"189_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL \u201989), pp. 179\u2013190. ACM, New York, NY, USA (1989)","DOI":"10.1145\/75277.75293"},{"issue":"1","key":"189_CR32","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"P Ramadge","year":"1987","unstructured":"Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206\u2013230 (1987)","journal-title":"SIAM J. Control Optim."},{"key":"189_CR33","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: ATVA, volume 4762 of Lecture Notes in Computer Science, pp. 474\u2013488. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-75596-8_33"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-013-0189-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-013-0189-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-013-0189-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T05:42:02Z","timestamp":1746078122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-013-0189-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,17]]},"references-count":33,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["189"],"URL":"https:\/\/doi.org\/10.1007\/s00236-013-0189-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2013,12,17]]}}}