×

zbMATH — the first resource for mathematics

Collaborative models for autonomous systems controller synthesis. (English) Zbl 1458.68219
Summary: 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.

MSC:
68T40 Artificial intelligence for robotics
68Q60 Specification and verification (program logics, model checking, etc.)
93A16 Multi-agent systems
93B50 Synthesis problems
93C85 Automated systems (robots, etc.) in control theory
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ackerman E NASA lets curiosity rover loose on Mars in autonomous driving mode. IEEE Spectrum, 29 August 2013
[2] Alur, R.; Henzinger, T., Reactive modules, Formal Methods Syst Des, 15, 7-48 (1999)
[3] 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 · Zbl 1271.68115
[4] 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] 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] 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] 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] 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] 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] 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 · Zbl 1046.68587
[11] Chatterjee, K.; Doyen, L., Partial-observation stochastic games: how to win when belief fails, ACM Trans Comput Log, 15, 2, 1-44 (2014) · Zbl 1291.91021
[12] Chutinan, A.; Krogh, B., Verification of infinite-state dynamic systems using approximate quotient transition systems, IEEE Trans Autom Control, 46, 9, 101-109 (2000)
[13] 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)
[14] 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] Draeger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Log Methods Comput Sci 11(2), (2015) · Zbl 1391.68076
[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)
[17] Dabney, J.; Harman, T., Mastering Simulink (2004), Upper Saddle River: Pearson/Prentice Hall, Upper Saddle River
[18] 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] 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) · Zbl 1360.90276
[20] Das, A.; Subbarao, K.; Lewis, F., Dynamic inversion with zero-dynamics stabilisation for quadrotor control, Control Theory Appl IET, 3, 3, 303-314 (2009)
[21] Etessami, K.; Kwiatkowska, M.; Vardi, M.; Yannakakis, M., Multi-objective model checking of Markov decision processes, Log Methods Comput Sci, 4, 1-21 (2008) · Zbl 1161.68565
[22] 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] Fisher, M.; Dennis, L.; Webster, M., Verifying autonomous systems, Commun ACM, 56, 9, 84-93 (2013)
[24] 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] 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 · Zbl 1315.68177
[26] 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] 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] 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] 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] Gibson-Robinson, T.; Lowe, G., Symmetry reduction in CSP model checking, Int J Softw Tools Technol Transf, 21, 567-605 (2019)
[31] Halbwachs, N.; Caspi, P.; Raymond, P.; Pilaud, D., The synchronous data flow programming language lustre, Proc IEEE, 79, 9, 1305-1320 (1991)
[32] 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 · Zbl 0959.68073
[33] 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] Hsu J U.S. navy’s drone boat swarm practices harbor defense. IEEE Spectrum, 19 December 2016
[35] Ireland, M., Investigations in multi-resolution modelling of the quadrotor micro air vehicle (2014), PhD: University of Glasgow, PhD
[36] 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)
[37] 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] 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) · Zbl 0934.93045
[39] 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) · Zbl 1233.90276
[40] 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] 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] 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 · Zbl 1410.68233
[43] 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)
[44] 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 · Zbl 1354.68197
[45] 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)
[46] Kemeny, J.; Snell, J.; Knapp, A., Denumerable Markov Chains (1976), Berlin: Springer, Berlin
[47] Kress-Gazit, H.; Wongpiromsarn, T.; Topcu, U., Correct, reactive, high-level robot control, IEEE Robot Autom Mag, 18, 3, 65-74 (2011)
[48] Lahijanian, M.; Andersson, S.; Belta, C., Formal verification and synthesis for discrete-time stochastic systems, IEEE Trans Autom Control, 60, 2031-2045 (2015) · Zbl 1360.93650
[49] 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] 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] 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] 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] Larsen, K.; Petterson, P.; Yi, W., Uppaal in a nutshell, Softw Tools Technol Transf, 1, 134-152 (1997) · Zbl 1060.68577
[54] 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] 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] Miller A, Donaldson A, Calder M (2006) Symmetry in temporal logic model checking. Comput Surv 36:8-es
[57] 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] 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] Norman, G.; Parker, D.; Zou, X., Verification and control of partially observable probabilistic systems, Real-Time Syst, 53, 354-402 (2017) · Zbl 1425.68266
[60] 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] 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 · Zbl 1364.93521
[62] Shapley L (1953) Stochastic games. In: Proceedings of National Academy of Science, pp 1095-1100 · Zbl 0051.35805
[63] Sharan R (2014) Formal methods for control synthesis in partially observed environments: application to autonomous robotic manipulation. PhD thesis, California Institute of Technology
[64] 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) · Zbl 1351.93138
[65] 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 · Zbl 1369.93715
[66] Tayebi, A.; McGilvray, S., Attitude Stabilization of a VTOL Quadrotor Aircraft, IEEE Trans Control Syst Technol, 14, 3, 562-571 (2006)
[67] HM Treasury. Autumn budget 2017: 25 things you need to know. UK Government website, 22 November 2017
[68] 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] 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] Wilson J Drones hacked and crashed by research team to expose design flaws. Engineering and Technology, 9 June 2016
[71] 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] Yadron D, Tynan D Tesla driver dies in first fatal crash while using autopilot mode. The Guardian, 30 June 2016
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.