Slides

Eastercon Talk Slides (PDF)

References and Links

Model Checking Rational Agents

The rational model of agency is generally attributed to Rao and Georgeff.

• Anand S. Rao and Michael P. Georgeff. Modeling Rational Agents within a BDI-Architecture. In James Allen, Richard Fikes, and Eric Sandewall, editors, Proceedings of the Second International Conference on Principles of Knowledge Representation and Reasoning (KR-91), pages 473-484. Morgan Kaufmann, April 1991. Available from citeseer

The verification of rational agents as discussed in the talk is described in detail in

• Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa, Sandor M. Veres. Practical Verification of Decision-Making in Agent-Based Autonomous Systems (available Open Access). Automated Software Engineering. The results mentioned in the paper can be reproduced using this Virtual Machine archived at recomputation.org.

and more generally in

• Michael Fisher, Louise A. Dennis, Matthew P. Webster. Verifying Autonomous Systems. Communications of the ACM 56(9): 85-93 (2013).

The software is part of the MCAPL Project on Sourceforge.

Verifying the Rules of the Air

• Matt Webster, Neil Cameron, Michael Fisher and Mike Jump. Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation (PDF preprint). Journal of Aerospace Information Systems, 11(5):258-279, 2014.

Ethical Robots

• Winfield AFT, Blum C and Liu W (2014), Towards an Ethical Robot: Internal Models, Consequences and Ethical Action Selection, pp 85-96 in Advances in Autonomous Robotics Systems, Lecture Notes in Computer Science Volume 8717, Eds. Mistry M, Leonardis A, Witkowski M and Melhuish C, Springer, 2014. Download final draft (pdf).
• Dennis LA, Fisher M and Winfield AFT (2015), Towards Verifiably Ethical Robot Behaviour, Proceedings of the 1st International Workshop on AI and Ethics, Austin, Texas, 2015. Download from University of Liverpool.

Alan Winfield also discusses the implementation of ethical robots on his blog.

Verifying Convoys

The work on convoys is part of the Verifiable Autonomy project (a joint project between the Universities of Liverpool, Sheffield and the West of England) and is currently unpublished. It is primarily being conducted by Owen McAree and Sandor Veres at the University of Sheffield and Maryam Kamali at the University of Liverpool.

Trustworthy Robotic Assistants

Trustworthy Robotic Assistants is a joint project between the Universities of Bristol, Hertfordshire and Liverpool.

The work on the interaction between model-checking, simulation and testing is in Dejanira Araiza-Illan, Clare Dixon, Kerstin Eder, Michael Fisher, Matt Webster and David Western, An Assurance-based Approach to Verification and Validation of Human–Robot Teams which has been submitted to IROS 2015.

Lego Robots

The Lego robot demonstrations were based on an activity taken into schools.

The Lego Rovers website discusses the activity including instructions for downloading and installing the code from github.

The code actually used in the demonstrations can be found (undocumented) on the EV3 branch of the MCAPL project.