Abstract
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 “compact.” 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.
Chapter PDF
Similar content being viewed by others
References
Almagor, S., Boker, U., Kupferman, O.: Formally reasoning about quality. J. ACM 63(3), 24:1–24:56 (2016), https://doi.org/10.1145/2875421
Bansal, S., Chaudhuri, S., Vardi, M.Y.: Comparator automata in quantitative verification. In: FOSSACS. Lecture Notes in Computer Science, vol. 10803, pp. 420–437. Springer (2018)
Bansal, S., Namjoshi, K.S., Sa’ar, Y.: Synthesis of coordination programs from linear temporal specifications. Proc. ACM Program. Lang. 4(POPL), 54:1–54:27 (2020)
Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep. 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)
Birget, J.: Partial orders on words, minimal elements of regular languages and state complexity. Theor. Comput. Sci. 119(2), 267–291 (1993)
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. 5643, pp. 140–156. Springer (2009)
Bloem, R., Chockler, H., Ebrahimi, M., Strichman, O.: Synthesizing non-vacuous systems. In: VMCAI. Lecture Notes in Computer Science, vol. 10145, pp. 55–72. Springer (2017)
Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Könighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY - A new requirements analysis tool with synthesis. In: CAV. Lecture Notes in Computer Science, vol. 6174, pp. 425–429. Springer (2010)
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. Journal of Computer and System Sciences 78(3), 911–938 (2012)
Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI. LNCS, vol. 8318, pp. 1–20. Springer (2014)
Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.: Acacia+, a tool for LTL synthesis. In: Proc. of CAV. pp. 652–657 (2012)
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
Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: QUASY: quantitative synthesis tool. In: TACAS. LNCS, vol. 6605, pp. 267–271. Springer (2011)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: CAV. LNCS, vol. 1633, pp. 495–499. Springer (1999), https://nusmv.fbk.eu/
Ehlers, R.: Symbolic bounded synthesis. In: Proc. of CAV. pp. 365–379 (2010)
Ehlers, R.: Unbeast: Symbolic bounded synthesis. In: Proc. of TACAS. pp. 272–275 (2011)
Ehlers, R., Raman, V.: Slugs: Extensible GR(1) synthesis. In: CAV. Lecture Notes in Computer Science, vol. 9780, pp. 333–339. Springer (2016), https://github.com/VerifiableRobotics/slugs
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–1072. Elsevier and MIT Press (1990). https://doi.org/10.1016/b978-0-444-88074-1.50021-4
Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: An experimentation framework for bounded synthesis. In: Proc. of CAV. pp. 325–332 (2017)
Filiot, E., Jin, N., Raskin, J.: An antichain algorithm for LTL realizability. In: Proc. of CAV. pp. 263–277 (2009)
Filiot, E., Jin, N., Raskin, J.: Compositional algorithms for LTL synthesis. In: Proc. of ATVA. pp. 112–127 (2010)
Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI. pp. 854–860. IJCAI/AAAI (2013)
Jobstmann, B., Roderick: Optimizations for LTL synthesis. In: Proc. of FMCAD. pp. 117–124 (2006)
Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. 44(1-2), 167–207 (1990)
Kretínský, J., Meggendorfer, T., Sickert, S.: Owl: A library for \(\omega \)-words, automata, and LTL. In: ATVA. LNCS, vol. 11138, pp. 543–550. Springer (2018), https://owl.model.in.tum.de/
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. of FOCS. pp. 531–540. IEEE, IEEE (2005)
Maoz, S., Ringert, J.O.: Spectra: a specification language for reactive systems. Softw. Syst. Model. 20(5), 1553–1586 (2021). https://doi.org/10.1007/s10270-021-00868-z
McCarthy, J.: Circumscription - A form of non-monotonic reasoning. Artif. Intell. 13(1-2), 27–39 (1980)
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–502. Edinburgh University Press (1969)
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–586. Springer (2018), https://strix.model.in.tum.de
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive (1) designs. In: International Conference on VMCAI. vol. 3855, pp. 364–380. Springer, Springer (2006)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Prof. of POPL. pp. 179–190 (1989)
Pnueli, A., Sa’ar, Y., Zuck, L.D.: JTLV: A framework for developing verification algorithms. In: Proc. of CAV. pp. 171–174 (2010)
Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. (141), 1–35 (1969)
Schewe, S., Finkbeiner, B.: Bounded synthesis. In: ATVA. Lecture Notes in Computer Science, vol. 4762, pp. 474–488. Springer (2007)
Schewe, S., Finkbeiner, B.: Bounded synthesis. Proc. of ATVA pp. 474–488 (2007)
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)
Tabajara, L.M., Vardi, M.Y.: Partitioning techniques in LTL\(f\) synthesis. In: IJCAI. pp. 5599–5606. ijcai.org (2019)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133–191. Elsevier and MIT Press (1990), https://doi.org/10.1016/b978-0-444-88074-1.50009-3
Zhu, S., Giacomo, G.D., Pu, G., Vardi, M.Y.: LTL\(f\) synthesis with fairness and stability assumptions. In: AAAI. pp. 3088–3095. AAAI Press (2020)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Namjoshi, K.S., Patel, N. (2022). Synthesis of Compact Strategies for Coordination Programs. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13243. Springer, Cham. https://doi.org/10.1007/978-3-030-99524-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-99524-9_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99523-2
Online ISBN: 978-3-030-99524-9
eBook Packages: Computer ScienceComputer Science (R0)