Verifying Agent-Based Autonomous Systems

While the idea of “Autonomous Systems” is both appealing and powerful, actually developing such systems to be reliable is far from simple. An important aspect is to be able to verify the truly autonomous decision-making that forms the core of many such systems. In this tutorial, we will describe a practical approach to the formal verification of decision making in agent-based autonomous systems. This will incorporate material on autonomous systems, agent programming languages, formal verification, agent model-checking, and the practical analysis of autonomous systems.

The tutorial will cover the use of model-checking to formally verify a rational agent at the heart of an autonomous system. This will include presentations on wider topics such as logic-based agent programming in the BDI (Beliefs-Desires-Intentions) paradigm and approaches to formal verification, particularly model-checking, before discussing the application of model-checking to agent systems and then agent-based autonomy. It will include discussion of several case studies and an exploration of some of the unusual requirements introduced by this area in which decision-making is required to take account of safe and ethical activities as well as purely operational constraints. Although there is no practical component to the tutorial, the software is open source and online tutorials are available for those who are interested in taking this further.

Tutorial Programme

  1. 14:00 - 14:20 Autonomous Systems
    1. motivation architectures and applications
    2. hybrid architectures and rational agents
    3. flexibility, applications, and potential
  2. 14:20 - 15:05 Agent Programming Languages
    1. BDI languages: beyond Prolog
    2. principles, some varieties
    3. operational semantics
    4. Gwendolen, examples
  3. 15:05 - 15:50 Formal Verification
    1. why bother?
    2. temporal logics
    3. verification, formal verification, different varieties
    4. model-checking, Buchi Automata
    5. program model-checking, JPF
  4. 15:50 - 16:15 Coffee Break
  5. 16:15 - 17:00 MCAPL/AJPF
    1. practical verification: the MCAPL interface
    2. running agent programs in the AIL
    3. (A)JPF system
    4. constructing Environments for Verification
    5. simple examples
  6. 17:00 - 17:30 Verification in Autonomous Systems
    1. where does verification fit in?
    2. a selection of examples, including: UAV verification and verifying ethical decisions
  7. 17:30 - 17:45 Future
    1. law, ethics, learning, abstractions, other model-checkers

Tutorial Slides

References/Further Reading

R. H. Bordini, M. Fisher, W. Visser, and M. Wooldridge. Model Checking Rational Agents. IEEE Intelligent Systems 19(5):46-52, 2004.

M. Fisher, M. P. Singh, D. F. Spears, and M. Wooldridge. Logic-Based Agent Verification. Special Issue of the Journal of Applied Logic 5(2):193-195, 2007

R. H. Bordini, M. Fisher, W. Visser, and M. Wooldridge. Verifying Multi-agent Programs by Model Checking. Autonomous Agents and Multi-Agent Systems 12(2):239-256, 2006.

L. A. Dennis, M. Fisher, M. P. Webster, and R. H. Bordini. Model Checking Agent Programming Languages. Automated Software Engineering 19(1):5-63, 2012.

L. A. Dennis, M. Fisher, N. Lincoln, A. Lisitsa, and S. Veres. Practical Verification of Decision-Making in Agent-Based Autonomous Systems. Automated Software Engineering 23(3:305-359, 2016.

L. A. Dennis, M. Fisher, and A. F. T. Winfield. Towards Verifiably Ethical Robot Behaviour. In AAAI-15 Workshop on AI and Ethics, 2015.

L. A. Dennis, M. Fisher, M. Slavkovik and M. P. Webster. Formal Verification of Ethical Choices in Autonomous Systems. Robotics and Autonomous Systems 77:1--14, 2016.

M. Fisher, L. A. Dennis and M. Webster. Verifying Autonomous Systems. Communications of the ACM 56(9):84-93, 2013.

M. Kamali, L. A. Dennis, O.McAree, M. Fisher and S. M. Veres. Formal Verification of Autonomous Vehicle Platooning. Science of Computer Programming 148:88-106. 2017.

M. Webster, N. Cameron, M. Jump, and M. Fisher. Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation. Journal of Aerospace Information Systems 11(5):258-279, 2014.