pubs.bib

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

@InBook{Wright2025,
author="Wright, Thomas and Dennis, Louise A. and Woodcock, Jim and Foster, Simon",
editor="Hinchey, Mike and Steffen, Bernhard",
title={Formal Verification of BDI Agents},
booktitle={The Combined Power of Research, Education, and Dissemination: Essays Dedicated to Tiziana Margaria on the Occasion of Her 60th Birthday},
year="2025",
publisher="Springer Nature Switzerland",
address="Cham",
pages="302--326",
isbn="978-3-031-73887-6",
doi="10.1007/978-3-031-73887-6_20",
note={[<span class="tas_vn">TAS Verifiability Node</span>]},
url="https://doi.org/10.1007/978-3-031-73887-6_20"
}

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


@inproceedings{quan-etal-2024-verification,
    title = "Verification and Refinement of Natural Language Explanations through {LLM}-Symbolic Theorem Proving",
    author = "Quan, Xin  and
      Valentino, Marco  and
      Dennis, Louise A.  and
      Freitas, Andre",
    editor = "Al-Onaizan, Yaser  and
      Bansal, Mohit  and
      Chen, Yun-Nung",
    booktitle = "Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing",
    month = nov,
    year = "2024",
    address = "Miami, Florida, USA",
    publisher = "Association for Computational Linguistics",
    url = "https://aclanthology.org/2024.emnlp-main.172",
    pages = "2933--2958",
    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.",
}

@INPROCEEDINGS{10704818,
  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},
  booktitle={2024 20th IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications (MESA)}, 
  title={Trustworthy ROS Software Architecture for Autonomous Drones Missions: From RoboChart Modelling to ROS Implementation}, 
  year={2024},
  volume={},
  number={},
  pages={1-7},
note={[<span class="tas_vn">TAS Verifiability Node</span>]},
  keywords={Mechatronics;Software architecture;Surveillance;Computer architecture;Software;Personnel;Formal specifications;Robots;Testing;Drones;robochart;ros;drone;firefighting;software;robots;trustworthy architecture;trustworthy},
  doi={10.1109/MESA61532.2024.10704818}}

@inproceedings{quan-etal-2024-enhancing,
    title = "Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement",
    author = "Quan, Xin  and
      Valentino, Marco  and
      Dennis, Louise  and
      Freitas, Andre",
    editor = "Graham, Yvette  and
      Purver, Matthew",
    booktitle = "Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers)",
    month = mar,
    year = "2024",
    address = "St. Julian{'}s, Malta",
    publisher = "Association for Computational Linguistics",
    url = "https://aclanthology.org/2024.eacl-long.1",
    pages = "1--22",
    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.",
	}

@inproceedings{10.5555/3635637.3663060, author = {Xu, Mengwei and Dennis, Louise A. and Mustafa, Mustafa A.},
	title = {Safeguard Privacy for Minimal Data Collection with Trustworthy Autonomous Agents},
	year = {2024}, isbn = {9798400704864}, publisher = {International Foundation for Autonomous Agents and Multiagent Systems}, address = {Richland, SC},
	abstract = {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, },
	series = {AAMAS '24},
note={[<span class="tas_vn">TAS Verifiability Node</span>, <span class="car">Computational Agent Responsibility</span>]}
}

@InProceedings{10.1007/978-3-031-43264-4_22,
author="Stringer, Peter
and Cardoso, Rafael C.
and Dixon, Clare
and Fisher, Michael
and Dennis, Louise A.",
editor="Malvone, Vadim
and Murano, Aniello",
title="Adaptive Cognitive Agents: Updating Action Descriptions and Plans",
booktitle="Multi-Agent Systems",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="345--362",
abstract="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.",
isbn="978-3-031-43264-4",
note={[<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>]}
}
@ARTICLE{10380243,
  author={Weir, Charles and Dyson, Anna and Jogunola, Olamide and Dennis, Louise and Paxton-Fear, Katie},
  journal={Computer}, 
  title={Interlinked Computing in 2040: Safety, Truth, Ownership, and Accountability}, 
  year={2024},
  volume={57},
  number={1},
  pages={59-68},
  doi={10.1109/MC.2023.3318377}}


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

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

@ARTICLE{10368348,
  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},
  journal={IEEE Transactions on Dependable and Secure Computing},
  title="{Security-Minded Verification of Cooperative Awareness Messages}",
  year={2024},
  volume={21},
  number={4},
  pages={4048-4065},
  keywords={Security;Protocols;Runtime;Safety;Monitoring;Computer crime;Threat modeling;Verification;security;safety;threat modeling;connected autonomous vehicles;cooperative awareness messages},
  doi={10.1109/TDSC.2023.3345543},
note={[<span class="tas_vn">TAS Verifiability Node</span>]}
}

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

@InProceedings{10.1007/978-3-031-47994-6_23,
author="Collenette, Joe
and Dennis, Louise
and Fisher, Michael",
editor="Bramer, Max
and Stahl, Frederic",
title="Prospective Responsibility for Multi-agent Systems",
booktitle="Artificial Intelligence XL",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="247--252",
abstract="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.",
isbn="978-3-031-47994-6",
note={[<span class="car">Computational Agent Responsibility</span>]}
}

@InProceedings{EXTRAAMAS23,
author="Xu, Yifan
and Collenette, Joe
and Dennis, Louise
and Dixon, Clare",
editor="Calvaresi, Davide
and Najjar, Amro
and Omicini, Andrea
and Aydogan, Reyhan
and Carli, Rachele
and Ciatto, Giovanni
and Mualla, Yazan
and Fr{\"a}mling, Kary",
title="Dialogue Explanations for Rule-Based AI Systems",
booktitle="Explainable and Transparent AI and Multi-Agent Systems",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="59--77",
abstract="The need for AI systems to explain themselves is increasingly recognised as a priority, particularly in domains where incorrect decisions can result in harm and, in the worst cases, death. Explainable Artificial Intelligence (XAI) tries to produce human-understandable explanations for AI decisions. However, most XAI systems prioritize factors such as technical complexities and research-oriented goals over end-user needs, risking information overload. This research attempts to bridge a gap in current understanding and provide insights for assisting users in comprehending the rule-based system's reasoning through dialogue. The hypothesis is that employing dialogue as a mechanism can be effective in constructing explanations. A dialogue framework for rule-based AI systems is presented, allowing the system to explain its decisions by engaging in ``Why?'' and ``Why not?'' questions and answers. We establish formal properties of this framework and present a small user study with encouraging results that compares dialogue-based explanations with proof trees produced by the AI System.",
note={[<span class="car">Computational Agent Responsibility</span>]},
isbn="978-3-031-4087}

@InProceedings{SGAI23,
author="Collenette, Joe and Dennis, Louise and Fisher, Michael",
editor="Bramer, Max and Stahl, Frederic",
title="{Prospective Responsibility for Multi-agent Systems}",
booktitle="Artificial Intelligence XL",
year="2023",
publisher="Springer",
pages="247--252",
note={[<span class="car">Computational Agent Responsibility</span>]},
isbn="978-3-031-47994-6"
}

@article{Anderson_2023,
	doi = {10.4204/eptcs.391.10},  
	url = {https://doi.org/10.4204%2Feptcs.391.10},
	year = 2023,
	month = {sep},
	publisher = {Open Publishing Association},
	volume = {391},
	pages = {83--88},
	author = {Christopher R. Anderson and Louise A. Dennis},
	title = {Autonomous Systems{\textquotesingle} Safety Cases for use in {UK} Nuclear Environments},
	journal = {Electronic Proceedings in Theoretical Computer Science},
	note={[<span class="rain">RAIN</span>]}
}

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

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

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

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

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

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

@inproceedings{DBLP:conf/atal/0001M23,
  author       = {Angelo Ferrando and
                  Vadim Malvone},
  editor       = {Noa Agmon and
                  Bo An and
                  Alessandro Ricci and
                  William Yeoh},
  title        = {Towards the Verification of Strategic Properties in Multi-Agent Systems
                  with Imperfect Information},
  booktitle    = {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},
  publisher    = {{ACM}},
  year         = {2023},
  url          = {https://dl.acm.org/doi/10.5555/3545946.3598713},
  doi          = {10.5555/3545946.3598713},
  timestamp    = {Tue, 23 May 2023 16:02:48 +0200},
  biburl       = {https://dblp.org/rec/conf/atal/0001M23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}



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

@book{dennisfisher23,
author={Louise A. Dennis and Michael Fisher},
title={Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines},
publisher={Cambridge University Press},
year={2023},
note = {[<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>]}
}

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

@ARTICLE{nallur23,
      title={A Partially Synthesized Position on the Automation of Machine Ethics},
      journal={DISO},
      volume=2,
      number=14,
      year=2023,
      doi={10.1007/s44206-023-00040-8},
      author={Vivek Nallur and Louise Dennis and Selmer Bringsjord and Naveen Govindarajulu},
      note = {[<span class="tas_vn">TAS Verifiability Node</span>]}
      }
      
@ARTICLE{Verifiability:IEEE:23,
  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},
  journal={IEEE Computer}, 
  title="{Trustworthy Autonomous Systems Through Verifiability}", 
  year={2023},
  volume={56},
  number={2},
  pages={40-47},
doi={10.1109/MC.2022.3192206},
note = {[<span class="tas_vn">TAS Verifiability Node</span>]}}

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

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

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

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

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

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

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

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

 @InProceedings{IFM_Keynote,
author="Dennis, Louise A.",
editor="ter Beek, Maurice H.
and Monahan, Rosemary",
title="Verifying Autonomous Systems",
booktitle="Integrated Formal Methods",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="3--17",
abstract="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.",
isbn="978-3-031-07727-2",
doi="10.1007/978-3-031-07727-2_1",
note = {[<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>]}
}

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

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

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

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

@article{DennisNetReason,
   author = {Dennis, Louise A and Fu, Yu and Slavkovik, Marija},
    title = "{Markov chain model representation of information diffusion in social networks}",
    journal = {Journal of Logic and Computation},
    year = {2022},
    month = {03},
    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.}",
    issn = {0955-792X},
    doi = {10.1093/logcom/exac018},
    url = {https://doi.org/10.1093/logcom/exac018},
    note = {exac018},
    eprint = {https://academic.oup.com/logcom/advance-article-pdf/doi/10.1093/logcom/exac018/42844230/exac018.pdf}
    }

@techreport{principles_white_paper_2021,
	title = {Principles for the {Development} and {Assurance} of {Autonomous} {Systems} for {Safe} {Use} in {Hazardous} {Environments}},
	copyright = {Creative Commons Attribution 4.0 International, Open Access},
	url = {https://zenodo.org/record/5012322},
	abstract = {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.},
	language = {en},
	urldate = {2021-08-30},
	institution = {Zenodo},
	author = {Luckcuck, Matt and Fisher, Michael and Dennis, Louise and Frost, Steve and White, Andy and Styles, Doug},
	month = jun,
	year = {2021},
	doi = {10.5281/ZENODO.5012322},
	keywords = {Robotics, Validation, Verification, Autonomous Systems, Assurance, Hazardous Environments},
	annote = {Other
This 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/},
note={[<span class="rain">RAIN</span>]}
}



@InProceedings{Cardoso21f,
author="Cardoso, Rafael C.
and Ferrando, Angelo
and Papacchini, Fabio
and Luckcuck, Matt
and Linker, Sven
and Payne, Terry R.",
editor="Ahlbrecht, Tobias
and Dix, J{\"u}rgen
and Fiekas, Niklas
and Krausburg, Tabajara",
title="MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest",
booktitle="The Multi-Agent Programming Contest 2021",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="82--107",
abstract="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.",
isbn="978-3-030-88549-6",
doi="10.1007/978-3-030-88549-6_4",
note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}
}

@article{TeachMe21,
author = {Kheng Lee Koay and Matt Webster and Clare Dixon and Paul Gainer and Dag Syrdal and Michael Fisher and Kerstin Dautenhahn},
doi = {doi:10.1515/pjbr-2021-0028},
url = {https://www.degruyter.com/document/doi/10.1515/pjbr-2021-0028/html},
title = "{Use and Usability of Software Verification Methods to Detect Behaviour Interference when Teaching an Assistive Home Companion Robot: A proof-of-concept study}",
journal = {Paladyn, Journal of Behavioral Robotics},
number = {1},
volume = {12},
year = {2021},
pages = {402--422},
note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}
}

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

@inproceedings{Zhang2021,
author={Tianyu Zhang and Louise A. Dennis and Matt Webster},
title={{AsteroidX}: An Asteroid Exploration Simulation and Visualisation Tool},
booktitle={Workshop on Advances in Space Robotics and back to Earth},
year=2021,
note={[<span class="fs">FAIR-Space</span>]}
}

@incollection{Slocombe2021,
author="Slocombe, Will
and Dennis, Louise",
editor="Dainton, Barry
and Slocombe, Will
and Tanyi, Attila",
title="Enforcing Machine Ethics: Considering Governor Modules through Martha Wells's Murderbot Diaries",
bookTitle="Minding the Future: Artificial Intelligence, Philosophical Visions and Science Fiction",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="65--86",
abstract="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.",
isbn="978-3-030-64269-3",
doi="10.1007/978-3-030-64269-3_4",
url="https://doi.org/10.1007/978-3-030-64269-3_4"
}

@Article{PDWJF21,
AUTHOR = {Page, Vincent and Dadswell, Christopher and Webster, Matt and Jump, Mike and Fisher, Michael},
TITLE = "{Towards the Determination of Safe Operating Envelopes for Autonomous UAS in Offshore Inspection Missions}",
JOURNAL = {Robotics},
VOLUME = {10},
YEAR = {2021},
NUMBER = {3},
ARTICLE-NUMBER = {97},
URL = {https://www.mdpi.com/2218-6581/10/3/97},
ISSN = {2218-6581},
ABSTRACT = {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.},
DOI = {10.3390/robotics10030097},
note={[<span class="orca">ORCA</span>]}
}

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

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


@article{luckcuck_using_2021,
author = {Matt Luckcuck},
title ={Using formal methods for autonomous systems: Five recipes for formal verification},
journal = {Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability},
volume = {0},
number = {0},
pages = {1748006X211034970},
year = {2021},
doi = {10.1177/1748006X211034970},
URL = { https://doi.org/10.1177/1748006X211034970},
eprint = { https://doi.org/10.1177/1748006X211034970 },
note={[<span class="rain">RAIN</span>]}
}

@Article{jsan10030041,
AUTHOR = {Alves, {Gleifer Vaz} and Dennis, Louise and Fisher, Michael},
TITLE = "{A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations}",
JOURNAL = {Journal of Sensor and Actuator Networks},
VOLUME = {10},
YEAR = {2021},
NUMBER = {3},
ARTICLE-NUMBER = {41},
URL = {https://www.mdpi.com/2224-2708/10/3/41},
ISSN = {2224-2708},
ABSTRACT = {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.},
DOI = {10.3390/jsan10030041},
note={[<span class="tas_vn">TAS Verifiability Node</span>]}
}

@Article{areaeditorial,
AUTHOR = {Cardoso, Rafael C. and Ferrando, Angelo and Briola, Daniela and Menghi, Claudio and Ahlbrecht, Tobias},
TITLE = {Special Issue: Agents and Robots for Reliable Engineered Autonomy},
JOURNAL = {Journal of Sensor and Actuator Networks},
VOLUME = {10},
YEAR = {2021},
NUMBER = {3},
ARTICLE-NUMBER = {47},
URL = {https://www.mdpi.com/2224-2708/10/3/47},
ISSN = {2224-2708},
ABSTRACT = {The study of autonomous agents is a well-established area that has been researched for decades, both from a design and implementation viewpoint [...]},
DOI = {10.3390/jsan10030047}
}

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

@inproceedings{Cardoso21e,
	author="Cardoso, Rafael C.
	and Ferrando, Angelo
	and Papacchini, Fabio",
	editor="Dignum, Frank
	and Corchado, Juan Manuel
	and De La Prieta, Fernando",
	title="Automated Planning and BDI Agents: A Case Study",
	booktitle="Advances in Practical Applications of Agents, Multi-Agent Systems, and Social Good. The PAAMS Collection",
	year="2021",
	publisher="Springer International Publishing",
	address="Cham",
	pages="52--63",
	abstract="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.",
	isbn="978-3-030-85739-4",
	doi={10.1007/978-3-030-85739-4_5},
	note={[<span class="raeng">RAEng</span>, <span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}
}

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

@inproceedings{fisher2021increasing,
  title={Increasing Confidence in Autonomous Systems},
  author={Fisher, Michael and Ferrando, Angelo and Cardoso, Rafael C.},
  booktitle={Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21)},
  year={2021},
  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>]}
}

@article{p7001,
  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},
TITLE={IEEE P7001: A Proposed Standard on Transparency},
JOURNAL={Frontiers in Robotics and AI},
VOLUME={8},
PAGES={225},
YEAR={2021},
URL={https://www.frontiersin.org/article/10.3389/frobt.2021.665729},
DOI={10.3389/frobt.2021.665729},
ISSN={2296-9144},
ABSTRACT={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.},
note={[<span class="tas_vn">TAS Verifiability Node</span>, <span class="va">Verifiable Autonomy</span>]}
}

@Article{Cardoso21d,
author={Cardoso, Rafael C.
and Kourtis, Georgios
and Dennis, Louise A.
and Dixon, Clare
and Farrell, Marie
and Fisher, Michael
and Webster, Matt},
title={A Review of Verification and Validation for Space Autonomous Systems},
journal={Current Robotics Reports},
year={2021},
month={Jun},
day={18},
abstract={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.},
issn={2662-4087},
doi={10.1007/s43154-021-00058-1},
url={https://doi.org/10.1007/s43154-021-00058-1},
note={[<span class="fs">FAIR-Space</span>]}
}

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


@article{cardoso21e,
AUTHOR = {Cardoso, Rafael C. and Ferrando, Angelo and Briola, Daniela and Menghi, Claudio and Ahlbrecht, Tobias},
TITLE = {Agents and Robots for Reliable Engineered Autonomy:A Perspective from the Organisers of AREA 2020},
JOURNAL = {Journal of Sensor and Actuator Networks},
VOLUME = {10},
YEAR = {2021},
NUMBER = {2},
ARTICLE-NUMBER = {33},
URL = {https://www.mdpi.com/2224-2708/10/2/33},
ISSN = {2224-2708},
ABSTRACT = {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.},
DOI = {10.3390/jsan10020033},
note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}
}

@article{robotics10020067,
author = {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},
title = {An Overview of Verification and Validation Challenges for Inspection Robots},
journal = {Robotics},
volume = {10},
year = {2021},
number = {2},
url = {https://www.mdpi.com/2218-6581/10/2/67},
issn = {2218-6581},
abstract = {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.},
doi = {10.3390/robotics10020067},
note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>, <span class="raeng">RAEng</span>]}
}

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

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

@inproceedings{Cardoso21c,
      author={Rafael C. Cardoso and Angelo Ferrando and Louise A. Dennis and Michael Fisher},
      title={Implementing Ethical Governors in BDI},
      booktitle={9th International Workshop on Engineering Multi-Agent Systems},
      year={2021},
      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>]}
      }


@InProceedings{Cardoso21b,
title={Agile Tasking of Robotic Systems with Explicit Autonomy},
volume={34},
DOI={10.32473/flairs.v34i1.128481},
booktitle={The International FLAIRS Conference Proceedings},
author={Cardoso, Rafael C. and Michaloski, John L. and Schlenoff, Craig and Ferrando, Angelo and Dennis, Louise A. and Fisher, Michael},
year={2021},
note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>]}
}

@article{Cardoso21a,
title={A Review of Agent-Based Programming for Multi-Agent Systems},
volume={10},
ISSN={2073-431X},
DOI={10.3390/computers10020016},
number={2},
journal={Computers},
publisher={MDPI AG},
author={Cardoso, Rafael C. and Ferrando, Angelo},
year={2021},
month={Jan},
pages={16},
note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}
}

@article{Ferrando21,
	author = {Ferrando, Angelo and Dennis, Louise A. and Cardoso, Rafael C. and Fisher, Michael and Ancona, Davide and Mascardi, Viviana},
	title = {Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems},
	year = {2021},
	issue_date = {May 2021},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {30},
	number = {4},
	issn = {1049-331X},
	url = {https://doi.org/10.1145/3447246},
	doi = {10.1145/3447246},
	abstract = {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.},
	journal = {ACM Trans. Softw. Eng. Methodol.},
	month = may,
	articleno = {43},
	numpages = {43},
	keywords = {autonomous systems, model checking, trace expressions, Runtime verification, MCAPL},
      	note={[<span class="rain">RAIN</span>, <span class="fs">FAIR-Space</span>, <span class="orca">ORCA</span>]}
     }

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

@article{DennisAAAI21,
author = {Louise A. Dennis and Martin Mose Bentzen and Felix Lindner and Michael Fisher},
title={Verifiable Machine Ethics in Changing Contexts},
volume={35},
url={https://ojs.aaai.org/index.php/AAAI/article/view/17366},
number={13},
journal={Proceedings of the AAAI Conference on Artificial Intelligence},
year={2021},
month={May},
pages={11470-11478} ,
      note={[<span class="va">Verifiable Autonomy</span>, <span class="tas_vn">TAS Verifiability Node</span>]}
      }

@article{FisherMRSWY21,
  author    = {Michael Fisher and
               Viviana Mascardi and
               Kristin Yvonne Rozier and
               Bernd{-}Holger Schlingloff and
               Michael Winikoff and
               Neil Yorke{-}Smith},
  title     = {Towards a Framework for Certification of Reliable Autonomous Systems},
  journal   = {Autonomous Agents and Multi Agent Systems},
  volume    = {35},
  number    = {1},
  pages     = {8},
  year      = {2021},
  doi       = {10.1007/s10458-020-09487-2},
  note={[<span class="s4">S4</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>]}
}



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

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

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

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

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

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

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

@InProceedings{Cardoso20d,
author="Cardoso, Rafael C.
and Ferrando, Angelo
and Papacchini, Fabio",
title="LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest",
booktitle="The Multi-Agent Programming Contest 2019",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="31--58",
isbn="978-3-030-59299-8",
doi={10.1007/978-3-030-59299-8_2},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}
}

@InProceedings{10.1007/978-3-030-54994-7_16,
author="Alves, Gleifer Vaz
and Dennis, Louise
and Fisher, Michael",
editor="Sekerinski, Emil
and Moreira, Nelma
and Oliveira, Jos{\'e} N.
and Ratiu, Daniel
and Guidotti, Riccardo
and Farrell, Marie
and Luckcuck, Matt
and Marmsoler, Diego
and Campos, Jos{\'e}
and Astarte, Troy
and Gonnord, Laure
and Cerone, Antonio
and Couto, Luis
and Dongol, Brijesh
and Kutrib, Martin
and Monteiro, Pedro
and Delmas, David",
title="Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent",
booktitle="Formal Methods. FM 2019 International Workshops",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="217--232",
abstract="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.",
isbn="978-3-030-54994-7",
note = {[<span class="va">Verifiable Autonomy</span>]}
}

@article{dennis_see_2020,
	Abstract = {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.},
	Author = {Dennis, Louise A. },
	Da = {2020/08/04},
	Date-Added = {2020-08-06 13:39:55 +0100},
	Date-Modified = {2020-08-06 13:39:55 +0100},
	Doi = {10.1007/s11948-020-00244-y},
	Id = {Dennis2020},
	Isbn = {1471-5546},
	Journal = {Science and Engineering Ethics},
	Title = {Computational Goals, Values and Decision-Making},
	Ty = {JOUR},
	Url = {https://doi.org/10.1007/s11948-020-00244-y},
	Year = {2020},
	Bdsk-Url-1 = {https://doi.org/10.1007/s11948-020-00244-y}}

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

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

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

@unpublished{Cardoso20c,
  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.},
  title     = {Verification and Validation for Space Robotics},
  year      = {2020},
  note = {Poster presented at the Opportunities and Challenges in Space Robotics Workshop held with ICRA 2020. [<span class="fs">FAIR-SPACE</span>]}
}

@InProceedings{Ferrando20a,
author="Ferrando, Angelo
and Cardoso, Rafael C.
and Fisher, Michael
and Ancona, Davide
and Franceschini, Luca
and Mascardi, Viviana",
title="ROSMonitoring: A Runtime Verification Framework for ROS",
booktitle="Towards Autonomous Robotic Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="387--399",
doi="10.1007/978-3-030-63486-5_40",
isbn="978-3-030-63486-5",
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}
}

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

@inproceedings{Dennis20,
  author="Dennis, Louise A.
and Slavkovik, Marija",
editor="Bassiliades, Nick
and Chalkiadakis, Georgios
and de Jonge, Dave",
title="Model-Checking Information Diffusion in Social Networks with PRISM",
booktitle="Multi-Agent Systems and Agreement Technologies",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="475--492",
abstract="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.",
isbn="978-3-030-66412-1"
}

@inproceedings{Cardoso20b,
  author="Cardoso, Rafael C.
and Ferrando, Angelo
and Dennis, Louise A.
and Fisher, Michael",
editor="Bassiliades, Nick
and Chalkiadakis, Georgios
and de Jonge, Dave",
title="An Interface for Programming Verifiable Autonomous Agents in ROS",
booktitle="Multi-Agent Systems and Agreement Technologies",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="191--205",
abstract="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.",
isbn="978-3-030-66412-1",
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

@inproceedings{Cardoso20a,
author="Cardoso, Rafael C.
and Farrell, Marie
and Luckcuck, Matt
and Ferrando, Angelo
and Fisher, Michael",
editor="Lee, Ritchie
and Jha, Susmit
and Mavridou, Anastasia
and Giannakopoulou, Dimitra",
title="Heterogeneous Verification of an Autonomous Curiosity Rover",
booktitle="NASA Formal Methods",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="353--360",
abstract="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.",
isbn="978-3-030-55754-6",
doi="10.1007/978-3-030-55754-6_20",
note = {[<span class="fs">FAIR-SPACE</span>]}
}

@incollection{Alves2020,
author="Alves, Gleifer Vaz
and Dennis, Louise
and Fernandes, Lucas
and Fisher, Michael",
editor="Leitner, Andrea
and Watzenig, Daniel
and Ibanez-Guzman, Javier",
title="Reliable Decision-Making in Autonomous Vehicles",
bookTitle="Validation and Verification of Automated Systems: Results of the ENABLE-S3 Project",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="105--117",
abstract="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.",
isbn="978-3-030-14628-3",
doi="10.1007/978-3-030-14628-3_10",
url="https://doi.org/10.1007/978-3-030-14628-3_10"
}

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

@article{Linker2019a,
author = {Sven Linker and Michele Sevegnani},
title = {Target counting with Presburger constraints and its application in sensor networks},
journal = {Proceedings of the Royal Society A},
volume = {475},
number = {2231},
year = {2019},
url = {https://doi.org/10.1098/rspa.2019.0278},
doi = {10.1098/rspa.2019.0278},
  note = {[<span class="s4">S4</span>]}
}

@inproceedings{Farrell2019b,
  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},
  title     = {Modular Verification of Autonomous Space Robotics},
  booktitle = {Assurance of Autonomy for Robotic Space Missions Workshop},
  year      = {2019},
  note = {[<span class="fs">FAIR-SPACE</span>]}
}

@InProceedings{Farrell2019,
author="Farrell, Marie
and Bradbury, Matthew
and Fisher, Michael
and Dennis, Louise A.
and Dixon, Clare
and Yuan, Hu
and Maple, Carsten",
editor="{\"O}lveczky, Peter Csaba
and Sala{\"u}n, Gwen",
title="Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages",
booktitle="Software Engineering and Formal Methods",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="471--490",
abstract="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.",
isbn="978-3-030-30446-1",
note = {[<span class="fs">FAIR-SPACE</span>]}
}

@InProceedings{Luckcuck2019Summary,
author="Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael",
editor="Ahrendt, Wolfgang and Tapia Tarifa, Silvia Lizeth",
title="A Summary of Formal Specification and Verification of Autonomous Robotic Systems",
booktitle="Integrated Formal Methods",
year="2019",
publisher="Springer International Publishing",
address="Cham",
doi = {10.1007/978-3-030-34968-4_33},
pages="538--541",
abstract="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.",
isbn="978-3-030-34968-4",
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}
}

@article{Luckcuck2019,
title = {{Formal Specification and Verification of Autonomous Robotic Systems: A Survey}},
author = {Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael},
doi = {10.1145/3342355},
eprint = {1807.00048},
issn = {03600300},
journal = {ACM Comput. Surv.},
month = {sep},
number = {5},
pages = {1--41},
url = {https://arxiv.org/abs/1807.00048 http://dl.acm.org/citation.cfm?doid=3362097.3342355},
volume = {52},
year = {2019},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}
}

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

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

@inproceedings{Koeman19EMAS,
author="Koeman, Vincent J.
and Dennis, Louise A.
and Webster, Matt
and Fisher, Michael
and Hindriks, Koen",
editor="Dennis, Louise A.
and Bordini, Rafael H.
and Lesp{\'e}rance, Yves",
title="The ``Why Did You Do That?'' Button: Answering Why-Questions for End Users of Robotic Systems",
booktitle="Engineering Multi-Agent Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="152--172",
abstract="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.",
isbn="978-3-030-51417-4",
  note = {[<span class="orca">ORCA</span>, <span class="va">Verifiable Autonomy</span>]}
}

@inproceedings{Cardoso19EMAS,
author="Cardoso, Rafael C.
and Dennis, Louise A.
and Fisher, Michael",
editor="Dennis, Louise A.
and Bordini, Rafael H.
and Lesp{\'e}rance, Yves",
title="Plan Library Reconfigurability in BDI Agents",
booktitle="Engineering Multi-Agent Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="195--212",
abstract="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.",
isbn="978-3-030-51417-4",
doi="10.1007/978-3-030-51417-4_10",
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

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

@ARTICLE{BremnerDFW19,
author={P. {Bremner} and L. A. {Dennis} and M. {Fisher} and A. F. {Winfield}},
journal={Proceedings of the IEEE},
title={On Proactive, Transparent, and Verifiable Ethical Reasoning for Robots},
year={2019},
volume={},
number={},
pages={1-21},
keywords={Robots;Cognition;Ethics;Predictive models;Safety;Standards;Computer architecture;Ethics;formal verification;intelligent robots;software architecture.},
doi={10.1109/JPROC.2019.2898267},
ISSN={0018-9219},
month={},
note = {[<span  class="va">Verifiable Autonomy</span>]}}

@inproceedings{Cardoso19AAMAS,
author = {Cardoso, Rafael C. and Bordini, Rafael H.},
title = {Decentralised Planning for Multi-Agent Programming Platforms},
year = {2019},
isbn = {9781450363099},
publisher = {International Foundation for Autonomous Agents and Multiagent Systems},
address = {Richland, SC},
booktitle = {Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems},
pages = {799–807},
numpages = {9},
keywords = {multi-agent development platforms, multi-agent planning, hierarchical task network, goal allocation},
location = {Montreal QC, Canada},
series = {AAMAS '19},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

@inproceedings{NalonHD18,
author = {Cl\'audia Nalon and Ullrich Hustadt and Clare Dixon},
title = "{KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments}",
journal = {Journal of Automated Reasoning},
year = {2018},
  volume    = {},
publisher = {Springer},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

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

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

@inproceedings{HustadtEtAl:PAAR2018,
author = {Ullrich Hustadt and Cl\'audia Nalon and Clare Dixon},
title = "{Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics}",
booktitle = {Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)},
year = {2018},
pages = {34--48},
editor = {Boris Konev and Josef Urban and Philipp R\"ummer},
number = 2162,
series = {CEUR Workshop Proceedings},
address = {Aachen},
issn = {1613-0073},
url = {http://ceur-ws.org/Vol-2162/#paper-04},
venue = {Oxford, UK},
eventdate = {2018-07-19},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

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

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

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

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

@InProceedings{Fisher:WoSoCer18,
   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
            and David Flynn and Valentin Robu and Xingu Zhao},
    title = "{Verifiable Self-Certifying Autonomous Systems}",
booktitle = {Proc. 8th IEEE International Workshop on Software Certification (WoSoCer)},
year = {2018},
address = {Memphis, USA},
note = {[<span class="orca">ORCA</span>]}
}

@INPROCEEDINGS{Dinmohammadi:PHM18,
author={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},
booktitle={Proc. Prognostics and System Health Management
     Conference (PHM-Chongqing)},
title="{Certification of Safe and Trusted Robotic Inspection of Assets}",
year={2018},
volume={},
number={},
address = {Chongqing, China},
pages={},
publisher = {IEEE},
note = {[<span class="orca">ORCA</span>]}
}

@InProceedings{WinikoffDF:EMAS18,
   author = {Michael Winikoff and Louise A. Dennis and Michael Fisher},
   title = "{Slicing Agent Programs for more Efficient Verification}",
booktitle = {Proc. 6th International Workshop in Engineering Multi-Agent Systems},
year = {2019},
volume={11375},
pages={139-157},
editor={D. Weyns and V. Mascardi and A. Ricci},
series={Lecture Notes in Computer Science},
address = {Stockholm, Sweden},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}
}

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

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

@InProceedings{8539217,
  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
            and David Flynn and Valentin Robu and Xingu Zhao},
  title     = {Verifiable Self-Certifying Autonomous Systems},
  booktitle = {2018 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)},
  year      = {2018},
  pages     = {341-348},
  month     = {Oct},
  doi       = {10.1109/ISSREW.2018.00028},
  note = {[<span class="orca">ORCA</span>]}
}

@inproceedings{DBLP:conf/icfem/GainerLDH018,
  author    = {Paul Gainer and
               Sven Linker and
               Clare Dixon and
               Ullrich Hustadt and
               Michael Fisher},
  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption
               in Networks of Pulse-Coupled Oscillators},
  booktitle = {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},
  year      = {2018},
  crossref  = {DBLP:conf/icfem/2018},
  url       = {https://doi.org/10.1007/978-3-030-02450-5\_10},
  doi       = {10.1007/978-3-030-02450-5\_10},
  timestamp = {Mon, 05 Nov 2018 11:04:23 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/icfem/GainerLDH018},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="s4">S4</span>]}
}



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

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

@inproceedings{DBLP:conf/fmics/GainerDDFHSW17,
  author    = {Paul Gainer and
               Clare Dixon and
               Kerstin Dautenhahn and
               Michael Fisher and
               Ullrich Hustadt and
               Joe Saunders and
               Matt Webster},
  title     = {CRutoN: Automatic Verification of a Robotic Assistant's Behaviours},
  booktitle = {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},
  year      = {2017},
  crossref  = {DBLP:conf/fmics/2017},
  url       = {https://doi.org/10.1007/978-3-319-67113-0\_8},
  doi       = {10.1007/978-3-319-67113-0\_8},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/fmics/GainerDDFHSW17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@inproceedings{DBLP:conf/cade/NalonMD14,
  author    = {Cl{\'{a}}udia Nalon and
               Jo{\~{a}}o Marcos and
               Clare Dixon},
  title     = {Clausal Resolution for Modal Logics of Confluence},
  booktitle = {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},
  year      = {2014},
  crossref  = {DBLP:conf/cade/2014},
  url       = {https://doi.org/10.1007/978-3-319-08587-6\_24},
  doi       = {10.1007/978-3-319-08587-6\_24},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/NalonMD14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

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

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

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

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

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

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

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

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

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

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

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

@inproceedings{DBLP:conf/atal/DennisSF16,
  author    = {Louise A. Dennis and
               Marija Slavkovik and
               Michael Fisher},
  title     = {"How Did They Know?" - Model-Checking for Analysis of Information
               Leakage in Social Networks},
  booktitle = {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},
  year      = {2016},
  crossref  = {DBLP:conf/atal/2016coin},
  url       = {https://doi.org/10.1007/978-3-319-66595-5\_3},
  doi       = {10.1007/978-3-319-66595-5\_3},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/atal/DennisSF16},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

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

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

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

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

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

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

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

@inproceedings{DBLP:conf/ecai/DennisF14,
  author    = {Louise A. Dennis and
               Michael Fisher},
  title     = {Actions with Durations and Failures in {BDI} Languages},
  booktitle = {{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},
  year      = {2014},
  crossref  = {DBLP:conf/ecai/2014},
  url       = {https://doi.org/10.3233/978-1-61499-419-0-995},
  doi       = {10.3233/978-1-61499-419-0-995},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/ecai/DennisF14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

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

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

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

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

@article{DBLP:journals/corr/abs-1803-10478,
  author    = {Muffy Calder and
               Simon Dobson and
               Michael Fisher and
               Julie A. McCann},
  title     = {Making Sense of the World: Models for Reliable Sensor-Driven Systems},
  journal   = {CoRR},
  volume    = {abs/1803.10478},
  year      = {2018},
  url       = {http://arxiv.org/abs/1803.10478},
  archivePrefix = {arXiv},
  eprint    = {1803.10478},
  timestamp = {Mon, 13 Aug 2018 16:46:50 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1803-10478},
  bibsource = {dblp computer science bibliography, https://dblp.org}
  note = {[<span class="s4">S4</span>]}
}

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

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

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

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

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


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


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

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

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

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

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

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

@inproceedings{DBLP:conf/ifm/SheridanML22,
  author       = {Ois{\'{\i}}n Sheridan and
                  Rosemary Monahan and
                  Matt Luckcuck},
  editor       = {Maurice H. ter Beek and
                  Rosemary Monahan},
  title        = {A Requirements-Driven Methodology: Formal Modelling and Verification
                  of an Aircraft Engine Controller},
  booktitle    = {Integrated Formal Methods - 17th International Conference, {IFM} 2022,
                  Lugano, Switzerland, June 7-10, 2022, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {13274},
  pages        = {352--356},
  publisher    = {Springer},
  year         = {2022},
  url          = {https://doi.org/10.1007/978-3-031-07727-2\_21},
  doi          = {10.1007/978-3-031-07727-2\_21},
  timestamp    = {Fri, 03 Jun 2022 16:42:30 +0200},
  biburl       = {https://dblp.org/rec/conf/ifm/SheridanML22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
  note = {[VALU3S]}
}



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

@article{BECKER2025104917,
title = "{An Expedited BDI Agent Architecture: Improving the Responsiveness of
         Agent-based Autonomous Systems for Handling Critical Situations}",
journal = {Robotics and Autonomous Systems},
volume = {186},
pages = {104917},
year = {2025},
issn = {0921-8890},
doi = {10.1016/j.robot.2025.104917},
author = {Leandro Buss Becker and Iago {de Oliveira Silvestre} and Jomi Fred Hubner and Michael Fisher},
note={[<span class="raeng">RAEng</span>]}
}