{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:35:22Z","timestamp":1765546522605,"version":"3.41.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>\n            This paper presents a method for synthesizing a reactive program to coordinate the actions of a group of other reactive programs so that the combined system satisfies a temporal specification of its desired long-term behavior. Traditionally, reactive synthesis has been applied to the construction of a stateful hardware circuit. This work is motivated by applications to other domains, such as the IoT (the Internet of Things) and robotics, where it is necessary to coordinate the actions of multiple sensors, devices, and robots to carry out a task. The mathematical model represents each agent as a process in Hoare\u2019s CSP model. Given a network of interacting agents, called an\n            <jats:italic>environment<\/jats:italic>\n            , and a temporal specification of long-term behavior, the synthesis method constructs a\n            <jats:italic>coordinator<\/jats:italic>\n            process (if one exists) that guides the actions of the environment agents so that the combined system is deadlock-free and satisfies the given specification. The main technical challenge is that a coordinator may have only\n            <jats:italic>partial information<\/jats:italic>\n            of the environment state, due to non-determinism within the environment and internal environment actions that are hidden from the coordinator. This is the first method to handle both sources of partial information and to do so for arbitrary linear temporal logic specifications. It is established that the coordination synthesis problem is\n            <jats:italic>PSPACE<\/jats:italic>\n            -hard in the size of the environment. A prototype implementation is able to synthesize compact solutions for a number of coordination problems.\n          <\/jats:p>","DOI":"10.1145\/3371122","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Synthesis of coordination programs from linear temporal specifications"],"prefix":"10.1145","volume":"4","author":[{"given":"Suguman","family":"Bansal","sequence":"first","affiliation":[{"name":"Rice University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[{"name":"Nokia Bell Labs, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yaniv","family":"Sa'ar","sequence":"additional","affiliation":[{"name":"Nokia Bell Labs, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"volume-title":"Proc","author":"Alur Rajeev","key":"e_1_2_2_1_1","unstructured":"Rajeev Alur , Salar Moarref , and Ufuk Topcu . 2016. Compositional synthesis of reactive controllers for multi-agent systems . In Proc . of CAV. Springer , 251\u2013269. Rajeev Alur, Salar Moarref, and Ufuk Topcu. 2016. Compositional synthesis of reactive controllers for multi-agent systems. In Proc. of CAV. Springer, 251\u2013269."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_20"},{"key":"e_1_2_2_4_1","volume-title":"Synthesis of Coordination Programs from Linear Temporal Specifications. arXiv","author":"Bansal Suguman","year":"1911","unstructured":"Suguman Bansal , Kedar S. Namjoshi , and Yaniv Sa\u2019ar . 2019. Synthesis of Coordination Programs from Linear Temporal Specifications. arXiv : 1911 .03807 Suguman Bansal, Kedar S. Namjoshi, and Yaniv Sa\u2019ar. 2019. Synthesis of Coordination Programs from Linear Temporal Specifications. arXiv: 1911.03807"},{"key":"e_1_2_2_5_1","volume-title":"Proc. of CONCUR. 76\u201390","author":"Benes Nikola","year":"2013","unstructured":"Nikola Benes , Beno\u00eet Delahaye , Uli Fahrenberg , Jan Kret\u00ednsk\u00fd , and Axel Legay . 2013 . Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory . In Proc. of CONCUR. 76\u201390 . Nikola Benes, Beno\u00eet Delahaye, Uli Fahrenberg, Jan Kret\u00ednsk\u00fd, and Axel Legay. 2013. Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. In Proc. of CONCUR. 76\u201390."},{"key":"e_1_2_2_6_1","volume-title":"Maurizio Lenzerini, and Massimo Mecella.","author":"Berardi Daniela","year":"2003","unstructured":"Daniela Berardi , Diego Calvanese , Giuseppe De Giacomo , Maurizio Lenzerini, and Massimo Mecella. 2003 . Automatic Composition of E-services That Export Their Behavior. In In proceedings of ICSOC. 43\u201358. Daniela Berardi, Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Massimo Mecella. 2003. Automatic Composition of E-services That Export Their Behavior. In In proceedings of ICSOC. 43\u201358."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_2_10_1","first-page":"367","article-title":"Solving sequential conditions by finite-state strategies","volume":"138","author":"Richard B\u00fcchi J.","year":"1969","unstructured":"J. Richard B\u00fcchi and L.H. Landweber . 1969 . Solving sequential conditions by finite-state strategies . Trans. Amer. Math. Soc. 138 (1969), 367 \u2013 378 . J. Richard B\u00fcchi and L.H. Landweber. 1969. Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138 (1969), 367\u2013378.","journal-title":"Trans. Amer. Math. Soc."},{"volume-title":"Summaries of the Summer Institute of Symbolic Logic.","author":"Church Alonzo","key":"e_1_2_2_11_1","unstructured":"Alonzo Church . 1957. Applications of recursive arithmetic to the problem of circuit synthesis . In Summaries of the Summer Institute of Symbolic Logic. Vol. I . Cornell Univ. , Ithaca, N.Y. , 3\u201350. Alonzo Church. 1957. Applications of recursive arithmetic to the problem of circuit synthesis. In Summaries of the Summer Institute of Symbolic Logic. Vol. I. Cornell Univ., Ithaca, N.Y., 3\u201350."},{"key":"e_1_2_2_12_1","volume-title":"Proc. Int. Congr. Math.","author":"Church Alonzo","year":"1963","unstructured":"Alonzo Church . 1963 . Logic, arithmetic, and automata . In Proc. Int. Congr. Math. 1962. Inst. Mittag-Leffler, Djursholm, Sweden, 23\u201335. Alonzo Church. 1963. Logic, arithmetic, and automata. In Proc. Int. Congr. Math. 1962. Inst. Mittag-Leffler, Djursholm, Sweden, 23\u201335."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2564959"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430536.2430543"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_33"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_25"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_20"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15643-4_10"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0228-z"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Nissim Francez. 1986. Fairness. Springer.  Nissim Francez. 1986. Fairness. Springer.","DOI":"10.1007\/978-1-4612-4886-6"},{"volume-title":"Proc. of TACAS. 187\u2013201","author":"Gibson-Robinson Thomas","key":"e_1_2_2_25_1","unstructured":"Thomas Gibson-Robinson , Philip J. Armstrong , Alexandre Boulgakov , and A. W. Roscoe . 2014. FDR3 \u2014 A Modern Refinement Checker for CSP . In Proc. of TACAS. 187\u2013201 . Thomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, and A. W. Roscoe. 2014. FDR3 \u2014 A Modern Refinement Checker for CSP. In Proc. of TACAS. 187\u2013201."},{"key":"e_1_2_2_26_1","volume-title":"Symposium on Principles of Programming Languages (POPL)","volume":"46","author":"William","unstructured":"William R. Harris and Sumit Gulwani. 2011. Spreadsheet table transformations from examples . In Symposium on Principles of Programming Languages (POPL) , Vol. 46 . 317\u2013328. William R. Harris and Sumit Gulwani. 2011. Spreadsheet table transformations from examples. In Symposium on Principles of Programming Languages (POPL), Vol. 46. 317\u2013328."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","key":"e_1_2_2_28_1","unstructured":"C. A. R. Hoare . 1985. Communicating Sequential Processes . Prentice-Hall . C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.22"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_19"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509402"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2005.66"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113738"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5119"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2013.2246095"},{"volume-title":"Proc. of FOSSACS. 395\u2013409","author":"Lustig Yoad","key":"e_1_2_2_36_1","unstructured":"Yoad Lustig and Moshe Y. Vardi . 2009. Synthesis from Component Libraries . In Proc. of FOSSACS. 395\u2013409 . Yoad Lustig and Moshe Y. Vardi. 2009. Synthesis from Component Libraries. In Proc. of FOSSACS. 395\u2013409."},{"key":"e_1_2_2_38_1","unstructured":"Zohar Manna and Amir Pnueli. 1987. Specification and Verification of Concurrent Programs By Forall-Automata. In Prof. of POPL. 1\u201312.  Zohar Manna and Amir Pnueli. 1987. Specification and Verification of Concurrent Programs By Forall-Automata. In Prof. of POPL. 1\u201312."},{"key":"e_1_2_2_39_1","volume-title":"Workshop. 253\u2013281","author":"Manna Zohar","year":"1981","unstructured":"Zohar Manna and Pierre Wolper . 1981 . Synthesis of Communicating Processes from Temporal Logic Specifications. In Logics of Programs , Workshop. 253\u2013281 . Zohar Manna and Pierre Wolper. 1981. Synthesis of Communicating Processes from Temporal Logic Specifications. In Logics of Programs, Workshop. 253\u2013281."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1960275.1960280"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33666-9_22"},{"key":"e_1_2_2_42_1","doi-asserted-by":"crossref","unstructured":"S. Moarref and H. Kress-Gazit. 2018. Reactive Synthesis for Robotic Swarms. Formal Modeling and Analysis of Timed Systems 71\u201387.  S. Moarref and H. Kress-Gazit. 2018. Reactive Synthesis for Robotic Swarms. Formal Modeling and Analysis of Timed Systems 71\u201387.","DOI":"10.1007\/978-3-030-00151-3_5"},{"key":"e_1_2_2_43_1","volume-title":"International Conference on VMCAI","volume":"3855","author":"Piterman Nir","year":"2006","unstructured":"Nir Piterman , Amir Pnueli , and Yaniv Sa\u2019ar . 2006 . Synthesis of reactive (1) designs . In International Conference on VMCAI , Vol. 3855 . Springer, Springer, 364\u2013380. Nir Piterman, Amir Pnueli, and Yaniv Sa\u2019ar. 2006. Synthesis of reactive (1) designs. In International Conference on VMCAI, Vol. 3855. Springer, Springer, 364\u2013380."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_45_1","unstructured":"Amir Pnueli and Roni Rosner. 1989a. On the Synthesis of a Reactive Module. In Prof. of POPL. 179\u2013190.  Amir Pnueli and Roni Rosner. 1989a. On the Synthesis of a Reactive Module. In Prof. of POPL. 179\u2013190."},{"key":"e_1_2_2_46_1","volume-title":"On the synthesis of an asynchronous reactive module. Automata, Languages and Programming","author":"Pnueli Amir","year":"1989","unstructured":"Amir Pnueli and Roni Rosner . 1989b. On the synthesis of an asynchronous reactive module. Automata, Languages and Programming ( 1989 ), 652\u2013671. Amir Pnueli and Roni Rosner. 1989b. On the synthesis of an asynchronous reactive module. Automata, Languages and Programming (1989), 652\u2013671."},{"key":"e_1_2_2_47_1","volume-title":"Zuck","author":"Pnueli Amir","year":"2010","unstructured":"Amir Pnueli , Yaniv Sa\u2019ar , and Lenore D . Zuck . 2010 . JTLV : A Framework for Developing Verification Algorithms. In Proc. of CAV. 171\u2013174. Amir Pnueli, Yaniv Sa\u2019ar, and Lenore D. Zuck. 2010. JTLV: A Framework for Developing Verification Algorithms. In Proc. of CAV. 171\u2013174."},{"key":"e_1_2_2_48_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin M.O.","year":"1969","unstructured":"M.O. Rabin . 1969 . Decidability of second-order theories and automata on infinite trees . Trans. Amer. Math. Soc. 141 (1969), 1 \u2013 35 . M.O. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141 (1969), 1\u201335.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","unstructured":"P.J.G. Ramadge and W.M. Wonham. 1989. The control of discrete event systems. IEEE Transactions on Control Theory 98 (1989).  P.J.G. Ramadge and W.M. Wonham. 1989. The control of discrete event systems. IEEE Transactions on Control Theory 98 (1989).","DOI":"10.1109\/5.21072"},{"key":"e_1_2_2_50_1","volume-title":"Henzinger","author":"Raskin Jean-Fran\u00e7ois","year":"2007","unstructured":"Jean-Fran\u00e7ois Raskin , Krishnendu Chatterjee , Laurent Doyen , and Thomas A . Henzinger . 2007 . Algorithms for OmegaRegular Games with Imperfect Information. Logical Methods in Computer Science 3, 3 (2007). Jean-Fran\u00e7ois Raskin, Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. 2007. Algorithms for OmegaRegular Games with Imperfect Information. Logical Methods in Computer Science 3, 3 (2007)."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90034-5"},{"volume-title":"The Theory and Practice of Concurrency","author":"Roscoe A. W.","key":"e_1_2_2_52_1","unstructured":"A. W. Roscoe . 1997. The Theory and Practice of Concurrency . Prentice Hall PTR , Upper Saddle River, NJ, USA. A. W. Roscoe. 1997. The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River, NJ, USA."},{"key":"e_1_2_2_53_1","volume-title":"Proc. of LOPSTR. 127\u2013142","author":"Schewe Sven","year":"2006","unstructured":"Sven Schewe and Bernd Finkbeiner . 2006 . Synthesis of Asynchronous Systems . In Proc. of LOPSTR. 127\u2013142 . Sven Schewe and Bernd Finkbeiner. 2006. Synthesis of Asynchronous Systems. In Proc. of LOPSTR. 127\u2013142."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"e_1_2_2_55_1","first-page":"404","article-title":"Combinatorial sketching for finite programs","volume":"34","author":"Solar-Lezama Armando","year":"2006","unstructured":"Armando Solar-Lezama , Liviu Tancau , Rastislav Bodik , Sanjit Seshia , and Vijay Saraswat . 2006 . Combinatorial sketching for finite programs . Proc. of (ASPLOS) 34 , 5 (2006), 404 \u2013 415 . Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial sketching for finite programs. Proc. of (ASPLOS) 34, 5 (2006), 404\u2013415.","journal-title":"Proc. of (ASPLOS)"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_1"},{"key":"e_1_2_2_58_1","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. 1982. Specification and Synthesis of Communicating Processes using an Extended Temporal Logic. In Prof. of POPL. 20\u201333.  Pierre Wolper. 1982. Specification and Synthesis of Communicating Processes using an Extended Temporal Logic. In Prof. of POPL. 20\u201333.","DOI":"10.1145\/582153.582156"},{"volume-title":"Proc. of CAV. 272\u2013281","author":"Wong-Toi Howard","key":"e_1_2_2_59_1","unstructured":"Howard Wong-Toi and David L. Dill . 1990. Synthesizing Processes and Schedulers from Temporal Specifications . In Proc. of CAV. 272\u2013281 . Howard Wong-Toi and David L. Dill. 1990. Synthesizing Processes and Schedulers from Temporal Specifications. In Proc. of CAV. 272\u2013281."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371122","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371122","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371122"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":58,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371122"],"URL":"https:\/\/doi.org\/10.1145\/3371122","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}