concerning their seriousness. Again,
these measures and probabilities
should be incorporated into the properties verified.
Similarly, there are important aspects of truly autonomous behavior,
such as the ability to plan and learn
that we have not considered in any
detail. We are interested in exploring how an agent might reason about
new plans, for instance, to ensure
their execution did not violate any
important properties and so provide
guarantees about the agents overall
behavior even in the face of changing
It is also important to assess if, and
how, other approaches to the formalization of autonomous behaviors, for
example, Arkin, 1 can be involved in our
Toward Certification. Certification
can be seen as the process of negotiating with a certain legal authority in order to convince them that relevant safety requirements have been explored
and mitigated in an appropriate way.
As part of this process, various items
of evidence are provided to advance
the applicant’s safety argument. This
approach is widely used for the certification of real systems, from aircraft to
safety critical software.
Clearly, we are mainly concerned
with the certification of autonomous
systems. As noted, systems might
generally be analyzed with respect to
the question, “Is it safe?” If there is
a human involved at some point, for
example, a pilot or controller, then
some view must be taken on whether
the human acts to preserve safety or
not. For example, within aircraft certification arguments, it is usually assumed that a pilot, given appropriate
information and capabilities, will act
to preserve the aircraft’s safety. Yet
in a safety analysis, we rarely go any
further. Essentially, the human is assumed to be benevolent.
Our approach provides a mecha-
nism for analyzing the agent choices
in the case of autonomous systems.
Thus, while a standard safety argu-
ment might skip over human choices,
assuming the pilot/driver/operator
will endeavor to remain safe, we can
formally verify the agent indeed tries
its best to remain safe. In this way, our
approach allows wider analysis—while
the intentions and choices of a pilot/
driver/operator must be assumed to
be good, we can actually examine the
intentions and choices of an autono-
mous system in detail.
Acknowledgments. This work was
partially supported by EPSRC, while
the Virtual Engineering Centre is a
University of Liverpool project partially
supported by both NWDA and ERDF.
We are grateful to our many collaborators, but particularly Rafael Bordini,
Neil Cameron, Mike Jump, Alexei Lisitsa, Nick Lincoln, Bertie Müller, and
1. arkin, r. governing lethal behavior: embedding ethics
in a hybrid deliberative/reactive robot architecture.
technical report gIt-gVu-07-11. georgia tech, 2007.
2. blackburn, P., van benthem, J. and wolter, f. eds.
Handbook of Modal Logic. elsevier, 2006.
3. bonasso, P., firby, J., gat, e., kortenkamp, D., miller,
D. and Slack, m. experiences with an architecture for
intelligent, reactive agents. J. Exp. Theor. Artif. Intel.
9, 23 (1997), 237–256.
4. bond, a. and gasser, l. eds. Readings in Distributed
Artificial Intelligence. morgan kaufmann, 1988.
5. bordini, r., Dastani, m., Dix, J. and el fallah-Seghrouchni, a. eds. Multi-Agent Programming:
Languages, Platforms and Applications. Springer,
6. bordini, r., Dastani, m., Dix, J. and el fallah-Seghrouchni, a. eds. Multi-Agent Programming:
Languages, Tools and Applications. Springer, 2009.
7. bordini, r., fisher, m., Visser, w. and wooldridge, m.
Verifying multi-agent programs by model checking. J.
Autonomous Agents and Multi-Agent Systems 12, 2
8. bordini, r., hübner, J. and wooldridge, m.
Programming Multi-agent Systems in AgentSpeak
using Jason. wiley, 2007.
9. bratman, m. Intentions, Plans, and Practical Reason.
harvard university Press, 1987.
10. brooks, r. a robust layered control system for a
mobile robot. IEEE J. Robotics and Automation 2, 10
11. Civil aviation authority. CaP 393 air navigation: the
order and the regulations; http://www.caa.co.uk/
docs/33/CaP393.pdf, april 2010.
12. Civil aviation authority. CaP 722 unmanned aircraft
System operations in uk airspace—guidance; http://
www.caa.co.uk/docs/33/CaP722.pdf, april 2010.
13. Clarke, e., grumberg, o. and Peled, D. model Checking.
mIt Press, 1999.
14. Cohen, P. and levesque, h. Intention is choice with
commitment. Artificial Intelligence 42 (1990),
15. Dennis, l. and farwer, b. G WENDOLEN: a bDI language
for verifiable agents. In Workshop on Logic and the
Simulation of Interaction and Reasoning. aISb, 2008.
16. Dennis, l., far wer, b., bordini, r., fisher, m. and
wooldridge, m. a common semantic basis for bDI
languages. In Proc. 7th Int. Workshop on Programming
Multiagent Systems, lnaI 4908 (2008). Springer,
17. Dennis, l., fisher, m., lincoln, n., lisitsa, a. and Veres,
S. Verifying Practical autonomous Systems. (under
18. Dennis, l., fisher, m., lisitsa, a., lincoln, n. and Veres,
S. satellite control using rational agent programming.
IEEE Intelligent Systems 25, 3 (may/June 2010),
19. Dennis, l., fisher, m., webster, m. and bordini, r. model
checking agent programming languages. Automated
Software Engineering 19, 1 (2012), 5–63.
20. Durfee, e., lesser, V. and Corkill, D. trends in
cooperative distributed problem solving. IEEE Trans.
Knowledge and Data Engineering 1, 1 (1989).
21. fisher, m. An Introduction to Practical Formal
Methods Using Temporal Logic. wiley, 2011.
22. franklin, S. and graesser, a. Is it an agent, or just
a program? a taxonomy for autonomous agents.
Intelligent Agents III, lnCS 1193 (1996), 21–35.
23. gat, e., bonnasso, r., murphy, r. and Press, a. on
three-layer architectures. Artificial Intelligence and
Mobile Robots. aaaI Press, 1997, 195–210.
24. havelund, k. and rosu, g. monitoring programs using
rewriting. In Proc. 16th IEEE Int. Conf. Automated
Software Engineering (2001). Ieee Computer Society,
25. Jones, C. Systematic Software Development Using
VDM. Prentice hall International, 1986.
26. Java Pathfinder. javapathfinder.sourceforge.net.
27. kitano, h. and tadokoro, S. roboCup rescue: a grand
challenge for multiagent and intelligent systems. AI
Magazine 22, 1 (2001), 39–52.
28. manna, Z. and Pnueli, a. The Temporal Logic of
Reactive and Concurrent Systems: Specification.
29. raimondi, f. and lomuscio, a. automatic verification
of multi-agent systems by model checking via ordered
binary decision diagrams. Journal of Applied Logic 5, 2
30. rao, a. AgentSpeak(l): bDI agents speak out in a
logical computable language. In Proc. 7th European
Workshop on Modeling Autonomous Agents in a Multi-Agent World, LNCS 1038 (1996). Springer, 42–55.
31. rao, a. Decision procedures for propositional linear-time belief-desire-intention logics. Journal of Logic
and Computation 8, 3 (1998), 293–342.
32. rao, a.S. and georgeff, m.P. bDI agents: from theory
to practice. In Proc. 1st Int. Conf. Multi-Agent Systems
(San francisco, Ca, 1995), 312–319.
33. rao, a.S. and georgeff, m.P. an abstract architecture
for rational agents. In Proc. 1st Int. Conf. Knowledge
Representation and Reasoning (1992), 439–449.
34. Shoham, y. agent-oriented programming. Artificial
Intelligence 60, 1 (1993), 51–92.
35. united States of america State of nevada legislature.
nevada revised Statutes Chapter 482a—autonomous
Vehicles, mar. 2012.
36. Visser, w., havelund, k., brat, g.P., Park, a. and lerda,
f. model checking programs. Automated Software
Engineering 10, 2 (2003), 203–232.
37. webster, m., fisher, m., Cameron, n. and Jump,
m. formal methods and the certification of
autonomous unmanned aircraft systems. In Proc.
30th International Conference on Computer Safety,
Reliability and Security. LNCS 6894 (2011). Springer,
38. wooldridge, m. An Introduction to Multiagent
Systems. wiley, 2002.
39. wooldridge, m. and rao, a., eds. Foundations of
Rational Agency. kluwer academic Publishers, 1999.
Michael Fisher ( firstname.lastname@example.org) is a professor
in the Department of Computer Science at the university
of liverpool, u.k.
Louise Dennis ( email@example.com) is a research
associate in the Department of Computer Science at the
university of liverpool, u.k.
Matt Webster ( firstname.lastname@example.org) is a research
associate in the Virtual engineering Centre at Daresbury
laboratory warrington, u.k.
© aCm 0001-0782/13/09 $15.00