Verifiable Autonomous Systems
Using Rational Agents to Provide Assurance about Decisions Made by Machines

A discussion of methods by which scientists may guarantee the behaviours of autonomous systems, from intelligent robots to driverless cars.

Louise A. Dennis (Author), Michael Fisher (Author)

9781108484992, Cambridge University Press

Hardback, published 8 June 2023

410 pages
23.5 x 15.8 x 2.7 cm, 0.71 kg

How can we provide guarantees of behaviours for autonomous systems such as driverless cars? This tutorial text, for professionals, researchers and graduate students, explains how autonomous systems, from intelligent robots to driverless cars, can be programmed in ways that make them amenable to formal verification. The authors review specific definitions, applications and the unique future potential of autonomous systems, along with their impact on safer decisions and ethical behaviour. Topics discussed include the use of rational cognitive agent programming from the Beliefs-Desires-Intentions paradigm to control autonomous systems and the role model-checking in verifying the properties of this decision-making component. Several case studies concerning both the verification of autonomous systems and extensions to the framework beyond the model-checking of agent decision-makers are included, along with complete tutorials for the use of the freely-available verifiable cognitive agent toolkit Gwendolen, written in Java.

1. Introduction
Part I. Foundations: 2. Autonomous systems architectures
3. Agent decision maker
4. Formal agent verification
5. Verifying autonomous systems
6. Agent-based autonomous system verification
Part II. Applications: 7. Multi-agent auctions
8. Autonomous satellite control
9. Certification of unmanned air systems
10. Ethical decision making
Part III. Extensions: 11. Compositional verification – widening our view beyond the agent
12. Runtime verification – recognising abstraction violations
13. Utilising external model-checkers
Part IV. Concluding Remarks: 14. Verifiable autonomous systems
15. The future
Appendix A. Gwendolen documentation
Appendix B. AIL toolkit documentation
Appendix C. AJPF documentation
Bibliography
Index.

Subject Areas: Artificial intelligence [UYQ], Computer architecture & logic design [UYF], Operating systems [UL], Robotics [TJFM1]