{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T11:32:28Z","timestamp":1780054348081,"version":"3.54.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030010898","type":"print"},{"value":"9783030010904","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-01090-4_27","type":"book-chapter","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T11:23:23Z","timestamp":1538220203000},"page":"458-475","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Maximum Realizability for Linear Temporal Logic Specifications"],"prefix":"10.1007","author":[{"given":"Rayna","family":"Dimitrova","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahsa","family":"Ghasemi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,9,30]]},"reference":[{"issue":"3","key":"27_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":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-70545-1_23","volume-title":"Computer Aided Verification","author":"R Alur","year":"2008","unstructured":"Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 240\u2013253. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_23"},{"key":"27_CR3","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking (2008)"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-78163-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Cimatti","year":"2008","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 52\u201367. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_9"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-540-73368-3_53","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2007","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean abstraction for temporal logic satisfiability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 532\u2013546. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_53"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Dimitrova, R., Ghasemi, M., Topcu, U.: Maximum realizability for linear temporal logic specifications. CoRR, abs\/1804.00415 (2018)","DOI":"10.1007\/978-3-030-01090-4_27"},{"key":"27_CR8","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 - a framework for LTL and $$\\omega $$ -automata manipulation. In: Proceedings of ATVA 2016. LNCS, vol. 9938 (2016)"},{"key":"27_CR9","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 SYNT 2014.EPTCS, vol. 157, pp. 117\u2013133 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"5\u2014-6","key":"27_CR10","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. STTT 15(5\u2014-6), 519\u2013539 (2013)","journal-title":"STTT"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-30353-1_10","volume-title":"Advances in Artificial Intelligence","author":"F Juma","year":"2012","unstructured":"Juma, F., Hsu, E.I., McIlraith, S.A.: Preference-based planning via MaxSAT. In: Kosseim, L., Inkpen, D. (eds.) AI 2012. LNCS (LNAI), vol. 7310, pp. 109\u2013120. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30353-1_10"},{"issue":"12","key":"27_CR12","doi-asserted-by":"publisher","first-page":"1515","DOI":"10.1177\/0278364915587034","volume":"34","author":"K Kim","year":"2015","unstructured":"Kim, K., Fainekos, G.E., Sankaranarayanan, S.: On the minimal revision problem of specification automata. Int. J. Robot. Res. 34(12), 1515\u20131535 (2015)","journal-title":"Int. J. Robot. Res."},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of FOCS 2005, pp. 531\u2013542 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"27_CR14","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 AAAI 2015 (2015)","DOI":"10.1609\/aaai.v29i1.9670"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Kwiatkowska, M.Z.: Specification revision for markov decision processes with optimal trade-off. In: Proceedings of CDC 2016, pp. 7411\u20137418 (2016)","DOI":"10.1109\/CDC.2016.7799414"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-319-09284-3_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"R Martins","year":"2014","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver\u2019. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438\u2013445. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_33"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-75596-8_33","volume-title":"Automated Technology for Verification and Analysis","author":"S Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474\u2013488. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_33"},{"key":"27_CR18","unstructured":"Tabuada, P., Neider, D.: Robust linear temporal logic. In: Proceedings of CSL 2016. LIPIcs, , vol. 62, pp. 10:1\u201310:21 (2016)"},{"issue":"7","key":"27_CR19","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 Inform. 54(7), 655\u2013692 (2017)","journal-title":"Acta Inform."},{"key":"27_CR20","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 HSCC 2013 (2013)","DOI":"10.1145\/2461328.2461330"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-01090-4_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,21]],"date-time":"2025-10-21T14:51:07Z","timestamp":1761058267000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-01090-4_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030010898","9783030010904"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01090-4_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}