research-article

Free access

Verifying autonomous systems

Authors:

Michael Fisher,

Louise Dennis,

Matt WebsterAuthors Info & Claims

Communications of the ACM, Volume 56, Issue 9

Pages 84 - 93

https://doi.org/10.1145/2494558

Published: 01 September 2013 Publication History

All formats PDF

Abstract

Exploring autonomous systems and the agents that control them.

References

[1]

Arkin, R. Governing lethal behavior: Embedding ethics in a hybrid deliberative/reactive robot architecture. Technical report GIT-GVU-07-11. Georgia Tech, 2007.

Google Scholar

[2]

Blackburn, P., van Benthem, J. and Wolter, F. eds. Handbook of Modal Logic. Elsevier, 2006.

Google Scholar

[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.

Google Scholar

[4]

Bond, A. and Gasser, L. eds. Readings in Distributed Artificial Intelligence. Morgan Kaufmann, 1988.

Digital Library

Google Scholar

[5]

Bordini, R., Dastani, M., Dix, J. and El Fallah-Seghrouchni, A. eds. Multi-Agent Programming: Languages, Platforms and Applications. Springer, 2005.

Google Scholar

[6]

Bordini, R., Dastani, M., Dix, J. and El Fallah-Seghrouchni, A. eds. Multi-Agent Programming: Languages, Tools and Applications. Springer, 2009.

Digital Library

Google Scholar

[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 (2006), 239-256.

Digital Library

Google Scholar

[8]

Bordini, R., Hübner, J. and Wooldridge, M. Programming Multi-agent Systems in <code>AgentSpeak</code> using Jason. Wiley, 2007.

Digital Library

Google Scholar

[9]

Bratman, M. Intentions, Plans, and Practical Reason. Harvard University Press, 1987.

Google Scholar

[10]

Brooks, R. A Robust layered control system for a mobile robot. IEEE J. Robotics and Automation 2, 10 (1986).

Crossref

Google Scholar

[11]

Civil Aviation Authority. CAP 393 Air Navigation: The Order and the Regulations; http://www.caa.co.uk/docs/33/CAP393.pdf, April 2010.

Google Scholar

[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.

Google Scholar

[13]

Clarke, E., Grumberg, O. and Peled, D. Model Checking. MIT Press, 1999.

Digital Library

Google Scholar

[14]

Cohen, P. and Levesque, H. Intention is choice with commitment. Artificial Intelligence 42 (1990), 213--261.

Digital Library

Google Scholar

[15]

Dennis, L. and Farwer, B. GWENDOLEN: A BDI Language for verifiable agents. In Workshop on Logic and the Simulation of Interaction and Reasoning. AISB, 2008.

Google Scholar

[16]

Dennis, L., Farwer, B., Bordini, R., Fisher, M. and Wooldridge, M. A common semantic basis for BDI languages. In Proc. 7^th Int. Workshop on Programming Multiagent Systems, LNAI 4908 (2008). Springer, 124--139.

Digital Library

Google Scholar

[17]

Dennis, L., Fisher, M., Lincoln, N., Lisitsa, A. and Veres, S. Verifying Practical Autonomous Systems. (Under review.)

Google Scholar

[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), 92--97.

Digital Library

Google Scholar

[19]

Dennis, L., Fisher, M., Webster, M. and Bordini, R. Model checking agent programming languages. Automated Software Engineering 19, 1 (2012), 5--63.

Digital Library

Google Scholar

[20]

Durfee, E., Lesser, V. and Corkill, D. Trends in cooperative distributed problem solving. IEEE Trans. Knowledge and Data Engineering 1, 1 (1989).

Digital Library

Google Scholar

[21]

Fisher, M. An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, 2011.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[23]

Gat, E., Bonnasso, R., Murphy, R. and Press, A. On three-layer architectures. Artificial Intelligence and Mobile Robots. AAAI Press, 1997, 195--210.

Digital Library

Google Scholar

[24]

Havelund, K. and Rosu, G. Monitoring programs using rewriting. In Proc. 16^th IEEE Int. Conf. Automated Software Engineering (2001). IEEE Computer Society, 135--143.

Digital Library

Google Scholar

[25]

Jones, C. Systematic Software Development Using VDM. Prentice Hall International, 1986.

Digital Library

Google Scholar

[26]

Java PathFinder. javapathfinder.sourceforge.net.

Google Scholar

[27]

Kitano, H. and Tadokoro, S. RoboCup rescue: A grand challenge for multiagent and intelligent systems. AI Magazine 22, 1 (2001), 39--52.

Google Scholar

[28]

Manna, Z. and Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, 1992.

Digital Library

Google Scholar

[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 (2007), 235--251.

Crossref

Google Scholar

[30]

Rao, A. <code>AgentSpeak</code>(L): BDI agents speak out in a logical computable language. In Proc. 7^th European Workshop on Modeling Autonomous Agents in a Multi-Agent World, LNCS 1038 (1996). Springer, 42--55.

Digital Library

Google Scholar

[31]

Rao, A. Decision procedures for propositional linear-time belief-desire-intention logics. Journal of Logic and Computation 8, 3 (1998), 293--342.

Google Scholar

[32]

Rao, A.S. and Georgeff, M.P. BDI agents: From theory to practice. In Proc. 1^st Int. Conf. Multi-Agent Systems (San Francisco, CA, 1995), 312--319.

Google Scholar

[33]

Rao, A.S. and Georgeff, M.P. An abstract architecture for rational agents. In Proc. 1^st Int. Conf. Knowledge Representation and Reasoning (1992), 439--449.

Google Scholar

[34]

Shoham, Y. Agent-oriented programming. Artificial Intelligence 60, 1 (1993), 51--92.

Digital Library

Google Scholar

[35]

United States of America State of Nevada Legislature. Nevada Revised Statutes Chapter 482A---Autonomous Vehicles, Mar. 2012.

Google Scholar

[36]

Visser, W., Havelund, K., Brat, G.P., Park, A. and Lerda, F. Model checking programs. Automated Software Engineering 10, 2 (2003), 203--232.

Digital Library

Google Scholar

[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, 228--242.

Digital Library

Google Scholar

[38]

Wooldridge, M. An Introduction to Multiagent Systems. Wiley, 2002.

Digital Library

Google Scholar

[39]

Wooldridge, M. and Rao, A., Eds. Foundations of Rational Agency. Kluwer Academic Publishers, 1999.

Crossref

Google Scholar

Cited By

View all

Yang YAgmon NAn BRicci AYeoh W(2023)Verifiably Safe Decision-Making for Autonomous SystemsProceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems10.5555/3545946.3599142(2973-2975)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.5555/3545946.3599142
Almpani SStefaneas PFrangos P(2023)Formalization of Ethical Decision MakingInternational Journal of Extreme Automation and Connectivity in Healthcare10.4018/IJEACH.3204885:1(1-13)Online publication date: 24-Mar-2023
https://dl.acm.org/doi/10.4018/IJEACH.320488
De Graaf MDragan AMalle BZiemke T(2021)Introduction to the Special Issue on Explainable Robotic SystemsACM Transactions on Human-Robot Interaction10.1145/346159710:3(1-4)Online publication date: 11-Jul-2021
https://dl.acm.org/doi/10.1145/3461597
Show More Cited By

Index Terms

Verifying autonomous systems

Recommendations

Verifying Autonomous Systems
Integrated Formal Methods
Abstract
This paper focuses on the work of the Autonomy and Verification Network (). In particular it will look at the use of model-checking to verify the choices made by a cognitive agent in control of decision ...
Agents and Autonomous Distributed Systems
ISADS '99: Proceedings of the The Fourth International Symposium on Autonomous Decentralized Systems

An Autonomous Distributed System (ADS) is a collection of autonomous entities, which realize a given function through mutual interactions. This concept of ADS allows the development of systems, which involves a large number of independent entities and ...
Verifying heterogeneous multi-agent programs
AAMAS '14: Proceedings of the 2014 international conference on Autonomous agents and multi-agent systems

We present a new approach to verifying heterogeneous multi-agent programs --- multi-agent systems in which the agents are implemented in different (BDI-based) agent programming languages. Our approach is based on meta-APL, a BDI-based agent programming ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Communications of the ACM Volume 56, Issue 9

September 2013

97 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/2500468

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2013

Published in CACM Volume 56, Issue 9

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Popular
Refereed

Funding Sources

Engineering and Physical Sciences Research Council
ERDF
NWDA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
9,965
Total Downloads

Downloads (Last 12 months)293
Downloads (Last 6 weeks)47

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Yang YAgmon NAn BRicci AYeoh W(2023)Verifiably Safe Decision-Making for Autonomous SystemsProceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems10.5555/3545946.3599142(2973-2975)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.5555/3545946.3599142
Almpani SStefaneas PFrangos P(2023)Formalization of Ethical Decision MakingInternational Journal of Extreme Automation and Connectivity in Healthcare10.4018/IJEACH.3204885:1(1-13)Online publication date: 24-Mar-2023
https://dl.acm.org/doi/10.4018/IJEACH.320488
De Graaf MDragan AMalle BZiemke T(2021)Introduction to the Special Issue on Explainable Robotic SystemsACM Transactions on Human-Robot Interaction10.1145/346159710:3(1-4)Online publication date: 11-Jul-2021
https://dl.acm.org/doi/10.1145/3461597
Fisher MMascardi VRozier KSchlingloff BWinikoff MYorke-Smith N(2021)Towards a framework for certification of reliable autonomous systemsAutonomous Agents and Multi-Agent Systems10.1007/s10458-020-09487-235:1Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10458-020-09487-2
Vistbakka ITroubitsyna E(2021)Modelling resilient collaborative multi-agent systemsComputing10.1007/s00607-020-00861-2103:4(535-557)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s00607-020-00861-2
Zhao XSalako KStrigini LRobu VFlynn D(2020)Assessing safety-critical systems from operational testingInformation and Software Technology10.1016/j.infsof.2020.106393128:COnline publication date: 1-Dec-2020
https://dl.acm.org/doi/10.1016/j.infsof.2020.106393
Bordini REl Fallah Seghrouchni AHindriks KLogan BRicci A(2020)Agent programming in the cognitive eraAutonomous Agents and Multi-Agent Systems10.1007/s10458-020-09453-y34:2Online publication date: 12-May-2020
https://dl.acm.org/doi/10.1007/s10458-020-09453-y
Fraser DGiaquinta RHoffmann RIreland MMiller ANorman G(2020)Collaborative models for autonomous systems controller synthesisFormal Aspects of Computing10.1007/s00165-020-00508-132:2-3(157-186)Online publication date: 1-Jul-2020
https://dl.acm.org/doi/10.1007/s00165-020-00508-1
Torres MGiacalone JAbou Faysal J(2020)A Case Study on Formally Validating Motion Rules for Autonomous CarsSoftware Engineering and Formal Methods. SEFM 2020 Collocated Workshops10.1007/978-3-030-67220-1_18(233-248)Online publication date: 14-Sep-2020
https://dl.acm.org/doi/10.1007/978-3-030-67220-1_18
Dennis LSlavkovik M(2020)Model-Checking Information Diffusion in Social Networks with PRISMMulti-Agent Systems and Agreement Technologies10.1007/978-3-030-66412-1_30(475-492)Online publication date: 22-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-66412-1_30
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Digital Edition

View this article in digital edition.

Digital Edition

Magazine Site

View this article on the magazine site (external)

Magazine Site

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations