Abstract
We consider the problem of synthesizing controllers automatically for distributed robots that are loosely coupled using a formal synthesis approach. Formal synthesis entails construction of game strategies for a discrete transition system such that the system under the strategy satisfies a specification, given for instance in linear temporal logic (LTL). The general problem of automated synthesis for distributed discrete transition systems suffers from state-space explosion because the combined state-space has size exponential in the number of subsystems. Motivated by multi-robot motion planning problems, we focus on distributed systems whose interaction is nearly decoupled, allowing the overall specification to be decomposed into specifications for individual subsystems and a specification about the joint system. We treat specifically reactive synthesis for the GR(1) fragment of LTL. Each robot is subject to a GR(1) formula, and a safety formula describes constraints on their interaction. We propose an approach wherein we synthesize strategies independently for each subsystem; then we patch the separate controllers around interaction regions such that the specification about the joint system is satisfied.
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
References
Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)
Belta, C., Bicchi, A., Egerstedt, M., Frazzoli, E., Klavins, E., Pappas, G.J.: Symbolic planning and control of robot motion: finding the missing pieces of current methods and ideas. IEEE Robot. Autom. Mag. 61–70 (2007)
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78, 911–938 (2012)
Bullo, F., Cortés, J., MartÃnez, S.: Distributed Control of Robotic Networks. Applied Mathematics Series. Princeton University Press (2009). http://coordinationbook.info
Chen, Y., Ding, X.C., Stefanescu, A., Belta, C.: Formal approach to the deployment of distributed robotic teams. IEEE Trans. Robot. 28(1), 158–171 (2012)
Emerson, E.A.: Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics, chapter Temporal and Modal Logic, pp. 995–1072. MIT Press (1990)
Gerkey, B.P., Matarić, M.J.: A formal analysis and taxonomy of task allocation in multi-robot systems. Int. J. Robot. Res. 23(9), 939–954 (2004)
Karaman, S., Frazzoli, E.: Vehicle routing problem with metric temporal logic specifications. In: Proceedings of the 47th IEEE Conference on Decision and Control (CDC), pp. 3953–3958, Cancun, Mexico, December (2008)
Karaman, S., Frazzoli, E.: Sampling-based algorithms for optimal motion planning with deterministic \(\mu \)-calculus specifications. In: Proceedings of the American Control Conference (ACC), pp. 735–742, Montréal, Canada, June (2012)
Lindemann, S.R., LaValle, S.M.: Simple and efficient algorithms for computing smooth, collision-free feedback laws over given cell decompositions. Int. J. Robot. Res. 28(5), 600–621 (2009)
Livingston, S.C., Murray, R.M.: Hot-swapping robot task goals in reactive formal synthesis. Technical report, California Institute of Technology, September (2014). http://resolver.caltech.edu/CaltechCDSTR:2014.001
Livingston, S.C., Prabhakar, P., Jose, A.B., Murray, R.M.: Patching task-level robot controllers based on a local \(\mu \)-calculus formula. In: Proceedings of the IEEE International Conference on Robotics and Automation (ICRA), pp. 4573–4580, Karlsruhe, Germany, May (2013)
Ozay, N., Topcu, U., Wongpiromsarn, T., Murray, R.M.: Distributed synthesis of control protocols for smart camera networks. In: International Conference on Cyber-physical Systems (2011)
Parker, L.E.: Current state of the art in distributed autonomous mobile robotics. In: Proceedings of Distributed Autonomous Robotic Systems, vol. 4, pp. 3–12. Springer, Japan (2000)
Parker, L.E.: Distributed intelligence: overview of the field and its application in multi-robot systems. J. Phys. Agents 2(1), 5–14 (2008)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’89, pp. 179–190, New York, USA. ACM (1989)
Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of the 31st Annual Symposium on Foundations of Computer Science, October (1990)
Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer (2009)
Zhu, M., Otte, M., Chaudhari, P., Frazzoli, E.: Game theoretic controller synthesis for multi-robot motion planning, Part I: trajectory based algorithms. In: Proceedings of the 2014 IEEE International Conference on Robotics and Automation (ICRA), pp. 1646–1651, Hong Kong, China (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer Japan
About this paper
Cite this paper
Livingston, S.C., Prabhakar, P. (2016). Decoupled Formal Synthesis for Almost Separable Systems with Temporal Logic Specifications. In: Chong, NY., Cho, YJ. (eds) Distributed Autonomous Robotic Systems. Springer Tracts in Advanced Robotics, vol 112 . Springer, Tokyo. https://doi.org/10.1007/978-4-431-55879-8_26
Download citation
DOI: https://doi.org/10.1007/978-4-431-55879-8_26
Published:
Publisher Name: Springer, Tokyo
Print ISBN: 978-4-431-55877-4
Online ISBN: 978-4-431-55879-8
eBook Packages: EngineeringEngineering (R0)