PuRSUE – from specification of robotic environments to synthesis of controllers. (English) Zbl 1458.68218

Summary: Developing robotic applications is a complex task, which requires skills that are usually only possessed by highly-qualified robotic developers. While formal methods that help developers in the creation and design of robotic applications exist, they must be explicitly customized to be impactful in the robotics domain and to support effectively the growth of the robotic market. Specifically, the robotic market is asking for techniques that: (i) enable a systematic and rigorous design of robotic applications though high-level languages; and (ii) enable the automatic synthesis of low-level controllers, which allow robots to achieve their missions. To address these problems we present the PuRSUE (Planner for RobotS in Uncontrollable Environments) approach, which aims to support developers in the rigorous and systematic design of high-level run-time control strategies for robotic applications. The approach includes PuRSUE-ML a high-level language that allows for modeling the environment, the agents deployed therein, and their missions. PuRSUE is able to check automatically whether a controller that allows robots to achieve their missions might exist and, then, it synthesizes a controller. We evaluated how PuRSUE helps designers in modeling robotic applications, the effectiveness of its automatic computation of controllers, and how the approach supports the deployment of controllers on actual robots. The evaluation is based on 13 scenarios derived from 3 different robotic applications presented in the literature. The results show that: (i) PuRSUE-ML is effective in supporting designers in the formal modeling of robotic applications compared to a direct encoding of robotic applications in low-level modeling formalisms; (ii) PuRSUE enables the automatic generation of controllers that are difficult to create manually; and (iii) the plans generated with PuRSUE are indeed effective when deployed on actual robots.


68T40 Artificial intelligence for robotics
93B50 Synthesis problems
93C85 Automated systems (robots, etc.) in control theory
Full Text: DOI


[1] Alur, R.; Dill, DL, Model-checking in dense real-time, Inf Comput, 104, 1, 2-34 (1993) · Zbl 0783.68076
[2] Alur, R.; Dill, DL, A theory of timed automata, Theor Comput Sci, 126, 2, 183-235 (1994) · Zbl 0803.68071
[3] Asarin E, Maler O, Pnueli A (1995) Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems II. Springer · Zbl 0884.68050
[4] Askarpour M, Mandrioli D, Rossi M, Vicentini F (2017) Modeling operator behavior in the safety analysis of collaborative robotic applications. In: Computer safety, reliability, and security. Springer, pp 89-104
[5] Askarpour, M.; Mandrioli, D.; Rossi, M.; Vicentini, F., Formal model of human erroneous behavior for safety analysis in collaborative robotics, Robot Comput Integr Manuf, 57, 465-476 (2019)
[6] Behrmann G, Cougnard A, David A, Fleury E, Larsen KG, Lime D (2007) Uppaal-tiga: time for playing games!. In: Computer aided verification. Springer, pp 121-125
[7] Barbosa, FS; Duberg, D.; Jensfelt, P.; Tůmová, J., Guiding autonomous exploration with signal temporal logic, IEEE Robot Autom Lett, 4, 4, 3332-3339 (2019)
[8] Behrmann G, David A, Larsen KG (2004) A tutorial on uppaal. In: Formal methods for the design of real-time systems. Springer, pp 200-236 · Zbl 1105.68350
[9] Bouyer P (2009) Model-checking timed temporal logics. In: Electronic notes in theoretical computer science. pp 231:323-341. Workshop on Methods for Modalities (M4M5 2007) · Zbl 1347.68218
[10] Barrett, A.; Rabideau, G.; Estlin, T.; Chien, S., Coordinated continual planning methods for cooperating rovers, IEEE Aerosp Electron Syst Mag, 22, 2, 27-33 (2007)
[11] Bozhinoski D, Ruscio DD, Malavolta I, Pelliccione P, Tivoli M (2015) FLYAQ: enabling non-expert users to specify and generate missions of autonomous multicopters. In: International conference on automated software engineering. IEEE, pp 801-806
[12] Bersani, MM; Rossi, M.; Pietro, PS, A tool for deciding the satisfiability of continuous-time metric temporal logic, Acta Inf, 53, 2, 171-206 (2016) · Zbl 1336.68230
[13] Berry, G.; Sethi, R., From regular expressions to deterministic automata, Theor Comput Sci, 48, 117-126 (1986) · Zbl 0626.68043
[14] Ceballos A, Bensalem S, Cesta A, de Silva L, Fratini S, Ingrand F, Ocón J, Orlandini A, Py F, Rajan K, Rasconi R, van Winnendael M (2011) A goal oriented autonomous controller for space exploration. http://robotics.estec.esa.int/ASTRA/Astra2011/Astra2011_Proceedings.zip1
[15] Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M., NuSMV: a new symbolic model checker, Int J Softw Tools Technol Transf, 2, 4, 410-425 (2000) · Zbl 1059.68582
[16] Cassez F, David A, Fleury E, Larsen KG, Lime D (2005) Efficient on-the-fly algorithms for the analysis of timed games. In: Concurrency theory. Springer, pp 66-80 · Zbl 1134.68382
[17] Campusano, M.; Fabry, J., Live robot programming: The language, its implementation, and robot API independence, Sci Comput Program, 133, 1-19 (2017)
[18] Chen T, Forejt V, Kwiatkowska M, Parker D, Simaitis A (2013) Prism-games: a model checker for stochastic multi-player games. In: International conference on TOOLS and algorithms for the construction and analysis of systems. Springer, pp 185-191 · Zbl 1381.68151
[19] Cimatti A, Hunsberger L, Micheli A, Roveri M (2014) Using timed game automata to synthesize execution strategies for simple temporal networks with uncertainty. In: AAAI. AAAI Press, pp 2242-2249
[20] Cassez F, Larsen KG, Raskin JF, Reynier PA (2011) Timed controller synthesis: an industrial case study. Deliverable no.: D5. 12 Title of Deliverable: Industrial Handbook, p 150
[21] Cesta A, Orlandini A, Umbrico A (2013) Toward a general purpose software environment for timeline-based planning. https://core.ac.uk/download/pdf/37835325.pdf
[22] Ciccozzi, F.; Di, RD; Malavolta, I.; Pelliccione, P., Adopting MDE for specifying and executing civilian missions of mobile multi-robot systems, IEEE Access, 4, 6451-6466 (2016)
[23] Damas, B.; Lima, P., Stochastic discrete event model of a multi-robot team playing an adversarial game, IFAC Proc, 37, 8, 974-979 (2004)
[24] Farinelli, A.; Iocchi, L.; Nardi, D., Multirobot systems: a classification focused on coordination, Trans Syst Man Cybern Part B (Cybern), 34, 5, 2015-2028 (2004)
[25] Finucane C, Jing G, Kress-Gazit H (2010) LTLMoP: Experimenting with language, temporal logic and robot control. In: Intelligent Robots and Systems. IEEE, pp 1988-1993
[26] Farrell M, Luckcuck M, Fisher M (2018) Robotics and integrated formal methods: necessity meets opportunity. In: Integrated formal methods. Springer, pp 161-171
[27] Foote T, Wise M (2019) Turtlebot home page, Last access 27 March https://www.turtlebot.com/
[28] Gainer P, Dixon C, Dautenhahn K, Fisher M, Hustadt U, Saunders J, Webster M (2017) Cruton: automatic verification of a robotic assistant’s behaviours. In: Critical systems: formal methods and automated verification. Springer, pp 119-133
[29] Götz S, Leuthäuser M, Reimann J, Schroeter J, Wende C, Wilke C, Aßmann U (2011) A role-based language for collaborative robot applications. In: International symposium on leveraging applications of formal methods, verification and validation. Springer, pp 1-15
[30] Gigante N, Montanari A, Mayer MC, Orlandini A, Reynolds M (2018) A game-theoretic approach to timeline-based planning with uncertainty. arXiv preprint arXiv:1807.04837
[31] García S, Pelliccione P, Menghi C, Berger T, Bures T (2019) High-level mission specification for multiple robots. In: International conference on software language engineering. ACM, pp 127-140
[32] Jessen JJ, Rasmussen JI, Larsen KG, David A (2007) Guided controller synthesis for climate controller using uppaal tiga. In: Formal modeling and analysis of timed systems. Springer, pp 227-240
[33] Konur S, Dixon C, Fisher M (2010) Formal verification of probabilistic swarm behaviours. In: International conference on swarm intelligence. Springer, pp 440-447
[34] Kress-Gazit, H.; Lahijanian, M.; Raman, V., Synthesis for robots: guarantees and feedback for robot behavior, Ann Rev Control Robot Auton Syst, 1, 1, 211-236 (2018)
[35] Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: Computer aided verification. Springer, pp 585-591
[36] Kunze L, Roehm T, Beetz M (2011) Towards semantic robot description languages. In: International conference on robotics and automation. IEEE, pp 5589-5595
[37] Luckcuck M, Farrell M, Dennis LA, Dixon C, Fisher M (2019) Formal specification and verification of autonomous robotic systems: a survey. ACM Comput Surv 52(5):100:1-100:41
[38] Largouët C, Krichen O, Zhao Y (2016) Temporal planning with extended timed automata. In: International conference on tools with artificial intelligence. IEEE, pp 522-529
[39] Lignos, C.; Raman, V.; Finucane, C.; Marcus, M.; Kress-Gazit, H., Provably correct reactive control from natural language, Auton Robots, 38, 1, 89-105 (2015)
[40] Loetzsch M, Risler M, Jüngel M (2006) XABSL-A pragmatic approach to behavior engineering. In: International Conference on Intelligent Robots and Systems. IEEE/RSG, pp 5124-5129
[41] Lopes, YK; Trenkwalder, SM; Leal, AB; Dodd, TJ; Groß, R., Supervisory control theory applied to swarm robotics, Swarm Intell, 10, 1, 65-97 (2016)
[42] Morse J, Araiza-Illan D, Lawry J, Richards A, Eder K (2016) Formal specification and analysis of autonomous systems under partial compliance. arXiv preprint arXiv:1603.01082
[43] Menghi C, García S, Pelliccione P, Tůmová J (2018) Multi-robot LTL planning under uncertainty. In: International symposium on formal methods. Springer, pp 399-417
[44] Menghi C, García S, Pelliccione P, Tůmová J (2018) Towards multi-robot applications planning under uncertainty. In: International conference on software engineering: companion proceeedings. ACM, pp 438-439
[45] Mayer MC, Orlandini A (2015) An executable semantics of flexible plans in terms of timed game automata. In: Temporal Representation and Reasoning. IEEE, pp 160-169
[46] Maoz S, Ringert JO (2019) Spectra. http://smlab.cs.tau.ac.il/syntech/spectra/userguide.pdf
[47] Miyazawa A, Ribeiro P, Li W, Cavalcanti A, Timmis J (2017) Automatic property checking of robotic applications. In: International conference on intelligent robots and systems. IEEE/RJS, pp 3869-3876
[48] Miyazawa A, Ribeiro P, Li W, Cavalcanti A, Timmis J, Woodcock J (2019) RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw Syst Model
[49] Menghi C, Tsigkanos C, Berger T, Pelliccione P, Ghezzi C (2018) Poster: property specification patterns for robotic missions. In: International conference on software engineering: companion proceeedings. IEEE/ACM, pp 434-435
[50] Menghi C, Tsigkanos C, Berger T, Pelliccione P (2019) Psalm: specification of dependable robotic missions. In: International conference on software engineering: companion proceedings. IEEE/ACM, pp 99-102
[51] Menghi C, Tsigkanos C, Pelliccione P, Ghezzi C, Berger T (2019) Specification patterns for robotic missions. IEEE Trans Softw Eng, pp 1-1
[52] https://www.ald.softbankrobotics.com/en/robots/nao/find-out-more-about-nao
[53] Nordmann A, Hochgeschwender N, Wrede S (2014) A survey on domain-specific languages in robotics. In: International Conference on Simulation, Modeling, and Programming for Autonomous Robots. Springer, pp 195-206
[54] Orlandini A, Finzi A, Cesta A, Fratini S, Tronci E (2011) Enriching apsi with validation capabilities: The keen environment and its use in robotics. In: Advanced Space Technologies in Robotics and Automation. http://robotics.estec.esa.int/ASTRA/Astra2011/Astra2011_Proceedings.zip1
[55] Online appendix, (2019) https://drive.google.com/drive/folders/117-MVWDYYo-6Gir6KAzlVTsvshGu2Uvf
[56] Peter H, Ehlers R, Mattmüller R (2011) Synthia: Verification and synthesis for timed automata. In: International conference on computer aided verification. Springer, pp 649-655
[57] Pinheiro LP, Lopes YK, Leal AB, Junior RS (2015) Nadzoru: a software tool for supervisory control of discrete event systems. IFAC-PapersOnLine 48(7):182 - 187. International Workshop on Dependable Control of Discrete Systems
[58] PuRSUE - Planner for RobotS in Uncontrollable Environments, (2019). https://github.com/deib-polimi/PuRSUE
[59] Quigley M, Conley K, Gerkey B, Faust J, Foote T, Leibs J, Wheeler R, Ng AY (2009) ROS: an open-source robot operating system. In: ICRA workshop on open source software, vol 3. IEEE, p 5
[60] Quattrini Li A, Fioratto R, Amigoni F, Isler V (2018) A search-based approach to solve pursuit-evasion games with limited visibility in polygonal environments. In: International conference on autonomous agents and multiAgent systems. ACM, pp 1693-1701
[61] Rugg-Gunn N, Cameron S (1994) A formal semantics for multiple vehicle task and motion planning. In: International conference on robotics and automation. IEEE, pp 2464-2469
[62] Ruscio DD, Malavolta I, Pelliccione P, Tivoli M (2016) Automatic generation of detailed flight plans from high-level mission descriptions. In: International conference on model driven engineering languages and systems. ACM, pp 45-55
[63] Siciliano, B.; Khatib, O., Springer handbook of robotics (2016), Berlin: Springer, Berlin · Zbl 1357.93001
[64] Tůmová J, Dimarogonas DV (2014) A receding horizon approach to multi-agent planning from local LTL specifications. In: 2014 American Control Conference. IEEE, pp 1775-1780
[65] Tůmová, J.; Dimarogonas, DV, Multi-agent planning under local LTL specifications and event-based synchronization, Automatica, 70, 239-248 (2016) · Zbl 1339.93080
[66] Truszkowski W, Rash J, Hinchey M, Rouff C. A survey of formal methods for intelligent swarms. https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20050156631.pdf · Zbl 1088.68154
[67] Tunggal, TP; Supriyanto, A.; Faishal, I.; Pambudi, I., Pursuit algorithm for robot trash can based on fuzzy-cell decomposition, Int J Electr Comput Eng, 6, 6, 2863 (2016)
[68] Vicentini, F.; Askarpour, M.; Rossi, M.; Mandrioli, D., Safety assessment of collaborative robotics through automated formal verification, IEEE Trans Robot, 31, 1, 42-61 (2020)
[69] Ecobot. https://youtu.be/w6SfCmgdCsk, https://youtu.be/XmOY-urEDD0
[70] Verginis CK, Vrohidis C, Bechlioulis CP, Kyriakopoulos KJ, Dimarogonas DV (2019) Reconfigurable motion planning and control in obstacle cluttered environments under timed temporal tasks. In: International Conference on Robotics and Automation. IEEE, pp 951-957
[71] International Federation of Robotics. https://ifr.org/worldrobotics/
[72] Zamani, M.; Arcak, M., Compositional abstraction for networks of control systems: a dissipativity approach, IEEE Trans Control Netw Syst, 5, 3, 1003-1015 (2018) · Zbl 07044967
[73] Zamani, M.; Pola, G.; Mazo, M.; Tabuada, P., Symbolic models for nonlinear control systems without stability assumptions, Trans Autom Control, 57, 7, 1804-1809 (2011) · Zbl 1369.93002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.