The Model Checking Agent Programming Language (MCAPL) framework is a suite of tools for building interpreters for agent programming languages and model checking programs executing in those interpreters. It consists of the AIL toolkit for building interpreters for rational agent programming languages (BDI languages) and the Agent Java PathFinder (AJPF) model checker. AJPF extends the JavaPathfinder model checker to prove Linear-time Temporal Logic (LTL) properties of BDI agents. This distribution also contains a number of programming languages implemented in the AIL. Chief among these are Gwendolen, the EASS variant of Gwendolen that can be used to program hybrid autonomous systems and GOAL.
Publications
Manual (including tutorials)
Key Descriptions
- Louise A. Dennis and Michael Fisher. Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines. Cambridge University Press. 2023.
- Louise A. Dennis. The MCAPL Framework including the Agent Infrastructure Layer and Agent Java Pathfinder. Journal of Open Source Software, 3(24), 617, 2018. DOI: 10.31105/joss.00617
- Louise A. Dennis. Gwendolen Semantics: 2017 . University of Liverpool, Computer Science, Technical Report ULCS-17-001.
- Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa, Sandor M. Veres. Practical Verification of Decision-Making in Agent-Based Autonomous Systems . Automated Software Engineering 23(3), 305-359, 2016. DOI: 10.1007/s10515-014-0168-9.
Descriptions of (Aspects of) the MCAPL Framework, AJPF, Gwendolen and their Usage
- Peter Stringer, Rafael C. Cardoso, Clare Dixon, Michael Fisher, and Louise A. Dennis (2023). Adaptive Cognitive Agents: Updating Action Descriptions and Plans. In: Malvone, V., Murano, A. (eds) Multi-Agent Systems. EUMAS 2023. Lecture Notes in Computer Science, vol 14282. Springer, Cham.
- Peter Stringer, Rafael C. Cardoso, Clare Dixon, Michael Fisher, and Louise A. Dennis. 2023. Updating Action Descriptions and Plans for Cognitive Agents. In Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems (AAMAS ‘23). International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC, 2370–2372.
- Louise A. Dennis. Verifying Autonomous Systems. In: ter Beek, M.H., Monahan, R. (eds) Integrated Formal Methods. IFM 2022. Lecture Notes in Computer Science, vol 13274. Springer, Cham.
- Stringer, P., Cardoso, R.C., Dixon, C., Dennis, L.A. (2022). Implementing Durative Actions with Failure Detection in GWENDOLEN. In: Alechina, N., Baldoni, M., Logan, B. (eds) Engineering Multi-Agent Systems. EMAS 2021. Lecture Notes in Computer Science, vol 13190. Springer, Cham.
- Angelo Ferrando, Louise A. Dennis, Rafael C. Cardoso, Michael Fisher, Davide Ancona and Viviana Mascardi. Towards a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems. ACM Transactions on Software Engineering and Methodology. 30(4). 2021.
- Rafael C. Cardoso, Louise A. Dennis and Michael Fisher. Plan Library Reconfigurability in BDI Agents. In: Dennis L., Bordini R., Lespérance Y. (eds) Engineering Multi-Agent Systems. EMAS 2019. Lecture Notes in Computer Science, vol 12058. Springer, Cham
- Vincent Koeman, Louise A. Dennis, Matt Webster, Michael Fisher and Koen Hindriks. The “Why did you do that?” Button: Answering Why-questions for end users of Robotic Systems. In: Dennis L., Bordini R., Lespérance Y. (eds) Engineering Multi-Agent Systems. EMAS 2019. Lecture Notes in Computer Science, vol 12058. Springer, Cham
- Louise A. Dennis, Michael Fisher, and Matt Webster. Two-stage agent program verification. Journal of Logic and Computation, Volume 28, issue 3, pp. 499-523, 2018. DOI: 10.1093/logcom/exv002.
- Michael Fisher, Louise A. Dennis, Matthew P. Webster. Verifying Autonomous Systems. Communications of the ACM 56(9): 85-93 (2013).
- Louise A. Dennis, Michael Fisher, Matthew P. Webster and Rafael H. Bordini. Model checking agent programming languages , Automated Software Engineering, 2011
Publications that use Agent Java Pathfinder
- Mengwei Xu, Louise A. Dennis, and Mustafa A. Mustafa. Safeguard Privacy for Minimal Data Collection with Trustworthy Autonomous Agents. In Proc. of the 23rd International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2024), Auckland, New Zealand, May 6 – 10, 2024, IFAAMAS.
- Gleifer Vas Alves, Louise Dennis, Lucas Fernandes, and Michael Fisher. Reliable Decision-Making in Autonomous Vehicles. In: Leitner A., Watzenig D., Ibanez-Guzman J. (eds) Validation and Verification of Automated Systems. 2020. Springer. DOI: 10.1007/978-3-030-14628-3_10
- Paul Bremner, Louise A. Dennis, Michael Fisher and Alan F. Winfield. On Proactive, Transparent and Verifiable Ethical Reasoning for Robots. Proceedings of the IEEE. Special Issue on Machine Ethics: The Design and Governance of Ethical AI and Autonomous Systems. 107(3), pp:541-561. DOI: 10.1109/JPROC.2019.2898267
- Maryam Kamali, Louise A. Dennis, Owen McAree, Michael Fisher and Sandor M. Veres. Formal verification of autonomous vehicle platooning. Science of Computer Programming, 148, pp. 88-106, 2017. DOI: 10.1016/j.scico.2017.05.006.
- Louise A. Dennis, Michael Fisher, Marija Slavkovik, and Matt Webster. Formal Verification of Ethical Choices in Autonomous Systems Robotics and Autonomous Systems. DOI:10.1016/j.robot.2015.11.012.
- Louise A. Dennis, Michael Fisher, and Alan Winfield. Towards Verifiably Ethical Robot Behaviour. Proceedings of the AAAI Workshop on Artificial Intelligence and Ethics (1st International Workshop on AI and Ethics).
Publications that use the Gwendolen Programming language
- Mengwei Xu, Louise A. Dennis, and Mustafa A. Mustafa. Safeguard Privacy for Minimal Data Collection with Trustworthy Autonomous Agents. In Proc. of the 23rd International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2024), Auckland, New Zealand, May 6 – 10, 2024, IFAAMAS.
- Gleifer Vas Alves, Louise Dennis, Lucas Fernandes, and Michael Fisher. Reliable Decision-Making in Autonomous Vehicles. In: Leitner A., Watzenig D., Ibanez-Guzman J. (eds) Validation and Verification of Automated Systems. 2020. Springer. DOI: 10.1007/978-3-030-14628-3_10
- Jonathan M. Aitken, Affan Shaukat, Elisa Cucco, Louise A. Dennis, Sandor M. Veres, Yang Gao, Michael Fisher, Jeffrey A. Kuo, Thomas Robinson, Paul E. Mort. Autonomous Nuclear Waste Management. IEEE Intelligent Systems 33(6), 2018. DOI: 10.1109/MIS.2018.111144814
- Gleifer Alves, Louise Dennis and Michael Fisher. Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent. Workshop on Verification and Validation of Autonomous Systems, pp. 26-28, 2018.
- Maryam Kamali, Louise A. Dennis, Owen McAree, Michael Fisher and Sandor M. Veres. Formal verification of autonomous vehicle platooning. Science of Computer Programming, 148, pp. 88-106, 2017. DOI: 10.1016/j.scico.2017.05.006.
- Louise A. Dennis, Jonathan M. Aitken, Joe Collenette, Elisa Cucco, Maryam Kamali, Owen McAree, Affan Shaukat, Katie Atkinson, Yang Gao, Sandor Veres, and Michael Fisher. Agent-based Autonomous Systems and Abstraction Engines: Theory meets Practice. Towards Autonomous Robotic Systems, 17th Annual Conference (TAROS 2016), 2016.
Links