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.
Author(s): Louise A. Dennis, Michael Fisher
Publisher: Cambridge University Press
Year: 2023
Language: English
Pages: 391
Introduction 1
1.1 What is an Autonomous System? 2
1.2 Why Autonomy? 4
1.3 Why use Formal Verification? 8
Part I Foundations
2 Autonomous Systems Architectures 13
2.1 Architectures for Autonomous Systems 13
2.2 Agent Architectures 16
2.3 Modularity in Modern Robotic Software 20
2.4 Practical Systems 21
3 Agent Decision-Maker 24
3.1 Agents and Cognitive Agents 24
3.2 Agent Programming 26
3.3 GWENDOLEN Programming Language 33
3.4 Agent Environments 40
4 Formal Agent Verification 42
4.1 What is Verification? 43
4.2 From Testing to Formal Verification 43
4.3 Varieties of Formal Verification 44
4.4 Understanding Program Model-Checking 45
4.5 Program Model-Checking with Java PathFinder 50
4.6 Logical Agent Requirements 53
4.7 Discussion 57
vii
viii Contents
5 Verifying Autonomous Systems 58
5.1 Modular Architectures for Autonomous Systems 61
5.2 Overview 62
5.3 Verifying Autonomous Choices 63
5.4 Onward 67
6 Agent-Based Autonomous System Verification 68
6.1 From Operational Semantics to Model-Checking 69
6.2 The Property Specification Language 69
6.3 Where Does the Automaton Representing a BDI Agent
Program Branch? 71
6.4 The Problem with Environments 72
6.5 Example: Cars on a Motorway 73
6.6 Moving on to Applications 79
Part II Applications
7 Multi-Agent Auctions 83
7.1 What is the System? 83
7.2 What Properties Do We Want to Establish? 88
7.3 GWENDOLEN Code 88
7.4 Environments 99
7.5 Example Verification 99
7.6 Issues 103
8 Autonomous Satellite Control 104
8.1 What is the System? 104
8.2 What Properties Do We Want to Establish? 106
8.3 GWENDOLEN Code 110
8.4 Environments 117
8.5 Example Verification 123
8.6 Issues 126
9 Certification of Unmanned Air Systems 127
9.1 What is the System? 127
9.2 What Properties Do We Want to Establish? 131
9.3 GWENDOLEN Code 137
9.4 Environments 145
9.5 Example Verification 146
9.6 Issues 148
Contents ix
10 Ethical Decision-Making 150
10.1 What is the System? 150
10.2 What Properties Do We Want to Establish? 158
10.3 ETHAN/GWENDOLEN Code 162
10.4 Environments 167
10.5 Example Verification 168
10.6 Issues 169
10.7 Cognitive Agents as Ethical Governors 170
Part III Extensions
11 Compositional Verification: Widening Our View beyond the
Agent 177
11.1 Example Systems 177
11.2 Why use a Compositional Approach to Verification? 180
11.3 Other Formal Tools 182
11.4 Some Verification Results 182
11.5 How Do We Combine These Results? 194
11.6 Discussion 202
12 Runtime Verification: Recognising Abstraction Violations 203
12.1 Example System 204
12.2 Formal Machinery 206
12.3 Integration of Monitor in the MCAPL Framework 214
12.4 Verification Results 215
12.5 Discussion 216
13 Utilising External Model-Checkers 218
13.1 Example Systems 219
13.2 Other Model-Checkers 224
13.3 Translation Approach 226
13.4 Verification Results 231
13.5 Discussion 237
Part IV Concluding Remarks
14 Verifiable Autonomous Systems 241
15 The Future 244
Appendix A Gwendolen Documentation 246
Appendix B AIL Toolkit Documentation 297
x Contents
