Abstract
We consider the problem of reactive synthesis for systems with non-instantaneous actions, i.e., it may take an arbitrary amount of time for the actions of the system to complete, and meanwhile the input from the environment may also change, possibly requiring a different response from the system. The problem can be modeled as a typical reactive synthesis problem by introducing auxiliary propositions and fairness assumptions, at the expense of additional computational complexity. We develop new realizability and synthesis algorithms that address the problem without adding auxiliary propositions or assumptions. We discuss the complexity of both approaches. We then apply our algorithms to synthesize controllers for a swarm robotic system. We implement both approaches and compare them using a specific swarm task.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
If \(\mathcal {H}^\mathbf {a}(\mathbf {o})\) is undefined for any \(\mathbf {o} \in \varSigma _\mathcal {O}\), let \(\mathcal {H}^\mathbf {a}(\mathbf {o})=\mathtt{{False}}\) in the definition of \(\tau ^\mathcal {A}\).
References
Raman, V., Piterman, N., Finucane, C., Kress-Gazit, H.: Timing semantics for abstraction and execution of synthesized high-level robot control. IEEE Trans. Robot. 31(3), 591–604 (2015)
Brambilla, M., Ferrante, E., Birattari, M., Dorigo, M.: Swarm robotics: a review from the swarm engineering perspective. Swarm Intell. 7(1), 1–41 (2013)
Nouyan, S., Campo, A., Dorigo, M.: Path formation in a robot swarm. Swarm Intell. 2(1), 1–23 (2008)
Soysal, O., Sahin, E.: Probabilistic aggregation strategies in swarm robotic systems. In: Proceedings 2005 IEEE Swarm Intelligence Symposium, SIS 2005, pp. 325–332. IEEE (2005)
Labella, T.H., Dorigo, M., Deneubourg, J.L.: Division of labor in a group of robots inspired by ants’ foraging behavior. ACM Trans. Auton. Adapt. Syst. (TAAS) 1(1), 4–25 (2006)
Bachrach, J., Beal, J., McLurkin, J.: Composable continuous-space programs for robotic swarms. Neural Comput. Appl. 19(6), 825–847 (2010)
Balch, T., Hybinette, M.: Social potentials for scalable multi-robot formations. In: IEEE International Conference on Robotics and Automation 2000. Proceedings of ICRA 2000, vol. 1, pp. 73–80. IEEE (2000)
Moarref, S., Kress-Gazit, H.: Decentralized control of robotic swarms from high-level temporal logic specifications. In: International Symposium on Multi-Robot and Multi-Agent Systems. IEEE (2017, to appear)
Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robot. 25(6), 1370–1381 (2009)
Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning. IEEE Trans. Autom. Control 57(11), 2817–2830 (2012)
Kress-gazit, H., Wongpiromsarn, T., Topcu, U.: Correct, reactive robot control from abstraction and temporal logic specifications. IEEE Robot. Autom. Mag. 18, 65–74 (2011)
Wongpiromsarn, T., Ulusoy, A., Belta, C., Frazzoli, E., Rus, D.: Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications. In: IEEE International Conference on Robotics and Automation, pp. 5011–5018. IEEE (2013)
Kloetzer, M., Belta, C.: Automatic deployment of distributed teams of robots from temporal logic motion specifications. IEEE Trans. Robot. 26(1), 48–61 (2010)
Nilsson, P., Ozay, N.: Control synthesis for large collections of systems with mode-counting constraints. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pp. 205–214. ACM (2016)
Kloetzer, M., Belta, C.: Hierarchical abstractions for robotic swarms. In: Proceedings 2006 IEEE International Conference on Robotics and Automation 2006. ICRA 2006, pp. 952–957. IEEE (2006)
Kloetzer, M., Ding, X.C., Belta, C.: Multi-robot deployment from LTL specifications with reduced communication. In: 2011 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC), pp. 4867–4872. IEEE (2011)
Kress-Gazit, H., Lahijanian, M., Raman, V.: Synthesis for robots: guarantees and feedback for robot behavior. Ann. Rev. Control Robot. Auton. Syst. 1, 211–236 (2018)
Church, A.: Logic, arithmetic and automata. In: Proceedings of the International Congress of Mathematicians, pp. 23–35 (1962)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages, pp. 179–190. ACM (1989)
Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992)
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive (1) designs. J. Comput. Syst. Sci. 78(3), 911–938 (2012)
Davoren, J.M., Coulthard, V., Markey, N., Moor, T.: Non-deterministic temporal logics for general flow systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 280–295. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24743-2_19
Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)
Dixon, C., Winfield, A.F., Fisher, M., Zeng, C.: Towards temporal verification of swarm robotic systems. Robot. Auton. Syst. 60(11), 1429–1441 (2012)
Gjondrekaj, E., et al.: Towards a formal verification methodology for collective robotic systems. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 54–70. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34281-3_7
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)
Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. Form. Methods Syst. Des. 28(1), 37–56 (2006)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive (1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_24
Raman, V., Kress-Gazit, H.: Synthesis for multi-robot controllers with interleaved motion. In: 2014 IEEE International Conference on Robotics and Automation (ICRA), pp. 4316–4321. IEEE (2014)
Vahidi, A.: JDD (2018). http://javaddlib.sourceforge.net/jdd/index.html. Accessed 16 June 2018
Ehlers, R., Raman, V.: Slugs: extensible GR(1) synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 333–339. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_18
Alur, R., Moarref, S., Topcu, U.: Compositional synthesis of reactive controllers for multi-agent systems. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 251–269. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_14
Filiot, E., Jin, N., Raskin, J.F.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261–296 (2011)
Acknowledgements
This research was supported by DARPA N66001-17-2-4058.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Moarref, S., Kress-Gazit, H. (2018). Reactive Synthesis for Robotic Swarms. In: Jansen, D., Prabhakar, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2018. Lecture Notes in Computer Science(), vol 11022. Springer, Cham. https://doi.org/10.1007/978-3-030-00151-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-00151-3_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00150-6
Online ISBN: 978-3-030-00151-3
eBook Packages: Computer ScienceComputer Science (R0)