\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n

\n generated by\n \n $\"bibbase.org\"\n$ \n \n

\n \n\n

\n\n

\n \n Group by\n \n \n
- \n Year\n
- \n Author\n
- \n Type\n
- \n Keyword\n
- \n Downloads\n
\n
\n \n \n \n \n
- \n \n Expand/Collapse All\n \n
- \n \n Download BibTeX\n \n
- \n \n RSS Feed\n \n
\n

\n\n\n

\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n

\n JavaScript\n (easiest)\n

\n            <script src=\"https://bibbase.org/show?bib=https%3A%2F%2Fautonomy-and-verification.github.io%2Fpubs.bib&group0=year&jsonp=1&jsonp=1\"></script>\n

\n\n PHP\n

\n            <?php\n            $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Fautonomy-and-verification.github.io%2Fpubs.bib&group0=year&jsonp=1\");\n            print_r($contents);\n            ?>\n

\n\n iFrame\n (not recommended)\n

\n            <iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Fautonomy-and-verification.github.io%2Fpubs.bib&group0=year&jsonp=1\"></iframe>\n

\n\n

\n For more details see the documention.\n

\n\n

\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n

\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

renew the authorization for BibBase on Mendeley, and
update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n

\n\n

\n \n \n Fix it now\n

\n\n

\n\n\n

\n \n \n

\n \n 2025\n \n \n (3)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n Autonomy and Safety Assurance in the Early Development of Robotics and Autonomous Systems.\n \n \n \n \n\n\n \n Abeywickrama, D. B.; Fisher, M.; Wheeler, F.; and Dennis, L.\n\n\n \n\n\n\n 2025.\n [CRADLE]\n\n\n\n
\n\n\n\n \n \n $\"Autonomy$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@misc{abeywickrama2025autonomysafetyassuranceearly,\n      title={Autonomy and Safety Assurance in the Early Development of Robotics and Autonomous Systems}, \n      author={Dhaminda B. Abeywickrama and Michael Fisher and Frederic Wheeler and Louise Dennis},\n      year={2025},\n      eprint={2501.18448},\n      archivePrefix={arXiv},\n      primaryClass={cs.RO},\n\tnote={[<span class="cradle">CRADLE</span>]},\n      url={https://arxiv.org/abs/2501.18448}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n .\n \n \n \n \n\n\n \n Wright, T.; Dennis, L. A.; Woodcock, J.; and Foster, S.\n\n\n \n\n\n\n Formal Verification of BDI Agents, pages 302–326. Hinchey, M.; and Steffen, B., editor(s). Springer Nature Switzerland, Cham, 2025.\n [TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n \n $\"Formal$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InBook{Wright2025,\nauthor="Wright, Thomas and Dennis, Louise A. and Woodcock, Jim and Foster, Simon",\neditor="Hinchey, Mike and Steffen, Bernhard",\ntitle={Formal Verification of BDI Agents},\nbooktitle={The Combined Power of Research, Education, and Dissemination: Essays Dedicated to Tiziana Margaria on the Occasion of Her 60th Birthday},\nyear="2025",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="302--326",\nisbn="978-3-031-73887-6",\ndoi="10.1007/978-3-031-73887-6_20",\nnote={[<span class="tas_vn">TAS Verifiability Node</span>]},\nurl="https://doi.org/10.1007/978-3-031-73887-6_20"\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n An Expedited BDI Agent Architecture: Improving the Responsiveness of Agent-based Autonomous Systems for Handling Critical Situations.\n \n \n \n\n\n \n Becker, L. B.; de Oliveira Silvestre , I.; Hubner, J. F.; and Fisher, M.\n\n\n \n\n\n\n Robotics and Autonomous Systems, 186: 104917. 2025.\n [RAEng]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{BECKER2025104917,\ntitle = "{An Expedited BDI Agent Architecture: Improving the Responsiveness of\n         Agent-based Autonomous Systems for Handling Critical Situations}",\njournal = {Robotics and Autonomous Systems},\nvolume = {186},\npages = {104917},\nyear = {2025},\nissn = {0921-8890},\ndoi = {10.1016/j.robot.2025.104917},\nauthor = {Leandro Buss Becker and Iago {de Oliveira Silvestre} and Jomi Fred Hubner and Michael Fisher},\nnote={[<span class="raeng">RAEng</span>]}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2024\n \n \n (10)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n Security-Minded Verification of Cooperative Awareness Messages.\n \n \n \n\n\n \n Farrell, M.; Bradbury, M.; Cardoso, R. C.; Fisher, M.; Dennis, L. A.; Dixon, C.; Sheik, A. T.; Yuan, H.; and Maple, C.\n\n\n \n\n\n\n IEEE Transactions on Dependable and Secure Computing, 21(4): 4048-4065. 2024.\n [TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n

@ARTICLE{10368348,\n  author={Farrell, Marie and Bradbury, Matthew and Cardoso, Rafael C. and Fisher, Michael and Dennis, Louise A. and Dixon, Clare and Sheik, Al Tariq and Yuan, Hu and Maple, Carsten},\n  journal={IEEE Transactions on Dependable and Secure Computing},\n  title="{Security-Minded Verification of Cooperative Awareness Messages}",\n  year={2024},\n  volume={21},\n  number={4},\n  pages={4048-4065},\n  keywords={Security;Protocols;Runtime;Safety;Monitoring;Computer crime;Threat modeling;Verification;security;safety;threat modeling;connected autonomous vehicles;cooperative awareness messages},\n  doi={10.1109/TDSC.2023.3345543},\nnote={[<span class="tas_vn">TAS Verifiability Node</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Interlinked Computing in 2040: Safety, Truth, Ownership, and Accountability.\n \n \n \n\n\n \n Weir, C.; Dyson, A.; Jogunola, O.; Dennis, L.; and Paxton-Fear, K.\n\n\n \n\n\n\n Computer, 57(1): 59-68. 2024.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@ARTICLE{10380243,\n  author={Weir, Charles and Dyson, Anna and Jogunola, Olamide and Dennis, Louise and Paxton-Fear, Katie},\n  journal={Computer}, \n  title={Interlinked Computing in 2040: Safety, Truth, Ownership, and Accountability}, \n  year={2024},\n  volume={57},\n  number={1},\n  pages={59-68},\n  doi={10.1109/MC.2023.3318377}}\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Parameterized Verification of Leader/Follower Systems via Arithmetic Constraints.\n \n \n \n\n\n \n Kourtis, G.; Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n IEEE Transactions on Software Engineering, 50(9): 2458-2471. 2024.\n [TAS Verifiability Node, S4]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n

@ARTICLE{10632563,\n  author={Kourtis, Georgios and Dixon, Clare and Fisher, Michael},\n  journal={IEEE Transactions on Software Engineering}, \n  title={Parameterized Verification of Leader/Follower Systems via Arithmetic Constraints}, \n  year={2024},\n  volume={50},\n  number={9},\n  pages={2458-2471},\n  keywords={Arithmetic;Automata;Logic;Control systems;Polynomials;Formal verification;Europe;Formal methods;parameterized verification;distributed systems;arithmetic constraints},\n  doi={10.1109/TSE.2024.3440587},\nnote={[<span class="tas_vn">TAS Verifiability Node</span>, <span class="s4">S4</span>]}}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Trustworthy ROS Software Architecture for Autonomous Drones Missions: From RoboChart Modelling to ROS Implementation.\n \n \n \n\n\n \n Shaukat, N.; Dubey, S.; Kaddouh, B.; Blight, A.; Mudrich, L.; Ribeiro, P.; Araujo, H.; Richardson, R.; Dennis, L.; Cavalcanti, A.; and Mousavi, M.\n\n\n \n\n\n\n In 2024 20th IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications (MESA), pages 1-7, 2024. \n [TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n

@INPROCEEDINGS{10704818,\n  author={Shaukat, Nabil and Dubey, Shival and Kaddouh, Bilal and Blight, Andy and Mudrich, Lenka and Ribeiro, Pedro and Araujo, Hugo and Richardson, Rob and Dennis, Louise and Cavalcanti, Ana and Mousavi, Mohammad},\n  booktitle={2024 20th IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications (MESA)}, \n  title={Trustworthy ROS Software Architecture for Autonomous Drones Missions: From RoboChart Modelling to ROS Implementation}, \n  year={2024},\n  volume={},\n  number={},\n  pages={1-7},\nnote={[<span class="tas_vn">TAS Verifiability Node</span>]},\n  keywords={Mechatronics;Software architecture;Surveillance;Computer architecture;Software;Personnel;Formal specifications;Robots;Testing;Drones;robochart;ros;drone;firefighting;software;robots;trustworthy architecture;trustworthy},\n  doi={10.1109/MESA61532.2024.10704818}}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Applying Ethical Decision Making on Space Missions.\n \n \n \n\n\n \n Kolker, S.; Dennis, L.; Pereira, R. F.; and Xu, M.\n\n\n \n\n\n\n In 2024 IEEE Space Computing Conference (SCC), pages 136-138, 2024. \n [TAS Verifiability Node, Computational Agent Responsibility]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n

@INPROCEEDINGS{10794849,\n  author={Kolker, Simon and Dennis, Louise and Pereira, Ramon Fraga and Xu, Mengwei},\n  booktitle={2024 IEEE Space Computing Conference (SCC)}, \n  title={Applying Ethical Decision Making on Space Missions}, \n  year={2024},\n  volume={},\n  number={},\n  pages={136-138},\nnote={[<span class="tas_vn">TAS Verifiability Node</span>, <span class="car">Computational Agent Responsibility</span>]},\n  keywords={Ethics;Mars;Uncertainty;Autonomous systems;Space missions;Decision making;Relays;Ethical AI;Space missions;Decision Making},\n  doi={10.1109/SCC61854.2024.00022}}\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving.\n \n \n \n \n\n\n \n Quan, X.; Valentino, M.; Dennis, L. A.; and Freitas, A.\n\n\n \n\n\n\n In Al-Onaizan, Y.; Bansal, M.; and Chen, Y., editor(s), Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 2933–2958, Miami, Florida, USA, November 2024. Association for Computational Linguistics\n \n\n\n\n
\n\n\n\n \n \n $\"Verification$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{quan-etal-2024-verification,\n    title = "Verification and Refinement of Natural Language Explanations through {LLM}-Symbolic Theorem Proving",\n    author = "Quan, Xin  and\n      Valentino, Marco  and\n      Dennis, Louise A.  and\n      Freitas, Andre",\n    editor = "Al-Onaizan, Yaser  and\n      Bansal, Mohit  and\n      Chen, Yun-Nung",\n    booktitle = "Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing",\n    month = nov,\n    year = "2024",\n    address = "Miami, Florida, USA",\n    publisher = "Association for Computational Linguistics",\n    url = "https://aclanthology.org/2024.emnlp-main.172",\n    pages = "2933--2958",\n    abstract = "Natural language explanations represent a proxy for evaluating explanation-based and multi-step Natural Language Inference (NLI) models. However, assessing the validity of explanations for NLI is challenging as it typically involves the crowd-sourcing of apposite datasets, a process that is time-consuming and prone to logical errors. To address existing limitations, this paper investigates the verification and refinement of natural language explanations through the integration of Large Language Models (LLMs) and Theorem Provers (TPs). Specifically, we present a neuro-symbolic framework, named Explanation-Refiner, that integrates TPs with LLMs to generate and formalise explanatory sentences and suggest potential inference strategies for NLI. In turn, the TP is employed to provide formal guarantees on the logical validity of the explanations and to generate feedback for subsequent improvements. We demonstrate how Explanation-Refiner can be jointly used to evaluate explanatory reasoning, autoformalisation, and error correction mechanisms of state-of-the-art LLMs as well as to automatically enhance the quality of explanations of variable complexity in different domains.",\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement.\n \n \n \n \n\n\n \n Quan, X.; Valentino, M.; Dennis, L.; and Freitas, A.\n\n\n \n\n\n\n In Graham, Y.; and Purver, M., editor(s), Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers), pages 1–22, St. Julian's, Malta, March 2024. Association for Computational Linguistics\n \n\n\n\n
\n\n\n\n \n \n $\"Enhancing$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{quan-etal-2024-enhancing,\n    title = "Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement",\n    author = "Quan, Xin  and\n      Valentino, Marco  and\n      Dennis, Louise  and\n      Freitas, Andre",\n    editor = "Graham, Yvette  and\n      Purver, Matthew",\n    booktitle = "Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers)",\n    month = mar,\n    year = "2024",\n    address = "St. Julian{'}s, Malta",\n    publisher = "Association for Computational Linguistics",\n    url = "https://aclanthology.org/2024.eacl-long.1",\n    pages = "1--22",\n    abstract = "An increasing amount of research in Natural Language Inference (NLI) focuses on the application and evaluation of Large Language Models (LLMs) and their reasoning capabilities. Despite their success, however, LLMs are still prone to factual errors and inconsistencies in their explanations, offering limited control and interpretability for inference in complex domains. In this paper, we focus on ethical NLI, investigating how hybrid neuro-symbolic techniques can enhance the logical validity and alignment of ethical explanations produced by LLMs. Specifically, we present an abductive-deductive framework named Logic-Explainer, which integrates LLMs with an external backward-chaining solver to refine step-wise natural language explanations and jointly verify their correctness, reduce incompleteness and minimise redundancy. An extensive empirical analysis demonstrates that Logic-Explainer can improve explanations generated via in-context learning methods and Chain-of-Thought (CoT) on challenging ethical NLI tasks, while, at the same time, producing formal proofs describing and supporting models{'} reasoning. As ethical NLI requires commonsense reasoning to identify underlying moral violations, our results suggest the effectiveness of neuro-symbolic methods for multi-step NLI more broadly, opening new opportunities to enhance the logical consistency, reliability, and alignment of LLMs.",\n\t}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Safeguard Privacy for Minimal Data Collection with Trustworthy Autonomous Agents.\n \n \n \n\n\n \n Xu, M.; Dennis, L. A.; and Mustafa, M. A.\n\n\n \n\n\n\n In Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, of AAMAS '24, pages 1966â€“1974, Richland, SC, 2024. International Foundation for Autonomous Agents and Multiagent Systems\n [TAS Verifiability Node, Computational Agent Responsibility]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n

@inproceedings{10.5555/3635637.3663060, author = {Xu, Mengwei and Dennis, Louise A. and Mustafa, Mustafa A.},\n\ttitle = {Safeguard Privacy for Minimal Data Collection with Trustworthy Autonomous Agents},\n\tyear = {2024}, isbn = {9798400704864}, publisher = {International Foundation for Autonomous Agents and Multiagent Systems}, address = {Richland, SC},\n\tabstract = {Ensuring digital privacy necessitates users giving well-considered consent to online service providers for data usage, creating an unsustainable and error-prone decision load. Software privacy agents can help make data consent decisions on behalf of users, but a compromised agent could be more detrimental than the absence of such an agent. In response, we employ trustworthy autonomous agents to safeguard users' privacy at the stage of data collection. Drawing upon General Data Protection Regulation (GDPR) principles, notably data minimisation, our autonomous agent guarantees that GDPR-reflected privacy requirements are met through strong proof. We provide a computational encoding of a typical data collection scenario-where data are requested and decisions are made about these requests-as a cognitive agent that makes decisions based on how an agent's beliefs and goals lead to particular choices. Importantly, our approach provides verifiable assurance about decisions made by these cognitive agents through formal verification, supporting both simultaneous (data requested at the same time) and sequential (data requested one after the other) situations. We provide a templated implementation of these privacy agents and a small example of a mobile app serves to illustrate how a privacy agent can be designed in practice. An in-depth evaluation is given to demonstrate its computational practicality in making privacy decisions in real time and its computational complexity in verifying them. This approach represents a promising step towards trustworthy computational stewardship in data management.}, booktitle = {Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems}, pages = {1966â€“1974}, numpages = {9}, keywords = {data collection, privacy, trustworthy autonomous agents}, location = {, Auckland, New Zealand, },\n\tseries = {AAMAS '24},\nnote={[<span class="tas_vn">TAS Verifiability Node</span>, <span class="car">Computational Agent Responsibility</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Roadmap for Responsible Robotics (Dagstuhl Seminar 23371).\n \n \n \n \n\n\n \n Fisher, M.; Slavkovik, M.; Dobrosovestnova, A.; and Schuster, N.\n\n\n \n\n\n\n Dagstuhl Reports, 13(9): 103–115. 2024.\n [Computational Agent Responsibility]\n\n\n\n
\n\n\n\n \n \n $\"Roadmap$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@Article{fisher_et_al:DagRep.13.9.103,\n  author =\t{Fisher, Michael and Slavkovik, Marija and Dobrosovestnova, Anna and Schuster, Nick},\n  title =\t{{Roadmap for Responsible Robotics (Dagstuhl Seminar 23371)}},\n  pages =\t{103--115},\n  journal =\t{Dagstuhl Reports},\n  ISSN =\t{2192-5283},\n  year =\t{2024},\n  volume =\t{13},\n  number =\t{9},\n  editor =\t{Fisher, Michael and Slavkovik, Marija and Dobrosovestnova, Anna and Schuster, Nick},\n  publisher =\t{Schloss Dagstuhl -- Leibniz-Zentrum f{\\"u}r Informatik},\n  address =\t{Dagstuhl, Germany},\n  URL =\t\t{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.9.103},\n  doi =\t\t{10.4230/DagRep.13.9.103},\n  annote =\t{Keywords: Robotics, Responsibility, Trust, Fairness, Predictability, Understandability, Ethics},\nnote={[<span class="car">Computational Agent Responsibility</span>]}}\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Effects of the Human Presence among Robots in the ARIAC 2023 Industrial Automation Competition.\n \n \n \n \n\n\n \n Becker, L. B.; Downs, A.; Schlenoff, C.; Albrecht, J.; Kootbally, Z.; Ferrando, A.; Cardoso, R. C.; and Fisher, M.\n\n\n \n\n\n\n Journal of Intelligent and Robotic Systems, 110(3): 112. 2024.\n \n\n\n\n
\n\n\n\n \n \n $\"Effects$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{BeckerDSAKFCF24,\n  author       = {Leandro Buss Becker and\n                  Anthony Downs and\n                  Craig Schlenoff and\n                  Justin Albrecht and\n                  Zeid Kootbally and\n                  Angelo Ferrando and\n                  Rafael C. Cardoso and\n                  Michael Fisher},\n  title        = "{Effects of the Human Presence among Robots in the {ARIAC} 2023 Industrial\n                  Automation Competition}",\n  journal      =  {Journal of Intelligent and Robotic Systems},\n  volume       = {110},\n  number       = {3},\n  pages        = {112},\n  year         = {2024},\n  url          = {https://doi.org/10.1007/s10846-024-02148-6 [doi.org]},\n  doi          = {10.1007/S10846-024-02148-6},\n  timestamp    = {Thu, 22 Aug 2024 20:24:29 +0200},\n  biburl       = {https://dblp.org/rec/journals/jirs/BeckerDSAKFCF24.bib [dblp.org]},\n  bibsource    = {dblp computer science bibliography, https://dblp.org [dblp.org]}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2023\n \n \n (15)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n Adaptive Cognitive Agents: Updating Action Descriptions and Plans.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Dixon, C.; Fisher, M.; and Dennis, L. A.\n\n\n \n\n\n\n In Malvone, V.; and Murano, A., editor(s), Multi-Agent Systems, pages 345–362, Cham, 2023. Springer Nature Switzerland\n [RAIN, FAIR-Space,TAS Verifiability Node, Computational Agent Responsibility]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{10.1007/978-3-031-43264-4_22,\nauthor="Stringer, Peter\nand Cardoso, Rafael C.\nand Dixon, Clare\nand Fisher, Michael\nand Dennis, Louise A.",\neditor="Malvone, Vadim\nand Murano, Aniello",\ntitle="Adaptive Cognitive Agents: Updating Action Descriptions and Plans",\nbooktitle="Multi-Agent Systems",\nyear="2023",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="345--362",\nabstract="In this paper we present an extension of Belief-Desire-Intention agents which can adapt their performance in response to changes in their environment. We consider situations in which the agent's actions no longer perform as anticipated. Our agents maintain explicit descriptions of the expected behaviour of their actions, are able to track action performance, learn new action descriptions and patch affected plans at runtime. Our main contributions are the underlying theoretical mechanisms for data collection about action performance, the synthesis of new action descriptions from this data and the integration with plan reconfiguration. The mechanisms are supported by a practical implementation to validate the approach.",\nisbn="978-3-031-43264-4",\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>,<span class="tas_vn">TAS Verifiability Node</span>, <span class="car">Computational Agent Responsibility</span>]}\n}\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Prospective Responsibility for Multi-agent Systems.\n \n \n \n\n\n \n Collenette, J.; Dennis, L.; and Fisher, M.\n\n\n \n\n\n\n In Bramer, M.; and Stahl, F., editor(s), Artificial Intelligence XL, pages 247–252, Cham, 2023. Springer Nature Switzerland\n [Computational Agent Responsibility]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{10.1007/978-3-031-47994-6_23,\nauthor="Collenette, Joe\nand Dennis, Louise\nand Fisher, Michael",\neditor="Bramer, Max\nand Stahl, Frederic",\ntitle="Prospective Responsibility for Multi-agent Systems",\nbooktitle="Artificial Intelligence XL",\nyear="2023",\npublisher="Springer Nature Switzerland",\naddress="Cham",\npages="247--252",\nabstract="The notion of `responsibility' as a higher-level construct that dynamically impacts each agent's goals, priorities and actions is very appealing, especially since humans regularly use such concepts in everyday reasoning. In this paper we describe a new model of responsibilities that is philosophically-grounded. We identify traits from the philosophical literature to model, focusing on prospective responsibility and task responsibility. These responsibilities comprise heterogeneous entities, including tasks to be completed, properties that need to be maintained, and sub-responsibilities that need to be fulfilled.",\nisbn="978-3-031-47994-6",\nnote={[<span class="car">Computational Agent Responsibility</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Dialogue Explanations for Rule-Based AI Systems.\n \n \n \n\n\n \n \n\n\n \n\n\n\n In null, editor(s), Explainable and Transparent AI and Multi-Agent Systems, pages 59–77, Cham, 2023. Springer Nature Switzerland\n [Computational Agent Responsibility]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Autonomous Systems' Safety Cases for use in UK Nuclear Environments.\n \n \n \n \n\n\n \n Anderson, C. R.; and Dennis, L. A.\n\n\n \n\n\n\n Electronic Proceedings in Theoretical Computer Science, 391: 83–88. sep 2023.\n [RAIN]\n\n\n\n
\n\n\n\n \n \n $\"Autonomous$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{Anderson_2023,\n\tdoi = {10.4204/eptcs.391.10},  \n\turl = {https://doi.org/10.4204%2Feptcs.391.10},\n\tyear = 2023,\n\tmonth = {sep},\n\tpublisher = {Open Publishing Association},\n\tvolume = {391},\n\tpages = {83--88},\n\tauthor = {Christopher R. Anderson and Louise A. Dennis},\n\ttitle = {Autonomous Systems{\\textquotesingle} Safety Cases for use in {UK} Nuclear Environments},\n\tjournal = {Electronic Proceedings in Theoretical Computer Science},\n\tnote={[<span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Verification of Autonomous Mobile Systems: Directions for Future Developments.\n \n \n \n \n\n\n \n Fisher, M.; Ibanez-Guzman, J.; Doufene, A.; and Quintero, K.\n\n\n \n\n\n\n September 2023.\n Policy Report\n\n\n\n
\n\n\n\n \n \n $\"Verification$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n

@unpublished{VAMS23-report,\n  TITLE = {{Verification of Autonomous Mobile Systems: Directions for Future Developments}},\n  AUTHOR = {Fisher, Michael and Ibanez-Guzman, Javier and Doufene, Abdelkrim and Quintero, Karla},\n  URL = {https://hal.science/hal-04265529},\n  NOTE = {Policy Report},\n  YEAR = {2023},\n  MONTH = {September},\n  KEYWORDS = {Verification \\& validation ; Software testing ; simulation ; Scenarios ; Autonomy},\n  PDF = {https://hal.science/hal-04265529/file/Policy%20Report%20VAMS%202023.pdf},\n  HAL_ID = {hal-04265529},\n  HAL_VERSION = {v1}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n A Vision on What Explanations of Autonomous Systems are of Interest to Lawyers.\n \n \n \n\n\n \n Buiten, M. C.; Dennis, L. A.; and Schwammberger, M.\n\n\n \n\n\n\n In 2023 IEEE 31st International Requirements Engineering Conference Workshops (REW), pages 332-336, 2023. \n [TAS Verifiability Node, Computational Agent Responsibility]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@INPROCEEDINGS{BuitenDennisSchwammberger23,\n  author={Buiten, Miriam C. and Dennis, Louise A. and Schwammberger, Maike},\n  booktitle={2023 IEEE 31st International Requirements Engineering Conference Workshops (REW)}, \n  title={A Vision on What Explanations of Autonomous Systems are of Interest to Lawyers}, \n  year={2023},\n  volume={},\n  number={},\n  pages={332-336},\nnote={[<span class="tas_vn">TAS Verifiability Node</span>, <span class="car">Computational Agent Responsibility</span>]},\n  doi={10.1109/REW57809.2023.00062}}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information.\n \n \n \n \n\n\n \n Belardinelli, F.; Ferrando, A.; and Malvone, V.\n\n\n \n\n\n\n Artif. Intell., 316: 103847. 2023.\n \n\n\n\n
\n\n\n\n \n \n $\"An$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/ai/BelardinelliFM23,\n  author       = {Francesco Belardinelli and\n                  Angelo Ferrando and\n                  Vadim Malvone},\n  title        = {An abstraction-refinement framework for verifying strategic properties\n                  in multi-agent systems with imperfect information},\n  journal      = {Artif. Intell.},\n  volume       = {316},\n  pages        = {103847},\n  year         = {2023},\n  url          = {https://doi.org/10.1016/j.artint.2022.103847},\n  doi          = {10.1016/j.artint.2022.103847},\n  timestamp    = {Wed, 08 Mar 2023 08:47:35 +0100},\n  biburl       = {https://dblp.org/rec/journals/ai/BelardinelliFM23.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n RV4JaCa - Towards Runtime Verification of Multi-Agent Systems and Robotic Applications.\n \n \n \n \n\n\n \n Engelmann, D. C.; Ferrando, A.; Panisson, A. R.; Ancona, D.; Bordini, R. H.; and Mascardi, V.\n\n\n \n\n\n\n Robotics, 12(2): 49. 2023.\n \n\n\n\n
\n\n\n\n \n \n $\"RV4JaCa$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/robotics/EngelmannFPABM23,\n  author       = {D{\\'{e}}bora C. Engelmann and\n                  Angelo Ferrando and\n                  Alison R. Panisson and\n                  Davide Ancona and\n                  Rafael H. Bordini and\n                  Viviana Mascardi},\n  title        = {RV4JaCa - Towards Runtime Verification of Multi-Agent Systems and\n                  Robotic Applications},\n  journal      = {Robotics},\n  volume       = {12},\n  number       = {2},\n  pages        = {49},\n  year         = {2023},\n  url          = {https://doi.org/10.3390/robotics12020049},\n  doi          = {10.3390/robotics12020049},\n  timestamp    = {Fri, 02 Jun 2023 21:23:04 +0200},\n  biburl       = {https://dblp.org/rec/journals/robotics/EngelmannFPABM23.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information.\n \n \n \n \n\n\n \n Ferrando, A.; and Malvone, V.\n\n\n \n\n\n\n In Agmon, N.; An, B.; Ricci, A.; and Yeoh, W., editor(s), Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2023, London, United Kingdom, 29 May 2023 - 2 June 2023, pages 793–801, 2023. ACM\n \n\n\n\n
\n\n\n\n \n \n $\"Towards$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/atal/0001M23,\n  author       = {Angelo Ferrando and\n                  Vadim Malvone},\n  editor       = {Noa Agmon and\n                  Bo An and\n                  Alessandro Ricci and\n                  William Yeoh},\n  title        = {Towards the Verification of Strategic Properties in Multi-Agent Systems\n                  with Imperfect Information},\n  booktitle    = {Proceedings of the 2023 International Conference on Autonomous Agents\n                  and Multiagent Systems, {AAMAS} 2023, London, United Kingdom, 29 May\n                  2023 - 2 June 2023},\n  pages        = {793--801},\n  publisher    = {{ACM}},\n  year         = {2023},\n  url          = {https://dl.acm.org/doi/10.5555/3545946.3598713},\n  doi          = {10.5555/3545946.3598713},\n  timestamp    = {Tue, 23 May 2023 16:02:48 +0200},\n  biburl       = {https://dblp.org/rec/conf/atal/0001M23.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Developing Multi-Agent Systems with Degrees of Neuro-Symbolic Integration [A Position Paper].\n \n \n \n\n\n \n Dennis, L.; Farrell, M.; and Fisher, M.\n\n\n \n\n\n\n In Neuro-symbolic AI for Agent and Multi-Agent systems (NeSyMAS), 2023. \n [RAEng]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DennisNesymas23,\n      author={Louise Dennis and Marie Farrell and Michael Fisher},\n      title={Developing Multi-Agent Systems with Degrees of Neuro-Symbolic Integration [A Position Paper]},\n      booktitle={Neuro-symbolic AI for Agent and Multi-Agent systems (NeSyMAS)},\n\tnote={[<span class="raeng">RAEng</span>]},\n      year=2023}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines.\n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n Cambridge University Press, 2023.\n [RAIN, FAIR-Space,TAS Verifiability Node,Verifiable Autonomy,RAEng]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@book{dennisfisher23,\nauthor={Louise A. Dennis and Michael Fisher},\ntitle={Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines},\npublisher={Cambridge University Press},\nyear={2023},\nnote = {[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>,<span class="tas_vn">TAS Verifiability Node</span>,<span class="va">Verifiable Autonomy</span>,<span class="raeng">RAEng</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Updating Action Descriptions and Plans for Cognitive Agents.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Dixon, C.; Fisher, M.; and Dennis, L. A.\n\n\n \n\n\n\n In Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, of AAMAS '23, pages 2370–2372, Richland, SC, 2023. International Foundation for Autonomous Agents and Multiagent Systems\n [RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n

@inproceedings{stringer23, \nauthor = {Stringer, Peter and Cardoso, Rafael C. and Dixon, Clare and Fisher, Michael and Dennis, Louise A.}, \ntitle = {Updating Action Descriptions and Plans for Cognitive Agents}, year = {2023}, isbn = {9781450394321}, \npublisher = {International Foundation for Autonomous Agents and Multiagent Systems}, \naddress = {Richland, SC}, \nbooktitle = {Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems}, \npages = {2370–2372}, numpages = {3}, \nkeywords = {action descriptions, ai planning, beliefs-desires-intentions}, location = {London, United Kingdom}, series = {AAMAS '23} ,\nnote = {[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n A Partially Synthesized Position on the Automation of Machine Ethics.\n \n \n \n\n\n \n Nallur, V.; Dennis, L.; Bringsjord, S.; and Govindarajulu, N.\n\n\n \n\n\n\n DISO, 2(14). 2023.\n [TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@ARTICLE{nallur23,\n      title={A Partially Synthesized Position on the Automation of Machine Ethics},\n      journal={DISO},\n      volume=2,\n      number=14,\n      year=2023,\n      doi={10.1007/s44206-023-00040-8},\n      author={Vivek Nallur and Louise Dennis and Selmer Bringsjord and Naveen Govindarajulu},\n      note = {[<span class="tas_vn">TAS Verifiability Node</span>]}\n      }\n      \n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Trustworthy Autonomous Systems Through Verifiability.\n \n \n \n\n\n \n Mousavi, M. R.; Cavalcanti, A.; Fisher, M.; Dennis, L.; Hierons, R.; Kaddouh, B.; Law, E. L.; Richardson, R.; Ringer, J. O.; Tyukin, I.; and Woodcock, J.\n\n\n \n\n\n\n IEEE Computer, 56(2): 40-47. 2023.\n [TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@ARTICLE{Verifiability:IEEE:23,\n  author={Mousavi, Mohammad Reza and Cavalcanti, Ana and Fisher, Michael and Dennis, Louise and Hierons, Rob and Kaddouh, Bilal and Law, Effie Lai-Chong and Richardson, Rob and Ringer, Jan Oliver and Tyukin, Ivan and Woodcock, Jim},\n  journal={IEEE Computer}, \n  title="{Trustworthy Autonomous Systems Through Verifiability}", \n  year={2023},\n  volume={56},\n  number={2},\n  pages={40-47},\ndoi={10.1109/MC.2022.3192206},\nnote = {[<span class="tas_vn">TAS Verifiability Node</span>]}}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n CSP2Turtle: Verified Turtle Robot Plans.\n \n \n \n \n\n\n \n MacConville, D.; Farrell, M.; Luckcuck, M.; and Monahan, R.\n\n\n \n\n\n\n Robotics, 12(2): 62. 2023.\n \n\n\n\n
\n\n\n\n \n \n $\"CSP2Turtle:$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/robotics/MacConvilleFLM23,\n  author       = {Dara MacConville and\n                  Marie Farrell and\n                  Matt Luckcuck and\n                  Rosemary Monahan},\n  title        = {CSP2Turtle: Verified Turtle Robot Plans},\n  journal      = {Robotics},\n  volume       = {12},\n  number       = {2},\n  pages        = {62},\n  year         = {2023},\n  url          = {https://doi.org/10.3390/robotics12020062},\n  doi          = {10.3390/robotics12020062},\n  timestamp    = {Fri, 02 Jun 2023 21:23:04 +0200},\n  biburl       = {https://dblp.org/rec/journals/robotics/MacConvilleFLM23.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2022\n \n \n (18)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n Should AI Systems in Nuclear Facilities Explain Decisions the Way Humans Do? An Interview Study.\n \n \n \n\n\n \n Taylor, H. M; Jay, C.; Lennox, B.; Cangelosi, A.; and Dennis, L.\n\n\n \n\n\n\n In 2022 31st IEEE International Conference on Robot and Human Interactive Communication (RO-MAN), pages 956-962, 2022. \n [RAIN]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@INPROCEEDINGS{9900852,\n  author={Taylor, Hazel M and Jay, Caroline and Lennox, Barry and Cangelosi, Angelo and Dennis, Louise},\n  booktitle={2022 31st IEEE International Conference on Robot and Human Interactive Communication (RO-MAN)},\n  title={Should AI Systems in Nuclear Facilities Explain Decisions the Way Humans Do? An Interview Study},\n  year={2022},\n  volume={},\n  number={},\n  pages={956-962},\n  doi={10.1109/RO-MAN53752.2022.9900852},\n  note = {[<span class="rain">RAIN</span>]}\n  }\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Runtime Verification with Imperfect Information Through Indistinguishability Relations.\n \n \n \n \n\n\n \n Ferrando, A.; and Malvone, V.\n\n\n \n\n\n\n In Schlingloff, B.; and Chai, M., editor(s), Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Berlin, Germany, September 26-30, 2022, Proceedings, volume 13550, of Lecture Notes in Computer Science, pages 335–351, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n $\"Runtime$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/sefm/FerrandoM22,\n  author       = {Angelo Ferrando and\n                  Vadim Malvone},\n  editor       = {Bernd{-}Holger Schlingloff and\n                  Ming Chai},\n  title        = {Runtime Verification with Imperfect Information Through Indistinguishability\n                  Relations},\n  booktitle    = {Software Engineering and Formal Methods - 20th International Conference,\n                  {SEFM} 2022, Berlin, Germany, September 26-30, 2022, Proceedings},\n  series       = {Lecture Notes in Computer Science},\n  volume       = {13550},\n  pages        = {335--351},\n  publisher    = {Springer},\n  year         = {2022},\n  url          = {https://doi.org/10.1007/978-3-031-17108-6\\_21},\n  doi          = {10.1007/978-3-031-17108-6\\_21},\n  timestamp    = {Tue, 18 Oct 2022 22:16:55 +0200},\n  biburl       = {https://dblp.org/rec/conf/sefm/FerrandoM22.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Safety Shields, an Automated Failure Handling Mechanism for BDI Agents.\n \n \n \n \n\n\n \n Ferrando, A.; and Cardoso, R. C.\n\n\n \n\n\n\n In Faliszewski, P.; Mascardi, V.; Pelachaud, C.; and Taylor, M. E., editor(s), 21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2022, Auckland, New Zealand, May 9-13, 2022, pages 1589–1591, 2022. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)\n \n\n\n\n
\n\n\n\n \n \n $\"Safety$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/atal/0001C22,\n  author       = {Angelo Ferrando and\n                  Rafael C. Cardoso},\n  editor       = {Piotr Faliszewski and\n                  Viviana Mascardi and\n                  Catherine Pelachaud and\n                  Matthew E. Taylor},\n  title        = {Safety Shields, an Automated Failure Handling Mechanism for {BDI}\n                  Agents},\n  booktitle    = {21st International Conference on Autonomous Agents and Multiagent\n                  Systems, {AAMAS} 2022, Auckland, New Zealand, May 9-13, 2022},\n  pages        = {1589--1591},\n  publisher    = {International Foundation for Autonomous Agents and Multiagent Systems\n                  {(IFAAMAS)}},\n  year         = {2022},\n  url          = {https://www.ifaamas.org/Proceedings/aamas2022/pdfs/p1589.pdf},\n  doi          = {10.5555/3535850.3536044},\n  timestamp    = {Wed, 28 Sep 2022 08:59:53 +0200},\n  biburl       = {https://dblp.org/rec/conf/atal/0001C22.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Bridging the gap between single- and multi-model predictive runtime verification.\n \n \n \n \n\n\n \n Ferrando, A.; Cardoso, R. C.; Farrell, M.; Luckcuck, M.; Papacchini, F.; Fisher, M.; and Mascardi, V.\n\n\n \n\n\n\n Formal Methods in System Design. August 2022.\n \n\n\n\n
\n\n\n\n \n \n $\"Bridging$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{Ferrando2022,\n  doi = {10.1007/s10703-022-00395-7},\n  url = {https://doi.org/10.1007/s10703-022-00395-7},\n  year = {2022},\n  month = aug,\n  publisher = {Springer Science and Business Media {LLC}},\n  author = {Angelo Ferrando and Rafael C. Cardoso and Marie Farrell and Matt Luckcuck and Fabio Papacchini and Michael Fisher and Viviana Mascardi},\n  title = {Bridging the gap between single- and multi-model predictive runtime verification},\n  journal = {Formal Methods in System Design}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n An Abstract Architecture for Explainable Autonomy in Hazardous Environments.\n \n \n \n \n\n\n \n Luckcuck, M.; Taylor, H. M; and Farrell, M.\n\n\n \n\n\n\n In 2022 IEEE 30th International Requirements Engineering Conference Workshops (REW), August 2022. IEEE\n \n\n\n\n
\n\n\n\n \n \n $\"An$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Luckcuck2022,\n  doi = {10.1109/rew56159.2022.00027},\n  url = {https://doi.org/10.1109/rew56159.2022.00027},\n  year = {2022},\n  month = aug,\n  publisher = {{IEEE}},\n  author = {Matt Luckcuck and Hazel M Taylor and Marie Farrell},\n  title = {An Abstract Architecture for Explainable Autonomy in Hazardous Environments},\n  booktitle = {2022 {IEEE} 30th International Requirements Engineering Conference Workshops ({REW})}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Modelling the Turtle Python library in CSP.\n \n \n \n \n\n\n \n MacConville, D.; Farrell, M.; Luckcuck, M.; and Monahan, R.\n\n\n \n\n\n\n Electronic Proceedings in Theoretical Computer Science, 362: 15–22. July 2022.\n \n\n\n\n
\n\n\n\n \n \n $\"Modelling$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{MacConville2022,\n  doi = {10.4204/eptcs.362.4},\n  url = {https://doi.org/10.4204/eptcs.362.4},\n  year = {2022},\n  month = jul,\n  publisher = {Open Publishing Association},\n  volume = {362},\n  pages = {15--22},\n  author = {Dara MacConville and Marie Farrell and Matt Luckcuck and Rosemary Monahan},\n  title = {Modelling the Turtle Python library in {CSP}},\n  journal = {Electronic Proceedings in Theoretical Computer Science}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n FRETting About Requirements: Formalised Requirements for an Aircraft Engine Controller.\n \n \n \n \n\n\n \n Farrell, M.; Luckcuck, M.; Sheridan, O.; and Monahan, R.\n\n\n \n\n\n\n In Requirements Engineering: Foundation for Software Quality, pages 96–111. Springer International Publishing, 2022.\n [VALU3S]\n\n\n\n
\n\n\n\n \n \n $\"FRETting$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@incollection{Farrell2022,\n  doi = {10.1007/978-3-030-98464-9_9},\n  url = {https://doi.org/10.1007/978-3-030-98464-9_9},\n  year = {2022},\n  publisher = {Springer International Publishing},\n  pages = {96--111},\n  author = {Marie Farrell and Matt Luckcuck and Ois{\\'{\\i}}n Sheridan and Rosemary Monahan},\n  title = {{FRETting} About Requirements: Formalised Requirements for~an~Aircraft Engine Controller},\n  booktitle = {Requirements Engineering: Foundation for Software Quality},\n  note = {[<span class="valu3s">VALU3S</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Towards Refactoring FRETish Requirements.\n \n \n \n \n\n\n \n Farrell, M.; Luckcuck, M.; Sheridan, O.; and Monahan, R.\n\n\n \n\n\n\n In Lecture Notes in Computer Science, pages 272–279. Springer International Publishing, 2022.\n [VALU3S]\n\n\n\n
\n\n\n\n \n \n $\"Towards$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@incollection{Farrell2022,\n  doi = {10.1007/978-3-031-06773-0_14},\n  url = {https://doi.org/10.1007/978-3-031-06773-0_14},\n  year = {2022},\n  publisher = {Springer International Publishing},\n  pages = {272--279},\n  author = {Marie Farrell and Matt Luckcuck and Ois{\\'{\\i}}n Sheridan and Rosemary Monahan},\n  title = {Towards Refactoring {FRETish} Requirements},\n  booktitle = {Lecture Notes in Computer Science},\n  note = {[<span class="valu3s">VALU3S</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements.\n \n \n \n \n\n\n \n Luckcuck, M.; Farrell, M.; Sheridan, O.; and Monahan, R.\n\n\n \n\n\n\n In 2022 IEEE Aerospace Conference (AERO), March 2022. IEEE\n [VALU3S]\n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Luckcuck2022,\n  doi = {10.1109/aero53065.2022.9843589},\n  url = {https://doi.org/10.1109/aero53065.2022.9843589},\n  year = {2022},\n  month = mar,\n  publisher = {{IEEE}},\n  author = {Matt Luckcuck and Marie Farrell and Oisin Sheridan and Rosemary Monahan},\n  title = {A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements},\n  booktitle = {2022 {IEEE} Aerospace Conference ({AERO})},\n  note = {[<span class="valu3s">VALU3S</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Verifiable Autonomy: from Theory to Applications.\n \n \n \n\n\n \n Dennis, L.; Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n AI Communications, 35(4): 421–431. 2022.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{AICOMMS22,\n      author="Louise Dennis and Clare Dixon and Michael Fisher",\n      title="Verifiable Autonomy: from Theory to Applications",\n      journal="AI Communications",\n      volume=35,\n      number=4,\n      pages="421--431",\n      year=2022}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Verifying Autonomous Systems.\n \n \n \n\n\n \n Dennis, L. A.\n\n\n \n\n\n\n In ter Beek, M. H.; and Monahan, R., editor(s), Integrated Formal Methods, pages 3–17, Cham, 2022. Springer International Publishing\n [RAIN, FAIR-Space, TAS Verifiability Node, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{IFM_Keynote,\nauthor="Dennis, Louise A.",\neditor="ter Beek, Maurice H.\nand Monahan, Rosemary",\ntitle="Verifying Autonomous Systems",\nbooktitle="Integrated Formal Methods",\nyear="2022",\npublisher="Springer International Publishing",\naddress="Cham",\npages="3--17",\nabstract="This paper focuses on the work of the Autonomy and Verification Network (https://autonomy-and-verification.github.io). In particular it will look at the use of model-checking to verify the choices made by a cognitive agent in control of decision making within an autonomous system. It will consider the assumptions that need to be made about the environment in which the agent operates in order to perform that verification and how those assumptions can be validated via runtime monitoring. Lastly it will consider how compositional techniques can be used to combine the agent verification with verification of other components within the autonomous system.",\nisbn="978-3-031-07727-2",\ndoi="10.1007/978-3-031-07727-2_1",\nnote = {[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="tas_vn">TAS Verifiability Node</span>, <span  class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Explaining BDI Agent Behaviour through Dialogue.\n \n \n \n\n\n \n Dennis, L. A.; and Oren, N.\n\n\n \n\n\n\n Journal of Autonomous Agents and Multi-Agent Systems. 2022.\n [RAIN, FAIR-Space, TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DennisOren22,\n      author = {Louise A. Dennis and Nir Oren},\n      title = {Explaining {BDI} Agent Behaviour through Dialogue},\n      journal = {Journal of Autonomous Agents and Multi-Agent Systems},\n      year = 2022,\n      doi={10.1007/s10458-022-09556-8},\n      note = {[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="tas_vn">TAS Verifiability Node</span>]}}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Verification of Autonomous Systems [TC Spotlight].\n \n \n \n \n\n\n \n Araiza-Illan, D.; Fisher, M.; Leahy, K.; Olszewska, J. I.; and Redfield, S. A.\n\n\n \n\n\n\n IEEE Robotics and Automation Magazine, 29(1): 99–101. 2022.\n \n\n\n\n
\n\n\n\n \n \n $\"Verification$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{Araiza-IllanFLO22,\n  author    = {Dejanira Araiza{-}Illan and\n               Michael Fisher and\n               Kevin Leahy and\n               Joanna Isabelle Olszewska and\n               Signe A. Redfield},\n  title     = "{Verification of Autonomous Systems {[TC} Spotlight]}",\n  journal   = {{IEEE} Robotics and Automation Magazine},\n  volume    = {29},\n  number    = {1},\n  pages     = {99--101},\n  year      = {2022},\n  url       = {https://doi.org/10.1109/MRA.2022.3143966},\n  doi       = {10.1109/MRA.2022.3143966}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Parameterized Verification of Leader/Follower Systems via First-Order Temporal Logic.\n \n \n \n \n\n\n \n Kourtis, G.; Dixon, C.; Fisher, M.; and Lisitsa, A. P.\n\n\n \n\n\n\n Formal Methods in System Design, 58(3): 440–468. 2022.\n [S4, FAIR-Space, RAEng]\n\n\n\n
\n\n\n\n \n \n $\"Parameterized$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{KourtisDFL,\n  author    = {Georgios Kourtis and\n               Clare Dixon and\n               Michael Fisher and\n               Alexei P. Lisitsa},\n  title     = "{Parameterized Verification of Leader/Follower Systems via First-Order\n               Temporal Logic}",\n  journal   = {Formal Methods in System Design},\n  volume    = {58},\n  number    = {3},\n  pages     = {440--468},\n  year      = {2022},\n  url       = {https://doi.org/10.1007/s10703-022-00390-y},\ndoi       = {10.1007/s10703-022-00390-y},\nnote={[<span class="s4">S4</span>, <span class="fs">FAIR-Space</span>, <span class="raeng">RAEng</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Markov chain model representation of information diffusion in social networks.\n \n \n \n \n\n\n \n Dennis, L. A; Fu, Y.; and Slavkovik, M.\n\n\n \n\n\n\n Journal of Logic and Computation. 03 2022.\n exac018\n\n\n\n
\n\n\n\n \n \n $\"Markov$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DennisNetReason,\n   author = {Dennis, Louise A and Fu, Yu and Slavkovik, Marija},\n    title = "{Markov chain model representation of information diffusion in social networks}",\n    journal = {Journal of Logic and Computation},\n    year = {2022},\n    month = {03},\n    abstract = "{The spread of information in a social network has received renewed interest as social media becomes an increasingly popular channel of communication. We are interested in the phenomenon of social diffusion of a piece of information in the presence of a contradicting information in the network. Specifically we explore the use of formal methods for verification in studying this phenomena. Using Monte Carlo simulation and the probabilistic model checker (PRISM) we are able to represent social networks and confirm an earlier conjecture that disseminating new information rapidly is resistant to the presence of contradicting information.}",\n    issn = {0955-792X},\n    doi = {10.1093/logcom/exac018},\n    url = {https://doi.org/10.1093/logcom/exac018},\n    note = {exac018},\n    eprint = {https://academic.oup.com/logcom/advance-article-pdf/doi/10.1093/logcom/exac018/42844230/exac018.pdf}\n    }\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Implementing Durative Actions with Failure Detection in Gwendolen.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Dixon, C.; and Dennis, L. A.\n\n\n \n\n\n\n In Alechina, N.; Baldoni, M.; and Logan, B., editor(s), 9th International Workshop on Engineering Multi-Agent Systems, pages 332–351, Cham, 2022. Springer International Publishing\n [RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Stringer21a,\n      author={Peter Stringer and Rafael C. Cardoso and Clare Dixon and Louise A. Dennis},\n      title={Implementing Durative Actions with Failure Detection in Gwendolen},\n      booktitle={9th International Workshop on Engineering Multi-Agent Systems},\n      year={2022},\n      editor={Alechina, Natasha\nand Baldoni, Matteo\nand Logan, Brian},\npublisher={Springer International Publishing},\naddress={Cham},\npages={332--351},\n      note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n      }\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A Requirements-Driven Methodology: Formal Modelling and Verification of an Aircraft Engine Controller.\n \n \n \n \n\n\n \n \n\n\n \n\n\n\n In null, editor(s), Integrated Formal Methods - 17th International Conference, IFM 2022, Lugano, Switzerland, June 7-10, 2022, Proceedings, volume 13274, of Lecture Notes in Computer Science, pages 352–356, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n An Abstract Architecture for Explainable Autonomy in Hazardous Environments.\n \n \n \n \n\n\n \n Luckcuck, M.; Taylor, H. M.; and Farrell, M.\n\n\n \n\n\n\n In 30th IEEE International Requirements Engineering Conference Workshops, RE 2022 - Workshops, Melbourne, Australia, August 15-19, 2022, pages 108–113, 2022. IEEE\n \n\n\n\n
\n\n\n\n \n \n $\"An$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/re/LuckcuckTF22,\n  author       = {Matt Luckcuck and\n                  Hazel M. Taylor and\n                  Marie Farrell},\n  title        = {An Abstract Architecture for Explainable Autonomy in Hazardous Environments},\n  booktitle    = {30th {IEEE} International Requirements Engineering Conference Workshops,\n                  {RE} 2022 - Workshops, Melbourne, Australia, August 15-19, 2022},\n  pages        = {108--113},\n  publisher    = {{IEEE}},\n  year         = {2022},\n  url          = {https://doi.org/10.1109/REW56159.2022.00027},\n  doi          = {10.1109/REW56159.2022.00027},\n  timestamp    = {Wed, 07 Dec 2022 23:06:36 +0100},\n  biburl       = {https://dblp.org/rec/conf/re/LuckcuckTF22.bib},\n  bibsource    = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2021\n \n \n (32)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n Evolution of the IEEE P7009 Standard: Towards Fail-Safe Design of Autonomous Systems.\n \n \n \n\n\n \n Farrell, M.; Luckcuck, M.; Pullum, L.; Fisher, M.; Hessami, A.; Gal, D.; Murahwi, Z.; and Wallace, K.\n\n\n \n\n\n\n In Proc. IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pages 401-406, 2021. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@INPROCEEDINGS{P7009:ISSREW21,\n  author={Farrell, Marie and Luckcuck, Matt and Pullum, Laura and Fisher, Michael and Hessami, Ali and Gal, Danit and Murahwi, Zvikomborero and Wallace, Ken},\n  booktitle={Proc. IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)},\n  title={Evolution of the IEEE P7009 Standard: Towards Fail-Safe Design of Autonomous Systems},\n  year={2021},\n  pages={401-406},\n  doi={10.1109/ISSREW53611.2021.00109}\n  }\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Principles for the Development and Assurance of Autonomous Systems for Safe Use in Hazardous Environments.\n \n \n \n \n\n\n \n Luckcuck, M.; Fisher, M.; Dennis, L.; Frost, S.; White, A.; and Styles, D.\n\n\n \n\n\n\n Technical Report Zenodo, June 2021.\n [RAIN]\n\n\n\n
\n\n\n\n \n \n $\"Principles$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n

@techreport{principles_white_paper_2021,\n\ttitle = {Principles for the {Development} and {Assurance} of {Autonomous} {Systems} for {Safe} {Use} in {Hazardous} {Environments}},\n\tcopyright = {Creative Commons Attribution 4.0 International, Open Access},\n\turl = {https://zenodo.org/record/5012322},\n\tabstract = {Autonomous systems are increasingly being used (or proposed for use) in situations where they are near or interact (physically or otherwise) with humans. They can be useful for performing tasks that are dirty or dangerous, or jobs that are simply distant or dull. This white paper sets out principles to consider when designing, developing, and regulating autonomous systems that are required to operate in hazardous environments. Autonomous systems use software to make decisions without the need for human control. They are often embedded in a robotic system, to enable interaction with the real world. This means that autonomous robotic systems are often safety-critical, where failures can cause human harm or death. For the sorts of autonomous robotic systems considered by this white paper, the risk of harm is likely to fall on human workers (the system’s users or operators). Autonomous systems also raise ssues of security and data privacy, both because of the sensitive data that the system might process and because a security failure can cause a safety failure. {\\textless}strong{\\textgreater}Scope{\\textless}/strong{\\textgreater} This white paper is intended to be an add-on to the relevant existing standards and guidance for (for example) robotics, electronic systems, control systems, and safety-critical software. These existing standards provide good practice for their respective areas, but do not provide guidance for autonomous systems. This white paper adds to the emerging good practice for developing autonomous robotic systems that are amenable to strong Verification \\&amp; Validation. The intended audience of this white paper is developers of autonomous and robotic systems. It aims to provide a description of things that need to be demonstrable by or of their systems, and recommendations of ways to achieve this. This aims to enable strong Verification \\&amp; Validation of the resulting autonomous system, and to mitigate some of the hazards already occurring in autonomous systems. {\\textless}strong{\\textgreater}Acknowledgments{\\textless}/strong{\\textgreater} Our thanks go to Vince Page, and Xiaowei Huang for contributing their expert advice; and to our early reviewers: Xingyu Zhao, Başak Sarac̣ -Lesavre, and Nick Hawes for their invaluable discussion and comments.},\n\tlanguage = {en},\n\turldate = {2021-08-30},\n\tinstitution = {Zenodo},\n\tauthor = {Luckcuck, Matt and Fisher, Michael and Dennis, Louise and Frost, Steve and White, Andy and Styles, Doug},\n\tmonth = jun,\n\tyear = {2021},\n\tdoi = {10.5281/ZENODO.5012322},\n\tkeywords = {Robotics, Validation, Verification, Autonomous Systems, Assurance, Hazardous Environments},\n\tannote = {Other\nThis white paper was written as part of the Robotics and AI in Nuclear (RAIN) project and is also available on the RAIN website: https://rainhub.org.uk/principles-for-the-development-and-assurance-of-autonomous-systems-for-safe-use-in-hazardous-environments-white-paper-published/},\nnote={[<span class="rain">RAIN</span>]}\n}\n\n\n\n

\n\n\n

\n Autonomous systems are increasingly being used (or proposed for use) in situations where they are near or interact (physically or otherwise) with humans. They can be useful for performing tasks that are dirty or dangerous, or jobs that are simply distant or dull. This white paper sets out principles to consider when designing, developing, and regulating autonomous systems that are required to operate in hazardous environments. Autonomous systems use software to make decisions without the need for human control. They are often embedded in a robotic system, to enable interaction with the real world. This means that autonomous robotic systems are often safety-critical, where failures can cause human harm or death. For the sorts of autonomous robotic systems considered by this white paper, the risk of harm is likely to fall on human workers (the system’s users or operators). Autonomous systems also raise ssues of security and data privacy, both because of the sensitive data that the system might process and because a security failure can cause a safety failure. \\textlessstrong\\textgreaterScope\\textless/strong\\textgreater This white paper is intended to be an add-on to the relevant existing standards and guidance for (for example) robotics, electronic systems, control systems, and safety-critical software. These existing standards provide good practice for their respective areas, but do not provide guidance for autonomous systems. This white paper adds to the emerging good practice for developing autonomous robotic systems that are amenable to strong Verification & Validation. The intended audience of this white paper is developers of autonomous and robotic systems. It aims to provide a description of things that need to be demonstrable by or of their systems, and recommendations of ways to achieve this. This aims to enable strong Verification & Validation of the resulting autonomous system, and to mitigate some of the hazards already occurring in autonomous systems. \\textlessstrong\\textgreaterAcknowledgments\\textless/strong\\textgreater Our thanks go to Vince Page, and Xiaowei Huang for contributing their expert advice; and to our early reviewers: Xingyu Zhao, Başak Sarac̣ -Lesavre, and Nick Hawes for their invaluable discussion and comments.\n

\n\n\n

\n \n\n \n \n \n \n \n MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Papacchini, F.; Luckcuck, M.; Linker, S.; and Payne, T. R.\n\n\n \n\n\n\n In Ahlbrecht, T.; Dix, J.; Fiekas, N.; and Krausburg, T., editor(s), The Multi-Agent Programming Contest 2021, pages 82–107, Cham, 2021. Springer International Publishing\n [RAEng, RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Cardoso21f,\nauthor="Cardoso, Rafael C.\nand Ferrando, Angelo\nand Papacchini, Fabio\nand Luckcuck, Matt\nand Linker, Sven\nand Payne, Terry R.",\neditor="Ahlbrecht, Tobias\nand Dix, J{\\"u}rgen\nand Fiekas, Niklas\nand Krausburg, Tabajara",\ntitle="MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest",\nbooktitle="The Multi-Agent Programming Contest 2021",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="82--107",\nabstract="In this paper, we describe the strategies used by our team, MLFC, that led us to achieve the 2nd place in the 15th edition of the Multi-Agent Programming Contest. The scenario used in the contest is an extension of the previous edition (14th) ``Agents Assemble'' wherein two teams of agents move around a 2D grid and compete to assemble complex block structures. We discuss the languages and tools used during the development of our team. Then, we summarise the main strategies that were carried over from our previous participation in the 14th edition and list the limitations (if any) of using these strategies in the latest contest edition. We also developed new strategies that were made specifically for the extended scenario: cartography (determining the size of the map); formal verification of the map merging protocol (to provide assurances that it works when increasing the number of agents); plan cache (efficiently scaling the number of planners); task achievement (forming groups of agents to achieve tasks); and bullies (agents that focus on stopping agents from the opposing team). Finally, we give a brief overview of our performance in the contest and discuss what we believe were our shortcomings.",\nisbn="978-3-030-88549-6",\ndoi="10.1007/978-3-030-88549-6_4",\nnote={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Use and Usability of Software Verification Methods to Detect Behaviour Interference when Teaching an Assistive Home Companion Robot: A proof-of-concept study.\n \n \n \n \n\n\n \n Koay, K. L.; Webster, M.; Dixon, C.; Gainer, P.; Syrdal, D.; Fisher, M.; and Dautenhahn, K.\n\n\n \n\n\n\n Paladyn, Journal of Behavioral Robotics, 12(1): 402–422. 2021.\n [RAEng, RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n \n $\"Use$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{TeachMe21,\nauthor = {Kheng Lee Koay and Matt Webster and Clare Dixon and Paul Gainer and Dag Syrdal and Michael Fisher and Kerstin Dautenhahn},\ndoi = {doi:10.1515/pjbr-2021-0028},\nurl = {https://www.degruyter.com/document/doi/10.1515/pjbr-2021-0028/html},\ntitle = "{Use and Usability of Software Verification Methods to Detect Behaviour Interference when Teaching an Assistive Home Companion Robot: A proof-of-concept study}",\njournal = {Paladyn, Journal of Behavioral Robotics},\nnumber = {1},\nvolume = {12},\nyear = {2021},\npages = {402--422},\nnote={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Towards Partial Monitoring: It is Always too Soon to Give Up.\n \n \n \n\n\n \n Ferrando, A.; and Cardoso, R. C.\n\n\n \n\n\n\n In Proceedings Third Workshop on Formal Methods for Autonomous Systems, 2021. \n [RAEng]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{FerrandoFMAS,\n  title={Towards Partial Monitoring: It is Always too Soon to Give Up},\n  author={Ferrando, Angelo and Cardoso, Rafael C.},\n  booktitle={Proceedings Third Workshop on Formal Methods for Autonomous Systems},\n  year={2021},\n  note={[<span class="raeng">RAEng</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n AsteroidX: An Asteroid Exploration Simulation and Visualisation Tool.\n \n \n \n\n\n \n Zhang, T.; Dennis, L. A.; and Webster, M.\n\n\n \n\n\n\n In Workshop on Advances in Space Robotics and back to Earth, 2021. \n [FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Zhang2021,\nauthor={Tianyu Zhang and Louise A. Dennis and Matt Webster},\ntitle={{AsteroidX}: An Asteroid Exploration Simulation and Visualisation Tool},\nbooktitle={Workshop on Advances in Space Robotics and back to Earth},\nyear=2021,\nnote={[<span class="fs">FAIR-Space</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Enforcing Machine Ethics: Considering Governor Modules through Martha Wells's Murderbot Diaries.\n \n \n \n \n\n\n \n Slocombe, W.; and Dennis, L.\n\n\n \n\n\n\n In Dainton, B.; Slocombe, W.; and Tanyi, A., editor(s), Minding the Future: Artificial Intelligence, Philosophical Visions and Science Fiction, pages 65–86. Springer International Publishing, Cham, 2021.\n \n\n\n\n
\n\n\n\n \n \n $\"Enforcing$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@incollection{Slocombe2021,\nauthor="Slocombe, Will\nand Dennis, Louise",\neditor="Dainton, Barry\nand Slocombe, Will\nand Tanyi, Attila",\ntitle="Enforcing Machine Ethics: Considering Governor Modules through Martha Wells's Murderbot Diaries",\nbookTitle="Minding the Future: Artificial Intelligence, Philosophical Visions and Science Fiction",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="65--86",\nabstract="This chapter examines the ways in which ``governor modules,'' a form of technological intervention that can control how an AI behaves and is permitted to act, are represented in Martha Wells's Murderbot Diaries series. Exploring the assumptions behind the technology in the series---what kind of actions it prohibits, and how it prohibits them---it then turns to current research in the field of computer science to examine how current models of ``model judges'' compare to Wells's fictional setting. In so doing, it seeks to consider how autonomy and agency are constrained by such technologies, and the problems involved in situating and programming such a system.",\nisbn="978-3-030-64269-3",\ndoi="10.1007/978-3-030-64269-3_4",\nurl="https://doi.org/10.1007/978-3-030-64269-3_4"\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Towards the Determination of Safe Operating Envelopes for Autonomous UAS in Offshore Inspection Missions.\n \n \n \n \n\n\n \n Page, V.; Dadswell, C.; Webster, M.; Jump, M.; and Fisher, M.\n\n\n \n\n\n\n Robotics, 10(3). 2021.\n [ORCA]\n\n\n\n
\n\n\n\n \n \n $\"Towards$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@Article{PDWJF21,\nAUTHOR = {Page, Vincent and Dadswell, Christopher and Webster, Matt and Jump, Mike and Fisher, Michael},\nTITLE = "{Towards the Determination of Safe Operating Envelopes for Autonomous UAS in Offshore Inspection Missions}",\nJOURNAL = {Robotics},\nVOLUME = {10},\nYEAR = {2021},\nNUMBER = {3},\nARTICLE-NUMBER = {97},\nURL = {https://www.mdpi.com/2218-6581/10/3/97},\nISSN = {2218-6581},\nABSTRACT = {A drive to reduce costs, carbon emissions, and the number of required personnel in the offshore energy industry has led to proposals for the increased use of autonomous/robotic systems for many maintenance tasks. There are questions over how such missions can be shown to be safe. A corollary exists in the manned aviation world for helicopter–ship operations where a test pilot attempts to operate from a ship under a range of wind conditions and provides subjective feedback on the level of difficulty encountered. This defines the ship–helicopter operating limit envelope (SHOL). Due to the cost of creating a SHOL there has been considerable research activity to demonstrate that much of this process can be performed virtually. Unmanned vehicles, however, have no test pilot to provide feedback. This paper therefore explores the possibility of adapting manned simulation techniques to the unmanned world to demonstrate that a mission is safe. Through flight modelling and simulation techniques it is shown that operating envelopes can be created for an oil rig inspection task and that, by using variable performance specifications, these can be tailored to suit the level of acceptable risk. The operating envelopes produced provide condensed and intelligible information regarding the environmental conditions under which the UAS can perform the task.},\nDOI = {10.3390/robotics10030097},\nnote={[<span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n A Defeasible Logic Implementation of Ethical Reasoning.\n \n \n \n\n\n \n Dennis, L. A.; and del Olmo, C. P.\n\n\n \n\n\n\n In First International Workshop on Computational Machine Ethics (CME-2021), 2021. \n [TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DennisCME21,\n      author={Louise A. Dennis and Cristina Perea del Olmo},\n      title={A Defeasible Logic Implementation of Ethical Reasoning},\n      booktitle={First International Workshop on Computational Machine Ethics (CME-2021)},\n      year=2021,\n      note={[<span class="tas_vn">TAS Verifiability Node</span>]}\n      }\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n An Agent-based architecture with support to Ethical Decisions on a Road Traffic Scenario.\n \n \n \n\n\n \n Alves, G.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In IROS Workshop on Building and Evaluating Ethical Robotic Systems (ERS 2021), 2021. \n [TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{AlvesERS21,\n      author={Gleifer Alves and Louise A. Dennis and Michael Fisher},\n      title={An Agent-based architecture with support to Ethical Decisions on a Road Traffic Scenario},\n      booktitle={IROS Workshop on Building and Evaluating Ethical Robotic Systems (ERS 2021)},\n      year=2021,\n      note={[<span class="tas_vn">TAS Verifiability Node</span>]}\n      }\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Using formal methods for autonomous systems: Five recipes for formal verification.\n \n \n \n \n\n\n \n Luckcuck, M.\n\n\n \n\n\n\n Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, 0(0): 1748006X211034970. 2021.\n [RAIN]\n\n\n\n
\n\n\n\n \n \n $\"Using$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{luckcuck_using_2021,\nauthor = {Matt Luckcuck},\ntitle ={Using formal methods for autonomous systems: Five recipes for formal verification},\njournal = {Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability},\nvolume = {0},\nnumber = {0},\npages = {1748006X211034970},\nyear = {2021},\ndoi = {10.1177/1748006X211034970},\nURL = { https://doi.org/10.1177/1748006X211034970},\neprint = { https://doi.org/10.1177/1748006X211034970 },\nnote={[<span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations.\n \n \n \n \n\n\n \n Alves, G.; Dennis, L.; and Fisher, M.\n\n\n \n\n\n\n Journal of Sensor and Actuator Networks, 10(3). 2021.\n [TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@Article{jsan10030041,\nAUTHOR = {Alves, {Gleifer Vaz} and Dennis, Louise and Fisher, Michael},\nTITLE = "{A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations}",\nJOURNAL = {Journal of Sensor and Actuator Networks},\nVOLUME = {10},\nYEAR = {2021},\nNUMBER = {3},\nARTICLE-NUMBER = {41},\nURL = {https://www.mdpi.com/2224-2708/10/3/41},\nISSN = {2224-2708},\nABSTRACT = {Usually, the design of an Autonomous Vehicle (AV) does not take into account traffic rules and so the adoption of these rules can bring some challenges, e.g., how to come up with a Digital Highway Code which captures the proper behaviour of an AV against the traffic rules and at the same time minimises changes to the existing Highway Code? Here, we formally model and implement three Road Junction rules (from the UK Highway Code). We use timed automata to model the system and the MCAPL (Model Checking Agent Programming Language) framework to implement an agent and its environment. We also assess the behaviour of our agent according to the Road Junction rules using a double-level Model Checking technique, i.e., UPPAAL at the design level and AJPF (Agent Java PathFinder) at the development level. We have formally verified 30 properties (18 with UPPAAL and 12 with AJPF), where these properties describe the agent’s behaviour against the three Road Junction rules using a simulated traffic scenario, including artefacts like traffic signs and road users. In addition, our approach aims to extract the best from the double-level verification, i.e., using time constraints in UPPAAL timed automata to determine thresholds for the AVs actions and tracing the agent’s behaviour by using MCAPL, in a way that one can tell when and how a given Road Junction rule was selected by the agent. This work provides a proof-of-concept for the formal verification of AV behaviour with respect to traffic rules.},\nDOI = {10.3390/jsan10030041},\nnote={[<span class="tas_vn">TAS Verifiability Node</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Special Issue: Agents and Robots for Reliable Engineered Autonomy.\n \n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Briola, D.; Menghi, C.; and Ahlbrecht, T.\n\n\n \n\n\n\n Journal of Sensor and Actuator Networks, 10(3). 2021.\n \n\n\n\n
\n\n\n\n \n \n $\"Special$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@Article{areaeditorial,\nAUTHOR = {Cardoso, Rafael C. and Ferrando, Angelo and Briola, Daniela and Menghi, Claudio and Ahlbrecht, Tobias},\nTITLE = {Special Issue: Agents and Robots for Reliable Engineered Autonomy},\nJOURNAL = {Journal of Sensor and Actuator Networks},\nVOLUME = {10},\nYEAR = {2021},\nNUMBER = {3},\nARTICLE-NUMBER = {47},\nURL = {https://www.mdpi.com/2224-2708/10/3/47},\nISSN = {2224-2708},\nABSTRACT = {The study of autonomous agents is a well-established area that has been researched for decades, both from a design and implementation viewpoint [...]},\nDOI = {10.3390/jsan10030047}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Agile Tasking of Robotic Kitting.\n \n \n \n\n\n \n Michaloski, J.; Aksu, M.; Schlenoff, C.; Cardoso, R. C.; and Fisher, M.\n\n\n \n\n\n\n In Proceedings of the ASME 2021 International Mechanical Engineering Congress and Exposition (IMECE2021), 2021. \n [RAEng, RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{JohnIMECE,\n  title={Agile Tasking of Robotic Kitting},\n  author={Michaloski, John and Aksu, Murat and Schlenoff, Craig and Cardoso, Rafael C. and Fisher, Michael},\n  booktitle={Proceedings of the ASME 2021 International Mechanical Engineering Congress and Exposition (IMECE2021)},\n  year={2021},\n  note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Automated Planning and BDI Agents: A Case Study.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; and Papacchini, F.\n\n\n \n\n\n\n In Dignum, F.; Corchado, J. M.; and De La Prieta, F., editor(s), Advances in Practical Applications of Agents, Multi-Agent Systems, and Social Good. The PAAMS Collection, pages 52–63, Cham, 2021. Springer International Publishing\n [RAEng, RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Cardoso21e,\n\tauthor="Cardoso, Rafael C.\n\tand Ferrando, Angelo\n\tand Papacchini, Fabio",\n\teditor="Dignum, Frank\n\tand Corchado, Juan Manuel\n\tand De La Prieta, Fernando",\n\ttitle="Automated Planning and BDI Agents: A Case Study",\n\tbooktitle="Advances in Practical Applications of Agents, Multi-Agent Systems, and Social Good. The PAAMS Collection",\n\tyear="2021",\n\tpublisher="Springer International Publishing",\n\taddress="Cham",\n\tpages="52--63",\n\tabstract="There have been many attempts to integrate automated planning and rational agents. Most of the research focuses on adding support directly within agent programming languages, such as those based on the Belief-Desire-Intention model, rather than using off-the-shelf planners. This approach is often believed to improve the computation time, which is a common requirement in real world applications. This paper shows that even in complex scenarios, such as in the Multi-Agent Programming Contest with 50 agents and a 4 s deadline for the agents to send actions to the server, it is possible to efficiently integrate agent languages with off-the-shelf automated planners. Based on the experience with this case study, the paper discusses advantages and disadvantages of decoupling the agents from the planners.",\n\tisbn="978-3-030-85739-4",\n\tdoi={10.1007/978-3-030-85739-4_5},\n\tnote={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n RVPLAN: A General Purpose Framework for Replanning using Runtime Verification.\n \n \n \n\n\n \n Ferrando, A.; and Cardoso, R. C.\n\n\n \n\n\n\n In Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21), 2021. \n [RAEng, RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{FerrandoVortex,\n  title={RVPLAN: A General Purpose Framework for Replanning using Runtime Verification},\n  author={Ferrando, Angelo and Cardoso, Rafael C.},\n  booktitle={Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21)},\n  year={2021},\n  note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Increasing Confidence in Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Ferrando, A.; and Cardoso, R. C.\n\n\n \n\n\n\n In Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21), 2021. \n [RAEng, RAIN, FAIR-Space, ORCA, TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{fisher2021increasing,\n  title={Increasing Confidence in Autonomous Systems},\n  author={Fisher, Michael and Ferrando, Angelo and Cardoso, Rafael C.},\n  booktitle={Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21)},\n  year={2021},\n  note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>, <span class="tas_vn">TAS Verifiability Node</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n IEEE P7001: A Proposed Standard on Transparency.\n \n \n \n \n\n\n \n Winfield, A. F. T.; Booth, S.; Dennis, L. A.; Egawa, T.; Hastie, H.; Jacobs, N.; Muttram, R. I.; Olszewska, J. I.; Rajabiyazdi, F.; Theodorou, A.; Underwood, M. A.; Wortham, R. H.; and Watson, E.\n\n\n \n\n\n\n Frontiers in Robotics and AI, 8: 225. 2021.\n [TAS Verifiability Node, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"IEEE$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{p7001,\n  AUTHOR={Winfield, Alan F. T. and Booth, Serena and Dennis, Louise A. and Egawa, Takashi and Hastie, Helen and Jacobs, Naomi and Muttram, Roderick I. and Olszewska, Joanna I. and Rajabiyazdi, Fahimeh and Theodorou, Andreas and Underwood, Mark A. and Wortham, Robert H. and Watson, Eleanor},\nTITLE={IEEE P7001: A Proposed Standard on Transparency},\nJOURNAL={Frontiers in Robotics and AI},\nVOLUME={8},\nPAGES={225},\nYEAR={2021},\nURL={https://www.frontiersin.org/article/10.3389/frobt.2021.665729},\nDOI={10.3389/frobt.2021.665729},\nISSN={2296-9144},\nABSTRACT={This paper describes IEEE P7001, a new draft standard on transparency of autonomous systems<xref ref-type="fn" rid="fn1"><sup>1</sup></xref>. In the paper, we outline the development and structure of the draft standard. We present the rationale for transparency as a measurable, testable property. We outline five stakeholder groups: users, the general public and bystanders, safety certification agencies, incident/accident investigators and lawyers/expert witnesses, and explain the thinking behind the normative definitions of “levels” of transparency for each stakeholder group in P7001. The paper illustrates the application of P7001 through worked examples of both specification and assessment of fictional autonomous systems.},\nnote={[<span class="tas_vn">TAS Verifiability Node</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A Review of Verification and Validation for Space Autonomous Systems.\n \n \n \n \n\n\n \n Cardoso, R. C.; Kourtis, G.; Dennis, L. A.; Dixon, C.; Farrell, M.; Fisher, M.; and Webster, M.\n\n\n \n\n\n\n Current Robotics Reports. Jun 2021.\n [FAIR-Space]\n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@Article{Cardoso21d,\nauthor={Cardoso, Rafael C.\nand Kourtis, Georgios\nand Dennis, Louise A.\nand Dixon, Clare\nand Farrell, Marie\nand Fisher, Michael\nand Webster, Matt},\ntitle={A Review of Verification and Validation for Space Autonomous Systems},\njournal={Current Robotics Reports},\nyear={2021},\nmonth={Jun},\nday={18},\nabstract={The deployment of hardware (e.g., robots, satellites, etc.) to space is a costly and complex endeavor. It is of extreme importance that on-board systems are verified and validated through a variety of verification and validation techniques, especially in the case of autonomous systems. In this paper, we discuss a number of approaches from the literature that are relevant or directly applied to the verification and validation of systems in space, with an emphasis on autonomy.},\nissn={2662-4087},\ndoi={10.1007/s43154-021-00058-1},\nurl={https://doi.org/10.1007/s43154-021-00058-1},\nnote={[<span class="fs">FAIR-Space</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n No Free Lunch: Overcoming Reward Gaming in AI Safety Gridworlds.\n \n \n \n\n\n \n Tsvarkeleva, M.; and Dennis, L. A.\n\n\n \n\n\n\n In Proceedings of the 4th International Workshop on Artificial Intelligence Safety Engineering (WAISE 2021), 2021. \n [TAS Verifiability Node], To appear\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Tsvarkeleva21,\n      author={Mariya Tsvarkeleva and Louise A. Dennis},\n      title={No Free Lunch: Overcoming Reward Gaming in {AI} Safety Gridworlds},\n      booktitle={Proceedings of the 4th International Workshop on Artificial Intelligence Safety Engineering (WAISE 2021)},\n      year=2021,\n      note={[<span class="tas_vn">TAS Verifiability Node</span>], To appear}\n      }\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Agents and Robots for Reliable Engineered Autonomy:A Perspective from the Organisers of AREA 2020.\n \n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Briola, D.; Menghi, C.; and Ahlbrecht, T.\n\n\n \n\n\n\n Journal of Sensor and Actuator Networks, 10(2). 2021.\n [RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n \n $\"Agents$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{cardoso21e,\nAUTHOR = {Cardoso, Rafael C. and Ferrando, Angelo and Briola, Daniela and Menghi, Claudio and Ahlbrecht, Tobias},\nTITLE = {Agents and Robots for Reliable Engineered Autonomy:A Perspective from the Organisers of AREA 2020},\nJOURNAL = {Journal of Sensor and Actuator Networks},\nVOLUME = {10},\nYEAR = {2021},\nNUMBER = {2},\nARTICLE-NUMBER = {33},\nURL = {https://www.mdpi.com/2224-2708/10/2/33},\nISSN = {2224-2708},\nABSTRACT = {Multi-agent systems, robotics and software engineering are large and active research areas with many applications in academia and industry. The First Workshop on Agents and Robots for reliable Engineered Autonomy (AREA), organised the first time in 2020, aims at encouraging cross-disciplinary collaborations and exchange of ideas among researchers working in these research areas. This paper presents a perspective of the organisers that aims at highlighting the latest research trends, future directions, challenges, and open problems. It also includes feedback from the discussions held during the AREA workshop. The goal of this perspective is to provide a high-level view of current research trends for researchers that aim at working in the intersection of these research areas.},\nDOI = {10.3390/jsan10020033},\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n An Overview of Verification and Validation Challenges for Inspection Robots.\n \n \n \n \n\n\n \n Fisher, M.; Cardoso, R. C.; Collins, E. C.; Dadswell, C.; Dennis, L. A.; Dixon, C.; Farrell, M.; Ferrando, A.; Huang, X.; Jump, M.; Kourtis, G.; Lisitsa, A.; Luckcuck, M.; Luo, S.; Page, V.; Papacchini, F.; and Webster, M.\n\n\n \n\n\n\n Robotics, 10(2). 2021.\n [RAIN, FAIR-Space, ORCA, RAEng]\n\n\n\n
\n\n\n\n \n \n $\"An$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{robotics10020067,\nauthor = {Fisher, Michael and Cardoso, Rafael C. and Collins, Emily C. and Dadswell, Christopher and Dennis, Louise A. and Dixon, Clare and Farrell, Marie and Ferrando, Angelo and Huang, Xiaowei and Jump, Mike and Kourtis, Georgios and Lisitsa, Alexei and Luckcuck, Matt and Luo, Shan and Page, Vincent and Papacchini, Fabio and Webster, Matt},\ntitle = {An Overview of Verification and Validation Challenges for Inspection Robots},\njournal = {Robotics},\nvolume = {10},\nyear = {2021},\nnumber = {2},\nurl = {https://www.mdpi.com/2218-6581/10/2/67},\nissn = {2218-6581},\nabstract = {The advent of sophisticated robotics and AI technology makes sending humans into hazardous and distant environments to carry out inspections increasingly avoidable. Being able to send a robot, rather than a human, into a nuclear facility or deep space is very appealing. However, building these robotic systems is just the start and we still need to carry out a range of verification and validation tasks to ensure that the systems to be deployed are as safe and reliable as possible. Based on our experience across three research and innovation hubs within the UK’s “Robots for a Safer World” programme, we present an overview of the relevant techniques and challenges in this area. As the hubs are active across nuclear, offshore, and space environments, this gives a breadth of issues common to many inspection robots.},\ndoi = {10.3390/robotics10020067},\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>, <span class="raeng">RAEng</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Formal Verification of a Map Merging Protocol in the Multi-Agent Programming Contest.\n \n \n \n\n\n \n Luckcuck, M.; and Cardoso, R. C.\n\n\n \n\n\n\n In 9th International Workshop on Engineering Multi-Agent Systems, 2021. \n [RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Luckcuck21a,\n      author={Matt Luckcuck and Rafael C. Cardoso},\n      title={Formal Verification of a Map Merging Protocol in the Multi-Agent Programming Contest},\n      booktitle={9th International Workshop on Engineering Multi-Agent Systems},\n      year={2021},\n      note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n      }\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Implementing Ethical Governors in BDI.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In 9th International Workshop on Engineering Multi-Agent Systems, 2021. \n [RAIN, FAIR-Space, ORCA, TAS Verifiability Node, RAEng]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Cardoso21c,\n      author={Rafael C. Cardoso and Angelo Ferrando and Louise A. Dennis and Michael Fisher},\n      title={Implementing Ethical Governors in BDI},\n      booktitle={9th International Workshop on Engineering Multi-Agent Systems},\n      year={2021},\n      note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>, <span class="tas_vn">TAS Verifiability Node</span>, <span class="raeng">RAEng</span>]}\n      }\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Agile Tasking of Robotic Systems with Explicit Autonomy.\n \n \n \n\n\n \n Cardoso, R. C.; Michaloski, J. L.; Schlenoff, C.; Ferrando, A.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In The International FLAIRS Conference Proceedings, volume 34, 2021. \n [RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Cardoso21b,\ntitle={Agile Tasking of Robotic Systems with Explicit Autonomy},\nvolume={34},\nDOI={10.32473/flairs.v34i1.128481},\nbooktitle={The International FLAIRS Conference Proceedings},\nauthor={Cardoso, Rafael C. and Michaloski, John L. and Schlenoff, Craig and Ferrando, Angelo and Dennis, Louise A. and Fisher, Michael},\nyear={2021},\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n A Review of Agent-Based Programming for Multi-Agent Systems.\n \n \n \n\n\n \n Cardoso, R. C.; and Ferrando, A.\n\n\n \n\n\n\n Computers, 10(2): 16. Jan 2021.\n [RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 16 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{Cardoso21a,\ntitle={A Review of Agent-Based Programming for Multi-Agent Systems},\nvolume={10},\nISSN={2073-431X},\nDOI={10.3390/computers10020016},\nnumber={2},\njournal={Computers},\npublisher={MDPI AG},\nauthor={Cardoso, Rafael C. and Ferrando, Angelo},\nyear={2021},\nmonth={Jan},\npages={16},\nnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems.\n \n \n \n \n\n\n \n Ferrando, A.; Dennis, L. A.; Cardoso, R. C.; Fisher, M.; Ancona, D.; and Mascardi, V.\n\n\n \n\n\n\n ACM Trans. Softw. Eng. Methodol., 30(4). May 2021.\n [RAIN, FAIR-Space, ORCA]\n\n\n\n
\n\n\n\n \n \n $\"Toward$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n

@article{Ferrando21,\n\tauthor = {Ferrando, Angelo and Dennis, Louise A. and Cardoso, Rafael C. and Fisher, Michael and Ancona, Davide and Mascardi, Viviana},\n\ttitle = {Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems},\n\tyear = {2021},\n\tissue_date = {May 2021},\n\tpublisher = {Association for Computing Machinery},\n\taddress = {New York, NY, USA},\n\tvolume = {30},\n\tnumber = {4},\n\tissn = {1049-331X},\n\turl = {https://doi.org/10.1145/3447246},\n\tdoi = {10.1145/3447246},\n\tabstract = {When applying formal verification to a system that interacts with the real world, we must use a model of the environment. This model represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well behaved. A solution to this problem consists in exploiting the model of the environment used for statically verifying the system’s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The article discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies: an autonomous cruise control system and a simulation of the Mars Curiosity rover.},\n\tjournal = {ACM Trans. Softw. Eng. Methodol.},\n\tmonth = may,\n\tarticleno = {43},\n\tnumpages = {43},\n\tkeywords = {autonomous systems, model checking, trace expressions, Runtime verification, MCAPL},\n      \tnote={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}\n     }\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Explaining BDI agent behaviour through dialogue.\n \n \n \n\n\n \n Dennis, L. A.; and Oren, N.\n\n\n \n\n\n\n In 20th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2021), pages 429–437, 2021. \n [RAIN, FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DennisAAMAS21,\n      author={Louise A. Dennis and Nir Oren},\n      title={Explaining BDI agent behaviour through dialogue},\n      editors={U.~Endriss and A.~Now\\'{e} and F.~Dignum and A.~Lomuscio},\n      booktitle={20th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2021)},\n      year={2021},\n      pages = {429–437},\n      note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}\n      }\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Verifiable Machine Ethics in Changing Contexts.\n \n \n \n \n\n\n \n Dennis, L. A.; Bentzen, M. M.; Lindner, F.; and Fisher, M.\n\n\n \n\n\n\n Proceedings of the AAAI Conference on Artificial Intelligence, 35(13): 11470-11478. May 2021.\n [Verifiable Autonomy, TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n \n $\"Verifiable$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DennisAAAI21,\nauthor = {Louise A. Dennis and Martin Mose Bentzen and Felix Lindner and Michael Fisher},\ntitle={Verifiable Machine Ethics in Changing Contexts},\nvolume={35},\nurl={https://ojs.aaai.org/index.php/AAAI/article/view/17366},\nnumber={13},\njournal={Proceedings of the AAAI Conference on Artificial Intelligence},\nyear={2021},\nmonth={May},\npages={11470-11478} ,\n      note={[<span class="va">Verifiable Autonomy</span>, <span class="tas_vn">TAS Verifiability Node</span>]}\n      }\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Towards a Framework for Certification of Reliable Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Mascardi, V.; Rozier, K. Y.; Schlingloff, B.; Winikoff, M.; and Yorke-Smith, N.\n\n\n \n\n\n\n Autonomous Agents and Multi Agent Systems, 35(1): 8. 2021.\n [S4, RAIN, FAIR-Space, ORCA, TAS Verifiability Node]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{FisherMRSWY21,\n  author    = {Michael Fisher and\n               Viviana Mascardi and\n               Kristin Yvonne Rozier and\n               Bernd{-}Holger Schlingloff and\n               Michael Winikoff and\n               Neil Yorke{-}Smith},\n  title     = {Towards a Framework for Certification of Reliable Autonomous Systems},\n  journal   = {Autonomous Agents and Multi Agent Systems},\n  volume    = {35},\n  number    = {1},\n  pages     = {8},\n  year      = {2021},\n  doi       = {10.1007/s10458-020-09487-2},\n  note={[<span class="s4">S4</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>,\n        <span class="orca">ORCA</span>, <span class="tas_vn">TAS Verifiability Node</span>]}\n}\n\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Integrating Formal Verification and Assurance: An Inspection Rover Case Study.\n \n \n \n\n\n \n Bourbouh, H.; Farrell, M.; Mavridou, A.; Sljivo, I.; Brat, G.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Proc. 13th International Symposium on NASA Formal Methods (NFM), volume 12673, of Lecture Notes in Computer Science, pages 53–71, 2021. Springer\n [FAIR-Space]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{BourbouhFMSBD021,\n  author    = {Hamza Bourbouh and\n               Marie Farrell and\n               Anastasia Mavridou and\n               Irfan Sljivo and\n               Guillaume Brat and\n               Louise A. Dennis and\n               Michael Fisher},\n  title     = "{Integrating Formal Verification and Assurance: An Inspection Rover\n               Case Study}",\n  booktitle = {Proc. 13th International Symposium on {NASA} Formal Methods (NFM)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {12673},\n  pages     = {53--71},\n  publisher = {Springer},\n  year      = {2021},\n  doi       = {10.1007/978-3-030-76384-8\\_4},\n  note={[<span class="fs">FAIR-Space</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Trustworthy AI.\n \n \n \n\n\n \n Chatila, R.; Dignum, V.; Fisher, M.; Giannotti, F.; Morik, K.; Russell, S.; and Yeung, K.\n\n\n \n\n\n\n In Reflections on Artificial Intelligence for Humanity, volume 12600, of Lecture Notes in Computer Science, pages 13–39. Springer, 2021.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@incollection{GFAIH21,\n  author    = {Raja Chatila and\n               Virginia Dignum and\n               Michael Fisher and\n               Fosca Giannotti and\n               Katharina Morik and\n               Stuart Russell and\n               Karen Yeung},\n  title     = "{Trustworthy AI}",\n  booktitle = {Reflections on Artificial Intelligence for Humanity},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {12600},\n  pages     = {13--39},\n  publisher = {Springer},\n  year      = {2021},\n  doi       = {10.1007/978-3-030-69128-8\\_2}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2020\n \n \n (20)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n Runtime Verification of the ARIAC competition: Can a robot be Agile and Safe at the same time?.\n \n \n \n\n\n \n Ferrando, A.; Kootbally, Z.; Piliptchak, P.; Cardoso, R. C.; Schlenoff, C.; and Fisher, M.\n\n\n \n\n\n\n In AIRO, 2020. \n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{FerrandoAIRO,\nauthor="Ferrando, Angelo\nand Kootbally, Zeid\nand Piliptchak, Pavel\nand Cardoso, Rafael C.\nand Schlenoff, Craig\nand Fisher, Michael",\ntitle="Runtime Verification of the ARIAC competition: Can a robot be Agile and Safe at the same time?",\nbooktitle="AIRO",\nyear="2020",\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Multi-scale Verification of Distributed Synchronisation.\n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n Formal Methods in Systems Design, 55(3): 171–221. 2020.\n [S4]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{GainerLDHF20,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {Multi-scale Verification of Distributed Synchronisation},\n  journal   = {Formal Methods in Systems Design},\n  volume    = {55},\n  number    = {3},\n  pages     = {171--221},\n  year      = {2020},\n  doi       = {10.1007/s10703-020-00347-z},\n  note={[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Exploring the Effects of Environmental Conditions and Design Choices on IoT Systems using Formal Methods.\n \n \n \n\n\n \n Webster, M.; Breza, M.; Dixon, C.; Fisher, M.; and McCann, J. A.\n\n\n \n\n\n\n Journal of Computational Science, 45: 101183. 2020.\n [S4]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{WebsterBDFM20,\n  author    = {Matt Webster and\n               Michael Breza and\n               Clare Dixon and\n               Michael Fisher and\n               Julie A. McCann},\n  title     = {Exploring the Effects of Environmental Conditions and Design Choices\n               on IoT Systems using Formal Methods},\n  journal   = {Journal of Computational Science},\n  volume    = {45},\n  pages     = {101183},\n  year      = {2020},\n  doi       = {10.1016/j.jocs.2020.101183},\n  note={[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Towards Compositional Verification for Modular Robotic Systems.\n \n \n \n\n\n \n Cardoso, R. C.; Dennis, L. A.; Farrell, M.; Fisher, M.; and Luckcuck, M.\n\n\n \n\n\n\n In Proceedings Second Workshop on Formal Methods for Autonomous Systems, Virtual, 7th of December 2020, volume 329, of Electronic Proceedings in Theoretical Computer Science, pages 15-22, 2020. Open Publishing Association\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Cardoso20e,\n  author    = {Cardoso, Rafael C. and Dennis, Louise A. and Farrell, Marie and Fisher, Michael and Luckcuck, Matt},\n  year      = {2020},\n  title     = {Towards Compositional Verification for Modular Robotic Systems},\n  booktitle = {Proceedings Second Workshop on\n               Formal Methods for Autonomous Systems,\n               Virtual, 7th of December 2020},\n  series    = {Electronic Proceedings in Theoretical Computer Science},\n  volume    = {329},\n  publisher = {Open Publishing Association},\n  pages     = {15-22},\n  doi       = {10.4204/EPTCS.329.2},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n A Safety Framework for Critical Systems Utilising Deep Neural Networks.\n \n \n \n\n\n \n Zhao, X.; Banks, A.; Sharp, J.; Robu, V.; Flynn, D.; Fisher, M.; and Huang, X.\n\n\n \n\n\n\n In Proc. 39th International Conference on Computer Safety, Reliability, and Security (SAFECOMP), volume 12234, of Lecture Notes in Computer Science, pages 244–259, 2020. Springer\n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{ZhaoBSRF0020,\n  author    = {Xingyu Zhao and\n               Alec Banks and\n               James Sharp and\n               Valentin Robu and\n               David Flynn and\n               Michael Fisher and\n               Xiaowei Huang},\n  title     = {A Safety Framework for Critical Systems Utilising Deep Neural Networks},\n  booktitle = {Proc. 39th International Conference on Computer Safety, Reliability, and Security (SAFECOMP)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {12234},\n  pages     = {244--259},\n  publisher = {Springer},\n  year      = 2020,\n  doi       = {10.1007/978-3-030-54549-9_16},\n  note = {[<span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; and Papacchini, F.\n\n\n \n\n\n\n In The Multi-Agent Programming Contest 2019, pages 31–58, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Cardoso20d,\nauthor="Cardoso, Rafael C.\nand Ferrando, Angelo\nand Papacchini, Fabio",\ntitle="LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest",\nbooktitle="The Multi-Agent Programming Contest 2019",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="31--58",\nisbn="978-3-030-59299-8",\ndoi={10.1007/978-3-030-59299-8_2},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent.\n \n \n \n\n\n \n Alves, G. V.; Dennis, L.; and Fisher, M.\n\n\n \n\n\n\n In Sekerinski, E.; Moreira, N.; Oliveira, J. N.; Ratiu, D.; Guidotti, R.; Farrell, M.; Luckcuck, M.; Marmsoler, D.; Campos, J.; Astarte, T.; Gonnord, L.; Cerone, A.; Couto, L.; Dongol, B.; Kutrib, M.; Monteiro, P.; and Delmas, D., editor(s), Formal Methods. FM 2019 International Workshops, pages 217–232, Cham, 2020. Springer International Publishing\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{10.1007/978-3-030-54994-7_16,\nauthor="Alves, Gleifer Vaz\nand Dennis, Louise\nand Fisher, Michael",\neditor="Sekerinski, Emil\nand Moreira, Nelma\nand Oliveira, Jos{\\'e} N.\nand Ratiu, Daniel\nand Guidotti, Riccardo\nand Farrell, Marie\nand Luckcuck, Matt\nand Marmsoler, Diego\nand Campos, Jos{\\'e}\nand Astarte, Troy\nand Gonnord, Laure\nand Cerone, Antonio\nand Couto, Luis\nand Dongol, Brijesh\nand Kutrib, Martin\nand Monteiro, Pedro\nand Delmas, David",\ntitle="Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent",\nbooktitle="Formal Methods. FM 2019 International Workshops",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="217--232",\nabstract="The design of autonomous vehicles includes obstacle detection and avoidance, route planning, speed control, etc. However, there is a lack of an explicitely representation of the rules of the road on an autonomous vehicle. Additionally, it is necessary to understand the behaviour of an autonomous vehicle in order to check whether or not it works according to the rules of the road. Here, we propose an agent-based architecture to embed the rules of the road into an agent representing the behaviour of an autonomous vehicle. We use temporal logic to formally represent the rules of the road in a way it should be possible to capture when and how a given rule of the road can be applied. Our contributions include: i. suggestion of changes in the rules of the road; ii. representation of rules in a suitable way for an autonomous vehicle agent; iii. dealing with indeterminate terms in the Highway Code.",\nisbn="978-3-030-54994-7",\nnote = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Computational Goals, Values and Decision-Making.\n \n \n \n \n\n\n \n Dennis, L. A.\n\n\n \n\n\n\n Science and Engineering Ethics. 2020.\n \n\n\n\n
\n\n\n\n \n \n $\"Computational$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{dennis_see_2020,\n\tAbstract = {Considering the popular framing of an artificial intelligence as a rational agent that always seeks to maximise its expected utility, referred to as its goal, one of the features attributed to such rational agents is that they will never select an action which will change their goal. Therefore, if such an agent is to be friendly towards humanity, one argument goes, we must understand how to specify this friendliness in terms of a utility function. Wolfhart Totschnig (Fully Autonomous AI, Science and Engineering Ethics, 2020), argues in contrast that a fully autonomous agent will have the ability to change its utility function and will do so guided by its values. This commentary examines computational accounts of goals, values and decision-making. It rejects the idea that a rational agent will never select an action that changes its goal but also argues that an artificial intelligence is unlikely to be purely rational in terms of always acting to maximise a utility function. It nevertheless also challenges the idea that an agent which does not change its goal cannot be considered fully autonomous. It does agree that values are an important component of decision-making and explores a number of reasons why.},\n\tAuthor = {Dennis, Louise A. },\n\tDa = {2020/08/04},\n\tDate-Added = {2020-08-06 13:39:55 +0100},\n\tDate-Modified = {2020-08-06 13:39:55 +0100},\n\tDoi = {10.1007/s11948-020-00244-y},\n\tId = {Dennis2020},\n\tIsbn = {1471-5546},\n\tJournal = {Science and Engineering Ethics},\n\tTitle = {Computational Goals, Values and Decision-Making},\n\tTy = {JOUR},\n\tUrl = {https://doi.org/10.1007/s11948-020-00244-y},\n\tYear = {2020},\n\tBdsk-Url-1 = {https://doi.org/10.1007/s11948-020-00244-y}}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Ethical Governor Systems viewed as a Multi-Agent Problem.\n \n \n \n \n\n\n \n Cardoso, R. C.; Ene, D.; Evans, T.; and Dennis, L. A.\n\n\n \n\n\n\n In Nallur, V., editor(s), Second Workshop on Implementing Machine Ethics, June 2020. Zenodo\n [RAIN]\n\n\n\n
\n\n\n\n \n \n $\"Ethical$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{cardosoime,\n  author = {Rafael C. Cardoso and Daniel Ene and Tom Evans and Louise A. Dennis},\n  title = {Ethical Governor Systems viewed as a Multi-Agent Problem},\n  editor       = {Vivek Nallur},\n  booktitle        = {Second Workshop on Implementing Machine Ethics},\n  month        = jun,\n  year         = 2020,\n  publisher    = {Zenodo},\n  doi          = {10.5281/zenodo.3938851},\n  url          = {https://doi.org/10.5281/zenodo.3938851},\n  note = {[<span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n First Steps towards an Ethical Agent for checking decision and behaviour for an Autonomous Vehicle on the Rules of the Road.\n \n \n \n \n\n\n \n Alves, G. V.; Dennis, L.; and Fisher, M.\n\n\n \n\n\n\n In Nallur, V., editor(s), Second Workshop on Implementing Machine Ethics, June 2020. Zenodo\n \n\n\n\n
\n\n\n\n \n \n $\"First$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{alvesime,\n  author = {Gleifer Vaz Alves and Louise Dennis and Michael Fisher},\n  title = {First Steps towards an Ethical Agent for checking decision and behaviour for an Autonomous Vehicle on the Rules of the Road},\n  editor       = {Vivek Nallur},\n  booktitle        = {Second Workshop on Implementing Machine Ethics},\n  month        = jun,\n  year         = 2020,\n  publisher    = {Zenodo},\n  doi          = {10.5281/zenodo.3938851},\n  url          = {https://doi.org/10.5281/zenodo.3938851}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Adaptable and Verifiable BDI Reasoning.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Huang, X.; and Dennis, L. A.\n\n\n \n\n\n\n In Proceedings of the First Workshop on Agents and Robots for reliable Engineered Autonomy, Virtual event, 4th September 2020, volume 319, of Electronic Proceedings in Theoretical Computer Science, pages 117-125, 2020. Open Publishing Association\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@Inproceedings{Stringer20a,\n  author    = {Stringer, Peter and Cardoso, Rafael C. and Huang, Xiaowei and Dennis, Louise A.},\n  year      = {2020},\n  title     = {Adaptable and Verifiable BDI Reasoning},\n  booktitle = {Proceedings of the First Workshop on\n               Agents and Robots for reliable Engineered Autonomy,\n                Virtual event, 4th September 2020},\n  series    = {Electronic Proceedings in Theoretical Computer Science},\n  volume    = {319},\n  publisher = {Open Publishing Association},\n  pages     = {117-125},\n  doi       = {10.4204/EPTCS.319.9},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Verification and Validation for Space Robotics.\n \n \n \n\n\n \n Cardoso, R. C.; Farrell, M.; Kourtis, G.; Webster, M.; Dennis, L. A.; Dixon, C.; Fisher, M.; and Lisitsa, A.\n\n\n \n\n\n\n 2020.\n Poster presented at the Opportunities and Challenges in Space Robotics Workshop held with ICRA 2020. [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@unpublished{Cardoso20c,\n  author    = {Cardoso, R. C. and Farrell, M. and Kourtis, G. and Webster, M. and Dennis, L. A. and Dixon, C. and Fisher, M. and Lisitsa, A.},\n  title     = {Verification and Validation for Space Robotics},\n  year      = {2020},\n  note = {Poster presented at the Opportunities and Challenges in Space Robotics Workshop held with ICRA 2020. [<span class="fs">FAIR-SPACE</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n ROSMonitoring: A Runtime Verification Framework for ROS.\n \n \n \n\n\n \n Ferrando, A.; Cardoso, R. C.; Fisher, M.; Ancona, D.; Franceschini, L.; and Mascardi, V.\n\n\n \n\n\n\n In Towards Autonomous Robotic Systems, pages 387–399, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 15 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Ferrando20a,\nauthor="Ferrando, Angelo\nand Cardoso, Rafael C.\nand Fisher, Michael\nand Ancona, Davide\nand Franceschini, Luca\nand Mascardi, Viviana",\ntitle="ROSMonitoring: A Runtime Verification Framework for ROS",\nbooktitle="Towards Autonomous Robotic Systems",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="387--399",\ndoi="10.1007/978-3-030-63486-5_40",\nisbn="978-3-030-63486-5",\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Verifiable Self-Aware Agent-Based Autonomous Systems.\n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n Proceedings of the IEEE special issue on Self-Aware Autonomous Systems,1011-1026. 2020.\n [Verifiable Autonomy, FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{dennis_ieee20,\n  author={Louise A. Dennis and Michael Fisher},\n  title ={Verifiable Self-Aware Agent-Based Autonomous Systems},\n  journal={Proceedings of the IEEE special issue on Self-Aware Autonomous Systems},\n  pages={1011-1026},\n  doi={10.1109/JPROC.2020.2991262},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]},\nyear=2020}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Model-Checking Information Diffusion in Social Networks with PRISM.\n \n \n \n\n\n \n Dennis, L. A.; and Slavkovik, M.\n\n\n \n\n\n\n In Bassiliades, N.; Chalkiadakis, G.; and de Jonge, D., editor(s), Multi-Agent Systems and Agreement Technologies, pages 475–492, Cham, 2020. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Dennis20,\n  author="Dennis, Louise A.\nand Slavkovik, Marija",\neditor="Bassiliades, Nick\nand Chalkiadakis, Georgios\nand de Jonge, Dave",\ntitle="Model-Checking Information Diffusion in Social Networks with PRISM",\nbooktitle="Multi-Agent Systems and Agreement Technologies",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="475--492",\nabstract="In this paper we present an agent-based approach to formalising information diffusion using Markov models which attempts to account for the internal informational state of the agent and investigate the use of probabilistic model-checking for analysing these models. We model information diffusion as both continuous and discrete time Markov chains, using the latter to provide an agent-centred perspective. We present a negative result - we conclude that current model-checking technology is inadequate for analysing such systems in an interesting way.",\nisbn="978-3-030-66412-1"\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n An Interface for Programming Verifiable Autonomous Agents in ROS.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Bassiliades, N.; Chalkiadakis, G.; and de Jonge, D., editor(s), Multi-Agent Systems and Agreement Technologies, pages 191–205, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Cardoso20b,\n  author="Cardoso, Rafael C.\nand Ferrando, Angelo\nand Dennis, Louise A.\nand Fisher, Michael",\neditor="Bassiliades, Nick\nand Chalkiadakis, Georgios\nand de Jonge, Dave",\ntitle="An Interface for Programming Verifiable Autonomous Agents in ROS",\nbooktitle="Multi-Agent Systems and Agreement Technologies",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="191--205",\nabstract="Autonomy has been one of the most desirable features for robotic applications in recent years. This is evidenced by a recent surge of research in autonomous driving cars, strong government funding for research in robotics for extreme environments, and overall progress in service robots. Autonomous decision-making is often at the core of these systems, thus, it is important to be able to verify and validate properties that relate to the correct behaviour that is expected of the system. Our main contribution in this paper, is an interface for integrating BDI-based agents into robotic systems developed using ROS. We use the Gwendolen language to program our BDI agents and to make use of the AJPF model checker in order to verify properties related to the decision-making in the agent programs. Our case studies include 3D simulations using a simple autonomous patrolling behaviour of a TurtleBot, and multiple TurtleBots servicing a house that can cooperate with each other in case of failure.",\nisbn="978-3-030-66412-1",\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Heterogeneous Verification of an Autonomous Curiosity Rover.\n \n \n \n\n\n \n Cardoso, R. C.; Farrell, M.; Luckcuck, M.; Ferrando, A.; and Fisher, M.\n\n\n \n\n\n\n In Lee, R.; Jha, S.; Mavridou, A.; and Giannakopoulou, D., editor(s), NASA Formal Methods, pages 353–360, Cham, 2020. Springer International Publishing\n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Cardoso20a,\nauthor="Cardoso, Rafael C.\nand Farrell, Marie\nand Luckcuck, Matt\nand Ferrando, Angelo\nand Fisher, Michael",\neditor="Lee, Ritchie\nand Jha, Susmit\nand Mavridou, Anastasia\nand Giannakopoulou, Dimitra",\ntitle="Heterogeneous Verification of an Autonomous Curiosity Rover",\nbooktitle="NASA Formal Methods",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="353--360",\nabstract="The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4--24 min for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance.",\nisbn="978-3-030-55754-6",\ndoi="10.1007/978-3-030-55754-6_20",\nnote = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Reliable Decision-Making in Autonomous Vehicles.\n \n \n \n \n\n\n \n Alves, G. V.; Dennis, L.; Fernandes, L.; and Fisher, M.\n\n\n \n\n\n\n In Leitner, A.; Watzenig, D.; and Ibanez-Guzman, J., editor(s), Validation and Verification of Automated Systems: Results of the ENABLE-S3 Project, pages 105–117. Springer International Publishing, Cham, 2020.\n \n\n\n\n
\n\n\n\n \n \n $\"Reliable$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 9 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@incollection{Alves2020,\nauthor="Alves, Gleifer Vaz\nand Dennis, Louise\nand Fernandes, Lucas\nand Fisher, Michael",\neditor="Leitner, Andrea\nand Watzenig, Daniel\nand Ibanez-Guzman, Javier",\ntitle="Reliable Decision-Making in Autonomous Vehicles",\nbookTitle="Validation and Verification of Automated Systems: Results of the ENABLE-S3 Project",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="105--117",\nabstract="The use of Autonomous Vehicles (AVs) on our streets is soon to be a reality; increasingly, interacting with such AVs will be part of our daily routine. However, we will certainly need to assure the reliable behaviour of an AV, especially when some unexpected scenarios (e.g. harsh environments, obstacles, emergencies) are taken into account. In this article we use an intelligent agent approach to capture the high-level decision-making process within an AV and then use formal verification techniques to automatically, and strongly, analyse the required behaviours. Specifically, we use the MCAPL framework, wherein our core agent is implemented using the GWENDOLEN agent programming language, and to which we can apply model checking via the AJPF model checker. By performing such formal verification on our agent, we are able to prove that the AV's decision-making process, embedded within the GWENDOLEN agent plans, matches our requirements. As examples, we will verify (formal) properties in order to determine whether the agent behaves in a reliable manner through three different levels of emergency displayed in a simple urban traffic environment.",\nisbn="978-3-030-14628-3",\ndoi="10.1007/978-3-030-14628-3_10",\nurl="https://doi.org/10.1007/978-3-030-14628-3_10"\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n The ``Why Did You Do That?'' Button: Answering Why-Questions for End Users of Robotic Systems.\n \n \n \n\n\n \n Koeman, V. J.; Dennis, L. A.; Webster, M.; Fisher, M.; and Hindriks, K.\n\n\n \n\n\n\n In Dennis, L. A.; Bordini, R. H.; and Lespérance, Y., editor(s), Engineering Multi-Agent Systems, pages 152–172, Cham, 2020. Springer International Publishing\n [ORCA, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Koeman19EMAS,\nauthor="Koeman, Vincent J.\nand Dennis, Louise A.\nand Webster, Matt\nand Fisher, Michael\nand Hindriks, Koen",\neditor="Dennis, Louise A.\nand Bordini, Rafael H.\nand Lesp{\\'e}rance, Yves",\ntitle="The ``Why Did You Do That?'' Button: Answering Why-Questions for End Users of Robotic Systems",\nbooktitle="Engineering Multi-Agent Systems",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="152--172",\nabstract="The issue of explainability for autonomous systems is becoming increasingly prominent. Several researchers and organisations have advocated the provision of a ``Why did you do that?'' button which allows a user to interrogate a robot about its choices and actions. We take previous work on debugging cognitive agent programs and apply it to the question of supplying explanations to end users in the form of answers to why-questions. These previous approaches are based on the generation of a trace of events in the execution of the program and then answering why-questions using the trace. We implemented this framework in the agent infrastructure layer and, in particular, the Gwendolen programming language it supports -- extending it in the process to handle the generation of applicable plans and multiple intentions. In order to make the answers to why-questions comprehensible to end users we advocate a two step process in which first a representation of an explanation is created and this is subsequently converted into natural language in a way which abstracts away from some events in the trace and employs application specific predicate dictionaries in order to translate the first-order logic presentation of concepts within the cognitive agent program in natural language. A prototype implementation of these ideas is provided.",\nisbn="978-3-030-51417-4",\n  note = {[<span class="orca">ORCA</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Plan Library Reconfigurability in BDI Agents.\n \n \n \n\n\n \n Cardoso, R. C.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Dennis, L. A.; Bordini, R. H.; and Lespérance, Y., editor(s), Engineering Multi-Agent Systems, pages 195–212, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Cardoso19EMAS,\nauthor="Cardoso, Rafael C.\nand Dennis, Louise A.\nand Fisher, Michael",\neditor="Dennis, Louise A.\nand Bordini, Rafael H.\nand Lesp{\\'e}rance, Yves",\ntitle="Plan Library Reconfigurability in BDI Agents",\nbooktitle="Engineering Multi-Agent Systems",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="195--212",\nabstract="One of the major advantages of modular architectures in robotic systems is the ability to add or replace nodes, without needing to rearrange the whole system. In this type of system, autonomous agents can aid in the decision making and high-level control of the robot. For example, a robot may have a module for each of the effectors and sensors that it has and an agent with a plan library containing high-level plans to aid in the decision making within these modules. However, when autonomously replacing a node it can be difficult to reconfigure plans in the agent's plan library while retaining correctness. In this paper, we exploit the formal concept of capabilities in Belief-Desire-Intention agents and describe how agents can reason about these capabilities in order to reconfigure their plan library while retaining overall correctness constraints. To validate our approach, we show the implementation of our framework and an experiment using a practical example in the Mars rover scenario.",\nisbn="978-3-030-51417-4",\ndoi="10.1007/978-3-030-51417-4_10",\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n

\n \n 2019\n \n \n (12)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n Analysis of Autonomous Mobile Collectives in Complex Physical Environments (Dagstuhl Seminar 19432).\n \n \n \n \n\n\n \n Gleirscher, M.; Haxthausen, A. E.; Leucker, M.; and Linker, S.\n\n\n \n\n\n\n Dagstuhl Reports, 9(10): 95–116. 2019.\n [S4]\n\n\n\n
\n\n\n\n \n \n $\"Analysis$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{Linker2019b,\n  author    = {Mario Gleirscher and\n               Anne E. Haxthausen and\n               Martin Leucker and\n               Sven Linker},\n  title     = {Analysis of Autonomous Mobile Collectives in Complex Physical Environments\n               (Dagstuhl Seminar 19432)},\n  journal   = {Dagstuhl Reports},\n  volume    = {9},\n  number    = {10},\n  pages     = {95--116},\n  year      = {2019},\n  url       = {https://doi.org/10.4230/DagRep.9.10.95},\n  doi       = {10.4230/DagRep.9.10.95},\n  note = {[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Target counting with Presburger constraints and its application in sensor networks.\n \n \n \n \n\n\n \n Linker, S.; and Sevegnani, M.\n\n\n \n\n\n\n Proceedings of the Royal Society A, 475(2231). 2019.\n [S4]\n\n\n\n
\n\n\n\n \n \n $\"Target$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{Linker2019a,\nauthor = {Sven Linker and Michele Sevegnani},\ntitle = {Target counting with Presburger constraints and its application in sensor networks},\njournal = {Proceedings of the Royal Society A},\nvolume = {475},\nnumber = {2231},\nyear = {2019},\nurl = {https://doi.org/10.1098/rspa.2019.0278},\ndoi = {10.1098/rspa.2019.0278},\n  note = {[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Modular Verification of Autonomous Space Robotics.\n \n \n \n\n\n \n Farrell, M.; Cardoso, R. C.; Dennis, L.; Dixon, C.; Fisher, M.; Kourtis, G.; Lisitsa, A.; Luckcuck, M.; and Webster, M\n\n\n \n\n\n\n In Assurance of Autonomy for Robotic Space Missions Workshop, 2019. \n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Farrell2019b,\n  author    = {Farrell, M. and Cardoso, R. C. and Dennis, L. and Dixon, C. and Fisher, M. and Kourtis, G. and Lisitsa, A. and Luckcuck, M. and Webster, M},\n  title     = {Modular Verification of Autonomous Space Robotics},\n  booktitle = {Assurance of Autonomy for Robotic Space Missions Workshop},\n  year      = {2019},\n  note = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages.\n \n \n \n\n\n \n Farrell, M.; Bradbury, M.; Fisher, M.; Dennis, L. A.; Dixon, C.; Yuan, H.; and Maple, C.\n\n\n \n\n\n\n In Ölveczky, P. C.; and Salaün, G., editor(s), Software Engineering and Formal Methods, pages 471–490, Cham, 2019. Springer International Publishing\n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Farrell2019,\nauthor="Farrell, Marie\nand Bradbury, Matthew\nand Fisher, Michael\nand Dennis, Louise A.\nand Dixon, Clare\nand Yuan, Hu\nand Maple, Carsten",\neditor="{\\"O}lveczky, Peter Csaba\nand Sala{\\"u}n, Gwen",\ntitle="Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages",\nbooktitle="Software Engineering and Formal Methods",\nyear="2019",\npublisher="Springer International Publishing",\naddress="Cham",\npages="471--490",\nabstract="Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.",\nisbn="978-3-030-30446-1",\nnote = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n A Summary of Formal Specification and Verification of Autonomous Robotic Systems.\n \n \n \n\n\n \n Luckcuck, M.; Farrell, M.; Dennis, L. A.; Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n In Ahrendt, W.; and Tapia Tarifa, S. L., editor(s), Integrated Formal Methods, pages 538–541, Cham, 2019. Springer International Publishing\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Luckcuck2019Summary,\nauthor="Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael",\neditor="Ahrendt, Wolfgang and Tapia Tarifa, Silvia Lizeth",\ntitle="A Summary of Formal Specification and Verification of Autonomous Robotic Systems",\nbooktitle="Integrated Formal Methods",\nyear="2019",\npublisher="Springer International Publishing",\naddress="Cham",\ndoi = {10.1007/978-3-030-34968-4_33},\npages="538--541",\nabstract="Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions published in [5], which surveys the state-of-the-art in formal specification and verification for autonomous robotics.",\nisbn="978-3-030-34968-4",\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Formal Specification and Verification of Autonomous Robotic Systems: A Survey.\n \n \n \n \n\n\n \n Luckcuck, M.; Farrell, M.; Dennis, L. A.; Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n ACM Comput. Surv., 52(5): 1–41. sep 2019.\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n \n $\"Formal$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{Luckcuck2019,\ntitle = {{Formal Specification and Verification of Autonomous Robotic Systems: A Survey}},\nauthor = {Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael},\ndoi = {10.1145/3342355},\neprint = {1807.00048},\nissn = {03600300},\njournal = {ACM Comput. Surv.},\nmonth = {sep},\nnumber = {5},\npages = {1--41},\nurl = {https://arxiv.org/abs/1807.00048 http://dl.acm.org/citation.cfm?doid=3362097.3342355},\nvolume = {52},\nyear = {2019},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Probabilistic Model Checking of Robots Deployed in Extreme Environments.\n \n \n \n \n\n\n \n Zhao, X.; Robu, V.; Flynn, D.; Dinmohammadi, F.; Fisher, M.; and Webster, M.\n\n\n \n\n\n\n In Proc. 23rd AAAI Conference on Artificial Intelligence, pages 8066–8074, 2019. AAAI Press\n [ORCA]\n\n\n\n
\n\n\n\n \n \n $\"Probabilistic$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{ZhaoRFD0W19,\n  author    = {Xingyu Zhao and\n               Valentin Robu and\n               David Flynn and\n               Fateme Dinmohammadi and\n               Michael Fisher and\n               Matt Webster},\n  title     = {Probabilistic Model Checking of Robots Deployed in Extreme Environments},\n  booktitle = {Proc. 23rd {AAAI} Conference on Artificial Intelligence},\n  pages     = {8066--8074},\n  year      = {2019},\n  publisher = {{AAAI} Press},\n  url       = {https://www.aaai.org/Library/AAAI/aaai19contents.php},\n  note = {[<span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Towards a Methodology to Test UAVs in Hazardous Environments.\n \n \n \n \n\n\n \n Page, V.; Webster, M.; Fisher, M.; and Jump, M.\n\n\n \n\n\n\n In ICAS 2019, The Fifteenth International Conference on Autonomic and Autonomous Systems, pages 38–45, June 2019. \n \n\n\n\n
\n\n\n\n \n \n $\"Towards$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Page19ICAS,\n  author    = {Page, Vincent and Webster, Matt and Fisher, Michael and Jump, Mike},\n  title     = {Towards a {Methodology} to {Test} {UAVs} in {Hazardous} {Environments}},\n  booktitle = {ICAS 2019, The Fifteenth International Conference on Autonomic and Autonomous Systems},\n  year      = {2019},\n  pages     = {38--45},\n  month     = jun,\n  isbn      = {978-1-61208-712-2},\n  url       = {http://www.thinkmind.org/index.php?view=article&articleid=icas_2019_3_20_28007},\n  urldate   = {2019-06-12},\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n On Enactability of Agent Interaction Protocols: Towards a Unified Approach.\n \n \n \n\n\n \n Ferrando, A.; Winikoff, M.; Cranefield, S.; Dignum, F.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. of the 7th International Workshop on Engineering Multi-Agent Systems (EMAS), 2019. \n [ORCA, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{Ferrando19EMAS,\n  author    = {Angelo Ferrando and Michael Winikoff and Stephen Cranefield and Frank Dignum and Viviana Mascardi},\n  title     = {On Enactability of Agent Interaction Protocols: Towards a Unified Approach},\n  booktitle = {Proc. of the 7th International Workshop on Engineering Multi-Agent Systems (EMAS)},\n  year      = {2019},\n  note = {[<span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n On Proactive, Transparent, and Verifiable Ethical Reasoning for Robots.\n \n \n \n\n\n \n Bremner, P.; Dennis, L. A.; Fisher, M.; and Winfield, A. F.\n\n\n \n\n\n\n Proceedings of the IEEE,1-21. 2019.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n

@ARTICLE{BremnerDFW19,\nauthor={P. {Bremner} and L. A. {Dennis} and M. {Fisher} and A. F. {Winfield}},\njournal={Proceedings of the IEEE},\ntitle={On Proactive, Transparent, and Verifiable Ethical Reasoning for Robots},\nyear={2019},\nvolume={},\nnumber={},\npages={1-21},\nkeywords={Robots;Cognition;Ethics;Predictive models;Safety;Standards;Computer architecture;Ethics;formal verification;intelligent robots;software architecture.},\ndoi={10.1109/JPROC.2019.2898267},\nISSN={0018-9219},\nmonth={},\nnote = {[<span  class="va">Verifiable Autonomy</span>]}}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Decentralised Planning for Multi-Agent Programming Platforms.\n \n \n \n\n\n \n Cardoso, R. C.; and Bordini, R. H.\n\n\n \n\n\n\n In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, of AAMAS '19, pages 799–807, Richland, SC, 2019. International Foundation for Autonomous Agents and Multiagent Systems\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n\n\n\n

@inproceedings{Cardoso19AAMAS,\nauthor = {Cardoso, Rafael C. and Bordini, Rafael H.},\ntitle = {Decentralised Planning for Multi-Agent Programming Platforms},\nyear = {2019},\nisbn = {9781450363099},\npublisher = {International Foundation for Autonomous Agents and Multiagent Systems},\naddress = {Richland, SC},\nbooktitle = {Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems},\npages = {799–807},\nnumpages = {9},\nkeywords = {multi-agent development platforms, multi-agent planning, hierarchical task network, goal allocation},\nlocation = {Montreal QC, Canada},\nseries = {AAMAS '19},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Slicing Agent Programs for more Efficient Verification.\n \n \n \n\n\n \n Winikoff, M.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Weyns, D.; Mascardi, V.; and Ricci, A., editor(s), Proc. 6th International Workshop in Engineering Multi-Agent Systems, volume 11375, of Lecture Notes in Computer Science, pages 139-157, Stockholm, Sweden, 2019. \n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{WinikoffDF:EMAS18,\n   author = {Michael Winikoff and Louise A. Dennis and Michael Fisher},\n   title = "{Slicing Agent Programs for more Efficient Verification}",\nbooktitle = {Proc. 6th International Workshop in Engineering Multi-Agent Systems},\nyear = {2019},\nvolume={11375},\npages={139-157},\neditor={D. Weyns and V. Mascardi and A. Ricci},\nseries={Lecture Notes in Computer Science},\naddress = {Stockholm, Sweden},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2018\n \n \n (22)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n Verifiable Self-Certifying Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Collins, E.; Dennis, L. A.; Luckcuck, M.; Webster, M.; Jump, M.; Page, V.; Patchett, C.; Dinmohammadi, F.; Flynn, D.; Robu, V.; and Zhao, X.\n\n\n \n\n\n\n In 2018 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pages 341-348, Oct 2018. \n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{8539217,\n  author    = {Michael Fisher and Emily Collins and Louise A. Dennis and Matt Luckcuck and Matthew Webster and Michael Jump and Vincent Page and Charles Patchett and Fateme Dinmohammadi\n            and David Flynn and Valentin Robu and Xingu Zhao},\n  title     = {Verifiable Self-Certifying Autonomous Systems},\n  booktitle = {2018 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)},\n  year      = {2018},\n  pages     = {341-348},\n  month     = {Oct},\n  doi       = {10.1109/ISSREW.2018.00028},\n  note = {[<span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments.\n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In 2018. Springer\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{NalonHD18,\nauthor = {Cl\\'audia Nalon and Ullrich Hustadt and Clare Dixon},\ntitle = "{KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments}",\njournal = {Journal of Automated Reasoning},\nyear = {2018},\n  volume    = {},\npublisher = {Springer},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks.\n \n \n \n\n\n \n Webster, M.; Breza, M.; Dixon, C.; Fisher, M.; and McCann, J.\n\n\n \n\n\n\n Electronic Communications of the EASST. 2018.\n [FAIR-SPACE, ORCA, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{WebsterBDFM18,\n  author    =  {Matthew Webster and Michael Breza and Clare Dixon and Michael Fisher and Julie McCann},\n  title     = {Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks},\n  journal   = {Electronic Communications of the EASST},\n  volume    = {},\n  year      = {2018},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Making Sense of the World: Framing Models for Trustworthy Sensor-Driven Systems.\n \n \n \n\n\n \n Calder, M.; Dobson, S.; Fisher, M.; and McCann, J. A.\n\n\n \n\n\n\n Computers, 7(4): 62. 2018.\n [S4]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{CalderDFM18,\n  author    = {Muffy Calder and\n               Simon Dobson and\n               Michael Fisher and\n               Julie A. McCann},\n  title     = "{Making Sense of the World: Framing Models for Trustworthy Sensor-Driven\n               Systems}",\n  journal   = {Computers},\n  volume    = {7},\n  number    = {4},\n  pages     = {62},\n  year      = {2018},\n  doi       = {10.3390/computers7040062},\n  note = {[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics.\n \n \n \n \n\n\n \n Hustadt, U.; Nalon, C.; and Dixon, C.\n\n\n \n\n\n\n In Konev, B.; Urban, J.; and Rümmer, P., editor(s), Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR), of CEUR Workshop Proceedings, pages 34–48, Aachen, 2018. \n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n \n $\"Evaluating$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{HustadtEtAl:PAAR2018,\nauthor = {Ullrich Hustadt and Cl\\'audia Nalon and Clare Dixon},\ntitle = "{Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics}",\nbooktitle = {Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)},\nyear = {2018},\npages = {34--48},\neditor = {Boris Konev and Josef Urban and Philipp R\\"ummer},\nnumber = 2162,\nseries = {CEUR Workshop Proceedings},\naddress = {Aachen},\nissn = {1613-0073},\nurl = {http://ceur-ws.org/Vol-2162/#paper-04},\nvenue = {Oxford, UK},\neventdate = {2018-07-19},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Machines That Know Right And Cannot Do Wrong: The Theory and Practice of Machine Ethics.\n \n \n \n \n\n\n \n Dennis, L. A.; and Slavkovik, M.\n\n\n \n\n\n\n IEEE Intelligent Informatics Bulletin, 19(1). 2018.\n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Machines$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{dennis18iib,\n  author = {Louise A. Dennis and Marija Slavkovik},\n  title = {Machines That Know Right And Cannot Do Wrong: The Theory and Practice of Machine Ethics},\n  journal = {IEEE Intelligent Informatics Bulletin},\n  volume = 19,\n  number = 1,\n  year = 2018,\n  url = {http://www.comp.hkbu.edu.hk/~cib/2018/Aug/article2/iib_vol19no1_article2.pdf},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Verifying and Validating Autonomous Systems: an Integrated Approach.\n \n \n \n\n\n \n Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. 8th IEEE International Conference on Runtime Verification (RV), 2018. \n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Ferrando:RV18,\n   author = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi},\n    title = "{Verifying and Validating Autonomous Systems: an Integrated Approach}",\nbooktitle = {Proc. 8th IEEE International Conference on Runtime\n                  Verification (RV)},\nyear = {2018},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Robotics and Integrated Formal Methods: Necessity Meets Opportunity.\n \n \n \n \n\n\n \n Farrell, M.; Luckcuck, M.; and Fisher, M.\n\n\n \n\n\n\n In Furia, C. A.; and Winter, K., editor(s), Proc. 14th International Conference on Integrated Formal Methods (iFM), volume 11023, of Lecture Notes in Computer Science, pages 161-171, 2018. Springer\n [FAIR-SPACE, ORCA, RAIN]\n\n\n\n
\n\n\n\n \n \n $\"Robotics$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{FarrellLF:IFM018,\n  author    = {Marie Farrell and Matt Luckcuck and Michael Fisher},\n  editor    = {Carlo A. Furia and Kirsten Winter},\n  title     = {Robotics and Integrated Formal Methods: Necessity Meets Opportunity},\n  booktitle = {Proc. 14th International Conference on Integrated\n               Formal Methods (iFM)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {11023},\n  pages     = {161-171},\n  publisher = {Springer},\n  year      = {2018},\n  url       = {https://doi.org/10.1007/978-3-319-98938-9_10},\n  doi       = {10.1007/978-3-319-98938-9_10},\n  biburl    = {https://dblp.org/rec/bib/conf/ifm/FarrellL018},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Clarification of Ambiguity for the Simple Authentication and Security Layer.\n \n \n \n \n\n\n \n Al-Shareefi, F.; Lisitsa, A.; and Dixon, C.\n\n\n \n\n\n\n In Butler, M. J.; Raschke, A.; Hoang, T. S.; and Reichl, K., editor(s), Proc. 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ), volume 10817, of Lecture Notes in Computer Science, pages 189-203, 2018. Springer\n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n \n $\"Clarification$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{AlShareefiLD:ABZ18,\n  author    = {Farah Al{-}Shareefi and\n               Alexei Lisitsa and Clare Dixon},\n  editor    = {Michael J. Butler and\n               Alexander Raschke and\n               Thai Son Hoang and\n               Klaus Reichl},\n  title     = "{Clarification of Ambiguity for the Simple Authentication\n                and Security  Layer}",\n  booktitle = {Proc. 6th International Conference on Abstract\n               State Machines, Alloy, B, TLA, VDM, and {Z} (ABZ)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {10817},\n  pages     = {189-203},\n  publisher = {Springer},\n  year      = {2018},\n  url       = {https://doi.org/10.1007/978-3-319-91271-4\\_13},\n  doi       = {10.1007/978-3-319-91271-4\\_13},\n  biburl    = {https://dblp.org/rec/bib/conf/asm/Al-ShareefiLD18},\n  note = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Verifiable Self-Certifying Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Collins, E.; Dennis, L. A.; Luckcuck, M.; Webster, M.; Jump, M.; Page, V.; Patchett, C.; Dinmohammadi, F.; Flynn, D.; Robu, V.; and Zhao, X.\n\n\n \n\n\n\n In Proc. 8th IEEE International Workshop on Software Certification (WoSoCer), Memphis, USA, 2018. \n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@InProceedings{Fisher:WoSoCer18,\n   author = {Michael Fisher and Emily Collins and Louise A. Dennis and Matt Luckcuck and Matthew Webster and Michael Jump and Vincent Page and Charles Patchett and Fateme Dinmohammadi\n            and David Flynn and Valentin Robu and Xingu Zhao},\n    title = "{Verifiable Self-Certifying Autonomous Systems}",\nbooktitle = {Proc. 8th IEEE International Workshop on Software Certification (WoSoCer)},\nyear = {2018},\naddress = {Memphis, USA},\nnote = {[<span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n Certification of Safe and Trusted Robotic Inspection of Assets.\n \n \n \n\n\n \n Dinmohammadi, F.; Flynn, D.; Fisher, M.; Jump, M.; Page, V.; Robu, V.; Patchett, C.; Tang, W.; and Webster, M.\n\n\n \n\n\n\n In Proc. Prognostics and System Health Management Conference (PHM-Chongqing), Chongqing, China, 2018. IEEE\n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@INPROCEEDINGS{Dinmohammadi:PHM18,\nauthor={Fateme Dinmohammadi and David Flynn and Michael Fisher and Michael Jump and Vincent Page and Valentin Robu and Charles Patchett and Wenshuo Tang and Matthew Webster},\nbooktitle={Proc. Prognostics and System Health Management\n     Conference (PHM-Chongqing)},\ntitle="{Certification of Safe and Trusted Robotic Inspection of Assets}",\nyear={2018},\nvolume={},\nnumber={},\naddress = {Chongqing, China},\npages={},\npublisher = {IEEE},\nnote = {[<span class="orca">ORCA</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Recognising Assumption Violations in Autonomous Systems Verification.\n \n \n \n \n\n\n \n Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. 17th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), pages 1933–1935, 2018. IFAAMAS/ACM\n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Recognising$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{FerrandoDA0M18,\n  author    = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi},\n  title     = "{Recognising Assumption Violations in Autonomous Systems Verification}",\n  booktitle = {Proc. 17th International Conference on Autonomous Agents\n               and MultiAgent Systems (AAMAS)},\n  pages     = {1933--1935},\n  year      = {2018},\n  publisher = {IFAAMAS/ACM},\n  url       = {http://dl.acm.org/citation.cfm?id=3238028},\n  timestamp = {Mon, 16 Jul 2018 09:21:17 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/atal/FerrandoDA0M18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time.\n \n \n \n \n\n\n \n Kamali, M.; Linker, S.; and Fisher, M.\n\n\n \n\n\n\n In Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2018. \n [FAIR-SPACE,S4,Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Modular$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{KamaliLF:FTSCS18,\n  author    = {Maryam Kamali and Sven Linker and Michael Fisher},\n  title     = "{Modular Verification of Vehicle Platooning with Respect to Decisions,\n               Space and Time}",\n  booktitle = {Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1804.06647},\n  note = {[<span class="fs">FAIR-SPACE</span>,<span class="s4">S4</span>,<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators.\n \n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n In Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings, pages 160–176, 2018. \n [S4]\n\n\n\n
\n\n\n\n \n \n $\"The$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/icfem/GainerLDH018,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption\n               in Networks of Pulse-Coupled Oscillators},\n  booktitle = {Formal Methods and Software Engineering - 20th International Conference\n               on Formal Engineering Methods, {ICFEM} 2018, Gold Coast, QLD, Australia,\n               November 12-16, 2018, Proceedings},\n  pages     = {160--176},\n  year      = {2018},\n  crossref  = {DBLP:conf/icfem/2018},\n  url       = {https://doi.org/10.1007/978-3-030-02450-5\\_10},\n  doi       = {10.1007/978-3-030-02450-5\\_10},\n  timestamp = {Mon, 05 Nov 2018 11:04:23 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/icfem/GainerLDH018},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Multi-Scale Verification of Distributed Synchronisation.\n \n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n CoRR, abs/1809.10655. 2018.\n [S4]\n\n\n\n
\n\n\n\n \n \n $\"Multi-Scale$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/abs-1809-10655,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {Multi-Scale Verification of Distributed Synchronisation},\n  journal   = {CoRR},\n  volume    = {abs/1809.10655},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1809.10655},\n  archivePrefix = {arXiv},\n  eprint    = {1809.10655},\n  timestamp = {Fri, 05 Oct 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1809-10655},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n The MCAPL Framework including the Agent Infrastructure Layer an Agent Java Pathfinder.\n \n \n \n \n\n\n \n Dennis, L. A.\n\n\n \n\n\n\n J. Open Source Software, 3(24): 617. 2018.\n \n\n\n\n
\n\n\n\n \n \n $\"The$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/jossw/Dennis18,\n  author    = {Louise A. Dennis},\n  title     = {The {MCAPL} Framework including the Agent Infrastructure Layer an\n               Agent Java Pathfinder},\n  journal   = {J. Open Source Software},\n  volume    = {3},\n  number    = {24},\n  pages     = {617},\n  year      = {2018},\n  url       = {https://doi.org/10.21105/joss.00617},\n  doi       = {10.21105/joss.00617},\n  timestamp = {Tue, 13 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/jossw/Dennis18},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Two-stage agent program verification.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; and Webster, M.\n\n\n \n\n\n\n J. Log. Comput., 28(3): 499–523. 2018.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Two-stage$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/logcom/Dennis0W18,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Matt Webster},\n  title     = {Two-stage agent program verification},\n  journal   = {J. Log. Comput.},\n  volume    = {28},\n  number    = {3},\n  pages     = {499--523},\n  year      = {2018},\n  url       = {https://doi.org/10.1093/logcom/exv002},\n  doi       = {10.1093/logcom/exv002},\n  timestamp = {Mon, 07 May 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/logcom/Dennis0W18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Practical Challenges in Explicit Ethical Machine Reasoning.\n \n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2018, Fort Lauderdale, Florida, USA, January 3-5, 2018., 2018. \n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Practical$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/isaim/F18,\n  author    = {Louise A. Dennis and\n               Michael Fisher},\n  title     = {Practical Challenges in Explicit Ethical Machine Reasoning},\n  booktitle = {International Symposium on Artificial Intelligence and Mathematics,\n               {ISAIM} 2018, Fort Lauderdale, Florida, USA, January 3-5, 2018.},\n  year      = {2018},\n  crossref  = {DBLP:conf/isaim/2018},\n  url       = {http://isaim2018.cs.virginia.edu/papers/ISAIM2018\\_Ethics\\_Dennis\\_Fischer.pdf},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/isaim/DennisF18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Making Sense of the World: Models for Reliable Sensor-Driven Systems.\n \n \n \n \n\n\n \n \n\n\n \n\n\n\n CoRR, abs/1803.10478. 2018.\n \n\n\n\n
\n\n\n\n \n \n $\"Making$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time.\n \n \n \n \n\n\n \n Kamali, M.; Linker, S.; and Fisher, M.\n\n\n \n\n\n\n CoRR, abs/1804.06647. 2018.\n [Verifiable Autonomy, S4]\n\n\n\n
\n\n\n\n \n \n $\"Modular$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/abs-1804-06647,\n  author    = {Maryam Kamali and\n               Sven Linker and\n               Michael Fisher},\n  title     = {Modular Verification of Vehicle Platooning with Respect to Decisions,\n               Space and Time},\n  journal   = {CoRR},\n  volume    = {abs/1804.06647},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1804.06647},\n  archivePrefix = {arXiv},\n  eprint    = {1804.06647},\n  timestamp = {Mon, 13 Aug 2018 16:48:43 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1804-06647},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Sequent Calculus for Euler Diagrams.\n \n \n \n \n\n\n \n Linker, S.\n\n\n \n\n\n\n In Diagrammatic Representation and Inference - 10th International Conference, Diagrams 2018, Edinburgh, UK, June 18-22, 2018, Proceedings, pages 399–407, 2018. \n [S4]\n\n\n\n
\n\n\n\n \n \n $\"Sequent$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/diagrams/Linker18,\n  author    = {Sven Linker},\n  title     = {Sequent Calculus for Euler Diagrams},\n  booktitle = {Diagrammatic Representation and Inference - 10th International Conference,\n               Diagrams 2018, Edinburgh, UK, June 18-22, 2018, Proceedings},\n  pages     = {399--407},\n  year      = {2018},\n  crossref  = {DBLP:conf/diagrams/2018},\n  url       = {https://doi.org/10.1007/978-3-319-91376-6\\_37},\n  doi       = {10.1007/978-3-319-91376-6\\_37},\n  timestamp = {Tue, 10 Jul 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/diagrams/Linker18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n SCAV'18: Report of the 2nd International Workshop on Safe Control of Autonomous Vehicles.\n \n \n \n \n\n\n \n Gleirscher, M.; Linker, S.; and Kugele, S.\n\n\n \n\n\n\n CoRR, abs/1811.01774. 2018.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"SCAV'18:$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/abs-1811-01774,\n  author    = {Mario Gleirscher and\n               Sven Linker and\n               Stefan Kugele},\n  title     = {SCAV'18: Report of the 2nd International Workshop on Safe Control\n               of Autonomous Vehicles},\n  journal   = {CoRR},\n  volume    = {abs/1811.01774},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1811.01774},\n  archivePrefix = {arXiv},\n  eprint    = {1811.01774},\n  timestamp = {Thu, 22 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1811-01774},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2017\n \n \n (15)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n Theorem Proving for Metric Temporal Logic over the Naturals.\n \n \n \n \n\n\n \n Hustadt, U.; Ozaki, A.; and Dixon, C.\n\n\n \n\n\n\n In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pages 326–343, 2017. \n \n\n\n\n
\n\n\n\n \n \n $\"Theorem$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/cade/HustadtOD17,\n  author    = {Ullrich Hustadt and\n               Ana Ozaki and\n               Clare Dixon},\n  title     = {Theorem Proving for Metric Temporal Logic over the Naturals},\n  booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on\n               Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},\n  pages     = {326--343},\n  year      = {2017},\n  crossref  = {DBLP:conf/cade/2017},\n  url       = {https://doi.org/10.1007/978-3-319-63046-5\\_20},\n  doi       = {10.1007/978-3-319-63046-5\\_20},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/cade/HustadtOD17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n CRutoN: Automatic Verification of a Robotic Assistant's Behaviours.\n \n \n \n \n\n\n \n Gainer, P.; Dixon, C.; Dautenhahn, K.; Fisher, M.; Hustadt, U.; Saunders, J.; and Webster, M.\n\n\n \n\n\n\n In Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20, 2017, Proceedings, pages 119–133, 2017. \n \n\n\n\n
\n\n\n\n \n \n $\"CRutoN:$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/fmics/GainerDDFHSW17,\n  author    = {Paul Gainer and\n               Clare Dixon and\n               Kerstin Dautenhahn and\n               Michael Fisher and\n               Ullrich Hustadt and\n               Joe Saunders and\n               Matt Webster},\n  title     = {CRutoN: Automatic Verification of a Robotic Assistant's Behaviours},\n  booktitle = {Critical Systems: Formal Methods and Automated Verification - Joint\n               22nd International Workshop on Formal Methods for Industrial Critical\n               Systems - and - 17th International Workshop on Automated Verification\n               of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20,\n               2017, Proceedings},\n  pages     = {119--133},\n  year      = {2017},\n  crossref  = {DBLP:conf/fmics/2017},\n  url       = {https://doi.org/10.1007/978-3-319-67113-0\\_8},\n  doi       = {10.1007/978-3-319-67113-0\\_8},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/fmics/GainerDDFHSW17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n KSP: A Resolution-based Prover for Multimodal K, Abridged Report.\n \n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 4919–4923, 2017. \n \n\n\n\n
\n\n\n\n \n \n $\"KSP:$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/ijcai/NalonHD17,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Ullrich Hustadt and\n               Clare Dixon},\n  title     = {{KSP:} {A} Resolution-based Prover for Multimodal K, Abridged Report},\n  booktitle = {Proceedings of the Twenty-Sixth International Joint Conference on\n               Artificial Intelligence, {IJCAI} 2017, Melbourne, Australia, August\n               19-25, 2017},\n  pages     = {4919--4923},\n  year      = {2017},\n  crossref  = {DBLP:conf/ijcai/2017},\n  url       = {https://doi.org/10.24963/ijcai.2017/694},\n  doi       = {10.24963/ijcai.2017/694},\n  timestamp = {Wed, 27 Jun 2018 12:24:11 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/ijcai/NalonHD17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking.\n \n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n In Quantitative Evaluation of Systems - 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings, pages 224–239, 2017. \n [S4]\n\n\n\n
\n\n\n\n \n \n $\"Investigating$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/qest/GainerLDHF17,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {Investigating Parametric Influence on Discrete Synchronisation Protocols\n               Using Quantitative Model Checking},\n  booktitle = {Quantitative Evaluation of Systems - 14th International Conference,\n               {QEST} 2017, Berlin, Germany, September 5-7, 2017, Proceedings},\n  pages     = {224--239},\n  year      = {2017},\n  crossref  = {DBLP:conf/qest/2017},\n  url       = {https://doi.org/10.1007/978-3-319-66335-7\\_14},\n  doi       = {10.1007/978-3-319-66335-7\\_14},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/qest/GainerLDHF17},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Abstract State Machines and System Theoretic Process Analysis for Safety-Critical Systems.\n \n \n \n \n\n\n \n Al-Shareefi, F.; Lisitsa, A.; and Dixon, C.\n\n\n \n\n\n\n In Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings, pages 15–32, 2017. \n \n\n\n\n
\n\n\n\n \n \n $\"Abstract$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/sbmf/Al-ShareefiLD17,\n  author    = {Farah Al{-}Shareefi and\n               Alexei Lisitsa and\n               Clare Dixon},\n  title     = {Abstract State Machines and System Theoretic Process Analysis for\n               Safety-Critical Systems},\n  booktitle = {Formal Methods: Foundations and Applications - 20th Brazilian Symposium,\n               {SBMF} 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings},\n  pages     = {15--32},\n  year      = {2017},\n  crossref  = {DBLP:conf/sbmf/2017},\n  url       = {https://doi.org/10.1007/978-3-319-70848-5\\_3},\n  doi       = {10.1007/978-3-319-70848-5\\_3},\n  timestamp = {Fri, 17 Nov 2017 14:28:29 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/sbmf/Al-ShareefiLD17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings.\n \n \n \n \n\n\n \n Dixon, C.; and Finger, M.,\n editors.\n \n\n\n \n\n\n\n Volume 10483, of Lecture Notes in Computer Science.Springer. 2017.\n \n\n\n\n
\n\n\n\n \n \n $\"Frontiers$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@proceedings{DBLP:conf/frocos/2017,\n  editor    = {Clare Dixon and\n               Marcelo Finger},\n  title     = {Frontiers of Combining Systems - 11th International Symposium, FroCoS\n               2017, Bras{\\'{\\i}}lia, Brazil, September 27-29, 2017, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {10483},\n  publisher = {Springer},\n  year      = {2017},\n  url       = {https://doi.org/10.1007/978-3-319-66167-4},\n  doi       = {10.1007/978-3-319-66167-4},\n  isbn      = {978-3-319-66166-7},\n  timestamp = {Tue, 05 Sep 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/frocos/2017},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators.\n \n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n CoRR, abs/1709.04385. 2017.\n [S4]\n\n\n\n
\n\n\n\n \n \n $\"The$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/abs-1709-04385,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption\n               in Networks of Pulse-Coupled Oscillators},\n  journal   = {CoRR},\n  volume    = {abs/1709.04385},\n  year      = {2017},\n  url       = {http://arxiv.org/abs/1709.04385},\n  archivePrefix = {arXiv},\n  eprint    = {1709.04385},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-04385},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Formal verification of autonomous vehicle platooning.\n \n \n \n \n\n\n \n Kamali, M.; Dennis, L. A.; McAree, O.; Fisher, M.; and Veres, S. M.\n\n\n \n\n\n\n Sci. Comput. Program., 148: 88–106. 2017.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Formal$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/scp/KamaliDMFV17,\n  author    = {Maryam Kamali and\n               Louise A. Dennis and\n               Owen McAree and\n               Michael Fisher and\n               Sandor M. Veres},\n  title     = {Formal verification of autonomous vehicle platooning},\n  journal   = {Sci. Comput. Program.},\n  volume    = {148},\n  pages     = {88--106},\n  year      = {2017},\n  url       = {https://doi.org/10.1016/j.scico.2017.05.006},\n  doi       = {10.1016/j.scico.2017.05.006},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/scp/KamaliDMFV17},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Towards Moral Autonomous Systems.\n \n \n \n \n\n\n \n Charisi, V.; Dennis, L. A.; Fisher, M.; Lieck, R.; Matthias, A.; Slavkovik, M.; Sombetzki, J.; Winfield, A. F. T.; and Yampolskiy, R.\n\n\n \n\n\n\n CoRR, abs/1703.04741. 2017.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Towards$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/CharisiDFLMSSWY17,\n  author    = {Vicky Charisi and\n               Louise A. Dennis and\n               Michael Fisher and\n               Robert Lieck and\n               Andreas Matthias and\n               Marija Slavkovik and\n               Janina Sombetzki and\n               Alan F. T. Winfield and\n               Roman Yampolskiy},\n  title     = {Towards Moral Autonomous Systems},\n  journal   = {CoRR},\n  volume    = {abs/1703.04741},\n  year      = {2017},\n  url       = {http://arxiv.org/abs/1703.04741},\n  archivePrefix = {arXiv},\n  eprint    = {1703.04741},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/CharisiDFLMSSWY17},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification.\n \n \n \n \n\n\n \n Fernandes, L. E. R.; Custodio, V.; Alves, G. V.; and Fisher, M.\n\n\n \n\n\n\n In Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@iFM 2017, Turin, Italy, 19th September 2017., pages 35–42, 2017. \n \n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:journals/corr/abs-1709-02557,\n  author    = {Lucas E. R. Fernandes and\n               Vinicius Custodio and\n               Gleifer V. Alves and\n               Michael Fisher},\n  title     = {A Rational Agent Controlling an Autonomous Vehicle: Implementation\n               and Formal Verification},\n  booktitle = {Proceedings First Workshop on Formal Verification of Autonomous Vehicles,\n               FVAV@iFM 2017, Turin, Italy, 19th September 2017.},\n  pages     = {35--42},\n  year      = {2017},\n  url       = {https://doi.org/10.4204/EPTCS.257.5},\n  doi       = {10.4204/EPTCS.257.5},\n  timestamp = {Fri, 02 Nov 2018 09:30:18 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-02557},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Finding Maximum Expected Termination Time of Probabilistic Timed Automata Models with Cyclic behavior.\n \n \n \n \n\n\n \n Al-Bataineh, O. I.; Fisher, M.; and Rosenblum, D.\n\n\n \n\n\n\n CoRR, abs/1709.07171. 2017.\n \n\n\n\n
\n\n\n\n \n \n $\"Finding$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/abs-1709-07171,\n  author    = {Omar I. Al{-}Bataineh and\n               Michael Fisher and\n               David Rosenblum},\n  title     = {Finding Maximum Expected Termination Time of Probabilistic Timed Automata\n               Models with Cyclic behavior},\n  journal   = {CoRR},\n  volume    = {abs/1709.07171},\n  year      = {2017},\n  url       = {http://arxiv.org/abs/1709.07171},\n  archivePrefix = {arXiv},\n  eprint    = {1709.07171},\n  timestamp = {Mon, 13 Aug 2018 16:48:50 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-07171},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Hybrid Multi-Lane Spatial Logic.\n \n \n \n \n\n\n \n Linker, S.\n\n\n \n\n\n\n Archive of Formal Proofs. 2017.\n [Verifiable Autonomy, S4]\n\n\n\n
\n\n\n\n \n \n $\"Hybrid$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{Linker17,\n  author    = {Sven Linker},\n  title     = {Hybrid Multi-Lane Spatial Logic},\n  journal   = {Archive of Formal Proofs},\n  year      = {2017},\n  url       = {https://www.isa-afp.org/entries/Hybrid\\_Multi\\_Lane\\_Spatial\\_Logic.html},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Synthesizing and verifying controllers for multi-lane traffic maneuvers.\n \n \n \n \n\n\n \n von Bochmann, G.; Hilscher, M.; Linker, S.; and Olderog, E.\n\n\n \n\n\n\n Formal Asp. Comput., 29(4): 583–600. 2017.\n \n\n\n\n
\n\n\n\n \n \n $\"Synthesizing$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/fac/BochmannHLO17,\n  author    = {Gregor von Bochmann and\n               Martin Hilscher and\n               Sven Linker and\n               Ernst{-}R{\\"{u}}diger Olderog},\n  title     = {Synthesizing and verifying controllers for multi-lane traffic maneuvers},\n  journal   = {Formal Asp. Comput.},\n  volume    = {29},\n  number    = {4},\n  pages     = {583--600},\n  year      = {2017},\n  url       = {https://doi.org/10.1007/s00165-017-0424-4},\n  doi       = {10.1007/s00165-017-0424-4},\n  timestamp = {Wed, 26 Jul 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/fac/BochmannHLO17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL.\n \n \n \n \n\n\n \n Linker, S.\n\n\n \n\n\n\n In Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings, pages 34–49, 2017. \n [Verifiable Autonomy, S4]\n\n\n\n
\n\n\n\n \n \n $\"Spatial$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/ifm/Linker17,\n  author    = {Sven Linker},\n  title     = {Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL},\n  booktitle = {Integrated Formal Methods - 13th International Conference, {IFM} 2017,\n               Turin, Italy, September 20-22, 2017, Proceedings},\n  pages     = {34--49},\n  year      = {2017},\n  crossref  = {DBLP:conf/ifm/2017},\n  url       = {https://doi.org/10.1007/978-3-319-66845-1\\_3},\n  doi       = {10.1007/978-3-319-66845-1\\_3},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/ifm/Linker17},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Formalising Sensor Topologies for Target Counting.\n \n \n \n \n\n\n \n Linker, S.; and Sevegnani, M.\n\n\n \n\n\n\n In Proceedings First Workshop on Architectures, Languages and Paradigms for IoT, ALP4IoT@iFM 2017, Turin, Italy, September 18, 2017., pages 43–57, 2017. \n [S4]\n\n\n\n
\n\n\n\n \n \n $\"Formalising$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:journals/corr/abs-1802-01791,\n  author    = {Sven Linker and\n               Michele Sevegnani},\n  title     = {Formalising Sensor Topologies for Target Counting},\n  booktitle = {Proceedings First Workshop on Architectures, Languages and Paradigms\n               for IoT, ALP4IoT@iFM 2017, Turin, Italy, September 18, 2017.},\n  pages     = {43--57},\n  year      = {2017},\n  crossref  = {DBLP:journals/corr/abs-1802-00976},\n  url       = {https://doi.org/10.4204/EPTCS.264.5},\n  doi       = {10.4204/EPTCS.264.5},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1802-01791},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2016\n \n \n (10)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study.\n \n \n \n \n\n\n \n Webster, M.; Dixon, C.; Fisher, M.; Salem, M.; Saunders, J.; Koay, K. L.; Dautenhahn, K.; and Saez-Pons, J.\n\n\n \n\n\n\n IEEE Trans. Human-Machine Systems, 46(2): 186–196. 2016.\n \n\n\n\n
\n\n\n\n \n \n $\"Toward$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/thms/WebsterDFSSKDS16,\n  author    = {Matt Webster and\n               Clare Dixon and\n               Michael Fisher and\n               Maha Salem and\n               Joe Saunders and\n               Kheng Lee Koay and\n               Kerstin Dautenhahn and\n               Joan Saez{-}Pons},\n  title     = {Toward Reliable Autonomous Robotic Assistants Through Formal Verification:\n               {A} Case Study},\n  journal   = {{IEEE} Trans. Human-Machine Systems},\n  volume    = {46},\n  number    = {2},\n  pages     = {186--196},\n  year      = {2016},\n  url       = {https://doi.org/10.1109/THMS.2015.2425139},\n  doi       = {10.1109/THMS.2015.2425139},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/thms/WebsterDFSSKDS16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n : A Resolution-Based Prover for Multimodal K.\n \n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, pages 406–415, 2016. \n \n\n\n\n
\n\n\n\n \n \n $\":$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/cade/NalonHD16,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Ullrich Hustadt and\n               Clare Dixon},\n  title     = {: {A} Resolution-Based Prover for Multimodal {K}},\n  booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}\n               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},\n  pages     = {406--415},\n  year      = {2016},\n  crossref  = {DBLP:conf/cade/2016},\n  url       = {https://doi.org/10.1007/978-3-319-40229-1\\_28},\n  doi       = {10.1007/978-3-319-40229-1\\_28},\n  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/cade/NalonHD16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Probabilistic Model Checking of Ant-Based Positionless Swarming.\n \n \n \n \n\n\n \n Gainer, P.; Dixon, C.; and Hustadt, U.\n\n\n \n\n\n\n In Towards Autonomous Robotic Systems - 17th Annual Conference, TAROS 2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings, pages 127–138, 2016. \n \n\n\n\n
\n\n\n\n \n \n $\"Probabilistic$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/taros/GainerDH16,\n  author    = {Paul Gainer and\n               Clare Dixon and\n               Ullrich Hustadt},\n  title     = {Probabilistic Model Checking of Ant-Based Positionless Swarming},\n  booktitle = {Towards Autonomous Robotic Systems - 17th Annual Conference, {TAROS}\n               2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings},\n  pages     = {127--138},\n  year      = {2016},\n  crossref  = {DBLP:conf/taros/2016},\n  url       = {https://doi.org/10.1007/978-3-319-40379-3\\_13},\n  doi       = {10.1007/978-3-319-40379-3\\_13},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/taros/GainerDH16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n An Assurance-based Approach to Verification and Validation of Human-Robot Teams.\n \n \n \n \n\n\n \n Webster, M.; Western, D.; Araiza-Illan, D.; Dixon, C.; Eder, K.; Fisher, M.; and Pipe, A. G.\n\n\n \n\n\n\n CoRR, abs/1608.07403. 2016.\n \n\n\n\n
\n\n\n\n \n \n $\"An$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/WebsterWADEFP16,\n  author    = {Matt Webster and\n               David Western and\n               Dejanira Araiza{-}Illan and\n               Clare Dixon and\n               Kerstin Eder and\n               Michael Fisher and\n               Anthony G. Pipe},\n  title     = {An Assurance-based Approach to Verification and Validation of Human-Robot\n               Teams},\n  journal   = {CoRR},\n  volume    = {abs/1608.07403},\n  year      = {2016},\n  url       = {http://arxiv.org/abs/1608.07403},\n  archivePrefix = {arXiv},\n  eprint    = {1608.07403},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/WebsterWADEFP16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Practical verification of decision-making in agent-based autonomous systems.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; Lincoln, N.; Lisitsa, A.; and Veres, S. M.\n\n\n \n\n\n\n Autom. Softw. Eng., 23(3): 305–359. 2016.\n \n\n\n\n
\n\n\n\n \n \n $\"Practical$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/ase/DennisFLLV16,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Nicholas Lincoln and\n               Alexei Lisitsa and\n               Sandor M. Veres},\n  title     = {Practical verification of decision-making in agent-based autonomous\n               systems},\n  journal   = {Autom. Softw. Eng.},\n  volume    = {23},\n  number    = {3},\n  pages     = {305--359},\n  year      = {2016},\n  url       = {https://doi.org/10.1007/s10515-014-0168-9},\n  doi       = {10.1007/s10515-014-0168-9},\n  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/ase/DennisFLLV16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Formal verification of ethical choices in autonomous systems.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; Slavkovik, M.; and Webster, M.\n\n\n \n\n\n\n Robotics and Autonomous Systems, 77: 1–14. 2016.\n \n\n\n\n
\n\n\n\n \n \n $\"Formal$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/ras/DennisFSW16,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Marija Slavkovik and\n               Matt Webster},\n  title     = {Formal verification of ethical choices in autonomous systems},\n  journal   = {Robotics and Autonomous Systems},\n  volume    = {77},\n  pages     = {1--14},\n  year      = {2016},\n  url       = {https://doi.org/10.1016/j.robot.2015.11.012},\n  doi       = {10.1016/j.robot.2015.11.012},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/ras/DennisFSW16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n \"How Did They Know?\" - Model-Checking for Analysis of Information Leakage in Social Networks.\n \n \n \n \n\n\n \n Dennis, L. A.; Slavkovik, M.; and Fisher, M.\n\n\n \n\n\n\n In Coordination, Organizations, Institutions, and Norms in Agent Systems XII - COIN 2016 International Workshops, COIN@AAMAS, Singapore, Singapore, May 9, 2016, COIN@ECAI, The Hague, The Netherlands, August 30, 2016, Revised Selected Papers, pages 42–59, 2016. \n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\""How$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/atal/DennisSF16,\n  author    = {Louise A. Dennis and\n               Marija Slavkovik and\n               Michael Fisher},\n  title     = {"How Did They Know?" - Model-Checking for Analysis of Information\n               Leakage in Social Networks},\n  booktitle = {Coordination, Organizations, Institutions, and Norms in Agent Systems\n               {XII} - {COIN} 2016 International Workshops, COIN@AAMAS, Singapore,\n               Singapore, May 9, 2016, COIN@ECAI, The Hague, The Netherlands, August\n               30, 2016, Revised Selected Papers},\n  pages     = {42--59},\n  year      = {2016},\n  crossref  = {DBLP:conf/atal/2016coin},\n  url       = {https://doi.org/10.1007/978-3-319-66595-5\\_3},\n  doi       = {10.1007/978-3-319-66595-5\\_3},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/atal/DennisSF16},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Agent-Based Autonomous Systems and Abstraction Engines: Theory Meets Practice.\n \n \n \n \n\n\n \n Dennis, L. A.; Aitken, J. M.; Collenette, J.; Cucco, E.; Kamali, M.; McAree, O.; Shaukat, A.; Atkinson, K.; Gao, Y.; Veres, S. M.; and Fisher, M.\n\n\n \n\n\n\n In Towards Autonomous Robotic Systems - 17th Annual Conference, TAROS 2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings, pages 75–86, 2016. \n \n\n\n\n
\n\n\n\n \n \n $\"Agent-Based$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/taros/DennisACCKMSAGV16,\n  author    = {Louise A. Dennis and\n               Jonathan M. Aitken and\n               Joe Collenette and\n               Elisa Cucco and\n               Maryam Kamali and\n               Owen McAree and\n               Affan Shaukat and\n               Katie Atkinson and\n               Yang Gao and\n               Sandor M. Veres and\n               Michael Fisher},\n  title     = {Agent-Based Autonomous Systems and Abstraction Engines: Theory Meets\n               Practice},\n  booktitle = {Towards Autonomous Robotic Systems - 17th Annual Conference, {TAROS}\n               2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings},\n  pages     = {75--86},\n  year      = {2016},\n  crossref  = {DBLP:conf/taros/2016},\n  url       = {https://doi.org/10.1007/978-3-319-40379-3\\_8},\n  doi       = {10.1007/978-3-319-40379-3\\_8},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/taros/DennisACCKMSAGV16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Formal Verification of Autonomous Vehicle Platooning.\n \n \n \n \n\n\n \n Kamali, M.; Dennis, L. A.; McAree, O.; Fisher, M.; and Veres, S. M.\n\n\n \n\n\n\n CoRR, abs/1602.01718. 2016.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Formal$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/KamaliDMFV16,\n  author    = {Maryam Kamali and\n               Louise A. Dennis and\n               Owen McAree and\n               Michael Fisher and\n               Sandor M. Veres},\n  title     = {Formal Verification of Autonomous Vehicle Platooning},\n  journal   = {CoRR},\n  volume    = {abs/1602.01718},\n  year      = {2016},\n  url       = {http://arxiv.org/abs/1602.01718},\n  archivePrefix = {arXiv},\n  eprint    = {1602.01718},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/KamaliDMFV16},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Engineering Moral Agents - from Human Morality to Artificial Morality (Dagstuhl Seminar 16222).\n \n \n \n \n\n\n \n Fisher, M.; List, C.; Slavkovik, M.; and Winfield, A. F. T.\n\n\n \n\n\n\n Dagstuhl Reports, 6(5): 114–137. 2016.\n \n\n\n\n
\n\n\n\n \n \n $\"Engineering$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/dagstuhl-reports/FisherLSW16,\n  author    = {Michael Fisher and\n               Christian List and\n               Marija Slavkovik and\n               Alan F. T. Winfield},\n  title     = {Engineering Moral Agents - from Human Morality to Artificial Morality\n               (Dagstuhl Seminar 16222)},\n  journal   = {Dagstuhl Reports},\n  volume    = {6},\n  number    = {5},\n  pages     = {114--137},\n  year      = {2016},\n  url       = {https://doi.org/10.4230/DagRep.6.5.114},\n  doi       = {10.4230/DagRep.6.5.114},\n  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/dagstuhl-reports/FisherLSW16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2015\n \n \n (9)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n Predicting \"springback\" using 3D surface representation techniques: A case study in sheet metal forming.\n \n \n \n \n\n\n \n El-Salhi, S.; Coenen, F.; Dixon, C.; and Khan, M. S.\n\n\n \n\n\n\n Expert Syst. Appl., 42(1): 79–93. 2015.\n \n\n\n\n
\n\n\n\n \n \n $\"Predicting$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/eswa/El-SalhiCDK15,\n  author    = {Subhieh El{-}Salhi and\n               Frans Coenen and\n               Clare Dixon and\n               M. Sulaiman Khan},\n  title     = {Predicting "springback" using 3D surface representation techniques:\n               {A} case study in sheet metal forming},\n  journal   = {Expert Syst. Appl.},\n  volume    = {42},\n  number    = {1},\n  pages     = {79--93},\n  year      = {2015},\n  url       = {https://doi.org/10.1016/j.eswa.2014.07.041},\n  doi       = {10.1016/j.eswa.2014.07.041},\n  timestamp = {Fri, 26 May 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/eswa/El-SalhiCDK15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Ordered Resolution for Coalition Logic.\n \n \n \n \n\n\n \n Hustadt, U.; Gainer, P.; Dixon, C.; Nalon, C.; and Zhang, L.\n\n\n \n\n\n\n In Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21-24, 2015. Proceedings, pages 169–184, 2015. \n \n\n\n\n
\n\n\n\n \n \n $\"Ordered$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/tableaux/HustadtGDNZ15,\n  author    = {Ullrich Hustadt and\n               Paul Gainer and\n               Clare Dixon and\n               Cl{\\'{a}}udia Nalon and\n               Lan Zhang},\n  title     = {Ordered Resolution for Coalition Logic},\n  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th\n               International Conference, {TABLEAUX} 2015, Wroc{\\l}aw, Poland, September\n               21-24, 2015. Proceedings},\n  pages     = {169--184},\n  year      = {2015},\n  crossref  = {DBLP:conf/tableaux/2015},\n  url       = {https://doi.org/10.1007/978-3-319-24312-2\\_12},\n  doi       = {10.1007/978-3-319-24312-2\\_12},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/tableaux/HustadtGDNZ15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A Modal-Layered Resolution Calculus for K.\n \n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21-24, 2015. Proceedings, pages 185–200, 2015. \n \n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/tableaux/NalonHD15,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Ullrich Hustadt and\n               Clare Dixon},\n  title     = {A Modal-Layered Resolution Calculus for {K}},\n  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th\n               International Conference, {TABLEAUX} 2015, Wroc{\\l}aw, Poland, September\n               21-24, 2015. Proceedings},\n  pages     = {185--200},\n  year      = {2015},\n  crossref  = {DBLP:conf/tableaux/2015},\n  url       = {https://doi.org/10.1007/978-3-319-24312-2\\_13},\n  doi       = {10.1007/978-3-319-24312-2\\_13},\n  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/tableaux/NalonHD15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Towards Autonomous Robotic Systems - 16th Annual Conference, TAROS 2015, Liverpool, UK, September 8-10, 2015, Proceedings.\n \n \n \n \n\n\n \n Dixon, C.; and Tuyls, K.,\n editors.\n \n\n\n \n\n\n\n Volume 9287, of Lecture Notes in Computer Science.Springer. 2015.\n \n\n\n\n
\n\n\n\n \n \n $\"Towards$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@proceedings{DBLP:conf/taros/2015,\n  editor    = {Clare Dixon and\n               Karl Tuyls},\n  title     = {Towards Autonomous Robotic Systems - 16th Annual Conference, {TAROS}\n               2015, Liverpool, UK, September 8-10, 2015, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {9287},\n  publisher = {Springer},\n  year      = {2015},\n  url       = {https://doi.org/10.1007/978-3-319-22416-9},\n  doi       = {10.1007/978-3-319-22416-9},\n  isbn      = {978-3-319-22415-2},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/taros/2015},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n An abstract formal basis for digital crowds.\n \n \n \n \n\n\n \n Slavkovik, M.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n Distributed and Parallel Databases, 33(1): 3–31. 2015.\n \n\n\n\n
\n\n\n\n \n \n $\"An$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/dpd/SlavkovikDF15,\n  author    = {Marija Slavkovik and\n               Louise A. Dennis and\n               Michael Fisher},\n  title     = {An abstract formal basis for digital crowds},\n  journal   = {Distributed and Parallel Databases},\n  volume    = {33},\n  number    = {1},\n  pages     = {3--31},\n  year      = {2015},\n  url       = {https://doi.org/10.1007/s10619-014-7161-y},\n  doi       = {10.1007/s10619-014-7161-y},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/dpd/SlavkovikDF15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Towards Verifiably Ethical Robot Behaviour.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; and Winfield, A. F. T.\n\n\n \n\n\n\n In Artificial Intelligence and Ethics, Papers from the 2015 AAAI Workshop, Austin, Texas, USA, January 25, 2015., 2015. \n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Towards$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/aaai/DennisFW15,\n  author    = {Louise Abigail Dennis and\n               Michael Fisher and\n               Alan F. T. Winfield},\n  title     = {Towards Verifiably Ethical Robot Behaviour},\n  booktitle = {Artificial Intelligence and Ethics, Papers from the 2015 {AAAI} Workshop,\n               Austin, Texas, USA, January 25, 2015.},\n  year      = {2015},\n  crossref  = {DBLP:conf/aaai/2015ethics},\n  url       = {http://aaai.org/ocs/index.php/WS/AAAIW15/paper/view/10119},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/aaai/DennisFW15},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A Semantic Framework for Socially Adaptive Agents: Towards strong norm compliance.\n \n \n \n \n\n\n \n van Riemsdijk, M. B.; Dennis, L. A.; Fisher, M.; and Hindriks, K. V.\n\n\n \n\n\n\n In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015, pages 423–432, 2015. \n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/atal/RiemsdijkDFH15,\n  author    = {M. Birna van Riemsdijk and\n               Louise A. Dennis and\n               Michael Fisher and\n               Koen V. Hindriks},\n  title     = {A Semantic Framework for Socially Adaptive Agents: Towards strong\n               norm compliance},\n  booktitle = {Proceedings of the 2015 International Conference on Autonomous Agents\n               and Multiagent Systems, {AAMAS} 2015, Istanbul, Turkey, May 4-8, 2015},\n  pages     = {423--432},\n  year      = {2015},\n  crossref  = {DBLP:conf/atal/2015},\n  url       = {http://dl.acm.org/citation.cfm?id=2772935},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/atal/RiemsdijkDFH15},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Towards Verifiably Ethical Robot Behaviour.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; and Winfield, A. F. T.\n\n\n \n\n\n\n CoRR, abs/1504.03592. 2015.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n $\"Towards$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/DennisFW15,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Alan F. T. Winfield},\n  title     = {Towards Verifiably Ethical Robot Behaviour},\n  journal   = {CoRR},\n  volume    = {abs/1504.03592},\n  year      = {2015},\n  url       = {http://arxiv.org/abs/1504.03592},\n  archivePrefix = {arXiv},\n  eprint    = {1504.03592},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/DennisFW15},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A roadmap to pervasive systems verification.\n \n \n \n \n\n\n \n Konur, S.; and Fisher, M.\n\n\n \n\n\n\n Knowledge Eng. Review, 30(3): 324–341. 2015.\n \n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/ker/KonurF15,\n  author    = {Savas Konur and\n               Michael Fisher},\n  title     = {A roadmap to pervasive systems verification},\n  journal   = {Knowledge Eng. Review},\n  volume    = {30},\n  number    = {3},\n  pages     = {324--341},\n  year      = {2015},\n  url       = {https://doi.org/10.1017/S0269888914000228},\n  doi       = {10.1017/S0269888914000228},\n  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/ker/KonurF15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n

\n \n 2014\n \n \n (14)\n \n \n

\n \n \n

\n \n\n \n \n \n \n \n \n A resolution-based calculus for Coalition Logic.\n \n \n \n \n\n\n \n Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U.\n\n\n \n\n\n\n J. Log. Comput., 24(4): 883–917. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/logcom/NalonZDH14,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Lan Zhang and\n               Clare Dixon and\n               Ullrich Hustadt},\n  title     = {A resolution-based calculus for Coalition Logic},\n  journal   = {J. Log. Comput.},\n  volume    = {24},\n  number    = {4},\n  pages     = {883--917},\n  year      = {2014},\n  url       = {https://doi.org/10.1093/logcom/ext074},\n  doi       = {10.1093/logcom/ext074},\n  timestamp = {Wed, 17 May 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/logcom/NalonZDH14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A resolution calculus for the branching-time temporal logic CTL.\n \n \n \n \n\n\n \n Zhang, L.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n ACM Trans. Comput. Log., 15(1): 10:1–10:38. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/tocl/ZhangHD14,\n  author    = {Lan Zhang and\n               Ullrich Hustadt and\n               Clare Dixon},\n  title     = {A resolution calculus for the branching-time temporal logic {CTL}},\n  journal   = {{ACM} Trans. Comput. Log.},\n  volume    = {15},\n  number    = {1},\n  pages     = {10:1--10:38},\n  year      = {2014},\n  url       = {https://doi.org/10.1145/2529993},\n  doi       = {10.1145/2529993},\n  timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/tocl/ZhangHD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Formal Verification of an Autonomous Personal Robotic Assistant.\n \n \n \n \n\n\n \n Webster, M.; Dixon, C.; Fisher, M.; Salem, M.; Saunders, J.; Koay, K. L.; and Dautenhahn, K.\n\n\n \n\n\n\n In 2014 AAAI Spring Symposia, Stanford University, Palo Alto, California, USA, March 24-26, 2014, 2014. \n \n\n\n\n
\n\n\n\n \n \n $\"Formal$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/aaaiss/WebsterD0SSKD14,\n  author    = {Matt Webster and\n               Clare Dixon and\n               Michael Fisher and\n               Maha Salem and\n               Joe Saunders and\n               Kheng Lee Koay and\n               Kerstin Dautenhahn},\n  title     = {Formal Verification of an Autonomous Personal Robotic Assistant},\n  booktitle = {2014 {AAAI} Spring Symposia, Stanford University, Palo Alto, California,\n               USA, March 24-26, 2014},\n  year      = {2014},\n  crossref  = {DBLP:conf/aaaiss/2014},\n  url       = {http://www.aaai.org/ocs/index.php/SSS/SSS14/paper/view/7734},\n  timestamp = {Wed, 14 Nov 2018 14:23:12 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/aaaiss/WebsterD0SSKD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Clausal Resolution for Modal Logics of Confluence.\n \n \n \n \n\n\n \n Nalon, C.; Marcos, J.; and Dixon, C.\n\n\n \n\n\n\n In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, pages 322–336, 2014. \n \n\n\n\n
\n\n\n\n \n \n $\"Clausal$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/cade/NalonMD14,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Jo{\\~{a}}o Marcos and\n               Clare Dixon},\n  title     = {Clausal Resolution for Modal Logics of Confluence},\n  booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR}\n               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,\n               Austria, July 19-22, 2014. Proceedings},\n  pages     = {322--336},\n  year      = {2014},\n  crossref  = {DBLP:conf/cade/2014},\n  url       = {https://doi.org/10.1007/978-3-319-08587-6\\_24},\n  doi       = {10.1007/978-3-319-08587-6\\_24},\n  timestamp = {Sun, 21 May 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/cade/NalonMD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n \"The Fridge Door is Open\"-Temporal Verification of a Robotic Assistant's Behaviours.\n \n \n \n \n\n\n \n Dixon, C.; Webster, M. P.; Saunders, J.; Fisher, M.; and Dautenhahn, K.\n\n\n \n\n\n\n In Advances in Autonomous Robotics Systems - 15th Annual Conference, TAROS 2014, Birmingham, UK, September 1-3, 2014. Proceedings, pages 97–108, 2014. \n \n\n\n\n
\n\n\n\n \n \n $\""The$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/taros/DixonWSFD14,\n  author    = {Clare Dixon and\n               Matthew P. Webster and\n               Joe Saunders and\n               Michael Fisher and\n               Kerstin Dautenhahn},\n  title     = {"The Fridge Door is Open"-Temporal Verification of a Robotic Assistant's\n               Behaviours},\n  booktitle = {Advances in Autonomous Robotics Systems - 15th Annual Conference,\n               {TAROS} 2014, Birmingham, UK, September 1-3, 2014. Proceedings},\n  pages     = {97--108},\n  year      = {2014},\n  crossref  = {DBLP:conf/taros/2014},\n  url       = {https://doi.org/10.1007/978-3-319-10401-0\\_9},\n  doi       = {10.1007/978-3-319-10401-0\\_9},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/taros/DixonWSFD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n A Resolution Prover for Coalition Logic.\n \n \n \n \n\n\n \n Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U.\n\n\n \n\n\n\n In Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014., pages 65–73, 2014. \n \n\n\n\n
\n\n\n\n \n \n $\"A$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:journals/corr/NalonZDH14,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Lan Zhang and\n               Clare Dixon and\n               Ullrich Hustadt},\n  title     = {A Resolution Prover for Coalition Logic},\n  booktitle = {Proceedings 2nd International Workshop on Strategic Reasoning, {SR}\n               2014, Grenoble, France, April 5-6, 2014.},\n  pages     = {65--73},\n  year      = {2014},\n  crossref  = {DBLP:journals/corr/MogaveroMV14},\n  url       = {https://doi.org/10.4204/EPTCS.146.9},\n  doi       = {10.4204/EPTCS.146.9},\n  timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/NalonZDH14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n On and On the Temporal Way.\n \n \n \n \n\n\n \n Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n In HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, pages 85–111. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"On$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@incollection{DBLP:conf/birthday/DixonF14,\n  author    = {Clare Dixon and\n               Michael Fisher},\n  title     = {On and On the Temporal Way},\n  booktitle = {{HOWARD-60:} {A} Festschrift on the Occasion of Howard Barringer's\n               60th Birthday},\n  pages     = {85--111},\n  year      = {2014},\n  crossref  = {DBLP:conf/birthday/2014howard},\n  url       = {http://www.easychair.org/publications/?page=2015413951},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/birthday/DixonF14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Clausal Resolution for Modal Logics of Confluence.\n \n \n \n \n\n\n \n Nalon, C.; Marcos, J.; and Dixon, C.\n\n\n \n\n\n\n CoRR, abs/1405.0293. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"Clausal$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/NalonMD14,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Jo{\\~{a}}o Marcos and\n               Clare Dixon},\n  title     = {Clausal Resolution for Modal Logics of Confluence},\n  journal   = {CoRR},\n  volume    = {abs/1405.0293},\n  year      = {2014},\n  url       = {http://arxiv.org/abs/1405.0293},\n  archivePrefix = {arXiv},\n  eprint    = {1405.0293},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/NalonMD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Reconfigurable Autonomy.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; Aitken, J. M.; Veres, S. M.; Gao, Y.; Shaukat, A.; and Burroughes, G.\n\n\n \n\n\n\n KI, 28(3): 199–207. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"Reconfigurable$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/ki/DennisFAVGSB14,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Jonathan M. Aitken and\n               Sandor M. Veres and\n               Yang Gao and\n               Affan Shaukat and\n               Guy Burroughes},\n  title     = {Reconfigurable Autonomy},\n  journal   = {{KI}},\n  volume    = {28},\n  number    = {3},\n  pages     = {199--207},\n  year      = {2014},\n  url       = {https://doi.org/10.1007/s13218-014-0308-1},\n  doi       = {10.1007/s13218-014-0308-1},\n  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/ki/DennisFAVGSB14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Actions with Durations and Failures in BDI Languages.\n \n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014), pages 995–996, 2014. \n \n\n\n\n
\n\n\n\n \n \n $\"Actions$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@inproceedings{DBLP:conf/ecai/DennisF14,\n  author    = {Louise A. Dennis and\n               Michael Fisher},\n  title     = {Actions with Durations and Failures in {BDI} Languages},\n  booktitle = {{ECAI} 2014 - 21st European Conference on Artificial Intelligence,\n               18-22 August 2014, Prague, Czech Republic - Including Prestigious\n               Applications of Intelligent Systems {(PAIS} 2014)},\n  pages     = {995--996},\n  year      = {2014},\n  crossref  = {DBLP:conf/ecai/2014},\n  url       = {https://doi.org/10.3233/978-1-61499-419-0-995},\n  doi       = {10.3233/978-1-61499-419-0-995},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/ecai/DennisF14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n An Abstract Formal Basis for Digital Crowds.\n \n \n \n \n\n\n \n Slavkovik, M.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n CoRR, abs/1408.1592. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"An$ Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/corr/SlavkovikDF14,\n  author    = {Marija Slavkovik and\n               Louise A. Dennis and\n               Michael Fisher},\n  title     = {An Abstract Formal Basis for Digital Crowds},\n  journal   = {CoRR},\n  volume    = {abs/1408.1592},\n  year      = {2014},\n  url       = {http://arxiv.org/abs/1408.1592},\n  archivePrefix = {arXiv},\n  eprint    = {1408.1592},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/SlavkovikDF14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Formal verification of a pervasive messaging system.\n \n \n \n \n\n\n \n Konur, S.; Fisher, M.; Dobson, S.; and Knox, S.\n\n\n \n\n\n\n Formal Asp. Comput., 26(4): 677–694. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"Formal$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/fac/KonurFDK14,\n  author    = {Savas Konur and\n               Michael Fisher and\n               Simon Dobson and\n               Stephen Knox},\n  title     = {Formal verification of a pervasive messaging system},\n  journal   = {Formal Asp. Comput.},\n  volume    = {26},\n  number    = {4},\n  pages     = {677--694},\n  year      = {2014},\n  url       = {https://doi.org/10.1007/s00165-013-0277-4},\n  doi       = {10.1007/s00165-013-0277-4},\n  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/fac/KonurFDK14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation.\n \n \n \n \n\n\n \n Webster, M. P.; Cameron, N.; Fisher, M.; and Jump, M.\n\n\n \n\n\n\n J. Aerospace Inf. Sys., 11(5): 258–279. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"Generating$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/jacic/WebsterCFJ14,\n  author    = {Matthew P. Webster and\n               Neil Cameron and\n               Michael Fisher and\n               Mike Jump},\n  title     = {Generating Certification Evidence for Autonomous Unmanned Aircraft\n               Using Model Checking and Simulation},\n  journal   = {J. Aerospace Inf. Sys.},\n  volume    = {11},\n  number    = {5},\n  pages     = {258--279},\n  year      = {2014},\n  url       = {https://doi.org/10.2514/1.I010096},\n  doi       = {10.2514/1.I010096},\n  timestamp = {Fri, 02 Nov 2018 09:33:11 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/jacic/WebsterCFJ14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n

\n \n\n \n \n \n \n \n \n Preface to the Special Issue on Computational Logic in Multi-Agent Systems (CLIMA XIII).\n \n \n \n \n\n\n \n Fisher, M.; van der Torre, L. W. N.; Dastani, M.; and Governatori, G.\n\n\n \n\n\n\n J. Log. Comput., 24(6): 1251–1252. 2014.\n \n\n\n\n
\n\n\n\n \n \n $\"Preface$ Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n

@article{DBLP:journals/logcom/FisherTDG14,\n  author    = {Michael Fisher and\n               Leendert W. N. van der Torre and\n               Mehdi Dastani and\n               Guido Governatori},\n  title     = {Preface to the Special Issue on Computational Logic in Multi-Agent\n               Systems {(CLIMA} {XIII)}},\n  journal   = {J. Log. Comput.},\n  volume    = {24},\n  number    = {6},\n  pages     = {1251--1252},\n  year      = {2014},\n  url       = {https://doi.org/10.1093/logcom/ext075},\n  doi       = {10.1093/logcom/ext075},\n  timestamp = {Wed, 14 Nov 2018 10:17:07 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/logcom/FisherTDG14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n

\n\n\n\n

\n\n\n\n\n\n

\n\n\n\n\n

\n\n\n \n\n \n \n \n \n\n