More Web Proxy on the site http://driver.im/

research-article

Open access

PuRSUE -from specification of robotic environments to synthesis of controllers

Authors:

Marcello M. Bersani,

Claudio Menghi,

Patrizio Pelliccione,

Matteo RossiAuthors Info & Claims

Formal Aspects of Computing, Volume 32, Issue 2-3

Pages 187 - 227

https://doi.org/10.1007/s00165-020-00509-0

Published: 01 July 2020 Publication History

Abstract

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.

References

References

[1]

Alur R and Dill DL Model-checking in dense real-time Inf Comput 1993 104 1 2-34

Digital Library

[2]

Alur R and Dill DL A theory of timed automata Theor Comput Sci 1994 126 2 183-235

Digital Library

[3]

Asarin E, Maler O, Pnueli A (1995) Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems II. Springer

[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, and Vicentini F Formal model of human erroneous behavior for safety analysis in collaborative robotics Robot Comput Integr Manuf 2019 57 465-476

Digital Library

[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, and Tůmová J Guiding autonomous exploration with signal temporal logic IEEE Robot Autom Lett 2019 4 4 3332-3339

[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

[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)

[10]

Barrett A, Rabideau G, Estlin T, and Chien S Coordinated continual planning methods for cooperating rovers IEEE Aerosp Electron Syst Mag 2007 22 2 27-33

[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, and Pietro PS A tool for deciding the satisfiability of continuous-time metric temporal logic Acta Inf 2016 53 2 171-206

Digital Library

[13]

Berry G and Sethi R From regular expressions to deterministic automata Theor Comput Sci 1986 48 117-126

[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, and Roveri M NuSMV: a new symbolic model checker Int J Softw Tools Technol Transf 2000 2 4 410-425

[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

[17]

Campusano M and Fabry J Live robot programming: The language, its implementation, and robot API independence Sci Comput Program 2017 133 1-19

[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

[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, and Pelliccione P Adopting MDE for specifying and executing civilian missions of mobile multi-robot systems IEEE Access 2016 4 6451-6466

[23]

Damas B and Lima P Stochastic discrete event model of a multi-robot team playing an adversarial game IFAC Proc 2004 37 8 974-979

[24]

Farinelli A, Iocchi L, and Nardi D Multirobot systems: a classification focused on coordination Trans Syst Man Cybern Part B (Cybern) 2004 34 5 2015-2028

Digital Library

[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, and Raman V Synthesis for robots: guarantees and feedback for robot behavior Ann Rev Control Robot Auton Syst 2018 1 1 211-236

[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, and Kress-Gazit H Provably correct reactive control from natural language Auton Robots 2015 38 1 89-105

Digital Library

[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, and Groß R Supervisory control theory applied to swarm robotics Swarm Intell 2016 10 1 65-97

[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 and Khatib O Springer handbook of robotics 2016 2 Berlin Springer

[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 and Dimarogonas DV Multi-agent planning under local LTL specifications and event-based synchronization Automatica 2016 70 239-248

Digital Library

[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

[67]

Tunggal TP, Supriyanto A, Faishal I, Pambudi I, et al. Pursuit algorithm for robot trash can based on fuzzy-cell decomposition Int J Electr Comput Eng 2016 6 6 2863

[68]

Vicentini F, Askarpour M, Rossi M, and Mandrioli D Safety assessment of collaborative robotics through automated formal verification IEEE Trans Robot 2020 31 1 42-61

[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 and Arcak M Compositional abstraction for networks of control systems: a dissipativity approach IEEE Trans Control Netw Syst 2018 5 3 1003-1015

[73]

Zamani M, Pola G, Mazo M, and Tabuada P Symbolic models for nonlinear control systems without stability assumptions Trans Autom Control 2011 57 7 1804-1809

Cited By

Gu R(2024)Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.411.11411(160-177)Online publication date: 21-Nov-2024
https://doi.org/10.4204/EPTCS.411.11
Tagliaferro ALestingi LRossi MFuria CLopes APlat NGnesi S(2024)Towards Verifiable Multi-Agent Interaction Pattern SpecificationProceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1145/3644033.3644379(122-126)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3644033.3644379
Tagliaferro ALestingi LRossi M(2024)Verification-Oriented Specification of Multi-agent Interaction PatternsAgents and Robots for reliable Engineered Autonomy10.1007/978-3-031-73180-8_3(38-53)Online publication date: 13-Oct-2024
https://doi.org/10.1007/978-3-031-73180-8_3
Show More Cited By

Recommendations

Formal Specification and Verification of Autonomous Robotic Systems: A Survey

Autonomous robotic systems are complex, hybrid, and often safety critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or ...
Compositional Synthesis with Parametric Reactive Controllers
HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

Reactive synthesis with the ambitious goal of automatically synthesizing correct-by-construction controllers from high-level specifications, has recently attracted significant attention in system design and control. In practice, complex systems are ...
Verifiable Control of Robotic Swarm from High-level Specifications
AAMAS '18: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems

Designing controllers for safe, scalable and flexible collective behaviors of large numbers of robots is an important and challenging problem in swarm robotics. In this paper, we focus on provably-correct controller synthesis from high-level ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 32, Issue 2-3

Jul 2020

203 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© The Author(s) 2020.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 July 2020

Accepted: 28 February 2020

Received: 01 April 2019

Published in FAC Volume 32, Issue 2-3

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
134
Total Downloads

Downloads (Last 12 months)59
Downloads (Last 6 weeks)8

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gu R(2024)Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.411.11411(160-177)Online publication date: 21-Nov-2024
https://doi.org/10.4204/EPTCS.411.11
Tagliaferro ALestingi LRossi MFuria CLopes APlat NGnesi S(2024)Towards Verifiable Multi-Agent Interaction Pattern SpecificationProceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1145/3644033.3644379(122-126)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3644033.3644379
Tagliaferro ALestingi LRossi M(2024)Verification-Oriented Specification of Multi-agent Interaction PatternsAgents and Robots for reliable Engineered Autonomy10.1007/978-3-031-73180-8_3(38-53)Online publication date: 13-Oct-2024
https://doi.org/10.1007/978-3-031-73180-8_3
Lestingi L(2024)Model-Driven Development of Formally Verified Human-Robot InteractionsSpecial Topics in Information Technology10.1007/978-3-031-51500-2_4(41-51)Online publication date: 20-Mar-2024
https://doi.org/10.1007/978-3-031-51500-2_4
Gu REnoiu E(2023)Model-Based Policy Synthesis and Test-Case Generation for Autonomous Systems2023 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)10.1109/ICSTW58534.2023.00017(18-27)Online publication date: Apr-2023
https://doi.org/10.1109/ICSTW58534.2023.00017
Lestingi LZerla DBersani MRossi M(2023)Specification, stochastic modeling and analysis of interactive service robotic applicationsRobotics and Autonomous Systems10.1016/j.robot.2023.104387163:COnline publication date: 1-May-2023
https://dl.acm.org/doi/10.1016/j.robot.2023.104387
Gleirscher M(2023)Supervision of Intelligent Systems: An OverviewApplicable Formal Methods for Safe Industrial Products10.1007/978-3-031-40132-9_13(202-221)Online publication date: 17-Aug-2023
https://doi.org/10.1007/978-3-031-40132-9_13
Monthe VNana LKouamou G(2022)A Model-Based Approach for Common Representation and Description of Robotics Software ArchitecturesApplied Sciences10.3390/app1206298212:6(2982)Online publication date: 15-Mar-2022
https://doi.org/10.3390/app12062982
Lestingi LSbrolli CScarmozzino PRomeo GBersani MRossi MGnesi SPlat NHartmanns ASchaefer I(2022)Formal modeling and verification of multi-robot interactive scenarios in service settingsProceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering10.1145/3524482.3527653(80-90)Online publication date: 18-May-2022
https://dl.acm.org/doi/10.1145/3524482.3527653
Lestingi LBersani MRossi M(2022)Model-Driven Development of Service Robot Applications Dealing With Uncertain Human BehaviorIEEE Intelligent Systems10.1109/MIS.2022.321569837:6(48-56)Online publication date: 1-Nov-2022
https://doi.org/10.1109/MIS.2022.3215698
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents