{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:15Z","timestamp":1779074595456,"version":"3.51.4"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2019,11,9]],"date-time":"2019-11-09T00:00:00Z","timestamp":1573257600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,9]],"date-time":"2019-11-09T00:00:00Z","timestamp":1573257600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["UTC 17-S8401-10-C1"],"award-info":[{"award-number":["UTC 17-S8401-10-C1"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8650-15-C-2546"],"award-info":[{"award-number":["FA8650-15-C-2546"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N000141613165"],"award-info":[{"award-number":["N000141613165"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"publisher","award":["NNX17AD04G"],"award-info":[{"award-number":["NNX17AD04G"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s00236-019-00348-4","type":"journal-article","created":{"date-parts":[[2019,11,9]],"date-time":"2019-11-09T20:02:40Z","timestamp":1573329760000},"page":"107-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Reactive synthesis with maximum realizability of linear temporal logic specifications"],"prefix":"10.1007","volume":"57","author":[{"given":"Rayna","family":"Dimitrova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4302-4806","authenticated-orcid":false,"given":"Mahsa","family":"Ghasemi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,9]]},"reference":[{"issue":"3","key":"348_CR1","doi-asserted-by":"publisher","first-page":"24:1","DOI":"10.1145\/2875421","volume":"63","author":"S Almagor","year":"2016","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formally reasoning about quality. J. ACM 63(3), 24:1\u201324:56 (2016)","journal-title":"J. ACM"},{"key":"348_CR2","unstructured":"Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Proceedings of International Conference on Computer-Aided Verification, vol. 5123 of LNCS (2008)"},{"key":"348_CR3","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT press (2008)"},{"key":"348_CR4","unstructured":"Berg, J., Hyttinen, A., J\u00e4rvisalo, M.: Applications of MaxSAT in data analysis. In: Pragmatics of SAT (2015)"},{"key":"348_CR5","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"348_CR6","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"Roderick Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T. A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Proceedings of International Conference on Computer-Aided Verification, vol. 5643 of LNCS, pp. 140\u2013156 (2009)"},{"key":"348_CR7","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation, LNCS (2008)"},{"key":"348_CR8","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-540-73368-3_53","volume-title":"Computer Aided Verification","author":"Alessandro Cimatti","year":"2007","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean abstraction for temporal logic satisfiability. In: Proceedings of International Conference on Computer-Aided Verification, vol. 4590 of LNCS, pp. 532\u2013546 (2007)"},{"key":"348_CR9","doi-asserted-by":"crossref","unstructured":"Dimitrova, R., Ghasemi, M., Topcu, U.: Maximum realizability for linear temporal logic specifications. In: Proceedings of Automated Technology for Verification and Analysis, pp. 458\u2013475. Springer (2018)","DOI":"10.1007\/978-3-030-01090-4_27"},{"key":"348_CR10","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"Alexandre Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Proceedings of Automated Technology for Verification and Analysis, vol. 9938 of LNCS (2016)"},{"key":"348_CR11","doi-asserted-by":"publisher","first-page":"117","DOI":"10.4204\/EPTCS.157.12","volume":"157","author":"R\u00fcdiger Ehlers","year":"2014","unstructured":"Ehlers, R., Raman, V.: Low-effort specification debugging and analysis. In: Proceedings of Workshop on Synthesis, vol. 157 of EPTCS, pp. 117\u2013133 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"348_CR12","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Peter Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M. N., Tentrup, L.: Encodings of bounded synthesis. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 10205 of LNCS, pp. 354\u2013370 (2017)"},{"issue":"5\u20136","key":"348_CR13","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 519\u2013539 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"348_CR14","first-page":"89","volume":"8","author":"M Janota","year":"2012","unstructured":"Janota, M., Lynce, I., Manquinho, V., Marques-Silva, J.: PackUp: tools for package upgradability solving. J. Satisf. Boolean Model. Comput. 8, 89\u201394 (2012)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"348_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-30353-1_10","volume-title":"Advances in Artificial Intelligence","author":"Farah Juma","year":"2012","unstructured":"Juma, F., Hsu, E. I., McIlraith, S. A.: Preference-based planning via MaxSAT. In: Proceedings of Advances in Artificial Intelligence, vol. 7310 of LNCS, pp. 109\u2013120 (2012)"},{"issue":"12","key":"348_CR16","doi-asserted-by":"publisher","first-page":"1515","DOI":"10.1177\/0278364915587034","volume":"34","author":"Kangjin Kim","year":"2015","unstructured":"Kim, K., Fainekos, G. E., Sankaranarayanan, S.: On the minimal revision problem of specification automata. International Journal of Robotics Research 34(12), 1515-1535 (2015)","journal-title":"The International Journal of Robotics Research"},{"key":"348_CR17","unstructured":"Kupferman, O., Vardi, M. Y.: Safraless decision procedures. In: Proceedings of IEEE Annual Symposium on Foundations of Computer Science, pp. 531\u2013542 (2005)"},{"issue":"3","key":"348_CR18","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"348_CR19","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Almagor, S., Fried, D., Kavraki, L. E., Vardi, M. Y.: This time the robot settles for a cost: a quantitative approach to temporal logic planning with partial satisfaction. In: Proceedings of Association for the Advancement of Artificial Intelligence (2015)","DOI":"10.1609\/aaai.v29i1.9670"},{"key":"348_CR20","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Kwiatkowska, M. Z.: Specification revision for Markov decision processes with optimal trade-off. In: Proceedings of IEEE Conference on Decision and Control, pp. 7411\u20137418, (2016)","DOI":"10.1109\/CDC.2016.7799414"},{"issue":"3","key":"348_CR21","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1109\/TRO.2016.2544339","volume":"32","author":"M Lahijanian","year":"2016","unstructured":"Lahijanian, M., Maly, M.R., Fried, D., Kavraki, L.E., Kress-Gazit, H., Vardi, M.Y.: Iterative temporal planning in uncertain environments with partial satisfaction guarantees. IEEE Trans. Robot. 32(3), 583\u2013599 (2016)","journal-title":"IEEE Trans. Robot."},{"key":"348_CR22","first-page":"438","volume-title":"Lecture Notes in Computer Science","author":"Ruben Martins","year":"2014","unstructured":"Martins, R., Manquinho, V. M., Lynce, I.: Open-WBO: a modular MaxSAT solver. In: Proceedings of SAT\u201914, vol. 8561 of LNCS, pp. 438\u2013445 (2014)"},{"key":"348_CR23","unstructured":"Park, J. D.: Using weighted MAX-SAT engines to solve MPE. In: Proceedings of American Association for Artificial Intelligence, pp. 682\u2013687 (2002)"},{"key":"348_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"348_CR25","doi-asserted-by":"crossref","unstructured":"Raman, V., Kress-Gazit, H.: Towards minimal explanations of unsynthesizability for high-level robot behaviors. In: Proceedings of IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 757\u2013762 (2013)","DOI":"10.1109\/IROS.2013.6696436"},{"key":"348_CR26","doi-asserted-by":"crossref","unstructured":"Robinson, N., Gretton, C., Pham, D. N., Sattar, A.: Partial weighted MaxSAT for optimal planning. In: Proceedings of Pacific rim international conference on artificial intelligence, pp. 231\u2013243. Springer (2010)","DOI":"10.1007\/978-3-642-15246-7_23"},{"key":"348_CR27","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Proceedings of Automated Technology for Verification and Analysis, vol. 4762 of LNCS, pp. 474\u2013488 (2007)","DOI":"10.1007\/978-3-540-75596-8_33"},{"issue":"7\u20138","key":"348_CR28","doi-asserted-by":"publisher","first-page":"908","DOI":"10.1016\/j.scico.2010.11.004","volume":"77","author":"V Schuppan","year":"2012","unstructured":"Schuppan, V.: Towards a notion of unsatisfiable and unrealizable cores for LTL. Sci. Comput. Program. 77(7\u20138), 908\u2013939 (2012)","journal-title":"Sci. Comput. Program."},{"key":"348_CR29","unstructured":"Tabuada, P., Neider, D.: Robust linear temporal logic. In: Proceedings of Computer Science Logic, vol. 62 of LIPIcs, pp. 10:1\u201310:21 (2016)"},{"issue":"7","key":"348_CR30","doi-asserted-by":"publisher","first-page":"655","DOI":"10.1007\/s00236-016-0280-3","volume":"54","author":"T Tomita","year":"2017","unstructured":"Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., Yonezaki, N.: Safraless LTL synthesis considering maximal realizability. Acta Inf. 54(7), 655\u2013692 (2017)","journal-title":"Acta Inf."},{"key":"348_CR31","doi-asserted-by":"crossref","unstructured":"Tumova, J., Hall, G. C., Karaman, S., Frazzoli, E., Rus, D.: Least-violating control strategy synthesis with safety rules. In: Proceedings of ACM International Conference on Hybrid Systems: Computation and Control (2013)","DOI":"10.1145\/2461328.2461330"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00348-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-019-00348-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00348-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,4]],"date-time":"2022-10-04T06:29:35Z","timestamp":1664864975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-019-00348-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,9]]},"references-count":31,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["348"],"URL":"https:\/\/doi.org\/10.1007\/s00236-019-00348-4","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,9]]},"assertion":[{"value":"15 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 October 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 November 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}