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

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.

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.

The particular approach we consider here is implemented as the Java Path-Finder (JPF) system, which is an explicit-state open source model-checker for Java programs. Programs in Java are compiled to a set of bytecodes which are then executed, when required, by a virtual machine, called the Java Virtual Machine (JVM). In order to allow this execution to be controlled, and indeed backtracked if necessary, JPF provides a special, modified JVM which can explore all executions including all non-deterministic choices, thread inter-leavings, and so on. Importantly, this new JVM records all the choices made and can backtrack to explore previous choice points. Note that this modified JVM is actually implemented in Java and so runs on top of a standard JVM.