Название: Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines
Автор: Louise A. Dennis, Michael Fisher
Издательство: Cambridge University Press
Год: 2023
Страниц: 391
Язык: английский
Формат: pdf
Размер: 10.2 MB
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. In this book we will be considering examples written in the Gwendolen programming language, a typical BDI language designed for use with the AJPF model-checker. Gwendolen and AJPF are both part of the MCAPL framework. For those familiar with the input languages for model-checkers, it should be noted that Gwendolen programs are intended for the actual programming of cognitive agents. Input languages for most model-checkers are normally designed to encourage abstractions (in particular the omission of details that may be important to the actual execution of the program but are irrelevant to the truth of the properties under consideration), and often have limited flexibility, in terms of program structuring, in order to maximise the efficiency of model-checking. While Gwendolen does contain optimisations to aid model-checking these appear in the implementation of its interpreter in Java not as restrictions to constructs available to a programmer to use.