{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T10:23:12Z","timestamp":1743157392736,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995232"},{"type":"electronic","value":"9783030995249"}],"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,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"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 multi-agent settings, such as IoT and robotics, it is necessary to coordinate the actions of independent agents in order to achieve a joint behavior. While it is often easy to specify the desired joint behavior, programming the necessary coordination can be difficult. In this work, we develop theory and methods to synthesize coordination strategies that are guaranteed not to initiate unnecessary actions. We refer to such strategies as being \u201ccompact.\u201d We formalize the intuitive notion of compactness; show that existing methods do not guarantee compactness; and propose a solution. The solution transforms a given temporal logic specification, using automata-theoretic constructions, to incorporate a notion of minimality. The central result is that the winning strategies for the transformed specification are precisely the compact strategies for the original. One can therefore apply known synthesis methods to produce compact strategies. We report on prototype implementations that synthesize compact strategies for temporal logic specifications and for specifications of multi-robot coordination.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_3","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"46-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Synthesis of Compact Strategies for Coordination Programs"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nisarg","family":"Patel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formally reasoning about quality. J. ACM 63(3), 24:1\u201324:56 (2016), https:\/\/doi.org\/10.1145\/2875421","DOI":"10.1145\/2875421"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Bansal, S., Chaudhuri, S., Vardi, M.Y.: Comparator automata in quantitative verification. In: FOSSACS. Lecture Notes in Computer Science, vol. 10803, pp. 420\u2013437. Springer (2018)","DOI":"10.1007\/978-3-319-89366-2_23"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Bansal, S., Namjoshi, K.S., Sa\u2019ar, Y.: Synthesis of coordination programs from linear temporal specifications. Proc. ACM Program. Lang. 4(POPL), 54:1\u201354:27 (2020)","DOI":"10.1145\/3371122"},{"key":"3_CR4","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep.\u00a011\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Birget, J.: Partial orders on words, minimal elements of regular languages and state complexity. Theor. Comput. Sci. 119(2), 267\u2013291 (1993)","DOI":"10.1016\/0304-3975(93)90160-U"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol.\u00a05643, pp. 140\u2013156. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Bloem, R., Chockler, H., Ebrahimi, M., Strichman, O.: Synthesizing non-vacuous systems. In: VMCAI. Lecture Notes in Computer Science, vol. 10145, pp. 55\u201372. Springer (2017)","DOI":"10.1007\/978-3-319-52234-0_4"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., K\u00f6nighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY - A new requirements analysis tool with synthesis. In: CAV. Lecture Notes in Computer Science, vol.\u00a06174, pp. 425\u2013429. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_37"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. Journal of Computer and System Sciences 78(3), 911\u2013938 (2012)","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI. LNCS, vol.\u00a08318, pp. 1\u201320. Springer (2014)","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.: Acacia+, a tool for LTL synthesis. In: Proc. of CAV. pp. 652\u2013657 (2012)","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Carroll, M., Namjoshi, K.S., Segall, I.: The Resh programming language for multirobot orchestration. In: 2021 IEEE International Conference on Robotics and Automation, ICRA. IEEE (2021), at https:\/\/arxiv.org\/abs\/2103.13921","DOI":"10.1109\/ICRA48506.2021.9561133"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: QUASY: quantitative synthesis tool. In: TACAS. LNCS, vol.\u00a06605, pp. 267\u2013271. Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_24"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: CAV. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer (1999), https:\/\/nusmv.fbk.eu\/","DOI":"10.1007\/3-540-48683-6_44"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: Proc. of CAV. pp. 365\u2013379 (2010)","DOI":"10.1007\/978-3-642-14295-6_33"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Unbeast: Symbolic bounded synthesis. In: Proc. of TACAS. pp. 272\u2013275 (2011)","DOI":"10.1007\/978-3-642-19835-9_25"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Ehlers, R., Raman, V.: Slugs: Extensible GR(1) synthesis. In: CAV. Lecture Notes in Computer Science, vol.\u00a09780, pp. 333\u2013339. Springer (2016), https:\/\/github.com\/VerifiableRobotics\/slugs","DOI":"10.1007\/978-3-319-41540-6_18"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 995\u20131072. Elsevier and MIT Press (1990). https:\/\/doi.org\/10.1016\/b978-0-444-88074-1.50021-4","DOI":"10.1016\/b978-0-444-88074-1.50021-4"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: An experimentation framework for bounded synthesis. In: Proc. of CAV. pp. 325\u2013332 (2017)","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.: An antichain algorithm for LTL realizability. In: Proc. of CAV. pp. 263\u2013277 (2009)","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.: Compositional algorithms for LTL synthesis. In: Proc. of ATVA. pp. 112\u2013127 (2010)","DOI":"10.1007\/978-3-642-15643-4_10"},{"key":"3_CR22","unstructured":"Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI. pp. 854\u2013860. IJCAI\/AAAI (2013)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Roderick: Optimizations for LTL synthesis. In: Proc. of FMCAD. pp. 117\u2013124 (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. 44(1-2), 167\u2013207 (1990)","DOI":"10.1016\/0004-3702(90)90101-5"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: A library for $$\\omega $$-words, automata, and LTL. In: ATVA. LNCS, vol. 11138, pp. 543\u2013550. Springer (2018), https:\/\/owl.model.in.tum.de\/","DOI":"10.1007\/978-3-030-01090-4_34"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. of FOCS. pp. 531\u2013540. IEEE, IEEE (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Maoz, S., Ringert, J.O.: Spectra: a specification language for reactive systems. Softw. Syst. Model. 20(5), 1553\u20131586 (2021). https:\/\/doi.org\/10.1007\/s10270-021-00868-z","DOI":"10.1007\/s10270-021-00868-z"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"McCarthy, J.: Circumscription - A form of non-monotonic reasoning. Artif. Intell. 13(1-2), 27\u201339 (1980)","DOI":"10.1016\/0004-3702(80)90011-9"},{"key":"3_CR29","unstructured":"McCarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 4, pp. 463\u2013502. Edinburgh University Press (1969)"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV. Lecture Notes in Computer Science, vol. 10981, pp. 578\u2013586. Springer (2018), https:\/\/strix.model.in.tum.de","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive (1) designs. In: International Conference on VMCAI. vol.\u00a03855, pp. 364\u2013380. Springer, Springer (2006)","DOI":"10.1007\/11609773_24"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Prof. of POPL. pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Sa\u2019ar, Y., Zuck, L.D.: JTLV: A framework for developing verification algorithms. In: Proc. of CAV. pp. 171\u2013174 (2010)","DOI":"10.1007\/978-3-642-14295-6_18"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. (141), 1\u201335 (1969)","DOI":"10.1090\/S0002-9947-1969-0246760-1"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: ATVA. Lecture Notes in Computer Science, vol.\u00a04762, pp. 474\u2013488. Springer (2007)","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. Proc. of ATVA pp. 474\u2013488 (2007)","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"3_CR37","unstructured":"Strasser, C., Antonelli, G.A.: Non-monotonic Logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2019 edn. (2019)"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Tabajara, L.M., Vardi, M.Y.: Partitioning techniques in LTL$$f$$ synthesis. In: IJCAI. pp. 5599\u20135606. ijcai.org (2019)","DOI":"10.24963\/ijcai.2019\/777"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133\u2013191. Elsevier and MIT Press (1990), https:\/\/doi.org\/10.1016\/b978-0-444-88074-1.50009-3","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Zhu, S., Giacomo, G.D., Pu, G., Vardi, M.Y.: LTL$$f$$ synthesis with fairness and stability assumptions. In: AAAI. pp. 3088\u20133095. AAAI Press (2020)","DOI":"10.1609\/aaai.v34i03.5704"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,21]],"date-time":"2024-09-21T05:09:08Z","timestamp":1726895348000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_3","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":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"159","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":"46","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":"4","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":"29% - 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","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":"10","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)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}