Advertisement

Strategy Synthesis for Autonomous Agents Using PRISM

  • Ruben Giaquinta
  • Ruth Hoffmann
  • Murray Ireland
  • Alice Miller
  • Gethin Norman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)

Abstract

We present probabilistic models for autonomous agent search and retrieve missions derived from Simulink models for an Unmanned Aerial Vehicle (UAV) and show how probabilistic model checking and the probabilistic model checker PRISM can be used for optimal controller generation. We introduce a sequence of scenarios relevant to UAVs and other autonomous agents such as underwater and ground vehicles. For each scenario we demonstrate how it can be modelled using the PRISM language, give model checking statistics and present the synthesised optimal controllers. We conclude with a discussion of the limitations when using probabilistic model checking and PRISM in this context and what steps can be taken to overcome them. In addition, we consider how the controllers can be returned to the UAV and adapted for use on larger search areas.

Notes

Acknowledgements

This work was supported by EPSRC grant EC/P51133X/1. We would like to thank Dave Anderson and Euan McGookin for discussions on the autonomous systems that inspired this paper.

References

  1. 1.
    Alur, R., Henzinger, T.: Reactive modules. FMSD 15, 7–48 (1999)Google Scholar
  2. 2.
    Bohn, C.: Heuristics for designing the control of a UAV fleet with model checking. In: Grundel, D., Murphey, R., Pardalos, P., Prokopyev, O. (eds.) Cooperative Systems. Lecture Notes in Economics and Mathematical Systems, vol. 588, pp. 21–36. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-48271-0_2 CrossRefGoogle Scholar
  3. 3.
    Chatterjee, K., Doyen, L.: Partial-observation stochastic games: how to win when belief fails. ACM Trans. Comput. Log. 15, 16 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: a model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185–191. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_13 CrossRefGoogle Scholar
  5. 5.
    Choi, J.: Model checking for decision making behaviour of heterogeneous multi-agent autonomous system. Ph.D. thesis, Cranfield University (2012)Google Scholar
  6. 6.
    Dennis, L., Fisher, M., Lincoln, N., Lisitsa, A., Veres, S.: Practical verification of decision-making in agent-based autonomous systems. ASE 23(3), 305–359 (2016)Google Scholar
  7. 7.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Draeger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. LMCS 11(2), 1–34 (2015)MathSciNetzbMATHGoogle Scholar
  9. 9.
    Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. LMCS 4, 1–21 (2008)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-21455-4_3 CrossRefGoogle Scholar
  11. 11.
    Fu, J., Topcu, U.: Computational methods for stochastic control with metric interval temporal logic specifications. In: Proceedings of CDC 2015 (2015)Google Scholar
  12. 12.
    Hoffmann, R., Ireland, M., Miller, A., Norman, G., Veres, S.: Autonomous agent behaviour modelled in PRISM – a case study. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 104–110. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-32582-8_7 CrossRefGoogle Scholar
  13. 13.
    Humphrey, L.: Model checking for verification in UAV cooperative control applications. In: Fahroo, F., Wang, L., Yin, G. (eds.) Recent Advances in Research on Unmanned Aerial Vehicles. LNCIS, vol. 444, pp. 69–117. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37694-8_4 CrossRefGoogle Scholar
  14. 14.
    Ireland, M., Hoffmann, R., Miller, A., Norman, G., Veres, S.: A continuous-time model of an autonomous aerial vehicle to inform and validate formal verification methods. http://arxiv.org/abs/1609.00177v1
  15. 15.
    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)Google Scholar
  16. 16.
    Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. FMSD 36, 246–280 (2010)zbMATHGoogle Scholar
  17. 17.
    Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976).  https://doi.org/10.1007/978-1-4684-9455-6 CrossRefzbMATHGoogle Scholar
  18. 18.
    Konur, S., Dixon, C., Fisher, M.: Analysing robot swarm behaviour via probabilistic model checking. Robot. Auton. Syst. 60(2), 199–213 (2012)CrossRefGoogle Scholar
  19. 19.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47 CrossRefGoogle Scholar
  20. 20.
    Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5–22. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-02444-8_2 CrossRefGoogle Scholar
  21. 21.
    Lacerda, B., Parker, D., Hawes, N.: Multi-objective policy generation for mobile robots under probabilistic time-bounded guarantees. In: Proceedings of ICAPS 2017 (2017)Google Scholar
  22. 22.
    Lahijanian, M., Andersson, S., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60, 2031–2045 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Lahijanian, M., Kwiatkowska, M.: Specification revision for Markov decision processes with optimal trade-off. In: Proceedings of CDC 2016. IEEE (2016)Google Scholar
  24. 24.
    Liu, W., Winfield, A., Sa, J.: Modelling swarm robotic systems: a case study in collective foraging. In: Proceedings of TAROS 2007 (2007)Google Scholar
  25. 25.
    Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. Comput. Surve. 36, 8 (2006)CrossRefGoogle Scholar
  26. 26.
    Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real-Time Syst. 53, 354–402 (2017)CrossRefzbMATHGoogle Scholar
  27. 27.
    O’Brien, M., Arkin, R.C., Harrington, D., Lyons, D., Jiang, S.: Automatic verification of autonomous robot missions. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds.) SIMPAR 2014. LNCS (LNAI), vol. 8810, pp. 462–473. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11900-7_39 Google Scholar
  28. 28.
    Shapley, L.: Stochastic games. Proc. Natl. Acad. Sci. 39, 1095–1100 (1953)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Sharan, R.: Formal methods for control synthesis in partially observed environments: application to autonomous robotic manipulation. Ph.D. thesis, California Institute of Technology (2014)Google Scholar
  30. 30.
    Soudjani, S., Majumdar, R.: Controller synthesis for reward collecting Markov processes in continuous space. In: Proceedings of HSCC 2017. ACM (2017)Google Scholar
  31. 31.
    Svoreňová, M., Chmelík, M., Leahy, K., Eniser, H., Chatterjee, K., Černá, I., Belta, C.: Temporal logic motion planning using POMDPs with parity objectives: case study paper. In: Proceedings of HSCC 2015. ACM (2015)Google Scholar
  32. 32.
    Svoreňová, M., Křetínský, J., Chmelík, M., Chatterjee, K., Cerna, I., Belta, C.: Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of HSCC 2015. ACM (2015)Google Scholar
  33. 33.
    Webster, M., Fisher, M., Cameron, N., Jump, M.: Formal methods for the certification of autonomous unmanned aircraft systems. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 228–242. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-24270-0_17 CrossRefGoogle Scholar
  34. 34.
    Wilson, J.: Drones hacked and crashed by research team to expose design flaws. Engineering and Technology (2016)Google Scholar
  35. 35.
    Wolff, E., Topcu, U., Murray, R.: Robust control of uncertain Markov decision processes with temporal logic specifications. In: Proceedings of CSC 2012. IEEE (2012)Google Scholar
  36. 36.
    Yoo, C., Finch, R., Sukkarieh, S.: Provably-correct stochastic motion planning with safety constraints. In: Proceedings of ICRA 2013. IEEE (2013)Google Scholar
  37. 37.

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Ruben Giaquinta
    • 1
  • Ruth Hoffmann
    • 3
  • Murray Ireland
    • 2
  • Alice Miller
    • 1
  • Gethin Norman
    • 1
  1. 1.School of Computing ScienceUniversity of GlasgowGlasgowUK
  2. 2.School of EngineeringUniversity of GlasgowGlasgowUK
  3. 3.School of Computer ScienceUniversity of St AndrewsSt AndrewsUK

Personalised recommendations