Collaborative models for autonomous systems controller synthesis

Abstract

We show how detailed simulation models and abstract Markov models can be developed collaboratively to generate and implement effective controllers for autonomous agent search and retrieve missions. We introduce a concrete simulation model of an Unmanned Aerial Vehicle (UAV). We then show how the probabilistic model checker PRISM is used for optimal strategy synthesis for a sequence of scenarios relevant to UAVs and potentially other autonomous agent systems. For each scenario we demonstrate how it can be modelled using PRISM, give model checking statistics and present the synthesised optimal strategies. We then show how our strategies can be returned to the controller for the simulation model and provide experimental results to demonstrate the effectiveness of one such strategy. Finally we explain how our models can be adapted, using symmetry, for use on larger search areas, and demonstrate the feasibility of this approach.

References

  1. Ack13

    Ackerman E NASA lets curiosity rover loose on Mars in autonomous driving mode. IEEE Spectrum, 29 August 2013

  2. AH99

    Alur, R., Henzinger, T.: Reactive modules. Formal Methods Syst Des 15, 7–48 (1999)

    Article  Google Scholar 

  3. ASK04

    Agrawal A, Simon G, Karsai G (2004) Semantic translation of simulink/stateflow models to hybrid automata using graph transformations. In: Proceedings of the international workshop on graph transformation and visual modelling techniques (GT-VMT'04), ENTCS, vol 109 , pp 43–56

  4. BBB+12

    Barnat J, Beran J, Brim J, Kratochvíla T, Roc̆kai P (2012) Tool chain to support automated verification of avionics Simulink designs. In: Proceedings of the international workshop on formal methods for industrial critical systems (FMICS'12), LNCS, vol 7436, pp 78–92

  5. BBFL18

    Bacci G, Bouyer P, Fahrenberg U, Larsen K (2018) Optimal and robust controller synthesis. In: Proceedings of the international symposium on formal methods (FM'18), LNCS, Springer, vol 10951, pp 2013–221

  6. BBH+13

    Barnat J, Brim L, Havel V, Havelic̆ek J, Kriho J, Lenc̆o M, Roc̆kai P, S̆till V, Weiser J (2013) DiVinE 3.0 - an explicit-state model checker for multithreaded C & C++ programs. In: Proceedings of the international conference on computer aided verifiication (CAV'13), LNCS, vol 8044, pp 863–868

  7. BCD+07

    Behrmann G, Cougnard A, David A, Fleury E, Larsen K, Lime Didier D (2007) Uppaal-Tiga: Time for playing games! In: Proceedings of the international conference on computer aided verification (CAV'07), LNCS, Springer, vol 4590, pp 121–125

  8. BDH+07

    Burdick J, DuToit N, Howard A, Looman C, Ma J, Wongpiromsarn T (2007) Sensing, navigation and reasoning technologies for the DARPA urban challenge. In: DARPA Urban Challenge Final Report, Technical Report

  9. BMS04

    Bouabdallah S, Murrieri P, Siegwart R (2004) Design and control of an indoor micro quadrotor. In: Proceedings of the international conference on robotics and automation (ICRA'04), IEEE, pp 4393–4398

  10. CCGR99

    Cimatti A, Clarke E, Giunchiglia F, Roveri M (1999) NUSMV: A new symbolic model verifier. In: Proceedings of the international conference on computer aided verification (CAV'99), pp 295–499

  11. CD14

    Chatterjee, K., Doyen, L.: Partial-observation stochastic games: how to win when belief fails. ACM Trans Comput Log 15(2), 1–44 (2014)

    MathSciNet  Article  Google Scholar 

  12. CK00

    Chutinan, A., Krogh, B.: Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Trans Autom Control 46(9), 101–109 (2000)

    MathSciNet  MATH  Google Scholar 

  13. CKNZ11

    Clarke, E., Klieber, W., Novác̆ek M, Zuliani P, : Model checking and the state explosion problem. Tools for practical software verification: laser, international summer school, LNCS, Springer 7682, 1–30 (2011)

    Google Scholar 

  14. DDL+12

    David A, Du D, Larsen K, Legay A, Mikuc̆ionis A, Poulsen M, Sedwards S (2012) Statistical model checking for stochastic hybrid systems. In: Proceedings of the international workshop on hybrid systems and biology (HSB'12), EPTCS, vol 92, pp 122–136

  15. DFK+15

    Draeger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Log Methods Comput Sci 11(2), (2015)

  16. DFL+16

    Dennis, L., Fisher, M., Lincoln, N., Lisitsa, A., Veres, S.: Practical verification of decision-making in agent-based autonomous systems. Autom Softw Eng 23(3), 1–55 (2016)

    Article  Google Scholar 

  17. DH04

    Dabney, J., Harman, T.: Mastering Simulink. Pearson/Prentice Hall, Upper Saddle River (2004)

    Google Scholar 

  18. DMP09

    Donaldson A, Miller A, Parker D (2009) Language-level symmetry reduction for probabilistic model checking. In: Proceedings of the international conference on quantitative evaluation of systems (QEST'09), IEEE, pp 289–298

  19. DSBR14

    Ding, X., Smith, S., Belta, C., Rus, D.: Optimal control of Markov decision processes with linear temporal logic constraints. IEEE Trans Autom Control 59, 1244–1257 (2014)

    MathSciNet  Article  Google Scholar 

  20. DSL09

    Das, A., Subbarao, K., Lewis, F.: Dynamic inversion with zero-dynamics stabilisation for quadrotor control. Control Theory Appl IET 3(3), 303–314 (2009)

    MathSciNet  Article  Google Scholar 

  21. EKVY08

    Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log Methods Comput Sci 4, 1–21 (2008)

    MathSciNet  MATH  Google Scholar 

  22. EP18

    ECI-PwC. Flying high: Drones to drive jobs in the construction sector. In: Presented at the national conference of the engineering council of India (ECI), 2018

  23. FDW13

    Fisher, M., Dennis, L., Webster, M.: Verifying autonomous systems. Commun ACM 56(9), 84–93 (2013)

    Article  Google Scholar 

  24. FIS19

    Foughali M, Ingrand F, Seceleanu C (2019) Statistical model checking of complex robotic systems. In: Proceedings of the international symposium on model checking of software (SPIN'19), LNCS, vol 11636, pp 114–134

  25. FKNP11

    Forejt V, Kwiatkowska M, Norman G, Parker D (2011) Automated verification techniques for probabilistic systems. In: Formal methods for eternal networked software systems (SFM'11), LNCS, Springer, vol 6659, pp 53–113

  26. FMM+16

    Filipovikj P, Mahmud N, Marinescu R, Seceleanu C, Ljungkrantz O (2016) Lönn H Simulink to uppaal statistical model checker: analyzing automotive industrial systems. In: Proceedings of the international symposium formal methods (FM'16), LNCS, vol 9995, pp 748–756

  27. FT15

    Fu J, Topcu U (2015) Computational methods for stochastic control with metric interval temporal logic specifications. In: Proceedings of the international conference on decision and control (CDC'15), IEEE, pp 7440–7447

  28. FWHT15

    Feng L, Wiltsche C, Humphrey L, Topcu U (2015) Controller synthesis for autonomous systems interacting with human operators. In: Proceedings of the international conference on cyber-physical systems (ICCPS'15), ACM, pp 70–79

  29. GHI+18

    Giaquinta R, Hoffmann R, Ireland M, Miller A, Norman G (2018) Strategy synthesis for autonomous agents using PRISM. In: Proceedings on NASA Formal Methods Symposium (NFM'2018), LNCS, Springer, vol 10811, pp 220–236

  30. GL19

    Gibson-Robinson, T., Lowe, G.: Symmetry reduction in CSP model checking. Int J Softw Tools Technol Transf 21, 567–605 (2019)

    Article  Google Scholar 

  31. HCRP91

    Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language lustre. Proc IEEE 79(9), 1305–1320 (1991)

    Article  Google Scholar 

  32. Hen96

    Henzinger T (1996) The theory of hybrid automata. In: Proceedings of the international symposium on logic in computer science (LICS'96), IEEE, pp 278–292

  33. HIM+16

    Hoffmann R, Ireland M, Miller A, Norman G, Veres S (2016) Autonomous agent behaviour modelled in PRISM: a case study. In: Proceedings of the international symposium model checking software (SPIN'16), LNCS, Springer, vol 9641, pp 104–110

  34. Hsu16

    Hsu J U.S. navy's drone boat swarm practices harbor defense. IEEE Spectrum, 19 December 2016

  35. Ire14

    Ireland, M.: Investigations in multi-resolution modelling of the quadrotor micro air vehicle. University of Glasgow, PhD (2014)

    Google Scholar 

  36. IVA15

    Ireland, M., Vargas, A., Anderson, D.: A comparison of closed-loop performance of multirotor configurations using non-linear dynamic inversion control. Aerospace 2(2), 325–352 (2015)

    Article  Google Scholar 

  37. JYL+16

    Jiang Y, Yang Y, Liu H, Kong H, Gu M, Sun J, Sha L (2016) From Stateflow simulation to verified implementation: a verified approach and a real-time train controller design. In: Proceedings of the international real-time and embedded technology and applications symposium (RTAS'16), IEEE, pp 1–11

  38. KEPS99

    Kowalewski, S., Engell, S., Preußig, J., Stursberg, O.: Verification of logic controllers for continuous plants using timed condition/event-system models. Automatica 35(3), 505–518 (1999)

    MathSciNet  Article  Google Scholar 

  39. KKNP10

    Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst Des 36, 246–280 (2010)

    Article  Google Scholar 

  40. KMP10

    Kubera Y, Mathieu P, Picault S (2010) Everything can be agent! (extended abstract). In: Proceedings of the international conference on autonomous agents and multi-agent systems (AAMAS10), pp 1547–1548

  41. KNP11

    Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Proceedings of the international conference on computer aided verification (CAV'11), LNCS, Springer, vol 6806, pp 585–591

  42. KP13

    Kwiatkowska M, Parker D (2013) Automated verification and strategy synthesis for probabilistic systems. In: Proceedings of the international symposium automated technology for verification and analysis (ATVA'13), LNCS, Springer, vol 8172, pp 5–22

  43. KP16

    Kalra, N., Paddock, S.: Driving to safety: How many miles of driving would it take to demonstrate autonomous vehicle reliability? Transp Res Part A Policy Pract 94, 182–193 (2016)

    Article  Google Scholar 

  44. KPR16

    Kamaleson N, Parker D, Rowe J (2016) Finite-horizon bisimulation minimisation for probabilistic systems. In: Proceedings of the international symposium model checking software (SPIN'16), LNCS, Springer, vol 9641, pp 147–164

  45. KPW17

    Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: Verification and strategy synthesis for stochastic multi-player games with multiple objectives. Int J Softw Tools Technol Transf 20(2), 195–210 (2017)

    Article  Google Scholar 

  46. KSK76

    Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, Berlin (1976)

    Book  Google Scholar 

  47. KWT11

    Kress-Gazit, H., Wongpiromsarn, T., Topcu, U.: Correct, reactive, high-level robot control. IEEE Robot Autom Mag 18(3), 65–74 (2011)

    Article  Google Scholar 

  48. LAB15

    Lahijanian, M., Andersson, S., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans Autom Control 60, 2031–2045 (2015)

    MathSciNet  Article  Google Scholar 

  49. LFD+18

    Luckcuck M, Farrell M, Dennis L, Dixon C, Fisher M (2018) Formal specification and verification of autonomous robotic systems: A survey. CoRR, arXiv:1807.00048

  50. LK16

    Lahijanian M, Kwiatkowska M (2016) Specification revision for Markov decision processes with optimal trade-off. In: Proceedings of the international conference decision and control (CDC'16). IEEE

  51. LKM+08

    Lerda F, Kapinski J, Maka H, Clarke E, Krogh B (2008) Model checking in-the-loop. In: Proceedings of American control conference (ACC'08), pp 2734–2740

  52. LPH17

    Lacerda B, Parker D, Hawes N (2017) Multi-objective policy generation for mobile robots under probabilistic time-bounded guarantees. In: Proceedings of the international conference on automated planning and scheduling (ICAPS'17), AAAI, pp 504–512

  53. LPY97

    Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. Softw Tools Technol Transf 1, 134–152 (1997)

    Article  Google Scholar 

  54. MBR06

    Meenakshi B, Bhatnagar A, Roy S (2006) Tool for translating Simulink models into input language of a model checker. In: Proceedings of the international conference on formal engineering methods (ICFEM'06), LNCS, pp 606–620

  55. MD14

    Mueller M, D'Andrea R (2014) Stability and control of a quadrocopter despite the complete loss of one, two, or three propellers. In: Proceedings of the international conference on robotics and automation (ICRA'14), IEEE, pp 45–52

  56. MDC06

    Miller A, Donaldson A, Calder M (2006) Symmetry in temporal logic model checking. Comput Surv 36:8-es

  57. Mil09

    Miller S (2009) Bridging the gap between model-based development and model checking. In: Proceedings of the international conference on tools and algorithms for the construction and analysis of systems (TACAS'09), LNCS, pp 443–453

  58. MMBC11

    Manamcheri K, Mitra S, Bak S, Caccamo M (2011) A step towards verification and synthesis from Simulink/Stateflow models. In: Proceedings of the international conference on hybrid systems: computation and control (HSCC'11), ACM, pp 317–318

  59. NPZ17

    Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real-Time Syst 53, 354–402 (2017)

    Article  Google Scholar 

  60. Rot16

    Rothwell J. US military tests `Sea Hunter,' world's largest unmanned ship, amid `deep concern' about China's naval expansion. The Telegraph, 3 May 2016

  61. SCL+15

    Svoreňová M, Chmelík M, Leahy K, Eniser H, Chatterjee K, Černá I, Belta C (2015) Temporal logic motion planning using POMDPs with parity objectives: case study paper. In: Proceedings of the international conference on hybrid systems: computation and control (HSCC'15), ACM, pp 233–238

  62. Sha53

    Shapley L (1953) Stochastic games. In: Proceedings of National Academy of Science, pp 1095–1100

  63. Sha14

    Sharan R (2014) Formal methods for control synthesis in partially observed environments: application to autonomous robotic manipulation. PhD thesis, California Institute of Technology

  64. SKC+17

    Svoreov, M., Ketnsk, J., Chmelk, M., Chatterjee, K., Cerna, I., Belta, C.: Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analys Hybrid Syst 23, 230–253 (2017)

    MathSciNet  Article  Google Scholar 

  65. SM17

    Soudjani S, Majumdar R (2017) Controller synthesis for reward collecting Markov processes in continuous space. In: Proceedings of the international conference on hybrid systems: computation and control (HSCC'17), ACM, pp 45–54

  66. TM06

    Tayebi, A., McGilvray, S.: Attitude Stabilization of a VTOL Quadrotor Aircraft. IEEE Trans Control Syst Technol 14(3), 562–571 (2006)

    Article  Google Scholar 

  67. Tre17

    HM Treasury. Autumn budget 2017: 25 things you need to know. UK Government website, 22 November 2017

  68. VNE+01

    Volpe R, Nesnas I, Estlin T, Mutz D, Petras R, Das H (2001) The CLARAty architecture for robotic autonomy. In: Proceedings of the international conference on aerospace (AeroConf'01), IEEE, pp 121–132

  69. Voo09

    Voos H (2009) Nonlinear control of a quadrotor micro-UAV using feedback-linearization. In: Proceedings of the international conference on mechatronics, IEEE, pp 1–6

  70. Wil16

    Wilson J Drones hacked and crashed by research team to expose design flaws. Engineering and Technology, 9 June 2016

  71. WTM12

    Wolff E, Topcu U, Murray R (2012) Robust control of uncertain Markov decision processes with temporal logic specifications. In: Proceedings of the international conference on Decision and Control (CSC'12), IEEE, pp 3372–3379

  72. YT16

    Yadron D, Tynan D Tesla driver dies in first fatal crash while using autopilot mode. The Guardian, 30 June 2016

Download references

Acknowledgments

The work described in this paper was supported by EPSRC grants EP/N508792/1, EP/N007565 and EC/P51133X/1. We would like to thank Dave Anderson, Euan McGookin and Sandor Veres for discussions on the autonomous systems that inspired this paper.

Author information

Affiliations

Authors

Corresponding author

Correspondence to Alice Miller.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Pedro Ribeiro and Ana Cavalcanti

Rights and permissions

Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, 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 licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence 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. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Fraser, D., Giaquinta, R., Hoffmann, R. et al. Collaborative models for autonomous systems controller synthesis. Form Asp Comp 32, 157–186 (2020). https://doi.org/10.1007/s00165-020-00508-1

Download citation

Keywords

  • Autonomous systems
  • Formal verification
  • Probabilistic model checking
  • Strategy synthesis