{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:15:15Z","timestamp":1762460115549,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131875"},{"type":"electronic","value":"9783031131882"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In many synthesis problems, it can be essential to generate implementations which not only satisfy functional constraints but are also <jats:italic>randomized<\/jats:italic> to improve variety, robustness, or unpredictability. The recently-proposed framework of control improvisation (CI) provides techniques for the correct-by-construction synthesis of randomized systems subject to hard and soft constraints. However, prior work on CI has focused on qualitative specifications, whereas in robotic planning and other areas we often have quantitative quality metrics which can be traded against each other. For example, a designer of a patrolling security robot might want to know by how much the average patrol time needs to be increased in order to ensure that a particular aspect of the robot\u2019s route is sufficiently diverse and hence unpredictable. In this paper, we enable this type of application by generalizing the CI problem to support quantitative soft constraints which bound the expected value of a given cost function, and randomness constraints which enforce diversity of the generated traces with respect to a given label function. We establish the basic theory of labelled quantitative CI problems, and develop efficient algorithms for solving them when the specifications are encoded by finite automata. We also provide an approximate improvisation algorithm based on constraint solving for any specifications encodable as Boolean formulas. We demonstrate the utility of our problem formulation and algorithms with experiments applying them to generate diverse near-optimal plans for robotic planning problems.\n<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_26","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"526-546","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Randomized Synthesis for\u00a0Diversity and\u00a0Cost Constraints with\u00a0Control Improvisation"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Gittis","sequence":"first","affiliation":[]},{"given":"Eric","family":"Vin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9992-9965","authenticated-orcid":false,"given":"Daniel J.","family":"Fremont","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","unstructured":"Akkaya, I., Fremont, D.J., Valle, R., Donz\u00e9, A., Lee, E.A., Seshia, S.A.: Control improvisation with probabilistic temporal specifications. In: First IEEE International Conference on Internet-of-Things Design and Implementation, IoTDI 2016, Berlin, Germany, 4\u20138 April 2016, pp. 187\u2013198. IEEE Computer Society (2016). https:\/\/doi.org\/10.1109\/IoTDI.2015.33, https:\/\/doi.org\/10.1109\/IoTDI.2015.33","DOI":"10.1109\/IoTDI.2015.33 10.1109\/IoTDI.2015.33"},{"key":"26_CR2","doi-asserted-by":"publisher","unstructured":"Almagor, S., Kupferman, O.: High-quality synthesis against stochastic environments. In: Talbot, J.M., Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 62, pp. 28:1\u201328:17. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.28, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2016\/6568","DOI":"10.4230\/LIPIcs.CSL.2016.28"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., Br\u00e1zdil, T., Gr\u00f6\u00dfer, M., Ku\u010dera, A.: Stochastic game logic. Acta informatica pp. 1\u201322 (2012)","DOI":"10.1007\/s00236-012-0156-0"},{"issue":"2","key":"26_CR4","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1006\/inco.2000.2885","volume":"163","author":"M Bellare","year":"2000","unstructured":"Bellare, M., Goldreich, O., Petrank, E.: Uniform generation of NP-witnesses using an NP-oracle. Inf. Comput. 163(2), 510\u2013526 (2000)","journal-title":"Inf. Comput."},{"key":"26_CR5","doi-asserted-by":"publisher","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. In: Proceedings of the 6th International Workshop on Compiler Optimization meets Compiler Verification (COCV 2007). Electronic Notes in Theoretical Computer Science, vol. 190, pp. 3\u201316. Elsevier (2007). https:\/\/doi.org\/10.1016\/j.entcs.2007.09.004, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S157106610700583X","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: On parallel scalable uniform SAT witness generator. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 304\u2013319 (4 2015)","DOI":"10.1007\/978-3-662-46681-0_25"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Balancing scalability and uniformity in sat-witness generator. In: Proceedings of Design Automation Conference (DAC), pp. 60:1\u201360:6, June 2014","DOI":"10.1145\/2593069.2593097"},{"key":"26_CR8","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic sat calls. In: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), July 2016"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-40313-2_25","volume-title":"Mathematical Foundations of Computer Science 2013","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 266\u2013277. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40313-2_25"},{"issue":"1","key":"26_CR10","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1137\/14098524x","volume":"26","author":"S Chubanov","year":"2016","unstructured":"Chubanov, S.: A polynomial-time descent method for separable convex optimization problems with linear constraints. SIAM J. Optim. 26(1), 856\u2013889 (2016). https:\/\/doi.org\/10.1137\/14098524x","journal-title":"SIAM J. Optim."},{"issue":"1","key":"26_CR11","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10009-011-0190-1","volume":"14","author":"A Denise","year":"2011","unstructured":"Denise, A., Gaudel, M.C., Gouraud, S.D., Lassaigne, R., Oudinet, J., Peyronnet, S.: Coverage-biased random exploration of large models and application to testing. Int. J. Softw. Tools Technol. Transfer 14(1), 73\u201393 (2011). https:\/\/doi.org\/10.1007\/s10009-011-0190-1","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"26_CR12","unstructured":"Donze, A., Libkind, S., Seshia, S.A., Wessel, D.: Control improvisation with application to music. Tech. Rep. UCB\/EECS-2013-183, EECS Department, University of California, Berkeley (Nov 2013). http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2013\/EECS-2013-183.html"},{"key":"26_CR13","unstructured":"Donz\u00e9, A., Valle, R., Akkaya, I., Libkind, S., Seshia, S.A., Wessel, D.: Machine improvisation with formal specifications. In: Music Technology meets Philosophy - From Digital Echos to Virtual Ethos: Joint Proceedings of the 40th International Computer Music Conference, ICMC 2014, and the 11th Sound and Music Computing Conference, SMC 2014, Athens, Greece, 14\u201320 September 2014. Michigan Publishing (2014). http:\/\/hdl.handle.net\/2027\/spo.bbp2372.2014.196"},{"key":"26_CR14","series-title":"NATO Science for Peace and Security Series, D: Information and Communication Security","first-page":"72","volume-title":"Dependable Software Systems Engineering","author":"B Finkbeiner","year":"2016","unstructured":"Finkbeiner, B.: Synthesis of reactive systems. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering. NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 45, pp. 72\u201398. IOS Press, Amsterdam (2016)"},{"key":"26_CR15","unstructured":"Fremont, D.J.: Algorithmic improvisation. Thesis (2019). https:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2019\/EECS-2019-133.pdf"},{"key":"26_CR16","doi-asserted-by":"publisher","unstructured":"Fremont, D.J., Donz\u00e9, A., Seshia, S.A., Wessel, D.: Control improvisation. In: Harsha, P., Ramalingam, G. (eds.) 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol. 45, pp. 463\u2013474. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2015). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2015.463, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2015\/5659","DOI":"10.4230\/LIPIcs.FSTTCS.2015.463"},{"key":"26_CR17","unstructured":"Fremont, D.J., Donz\u00e9, A., Seshia, S.A.: Control improvisation (2017). https:\/\/arxiv.org\/abs\/1704.06319"},{"key":"26_CR18","doi-asserted-by":"publisher","unstructured":"Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 63\u201378. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314633, https:\/\/doi.org\/10.1145\/3314221.3314633","DOI":"10.1145\/3314221.3314633 10.1145\/3314221.3314633"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-96145-3_17","volume-title":"Computer Aided Verification","author":"DJ Fremont","year":"2018","unstructured":"Fremont, D.J., Seshia, S.A.: Reactive control improvisation. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 307\u2013326. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_17"},{"key":"26_CR20","doi-asserted-by":"publisher","unstructured":"Gittis, A., Vin, E., Fremont, D.J.: Randomized synthesis for diversity and cost constraints with control improvisation (artifact). https:\/\/doi.org\/10.5281\/zenodo.6558391","DOI":"10.5281\/zenodo.6558391"},{"key":"26_CR21","unstructured":"Gittis, A., Vin, E., Fremont, D.J.: Randomized synthesis for diversity and cost constraints with control improvisation (2022). https:\/\/arxiv.org\/abs\/2206.02775"},{"issue":"5","key":"26_CR22","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"4","key":"26_CR23","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1137\/0212044","volume":"12","author":"T Hickey","year":"1983","unstructured":"Hickey, T., Cohen, J.: Uniform random generation of strings in a context-free language. SIAM J. Comput. 12(4), 645\u2013655 (1983). https:\/\/doi.org\/10.1137\/0212044","journal-title":"SIAM J. Comput."},{"key":"26_CR24","unstructured":"Kozierok, C.M.: The TCP\/IP guide. http:\/\/tcpipguide.com\/free\/t_TCPOperationalOverviewandtheTCPFiniteStateMachineF-2.htm, (Accessed Jan 21 2022)"},{"issue":"6","key":"26_CR25","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Rob. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Rob."},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Soos, M., Gocht, S., Meel, K.S.: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: Proceedings of International Conference on Computer-Aided Verification (CAV), July 2020","DOI":"10.1007\/978-3-030-53288-8_22"},{"key":"26_CR28","unstructured":"Soos, M., Meel, K.S.: Arjun: an efficient independent support computation technique and its applications to counting and sampling. CoRR abs\/2110.09026 (2021). https:\/\/arxiv.org\/abs\/2110.09026"},{"key":"26_CR29","unstructured":"Sutton, M., Greene, A., Amini, P.: Fuzzing: Brute Force Vulnerability Discovery. Addison-Wesley (2007)"},{"key":"26_CR30","doi-asserted-by":"publisher","unstructured":"Vazquez-Chanlatte, M., Junges, S., Fremont, D.J., Seshia, S.: Entropy-guided control improvisation (2021). https:\/\/doi.org\/10.15607\/RSS.2021.XVII.051, https:\/\/doi.org\/10.15607\/RSS.2021.XVII.051","DOI":"10.15607\/RSS.2021.XVII.051 10.15607\/RSS.2021.XVII.051"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T17:05:17Z","timestamp":1659719117000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}