Abstract
The use of Autonomous Vehicles (AVs) on our streets is soon to be a reality; increasingly, interacting with such AVs will be part of our daily routine. However, we will certainly need to assure the reliable behaviour of an AV, especially when some unexpected scenarios (e.g. harsh environments, obstacles, emergencies) are taken into account. In this article we use an intelligent agent approach to capture the high-level decision-making process within an AV and then use formal verification techniques to automatically, and strongly, analyse the required behaviours. Specifically, we use the MCAPL framework, wherein our core agent is implemented using the GWENDOLEN agent programming language, and to which we can apply model checking via the AJPF model checker. By performing such formal verification on our agent, we are able to prove that the AV’s decision-making process, embedded within the GWENDOLEN agent plans, matches our requirements. As examples, we will verify (formal) properties in order to determine whether the agent behaves in a reliable manner through three different levels of emergency displayed in a simple urban traffic environment.
Work partially supported by EPSRC projects EP/L024845 and EP/M027309.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
To showcase the approach, we take a very simple grid model of the environment.
References
Aitken, J., Shaukat, A., Cucco, E., Dennis, L., Veres, S., Gao, Y., Fisher, M., Kuo, J., Robinson, T., Mort, P.: Autonomous nuclear waste management. IEEE Intell. Syst. PP(99), 1 (2018)
Alves, G.V., Dennis, L., Fisher, M.: Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent. In: International Workshop on Verification and Validation of Autonomous Systems, pp. 1–2, Oxford, UK (2018)
Bonnefon, J.-F., Shariff, A., Rahwan, I.: The social dilemma of autonomous vehicles. Science 352(6293), 1573–1576 (2016)
Bordini, R.H., Dennis, L.A., Farwer, B., Fisher, M.: Automated verification of multi-agent programs. In: Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE ’08, pp. 69–78. Washington, DC, USA. IEEE Computer Society, Piscataway (2008)
Bratman, M.E.: Intentions, Plans, and Practical Reason. Harvard University Press, Cambridge (1987)
Cunningham, M.L., Regan, M.: Driver inattention, distraction and autonomous vehicles. In: 4th International Driver Distraction and Inattention Conference (2015)
Davnall, R.: Solving the single-vehicle self-driving car trolley problem using risk theory and vehicle dynamics. Sci. Eng. Ethics 1–19 (2019). ISSN 1471-5546, https://doi.org/10.1007/s11948-019-00102-6
Dennis, L.A.: Gwendolen semantics: 2017. Technical Report ULCS-17-001, University of Liverpool, Department of Computer Science (2017)
Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5–63 (2012)
Dennis, L.A., Fisher, M., Winfield, A.F.T.: Towards verifiably ethical robot behaviour. In: Proc. AAAI Workshop on AI and Ethics (2015)
Dennis, L.A., Fisher, M., Lincoln, N.K., Lisitsa, A., Veres, S.M.: Practical verification of decision-making in agent-based autonomous systems. Autom. Softw. Eng. 23(3), 305–359 (2016)
Dennis, L.A., Fisher, M., Slavkovik, M., Webster, M.P.: Formal verification of ethical choices in autonomous systems. Robot. Auton. Syst. 77, 1–14 (2016)
Department for Transport—UK. Testing automated vehicle technologies in public. Available at: https://www.gov.uk/government/publications/automated-vehicle-technologies-testing-code-of-practice (2015)
Department for Transport—UK. Regulations for driverless cars. Available at: https://www.gov.uk/government/publications/driverless-cars-in-the-uk-a-regulatory-review (2015)
Department for Transport—UK. Using the road (159 to 203)—The Highway Code—Guidance. Available at: https://www.gov.uk/guidance/the-highway-code/using-the-road-159-to-203 (2017)
Fernandes, L.E.R., Custodio, V., Alves, G.V., Fisher, M.: A rational agent controlling an autonomous vehicle: implementation and formal verification. In: Bulwahn, L., Kamali, M., Linker, S. (eds.) Proceedings First Workshop on Formal Verification of Autonomous Vehicles. Electronic Proceedings in Theoretical Computer Science, vol. 257, pp. 35–42 (2017)
Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, Hoboken (2011)
Fisher, M., Dennis, L.A., Webster, M.: Verifying autonomous systems. Commun. ACM 56(9), 84–93 (2013)
Foot, P.: The problem of abortion and the doctrine of double effect. Oxf. Rev. 5, 5–15 (1967)
Hawkins, A.J.: A day in the life of a Waymo self-driving taxi—The Verge. Available at: https://www.theverge.com/2018/8/21/17762326/waymo-self-driving-ride-hail-fleet-management (2018)
Herrmann, A., Brenner, W., Stadler, R.: Autonomous Driving: How the Driverless Revolution Will Change the World, 1st edn. Emerald Publishing, Bingley (2018). OCLC: 1031123857
Law Commission–Centre for Connected and Autonomous Vehicles: Automated Vehicles: a joint preliminary consultation paper. https://www.lawcom.gov.uk/project/automated-vehicles/. Accessed 8 Nov 2018
Lincoln, N., Veres, S.M., Dennis, L.A., Fisher, M., Lisitsa, A.: An agent based framework for adaptive control and decision making of autonomous vehicles. In: Proc. IFAC Workshop on Adaptation and Learning in Control and Signal Processing (ALCOSP) (2010)
Rao, A.S., Georgeff, M.P.: An abstract architecture for rational agents. In: Proc. International Conference on Knowledge Representation and Reasoning (KR&R), pp. 439–449. Morgan Kaufmann, Burlington (1992)
Vellinga, N.E.: From the testing to the deployment of self-driving cars: Legal challenges to policymakers on the road ahead. Comput. Law Secur. Rev. 33(6), 847–863 (2017)
Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)
Wicks, E.: The right to life and conflicting interests, pp. 1–288. Oxford University Press, Oxford (2010)
Wooldridge, M., Rao, A.: Foundations of Rational Agency, Applied Logic Series, vol. 14. Springer, Netherlands (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Alves, G.V., Dennis, L., Fernandes, L., Fisher, M. (2020). Reliable Decision-Making in Autonomous Vehicles. In: Leitner, A., Watzenig, D., Ibanez-Guzman, J. (eds) Validation and Verification of Automated Systems. Springer, Cham. https://doi.org/10.1007/978-3-030-14628-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-14628-3_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-14627-6
Online ISBN: 978-3-030-14628-3
eBook Packages: EnergyEnergy (R0)