Dennis BibTeX References
@InProceedings{10.1007/978-3-031-48539-8_1,
author="Cardoso, Rafael C.
and Ferrando, Angelo
and Collenette, Joe
and Dennis, Louise A.
and Fisher, Michael",
editor="Ciortea, Andrei
and Dastani, Mehdi
and Luo, Jieting",
title="Towards Forward Responsibility in BDI Agents",
booktitle="Engineering Multi-Agent Systems",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="3--22",
abstract="In this paper, we discuss forward responsibilities in Belief-Desire-Intention agents, that is, responsibilities that can drive future decision-making. We focus on individual rather than global notions of responsibility. Our contributions include: (a) extended operational semantics for responsibility-aware rational agents; (b) hierarchical responsibilities for improving intention selection based on the priorities (i.e., hierarchical level) of a responsibility; and (c) shared responsibilities which allow agents with the same responsibility to update their priority levels (and consequently commit or not to the responsibility) depending on the lack (or surplus) of agents that are currently engaged with it.",
isbn="978-3-031-48539-8"
}
@InProceedings{10.1007/978-3-031-49133-7_9,
author="Kolker, Simon
and Dennis, Louise
and Fraga Pereira, Ramon
and Xu, Mengwei",
editor="Fornara, Nicoletta
and Cheriyan, Jithin
and Mertzani, Asimina",
title="Uncertain Machine Ethical Decisions Using Hypothetical Retrospection",
booktitle="Coordination, Organizations, Institutions, Norms, and Ethics for Governance of Multi-Agent Systems XVI",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="161--181",
abstract="We propose the use of the hypothetical retrospection argumentation procedure, developed by Sven Ove Hansson to improve existing approaches to machine ethical reasoning by accounting for probability and uncertainty from a position of Philosophy that resonates with humans. Actions are represented with a branching set of potential outcomes, each with a state, utility, and either a numeric or poetic probability estimate. Actions are chosen based on comparisons between sets of arguments favouring actions from the perspective of their branches, even those branches that led to an undesirable outcome. This use of arguments allows a variety of philosophical theories for ethical reasoning to be used, potentially in flexible combination with each other. We implement the procedure, applying consequentialist and deontological ethical theories, independently and concurrently, to an autonomous library system use case. We introduce a preliminary framework that seems to meet the varied requirements of a machine ethics system: versatility under multiple theories and a resonance with humans that enables transparency and explainability.",
isbn="978-3-031-49133-7"
}
@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"
}
@ARTICLE {10368348,
author = {M. Farrell and M. Bradbury and R. C. Cardoso and M. Fisher and L. A. Dennis and C. Dixon and A. Sheik and H. Yuan and C. Maple},
journal = {IEEE Transactions on Dependable and Secure Computing},
title = {Security-Minded Verification of Cooperative Awareness Messages},
year = {5555},
volume = {},
number = {01},
issn = {1941-0018},
pages = {1-18},
abstract = {Autonomous robotic systems systems are both safety- and security-critical, since a breach in system security may impact safety. In such critical systems, formal verification is used to model the system and verify that it obeys specific functional and safety properties. Independently, threat modelling is used to analyse and manage the cyber security threats that such systems may encounter. Both verification and threat analysis serve the purpose of ensuring that the system will be reliable, albeit from differing perspectives. In prior work, we argued that these analyses should be used to inform one another and, in this paper, we extend our previously defined methodology for security-minded verification by incorporating runtime verification. To illustrate our approach, we analyse an algorithm for sending Cooperative Awareness Messages between autonomous vehicles. Our analysis centres on identifying STRIDE security threats. We show how these can be formalised, and subsequently verified, using a combination of formal tools for static aspects, namely Promela/SPIN and Dafny, and generate runtime monitors for dynamic verification. Our approach allows us to focus our verification effort on those security properties that are particularly important and to consider safety and security in tandem, both statically and at runtime.},
keywords = {security;protocols;runtime;safety;monitoring;computer crime;threat modeling},
doi = {10.1109/TDSC.2023.3345543},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
month = {dec}
}
@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}}
@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"
}
@InProceedings{10.1007/978-3-031-40878-6_4,
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.",
isbn="978-3-031-4087}
@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}
}
@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},
doi={10.1109/REW57809.2023.00062}}
@inproceedings{10.5555/3545946.3598937, 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}, 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. Our main contributions are the underlying theoretical mechanisms for data collection about action performance, the synthesis of new action descriptions from this data, the integration with plan reconfiguration, and a practical implementation to validate the semantics.}, booktitle = {Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems}, pages = {2370–2372}, numpages = {3}, keywords = {beliefs-desires-intentions, action descriptions, ai planning}, location = {London, United Kingdom}, series = {AAMAS '23} }
@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)},
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}
}
@article{nallur23,
author={Vivek Nallur and Louise Dennis and Selmer Bringsjord and Naveen Govindarajulu},
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}
}
@ARTICLE{10042118, 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={Computer}, title={Trustworthy Autonomous Systems Through Verifiability}, year={2023}, volume={56}, number={2}, pages={40-47}, doi={10.1
109/MC.2022.3192206}}
@inproceedings{xu_xlokr22,
author={Yifan Xu and Joe Collenette and Louise A. Dennis and Clare Dixon},
title={Dialogue-Based Explanations for Reasoning in Rule-based Systems},
booktitle={Explainable Logic-Based Knowledge Representation (XLoKR 2022)},
year=2022}
@article{Collenette_2022,
doi = {10.4204/eptcs.371.5},
url = {https://doi.org/10.4204%2Feptcs.371.5},
year = 2022,
month = {sep},
publisher = {Open Publishing Association},
volume = {371},
pages = {62--76},
author = {Joe Collenette and Louise A. Dennis and Michael Fisher},
title = {Advising Autonomous Cars about the Rules of the Road},
journal = {Electronic Proceedings in Theoretical Computer Science}
}
@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}}
@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{10.1007/978-3-031-07727-2_1,
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"
}
@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}
@article{10.1093/logcom/exac018,
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},
}
@CHAPTER{
iet:/content/books/10.1049/pbce131e_ch11,
author = {Rafael C. Cardoso},
affiliation = {Department of Computer Science, University of Manchester},
author = {Marie Farrell},
affiliation = {Department of Computer Science, Maynooth University},
author = {Georgios Kourtis},
affiliation = {Department of Computer Science, University of Manchester},
author = {Matt Webster},
affiliation = {School of Computer Science and Mathematics, Liverpool John Moores University},
author = {Louise A. Dennis},
affiliation = {Department of Computer Science, University of Manchester},
author = {Clare Dixon},
affiliation = {Department of Computer Science, University of Manchester},
author = {Michael Fisher},
affiliation = {Department of Computer Science, University of Manchester},
author = {Alexei Lisitsa},
affiliation = {Department of Computer Science, University of Liverpool},
title = {Verification for space robotics},
booktitle = Space Robotics and Autonomous Systems: Technologies, advances and applications,
publisher = {Institution of Engineering and Technology},
year = {2021},
pages = {377-408},
series = {Control, Robotics & Sensors},
doi = {10.1049/PBCE131E_ch11},
url = {https://digital-library.theiet.org/content/books/10.1049/pbce131e_ch11}
}
@Inbook{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"
}
@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,
}
@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,
}
@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,
}
@Inbook{Dennis2021,
author="Dennis, Louise
and Fisher, Michael",
editor="Cavalcanti, Ana
and Dongol, Brijesh
and Hierons, Rob
and Timmis, Jon
and Woodcock, Jim",
title="Verifiable Autonomy and Responsible Robotics",
bookTitle="Software Engineering for Robotics",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="189--217",
abstract="The move towards greater autonomy presents challenges for software engineering. As we may be delegating greater responsibility to software systems and as these autonomous systems can make their own decisions and take their own actions, a step change in the way the systems are developed and verified is needed. This step involves moving from just considering what the system does, but also why it chooses to do it (since decision-making may be delegated). In this chapter, we provide an overview of our programme of work in this area: utilising hybrid agent architectures, exposing and verifying the reasons for decisions, and applying this to assessing a range of properties of autonomous systems.",
isbn="978-3-030-66494-7",
doi="10.1007/978-3-030-66494-7_7",
url="https://doi.org/10.1007/978-3-030-66494-7_7"
}
@ARTICLE{10.3389/frobt.2021.665729,
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 proposed standard on transparency of autonomous systems1. 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.}
}
@misc{luckcuck_matt_2021_5012322,
author = {Luckcuck, Matt and
Fisher, Michael and
Dennis, Louise and
Frost, Steve and
White, Andy and
Styles, Doug},
title = {{Principles for the Development and Assurance of
Autonomous Systems for Safe Use in Hazardous
Environments}},
month = jun,
year = 2021,
note = {{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/}},
publisher = {Zenodo},
doi = {10.5281/zenodo.5012322},
url = {https://doi.org/10.5281/zenodo.5012322}
}
@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}
}
@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
}
@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},
ARTICLE-NUMBER = {67},
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}
}
@inproceedings{StringerEMAS21,
author="Stringer, Peter
and Cardoso, Rafael C.
and Dixon, Clare
and Dennis, Louise A.",
editor="Alechina, Natasha
and Baldoni, Matteo
and Logan, Brian",
title="Implementing Durative Actions with Failure Detection in Gwendolen",
booktitle="Engineering Multi-Agent Systems",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="332--351",
abstract="We present an extension of the semantics for action execution in the Gwendolen BDI programming language. This extension firstly explicitly assumes that actions have durations and, moreover, that the reasoning cycle of the agent can not be stopped while such an action is executing but needs to continue in order to monitor for important external events. Secondly, the extension assumes that actions may often fail and this needs to be detected. This forms part of a larger project to develop a framework plan/action adaptation within BDI agents in order to enable long-term autonomy. We have implemented the extension and demonstrate its operation in a simple case study.",
isbn="978-3-030-97457-2"
}
@inproceedings{CardosoEMAS21,
author="Cardoso, Rafael C.
and Ferrando, Angelo
and Dennis, Louise A.
and Fisher, Michael",
editor="Alechina, Natasha
and Baldoni, Matteo
and Logan, Brian",
title="Implementing Ethical Governors in BDI",
booktitle="Engineering Multi-Agent Systems",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="22--41",
abstract="Increasingly, BDI agents are being used not just for basic decision-making, but for more abstract ethical decisions. Several authors have built ad-hoc extensions of BDI systems that provide varying levels of sophistication. In this paper, we introduce a general-purpose approach for implementing ethical governors in BDI systems. With this we aim to provide a broad, flexible and consistent framework for implementing increasingly complex ethical reasoning. Our approach is based on a set of domain-independent abstract agents (evidential reasoner, arbiter and execution agent) that together represent an ethical governor. We discuss the implementation of these abstract agents in the Jason agent programming language and demonstrate how they can be used in practice by instantiating agents in two different case studies, one using utilitarianism and the other deontic logic for reasoning about ethical decisions.",
isbn="978-3-030-97457-2"
}
@article{CardosoCROB21,
author={Rafael C. Cardoso and Georgios Kourtis and Louise A. Dennis and Clare Dixon and Marie Farrell and Michael Fisher and Matt Webster},
title={A Review of Verification and Validation for Space Autonomous Systems},
journal={Journal of Current Robotics Reports},
DOI = {10.1007/s43154-021-00058-1},
year=2021}
@article{Cardoso_Michaloski_Schlenoff_Ferrando_Dennis_Fisher_2021, title={Agile Tasking of Robotic Systems with Explicit Autonomy}, volume={34}, url={https://journals.flvc.org/FLAIRS/article/view/128481}, DOI={10.32473/flairs.v34i1.128481}, abstractNote={<p>Task agility is an increasingly desirable feature for robots in application domains such as manufacturing. The Canonical Robot Command Language (CRCL) is a lightweight information model built for agile tasking of robotic systems. CRCL replaces the underlying complex proprietary robot programming interface with a standard interface. In this paper, we exchange the automated planning component that CRCL used in the past for a rational agent in the Gwendolen agent programming language, thus providing greater possibilities for formal verification and explicit autonomy. We evaluate our approach by performing agile tasking in a kitting case study.</p>}, journal={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}, month={Apr.} }
@InProceedings{10.1007/978-3-030-76384-8_4,
author="Bourbouh, Hamza
and Farrell, Marie
and Mavridou, Anastasia
and Sljivo, Irfan
and Brat, Guillaume
and Dennis, Louise A.
and Fisher, Michael",
editor="Dutle, Aaron
and Moscato, Mariano M.
and Titolo, Laura
and Mu{\~{n}}oz, C{\'e}sar A.
and Perez, Ivan",
title="Integrating Formal Verification and Assurance: An Inspection Rover Case Study",
booktitle="NASA Formal Methods",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="53--71",
abstract="The complexity and flexibility of autonomous robotic systems necessitates a range of distinct verification tools. This presents new challenges not only for design verification but also for assurance approaches. Combining the distinct formal verification tools, while maintaining sufficient formal coherence to provide compelling assurance evidence is difficult, often being abandoned for less formal approaches. In this paper we demonstrate, through a case study, how a variety of distinct formal techniques can be brought together in order to develop a justifiable assurance case. We use the AdvoCATE assurance case tool to guide our analyses and to integrate the artifacts from the formal methods that we use, namely: fret, cocosim and Event-B. While we present our methodology as applied to a specific Inspection Rover case study, we believe that this combination provides benefits in maintaining coherent formal links across development and assurance processes for a wide range of autonomous robotic systems.",
isbn="978-3-030-76384-8"
}
@article{10.1145/3447246, 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 = {MCAPL, trace expressions, autonomous systems, model checking, Runtime verification} }
@inbook{10.5555/3463952.3464007, author = {Dennis, Louise A. and Oren, Nir}, title = {Explaining BDI Agent Behaviour through Dialogue}, year = {2021}, isbn = {9781450383073}, publisher = {International Foundation for Autonomous Agents and Multiagent Systems}, address = {Richland, SC}, abstract = {BDI agents act in response to external inputs and their internal plan library. Understanding the root cause of BDI agent action is often difficult, and in this paper we present a dialogue based approach for explaining the behaviour of a BDI agent. We consider two dialogue participants who may have different views regarding the beliefs, plans and external events which drove agent action (encoded via traces). These participants make utterances which incrementally reveal their traces to each other, allowing them to identify divergences in the traces, or to conclude that their traces agree. In practice, we envision a human taking on the role of a dialogue participant, with the BDI agent itself acting as the other participant. The dialogue then facilitates explanation, understanding and debugging of BDI agent behaviour. After presenting our formalism and its properties, we describe our implementation of the system and provide an example of its use in a simple scenario.}, booktitle = {Proceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems}, pages = {429–437}, numpages = {9} }
@article{Dennis_Bentzen_Lindner_Fisher_2021, title={Verifiable Machine Ethics in Changing Contexts}, volume={35}, url={https://ojs.aaai.org/index.php/AAAI/article/view/17366}, abstractNote={Many systems proposed for the implementation of ethical reasoning involve an encoding of user values as a set of rules or a model. We consider the question of how changes of context affect these encodings.
We propose the use of a reasoning cycle, in which information about the ethical reasoner’s context is imported in a logical form, and we propose that context-specific aspects of an ethical encoding be prefaced by a guard formula. This guard formula should evaluate to true when the reasoner is in the appropriate context and the relevant parts of the reasoner’s rule set or model should be updated accordingly. This architecture allows techniques for the model-checking of agent-based autonomous systems to be used to verify that all contexts respect key stakeholder values. We implement this framework using the hybrid ethical reasoning agents system (HERA) and the model-checking agent programming languages (MCAPL) framework.}, number={13}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Dennis, Louise A. and Bentzen, Martin Mose and Lindner, Felix and Fisher, Michael}, year={2021}, month={May}, pages={11470-11478} }
@Inproceedings{EPTCS329.2,
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},
editor = {Luckcuck, Matt and Farrell, Marie},
booktitle = {{\rm Proceedings Second Workshop on}
Formal Methods for Autonomous Systems,
{\rm 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},
}
@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}}
@misc{cardoso_ime,
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}
}
@misc{alves_ime,
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{EPTCS319.9,
author = {Stringer, Peter and Cardoso, Rafael C. and Huang, Xiaowei and Dennis, Louise A.},
year = {2020},
title = {Adaptable and Verifiable BDI Reasoning},
editor = {Cardoso, Rafael C. and Ferrando, Angelo and Briola, Daniela and Menghi, Claudio and Ahlbrecht, Tobias},
booktitle = {{\rm Proceedings of the First Workshop on}
Agents and Robots for reliable Engineered Autonomy,
{\rm 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}
}
@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},
doi="10.1109/JPROC.2020.2991262",
pages={1--16},
year=2020}
}@InProceedings{10.1007/978-3-030-66412-1_13,
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"
}
@InProceedings{10.1007/978-3-030-66412-1_30,
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{Webster20,
author="Matt Webster and Louise A. Dennis and Clare Dixon and Michael Fisher and Richard Stocker and Maarten Sierhuis.",
title="Formal Verification of Astronaut-Rover Teams for Planetary Surface Operations.",
booktitle="IEEE Aerospace Conference (AeroConf) 2020.",
year=2020
}
@Inbook{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"
}
@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"
}
@misc{farrell2019modular,
title={Modular Verification of Autonomous Space Robotics},
author={Marie Farrell and Rafael C. Cardoso and Louise A. Dennis and Clare Dixon and Michael Fisher and Georgios Kourtis and Alexei Lisitsa and Matt Luckcuck and Matt Webster},
year={2019},
eprint={1908.10738},
archivePrefix={arXiv},
primaryClass={cs.SE}
}
@InProceedings{10.1007/978-3-030-30446-1_25,
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"
}
@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}
}
@InProceedings{koeman_emas19,
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"
}
@InProceedings{cardoso_emas19,
author = {Rafael C. Cardoso and Louise A. Dennis and Michael Fisher},
title = {Plan Library Reconfigurability in BDI Agents},
booktitle = {Proceedings of the 7th International Workshop in Engineering Multi-Agent Systems},
year = 2019,
address = {Montreal, Canada},
url={http://cgi.csc.liv.ac.uk/~lad/emas2019/accepted/EMAS2019_paper_24.pdf}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"
}
@article{bremner19,
author={Paul Bremner and Louise A. Dennis and Michael Fisher and Alan F. Winfield},
title ={On Proactive, Transparent and Verifiable Ethical Reasoning for Robots},
journal={Proceedings of the IEEE special issue on Machine Ethics: The Design and Governance of Ethical AI and Autonomous Systems},
volume=107,
issue=3,
pages={541--561},
year=2019}
@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}
@TechReport{dennis18rais,
author = {Louise A. Dennis},
title = {Reconfigurable Autonomy: Architecture and Configuration Language},
institution = {University of Liverpool, Department of Computer Science},
year = 2018,
number = {ULCS-18-002}
}
@InProceedings{10.1007/978-3-030-03769-7_15,
author="Ferrando, Angelo
and Dennis, Louise A.
and Ancona, Davide
and Fisher, Michael
and Mascardi, Viviana",
editor="Colombo, Christian
and Leucker, Martin",
title="Verifying and Validating Autonomous Systems: Towards an Integrated Approach",
booktitle="Runtime Verification",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="263--281",
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, but 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 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 paper discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. Trace expressions are used to model the environment for both static formal verification and runtime verification.",
isbn="978-3-030-03769-7"
}
@InProceedings{fisher_wosocer18,
author = {Michael Fisher and Emily C. Collins and Louise A. Dennis and Matthew Luckcuck and Matthew P. Webster and Mike Jump and Vincent Page and Charles Patchet and Fateme Dinmohammadi and David Flynn and Valentin Robu and Xingu Zhao},
title = {Verifiable Self-Certifying Autonomous Systems},
booktitle = {8th IEEE International Workshop on Software Certification (WoSoCer)},
year = 2018
}
@InProceedings{bentzen_vavas18,
author = {Martin Mose Bentzen and Felix Lindner and Louise Dennis and Michael Fisher},
title = {Moral Permissability of Actions in Smart Home Systems},
booktitle = {Workshop on Robots, Morality, and Trust through the Verification Lens},
year = 2018
}
@InProceedings{alves_vavas18,
author = {Gleifer Alves and Louise Dennis and Michael Fisher},
title = "{Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent}",
booktitle = {Workshop on Verification and Validation of Autonomous Systems},
year = 2018
}
@InProceedings{10.1007/978-3-030-25693-7_8,
author="Winikoff, Michael
and Dennis, Louise
and Fisher, Michael",
editor="Weyns, Danny
and Mascardi, Viviana
and Ricci, Alessandro",
title="Slicing Agent Programs for More Efficient Verification",
booktitle="Engineering Multi-Agent Systems",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="139--157",
abstract="Agent programs are increasingly used as the core high-level decision-making components within a range of autonomous systems and, as the deployment of such systems in safety-critical scenarios develops, the need for strong and trustworthy verification becomes acute. Formal verification techniques such as model-checking provide this high level of assurance yet they are typically both complex and slow to deploy. In this chapter we introduce, develop and evaluate a program slicing technique that significantly improves the efficiency of such verification, hence providing more effective routes to the assurance of safety, reliability, and ethics in autonomous systems.",
isbn="978-3-030-25693-7"
}
@InProceedings{ferrando_aamas18,
author = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi}.
title = "{Recognising Assumption Violations in Autonomous Systems Verificaion}",
booktitle = {Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems},
year = 2018,
address = {Stockholm, Sweden},
pages={1933-1936}
}
@Article{dennis18:mcapl,
author="Louise A Dennis",
title="The MCAPL Framework including the Agent Infrastructure Layer and Agent Java Pathfinder",
journal = "The Journal of Open Source Software",
year = 2018,
volume=3,
number=24}
@InProceedings{dennis_isaim18,
author = {Louise A. Dennis and Michael Fisher},
title = "{Practical Challenges in Explicit Ethical Machine Reasoning}",
booktitle = {International Symposium on Artificial Intelligence and Mathematics},
year = 2018,
address = {Fort Lauderdale, USA},
url={http://isaim2018.cs.virginia.edu/papers/ISAIM2018_Ethics_Dennis_Fischer.pdf},
note={Also available as ArXiv pre-print 1801.01422}
}
@InProceedings{dignum18,
author = {Virginia Dignum and Matteo Baldoni and Cristina Baroglio and Maurizio Caon and Raja Chatila and Louise Dennis and Gonzalo G\'{e}nova and Malte Klie{\ss} and Maite Lopez-Sanchez and Roberto Micalizio and Juan Pav\'{o}n and Marija Slavkovik and Matthijs Smakman and Marlies van Steenbergen and Stefano Tedeschi and Leon van der Torre and Serena Villata and Tristan de Wildt and Galit Haim},
title = {Ethics by Design: necessity or curse?},
booktitle = {AAAI/ACM Conference on Artificial Intelligence, Ethics and Society},
year = 2018,
address = {New Orleans, USA}}
@InProceedings{bjorgen18,
author = {Edvard P. Bj{\o}rgen and Simen Madsen and Therese S. Bj{\o}rknes and Fredrik V. Heims{\ae}ter and Robin H{\aa}vik and Morten Linderud and Per-Niklas Longberg and Louise A. Dennis and Marija Slavkovik},
title = {Cake, death, and trolleys: dilemmas as benchmarks of ethical decision-making},
booktitle = {AAAI/ACM Conference on Artificial Intelligence, Ethics and Society},
year = 2018,
address = {New Orleans, USA}}
@Article{aitken17:_auton_nuclear_waste_manag,
author = {Jonathan M. Aitken and Affan Shaukat and Elisa Cucco and Louise A. Dennis and Sandor M. Veres and Yang Gao and Michael Fisher and Jeffrey A. Kuo and Thomas Robinson and Paul E. Mort},
title = {Autonomous Nuclear Waste Management},
journal = {IEEE Intelligent Systems},
year = 2017,
note = {In Press}}
@Inbook{Dennis2017,
author="Dennis, Louise A.
and Slavkovik, Marija
and Fisher, Michael",
editor="Cranefield, Stephen
and Mahmoud, Samhar
and Padget, Julian
and Rocha, Ana Paula",
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",
year="2017",
publisher="Springer International Publishing",
address="Cham",
pages="42--59",
abstract="We examine the use of model-checking in the analysis of information leakage in social networks. We take previous work on the formal analysis of digital crowds and show how a variation on the formalism can naturally model the interaction of people and groups of followers in intersecting social networks. We then show how probabilistic models of the forwarding and reposting behaviour of individuals can be used to analyse the risk that information will leak to unwanted parties. We illustrate our approach by analysing several simple examples.",
isbn="978-3-319-66595-5",
doi="10.1007/978-3-319-66595-5_3",
url="https://doi.org/10.1007/978-3-319-66595-5_3"
}
@InProceedings{dennis17:_gener_archit_flexib_auton_system,
author = {Louise Dennis and Elisa Cucco and Michael Fisher},
title = {A General Architecture for Flexible Autonomous Systems},
booktitle = {Workshop on Architectures for Generality and Autonomy (AGA 2017)},
year = 2017,
address = {Melbourne, Australia},
note = {Available at http://cadia.ru.is/workshops/aga2017/}}
@InProceedings{cucco17:_towar_robot_social_engag,
author = {Elisa Cucco and Michael Fisher and Louise Dennis and Clare Dixon and Matt Webster and Bastian Broecker and Richard Williams and Joe Collenette and Katie Atkinson and Karl Tuyls},
title = {Towards Robots for Social Engagement},
booktitle = {Workshop on Human-Robot Engagement in the Home, Workplace and Public Spaces (WHRE 2017)},
year = 2017,
note = {Published at http://ijcaihumanrobotengagement.webnode.com}}
@article{Kamali2017,
title = "Formal verification of autonomous vehicle platooning ",
journal = "Science of Computer Programming ",
volume = "148",
number = "",
pages = "88--106",
year = "2017",
note = "",
issn = "0167-6423",
doi = "https://doi.org/10.1016/j.scico.2017.05.006",
url = "http://www.sciencedirect.com/science/article/pii/S0167642317301168",
author = "Maryam Kamali and Louise A. Dennis and Owen McAree and Michael Fisher and Sandor M. Veres",
keywords = "Vehicle platooning",
keywords = "Agent programming",
keywords = "Model checking "
}
@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},
timestamp = {Tue, 01 Mar 2016 17:47:25 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/KamaliDMFV16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@ARTICLE{2017arXiv170304741C,
author = {{Charisi}, V. and {Dennis}, L. and {Fisher}, M. and {Lieck}, R. and
{Matthias}, A. and {Slavkovik}, M. and {Sombetzki}, J. and {Winfield}, A.~F.~T. and
{Yampolskiy}, R.},
title = "{Towards Moral Autonomous Systems}",
journal = {ArXiv e-prints},
archivePrefix = "arXiv",
eprint = {1703.04741},
primaryClass = "cs.AI",
keywords = {Computer Science - Artificial Intelligence},
year = 2017,
month = mar,
adsurl = {http://adsabs.harvard.edu/abs/2017arXiv170304741C},
adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}
@TechReport{dennis17gwen,
author = {Louise A. Dennis},
title = {Gwendolen Semantics: 2017},
institution = {University of Liverpool, Department of Computer Science},
year = 2017,
number = {ULCS-17-001}
}
@Inbook{Dennis2016,
author="Dennis, Louise A.
and Aitken, Jonathan M.
and Collenette, Joe
and Cucco, Elisa
and Kamali, Maryam
and McAree, Owen
and Shaukat, Affan
and Atkinson, Katie
and Gao, Yang
and Veres, Sandor M.
and Fisher, Michael",
editor="Alboul, Lyuba
and Damian, Dana
and Aitken, M. Jonathan",
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",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="75--86",
isbn="978-3-319-40379-3",
doi="10.1007/978-3-319-40379-3_8",
url="http://dx.doi.org/10.1007/978-3-319-40379-3_8"
}
@ARTICLE{6632950,
author={Lincoln, N.K. and Veres, S.M. and Dennis, L.A. and Fisher, M. and Lisitsa, A.},
journal={Computational Intelligence Magazine, IEEE},
title={Autonomous Asteroid Exploration by Rational Agents},
year={2013},
volume={8},
number={4},
pages={25-38},
keywords={asteroids;formal verification;natural language processing;object-oriented programming;software agents;agent reasoning;autonomous asteroid exploration;autonomous space missions;belief-desire-intention architectures;formal verifiability;natural language definitions;novel anthropomorphic agent architecture;rational agents;real-time decision-making;skill descriptions;software agent architectures;Asteroids;Computer architecture;Real-time systems;Software agents;Software architecture;Space vehicles},
doi={10.1109/MCI.2013.2279559},
ISSN={1556-603X},
month={Nov},}
@article{Dennis2015,
title = "Formal verification of ethical choices in autonomous systems ",
journal = "Robotics and Autonomous Systems ",
volume = "",
number = "",
pages = " - ",
year = "2015",
note = "",
issn = "0921-8890",
doi = "http://dx.doi.org/10.1016/j.robot.2015.11.012",
url = "http://www.sciencedirect.com/science/article/pii/S0921889015003000",
author = "Louise Dennis and Michael Fisher and Marija Slavkovik and Matt Webster",
keywords = "Autonomous systems",
keywords = "Ethics",
keywords = "BDI programs",
keywords = "Formal verification "
}
@inproceedings{vanRiemsdijk:2015:SFS:2772879.2772935,
author = {van Riemsdijk, M. Birna and Dennis, Louise and Fisher, Michael and Hindriks, Koen V.},
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},
series = {AAMAS '15},
year = {2015},
isbn = {978-1-4503-3413-6},
location = {Istanbul, Turkey},
pages = {423--432},
numpages = {10},
url = {http://dl.acm.org/citation.cfm?id=2772879.2772935},
acmid = {2772935},
publisher = {International Foundation for Autonomous Agents and Multiagent Systems},
address = {Richland, SC},
keywords = {agent programming languages, executable temporal logic, formal semantics, norm compliance, norm-aware agents},
}
@InProceedings{dennis15:_towar_verif_ethic_robot_behav,
author = {Louise A. Dennis and Michael Fisher and Alan F. T. Winfield},
title = {Towards Verifiably Ethical Robot Behaviour},
booktitle = {AAAI Workshop on AI and Ethics (1st International Conference on AI and Ethics)},
year = 2015,
month = {January},
address = {Austin, TX}}
@article{slavkovik15,
year=2015,
issn={0926-8782},
journal={Distributed and Parallel Databases},
volume=33,
number=1,
doi={10.1007/s10619-014-7161-y},
title={An abstract formal basis for digital crowds},
url={http://dx.doi.org/10.1007/s10619-014-7161-y},
publisher={Springer US},
keywords={Logical foundations; Crowd specification; Formal verification; Predictability},
author={Slavkovik, Marija and Dennis, LouiseA. and Fisher, Michael},
pages={3-31},
language={English}
}
@article{Dennis16022015,
author = {Dennis, Louise A. and Fisher, Michael and Webster, Matt},
title = {Two-stage agent program verification},
year = {2018},
doi = {10.1093/logcom/exv002},
volume=28,
issue=3,
pages={499-523},
abstract ={We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it potentially improves the efficiency of the model-checking process and provides access to richer property specification languages. We illustrate the approach by describing the export of AJPF program models to both the SPIN and Prism model-checkers. We also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.},
URL = {http://logcom.oxfordjournals.org/content/early/2015/02/16/logcom.exv002.abstract},
eprint = {http://logcom.oxfordjournals.org/content/early/2015/02/16/logcom.exv002.full.pdf+html},
journal = {Journal of Logic and Computation}
}
@TechReport{dennis14ros,
author = {Louise A. Dennis},
title = {{ROS}-{AIL} Integration},
institution = {University of Liverpool, Department of Computer Science},
year = 2014,
number = {ULCS-14-004}
}
@article{dennis_ase14,
year={2016},
issn={0928-8910},
journal={Automated Software Engineering},
doi={10.1007/s10515-014-0168-9},
title={Practical verification of decision-making in agent-based autonomous systems},
url={http://dx.doi.org/10.1007/s10515-014-0168-9},
publisher={Springer US},
keywords={Hybrid systems; Model checking; Agent architectures},
author={Dennis, Louise A. and Fisher, Michael and Lincoln, Nicholas K. and Lisitsa, Alexei and Veres, Sandor M.},
volume=23,
number=3,
pages={305-359},
language={English}
}
@incollection{
year={2014},
isbn={978-3-662-43644-8},
booktitle={Towards Autonomous Robotic Systems},
series={Lecture Notes in Computer Science},
editor={Natraj, Ashutosh and Cameron, Stephen and Melhuish, Chris and Witkowski, Mark},
doi={10.1007/978-3-662-43645-5_45},
title={Ethical Choice in Unforeseen Circumstances},
url={http://dx.doi.org/10.1007/978-3-662-43645-5_45},
publisher={Springer Berlin Heidelberg},
author={Dennis, Louise and Fisher, Michael and Slavkovik, Marija and Webster, Matt},
pages={433-445},
language={English}
}
@InProceedings{dennis14:_action_durat_failur_bdi_languag,
author = {Louise A. Dennis and Michael Fisher},
title = {Actions with Durations and Failures in BDI Languages},
booktitle = {21st European Conference on Artificial Intelligence (ECAI 2014)},
year = 2014,
editor = {Torsten Schaub},
series = {Frontiers in Artificial Intelligence and Applications},
volume = 263,
pages = {995--996},
publisher = {IOS Press}}
@TechReport{dennis14,
author = {Louise A. Dennis and Michael Fisher},
title = {Actions with Durations and Failures in BDI Languages},
institution = {University of Liverpool, Department of Computer Science},
year = 2014,
number = {ULCS-14-003}
}
@article{
year={2014},
issn={0933-1875},
journal={KI - Künstliche Intelligenz},
volume={28},
number={3},
doi={10.1007/s13218-014-0308-1},
title={Reconfigurable Autonomy},
url={http://dx.doi.org/10.1007/s13218-014-0308-1},
publisher={Springer Berlin Heidelberg},
keywords={Hybrid systems; Autonomous vehicles; Intelligent agents; Robotics},
author={Dennis, Louise A. and Fisher, Michael and Aitken, Jonathan M. and Veres, Sandor M. and Gao, Yang and Shaukat, Affan and Burroughes, Guy},
pages={199-207},
language={English}
}
@inproceedings{DBLP:conf/clima/DennisFW13,
author = {Louise A. Dennis and
Michael Fisher and
Matthew P. Webster},
title = {Using Agent JPF to Build Models for Other Model Checkers},
editor = {Jo{\~a}o Leite and
Tran Cao Son and
Paolo Torroni and
Leon van der Torre and
Stefan Woltran},
booktitle = {Computational Logic in Multi-Agent Systems - 14th International
Workshop, CLIMA XIV, Corunna, Spain, September 16-18, 2013.
Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8143},
year = {2013},
pages = {273-289},
ee = {http://dx.doi.org/10.1007/978-3-642-40624-9_17},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/atal/RiemsdijkDFH13,
author = {M. Birna van Riemsdijk and
Louise A. Dennis and
Michael Fisher and
Koen V. Hindriks},
title = {Agent reasoning for norm compliance: a semantic approach},
editor = {Maria L. Gini and
Onn Shehory and
Takayuki Ito and
Catholijn M. Jonker},
booktitle = {International conference on Autonomous Agents and Multi-Agent
Systems, AAMAS '13, Saint Paul, MN, USA, May 6-10, 2013},
year = {2013},
pages = {499-506},
ee = {http://dl.acm.org/citation.cfm?id=2485000},
isbn = {978-1-4503-1993-5},
publisher = {IFAAMAS},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/cacm/FisherDW13,
author = {Michael Fisher and
Louise A. Dennis and
Matthew P. Webster},
title = {Verifying autonomous systems},
journal = {Commun. ACM},
volume = {56},
number = {9},
year = {2013},
pages = {84-93},
ee = {http://doi.acm.org/10.1145/2494558},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/eceasst/ArapinisCDFGKMRRSUY09,
author = {Myrto Arapinis and
Muffy Calder and
Louise A. Dennis and
Michael Fisher and
Philip D. Gray and
Savas Konur and
Alice Miller and
Eike Ritter and
Mark Ryan and
Sven Schewe and
Chris Unsworth and
Rehana Yasmin},
title = {Towards the Verification of Pervasive Systems},
journal = {ECEASST},
volume = {22},
year = {2009},
ee = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/article/view/315},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/clima/StockerSDDF11,
author = {Richard Stocker and
Maarten Sierhuis and
Louise A. Dennis and
Clare Dixon and
Michael Fisher},
title = {A Formal Semantics for Brahms},
year = {2011},
pages = {259-274},
ee = {http://dx.doi.org/10.1007/978-3-642-22359-4_18},
editor = {Jo{\~a}o Leite and
Paolo Torroni and
Thomas {\AA}gotnes and
Guido Boella and
Leon van der Torre},
booktitle = {Computational Logic in Multi-Agent Systems - 12th International
Workshop, CLIMA XII, Barcelona, Spain, July 17-18, 2011.
Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6814},
year = {2011},
isbn = {978-3-642-22358-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/jelia/StockerDDF12,
author = {Richard Stocker and
Louise A. Dennis and
Clare Dixon and
Michael Fisher},
title = {Verifying Brahms Human-Robot Teamwork Models},
year = {2012},
pages = {385-397},
ee = {http://dx.doi.org/10.1007/978-3-642-33353-8_30},
editor = {Luis Fari{\~n}as del Cerro and
Andreas Herzig and
J{\'e}r{\^o}me Mengin},
booktitle = {Logics in Artificial Intelligence - 13th European Conference,
JELIA 2012, Toulouse, France, September 26-28, 2012. Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7519},
year = {2012},
isbn = {978-3-642-33352-1},
ee = {http://dx.doi.org/10.1007/978-3-642-33353-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@incollection{
year={2012},
isbn={978-3-642-29112-8},
booktitle={Declarative Agent Languages and Technologies IX},
volume={7169},
series={Lecture Notes in Computer Science},
editor={Sakama, Chiaki and Sardina, Sebastian and Vasconcelos, Wamberto and Winikoff, Michael},
doi={10.1007/978-3-642-29113-5_2},
Title={Plan Indexing for State-Based Plans},
url={http://dx.doi.org/10.1007/978-3-642-29113-5_2},
publisher={Springer Berlin Heidelberg},
author={Dennis, Louise A.},
pages={3-15}
}
@inproceedings{LVDFL10:ALCOSP,
author=" Lincoln, N. and Veres, S. M. and Dennis, L. A. and Fisher, M. and
and Lisitsa, A.",
title="{An Agent Based Framework for
Adaptive Control and Decision Making of Autonomous Vehicles}",
booktitle="Proc. IFAC Workshop on Adaptation and Learning in Control
and Signal Processing (ALCOSP)",
year=2010
}
@inproceedings{DALT10:abstraction,
author="Dennis, L. A. and Fisher, M. and
Lincoln, N. and Lisitsa, A. and Veres, S. M.",
title="{Declarative Abstractions for Agent Based Hybrid Control Systems}",
booktitle="Proc. 8th International Workshop on Declarative Agent Languages and Technologies (DALT)",
series="{LNCS}",
publisher="Springer",
volume=6619,
pages="96--111",
year=2010
}
@article{springerlink:10.1007/s10515-011-0088-x,
author = {Dennis, Louise and Fisher, Michael and Webster, Matthew and Bordini, Rafael},
affiliation = {Department of Computer Science, University of Liverpool, Liverpool, L69 3BX UK},
title = {Model checking agent programming languages},
journal = {Automated Software Engineering},
publisher = {Springer Netherlands},
issn = {0928-8910},
keyword = {Computer Science},
pages = {1-59},
url = {http://dx.doi.org/10.1007/s10515-011-0088-x},
note = {10.1007/s10515-011-0088-x},
year = {2011}
}
@InCollection{r.10:_direc_agent_model_check,
author = {R. H. Bordini, L. A. Dennis, B. Farwer and M. Fisher},
title = {Directions for Agent Model Checking},
booktitle = {Specification and Verification of Multi-agent Systems},
pages = {103--123},
publisher = {Springer US},
year = 2010,
editor = {M. Dastani, K. V. Hindriks, J.-J. C. Meyer},
chapter = 4,
url= {http://dx.doi.org/10.1007/978-1-4419-6984-2}
}
@article {springerlink:10.1007/s10817-010-9177-y,
author = {Dennis, Louise and Green, Ian and Smaill, Alan},
affiliation = {University of Liverpool School of Computer Science Liverpool L69 3BX UK},
title = {The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling},
journal = {Journal of Automated Reasoning},
volume = {47},
issue = {1},
publisher = {Springer Netherlands},
issn = {0168-7433},
keyword = {Computer Science},
pages = {57-105},
url = {http://dx.doi.org/10.1007/s10817-010-9177-y},
note = {10.1007/s10817-010-9177-y},
year = {2011}
}
@InProceedings{louise10:_reduc_code_compl_hybrid_auton_contr_system,
author = {Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa, and Sandor M. Veres},
title = {Reducing Code Complexity in Hybrid Autonomous Control Systems},
booktitle = {The 10th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS 2010)},
year = 2010,
editor = {Takashi Kubota}
}
@article{DBLP:journals/expert/DennisFLLV10,
author = {Louise A. Dennis and
Michael Fisher and
Alexei Lisitsa and
Nicholas Lincoln and
Sandor M. Veres},
title = {Satellite Control Using Rational Agent Programming},
journal = {IEEE Intelligent Systems},
volume = {25},
number = {3},
year = {2010},
pages = {92-97},
ee = {http://dx.doi.org/10.1109/MIS.2010.88},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/clima/DennisTM09,
author = {Louise A. Dennis and
Nick A. M. Tinnemeier and
John-Jules Ch. Meyer},
title = {Model Checking Normative Agent Organisations},
editor = {J{\"u}rgen Dix and
Michael Fisher and
Peter Nov{\'a}k},
booktitle = {Computational Logic in Multi-Agent Systems - 10th International
Workshop, CLIMA X, Hamburg, Germany, September 9-10, 2009,
Revised Selected and Invited Papers},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 6214,
isbn = {978-3-642-16866-6},
year = 2009,
pages = {64-82},
ee = {http://dx.doi.org/10.1007/978-3-642-16867-3_4},
crossref = {DBLP:conf/clima/2009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:journals/corr/abs-1003-0617,
author = {Louise A. Dennis and
Michael Fisher and
Nicholas Lincoln and
Alexei Lisitsa and
Sandor M. Veres},
title = {Agent Based Approaches to Engineering Autonomous Space Software},
editor = {Manuela L. Bujorianu and
Michael Fisher},
booktitle = {Proceedings FM-09 Workshop on Formal Methods for Aerospace},
series = {EPTCS},
volume = 20,
year = 2009,
pages = {63-67},
ee = {http://dx.doi.org/10.4204/EPTCS.20.6},
}
@INPROCEEDINGS{BDFF08:ASE,
author = {R. H. Bordini and L. A. Dennis and B. Farwer and M. Fisher},
title = {{Automated Verification of Multi-Agent Programs}},
booktitle = {Proc. 23rd IEEE/ACM International Conference on Automated Software
Engineering (ASE)},
year = {2008},
publisher=2008,
pages = {69--78}
}
@TechReport{fisher09,
author = {Michael Fisher and Louise Dennis and Anthony Hepple},
title = {Modular Multi-Agent Design},
institution = {University of Liverpool, Department of Computer Science},
year = 2009,
number = {ULCS-09-002}
}
@TechReport{webster09,
author = {Matt Webster and Louise Dennis and Michael Fisher},
title = {Model Checking Auctions, Coalitions and Trust},
institution = {University of Liverpool, Department of Computer Science},
year = 2009,
number = {ULCS-09-004}
}
@InProceedings{dennis08:_gwend,
author = {Louise A. Dennis and Berndt Farwer},
title = {Gwendolen: A BDI Language for Verifiable Agents},
booktitle = {Logic and the Simulation of Interaction and Reasoning},
year = 2008,
editor = {Benedikt L{\"o}we},
address = {Aberdeen},
publisher = {AISB},
note = {AISB'08 Workshop}
}
@InProceedings{dennis08:_progr_verif_heter_agent_system,
author = {Louise A. Dennis and Michael Fisher},
title = {Programming Verifiable Heterogeneous Agent Systems},
booktitle = {Sixth International Workshop on Programming in Multi-Agent Systems (ProMAS'08)},
year = 2008,
address = {Estoril, Portugal},
pages = {27-42},
editor = {Koen Hindriks and Alexander Pokahr and Sebastian Sardina},
month = {May},
}
@InProceedings{dennis08:_progr_verif_heter_agent_system,
author = {Louise A. Dennis and Michael Fisher},
title = {Programming Verifiable Heterogeneous Agent Systems},
editor = {Koen Hindriks and Alexander Pokahr and Sebastian Sardina},
booktitle = {Sixth International Workshop on Programming in Multi-Agent Systems (ProMAS'08)},
year = 2008,
pages = {27-42},
address = {Estoril, Portugal},
month = {May},
}
@InProceedings{farwer07:_trans,
author = {B. Farwer and L. Dennis},
title = {Translating into an intermediate agent layer: A prototype in Maude},
booktitle = {Proceedings of Concurrency, Specification and Programming (CS\&P 2007)},
year = 2007,
address = {Lagow, Poland}
}
@InProceedings{hepple07:_common_basis_agent_organ_bdi_languag,
author = {Anthony Hepple and Louise A. Dennis and Michael Fisher},
title = {A Common Basis for Agent Organisation in BDI Languages},
booktitle = {Languages, Methodologies and Development Tools for Multi-Agent Systems (LADS'07)},
year = 2007,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
}
@InProceedings{dennis07:_found_flexib_multi_agent_progr,
author = {Louise A. Dennis and Michael Fisher and Antony Hepple},
title = {Foundations of Flexible Multi-Agent Programming},
booktitle = {Eighth Workshop on Computational Logic in
Multi-Agent Systems (CLIMA-VIII)},
year = 2007
}
@InProceedings{dennis07:_common_seman_basis_bdi_languag,
author = {Louise A. Dennis and Rafael H. Bordini and Berndt
Farwer and Michael Fisher and Michael Wooldridge},
M3 = {10.1007/978-3-540-79043-3{\_}8},
Pages = {124--139},
Title = {A Common Semantic Basis for BDI Languages},
Url = {http://dx.doi.org/10.1007/978-3-540-79043-3_8},
Year = {2008},
Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-79043-3_8}
booktitle = {Fifth International Workshop on Programming in Multi-Agent Systems (ProMAS'07)},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
volume = {4908}
}
@TechReport{dennis07:_chall_probl_induc_theor_prover,
author = {Louise A. Dennis and Jeremy Gow and Carsten Sch{\"u}rmann},
title = {Challenge Problems for Inductive Theorem Provers v1.0},
institution = {University of Liverpool, Department of Computer Science},
year = 2007,
number = {ULCS-07-004}
}
@InCollection{attfield06,
author = {Thomas D. Attfield and Monica C. Duarte and Lin Li and Ho-Ying Mak and Adam M. Neal and Lewis M. Toft and Zixuan Wang and Louise A. Dennis},
title = {26.11 Induction Challenge OMDoc Manager (ICOM)},
booktitle = {{OMD}oc --
An Open Markup Format for Mathematical Documents [version 1.2]},
pages = {278--280},
publisher = {Springer},
year = 2006,
editor = {Michael Kohlhase},
volume = 4180,
series = {Lecture Notes in Artificial Intelligence},
chapter = {26 Applications and Project},
note = {AI Systems Subseries}
}
@InProceedings{dennis06:_progr_slicin_middl_out_reason,
author = {Louise A. Dennis},
title = {Program Slicing and Middle-Out Reasoning for Error
Location and Repair},
booktitle = {Disproving: Non-Theorems, Non-Validity and Non-Provability},
year = 2006
}
@Article{dennis07:_enhan_theor_prover_inter_progr_slice_infor,
author = {Louise A. Dennis},
title = {Enhancing Theorem Prover Interfaces with Program Slice Information},
journal = {Electronic Notes in Theoretical Computer Science (ENTCS)},
year = 2007,
volume = 174,
number = 2,
pages = {19--33},
month = {May},
note = {Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)}
}
@InProceedings{dennis05:_compar_proof_plann_system,
author = {L. A. Dennis and M. Jamnik and M. Pollet},
title = {On the Comparison of Proof Planning Systems: {L}ambda{C}lam, {O}meg
a and {I}sa{P}lanner},
booktitle = {12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2005},
year = 2006,
series = {ENTCS},
volume = 151,
issue = 1,
papges = {93--110}
}
@InProceedings{dennis06:_proof_debug_repair,
author = {L. A. Dennis and R. Monroy and P. Nogueira},
title = {Proof-directed Debugging and Repair},
booktitle = {Seventh Symposium on Trends in Functional Programming 2006},
pages = {131--140},
year = 2006,
editor = {H. Nilsson and M. van Eekelen}
}
@inproceedings{Dennis:plagiarism04,
author="L. A. Dennis",
editor="A. P. Smith and F. Duggan",
pages="57--64",
title="Student Attitudes to Plagiarism and Collusion within Computer
Science",
booktitle="Plagiarism: Prevention, Practice and Policy Conference
28--30 June 2004",
publisher="Northumbria University Press",
year=2005}
@inproceedings{Dennis:tphols05,
author="L. A. Dennis and P. Nogueira",
editor="J. Hurd and E. Smith and A. Darbari",
pages="45--58",
title="What can be Learned from Failed Proofs of Non-Theorems?",
booktitle="Theorem Proving in Higher Order Logics (TPHOLs 2005):
Emerging Trends Proceedings",
note="Technical Report PRG-RP-05-2, Oxford University Computer Laboratory",
year=2005}
@inproceedings{Dennis:ijcai05,
author="L. A. Dennis",
editor="L. P. Kaelbling and A. Saffiotti",
pages="1558--1559",
title="An Architecture for Proof Planning Systems",
booktitle="Nineteenth International Joint Conference on Artificial
Intelligence, IJCAI-05",
publisher="IJCAI Inc.",
year=2005}
@technicalreport{Dennisetal05,
author="L. A. Dennis and I. Green and A. Smaill",
title="Embeddings as a Higher-Order Representation of Annotations
for Rippling",
number="Computer Science Technical Report No. NOTTCS-WP-SUB-0503230955-5470",
institution="University of Nottingham",
year=2005,
notes="Submitted to Journal of Automated Reasoning"}
@article{Sellers:janat04,
author="W. I. Sellers and L. A. Dennis and W.-J. Wang and R. H. Crompton",
title="Evaluating alternative gait strategies using evolutionary robotics",
year="2004",
journal="Journal of Anatomy",
volume=204,
pages="343--351"}
@InProceedings{AdamsDennis:strata03,
author="A. A. Adams and L. A. Denns",
title="Rippling in PVS",
editor="M. Archer and B. Di Vito and C. Munoz",
booktitle="Proceedings of Design and Application of
Strategies/Tactics in Higher Order Logics (STRATA 2003)",
year=2003,
pages="84--91",
publisher="NASA Technical Report CP-2003-212448"}
@InProceedings{Dennis:disproving04,
author="L. A. Dennis",
title="The Use of Proof Planning Critics to Diagnose Errors in the
Base Cases of Recursive Programs",
year="2004",
editor="W. Ahrendt and P. Baumgartner and H. de Nivelle",
pages="47--58",
booktitle="IJCAR 2004 Workshop on Disproving: Non-Theorems,
Non-Validity, Non-Provability"}
@article{Dennis:sttt03,
author="L. A. Dennis and G. Collins and M. Norrish and R. J. Boulton and K. Slind and T. F. Melham",
title = "The {\sc PROSPER} toolkit",
year=2003,
journal="International Journal on Software Tools for Technology Transfer",
volume=4,
number = 2,
year = 2003,
pages="189--210"}
@article{Sellers:jeb03,
author="W. I. Sellers and L. A. Dennis and R. H. Crompton",
title = "Predicting the metabolic energy costs of bipedalism using evolutionary robotics",
year=2003,
journal="Journal of Experimental Biology",
volume=206,
pages="1127--1136"}
@InProceedings{Zimmer:calculemus02,
author="J. Zimmer and L. A. Dennis",
title="Inductive Theorem Proving and Computer Algebra in the Mathweb
Software Bus",
year="2002",
editor="J. Calmet and B. Belaid and O. Caprotti and L. Henocque
and V. Sorge (Eds.)",
pages="319--331",
series="LNAI",
booktitle="Artificial Intelligence, Automated Reasoning and Symbolic
Computation, Calculemus 2002",
number="2385",
publisher="Springer-Verlag"}
@InProceedings{Dennis:tphols02,
author="L. A. Dennis and A. Bundy",
title="A Comparison of two Proof Critics: Power vs. Robustness",
booktitle="Theorem Proving in Higher Order Logics, 15th
International Conference, TPHOLs 2002",
year="2002",
editor="V. A Carreno and C. A. Munoz and S. Tahar",
pages="182--197",
series="LNCS",
number="2410",
publisher="Springer-Verlag"}
@article{Dennis:amai00,
author = "Dennis, L. and Bundy, A. and Green, I.",
title = "Making a productive use of failure to generate
witness for coinduction from divergent proof
attempts",
journal = "Annals of Mathematics and Artificial Intelligence",
volume = 29,
pages = "99--138",
year = 2000,
note = "also paper no. RR0004 in the Informatics Report
Series"
}
@InProceedings{Colton:AIM02,
author="S. Colton and L. Dennis",
title="The NumbersWithNames Program",
booktitle="AI&M 3-2002, Seventh
International Symposium on Artificial Intelligence and Mathematics",
month="January 2-4",
year="2002",
location="Fort Lauderdale, Florida.",
notes="Available from http://rutcor.rutgers.edu/~amai/aimath02/"}
@InProceedings{Dennis:TPHOLs01,
author="L. A. Dennis and A. Smaill",
title="Ordinal Arithimetic: A Case Study for Rippling in a Higher Order Domain",
booktitle="Theorem Proving in Higher Order Logics: 14th Internional Conference, TPHOLs 2001",
pages="185--200",
series="Lecture Notes in Computer Science",
number=2152,
year=2001,
publisher="Springer-Verlag",
editor="R. J. Boulton and P. B. Jackson",
month="September",
location="Edinburgh, Scotland, UK"}
@techreport{Stevenson:TPHOLs00,
author="A. Stevenson and L. A. Dennis",
title="Integrating {SVC} and {HOL} with the {\sc Prosper} Toolkit",
booktitle="Theorem Proving in Higher Order Logics (TPHOLs2000), Supplemental Proceedings",
year=2000,
pages="199--206",
instituion="Oregon Graduate Institue",
number="CSE00-009"}
@InProceedings{Dennis:CADE97,
author = "L. A. Dennis and A. Bundy and I. Green",
title = "Using a generalisation critic to find bisimulations
for coinductive proofs",
booktitle = "Automated Deduction (CADE-14)",
pages = "276--290",
series = "Lecture Notes in Artificial Intelligence",
number = 1249,
year = 1997,
publisher = "Springer-Verlag",
editor = "W. McCune"
}
@inproceedings{Dennis:TACAS00,
author = {L. A. Dennis and G. Collins and M. Norrish and R. Boulton and K. Slind and G. Robinson and M. Gordon and T. Melham},
title = {The PROSPER Toolkit},
booktitle = {Tools and Algorithms for Constructing Systems (TACAS 2000)},
editor = {Graf, S. and Schwartbach, M.},
series = {Lecture Notes in Computer Science},
number = 1785,
year = 2000,
pages = {78--92},
publisher = {Springer-Verlag}}
@InProceedings{Collins:CADE00,
author = "G. Collins and L. A. Dennis",
title = "System Description: Embedding Verification into Microsoft Excel",
booktitle = "Automated Deduction (CADE-17)",
pages = "497--501",
series = "Lecture Notes in Artificial Intelligence",
number = 1831,
year = 2000,
publisher = "Springer-Verlag",
editor = "D. McAllester"
}
@PhDThesis(Dennis:Thesis,
author = "Dennis, L. A.",
title = "Proof Planning Coinduction",
school = "Edinburgh University",
year = 1998)
@MScThesis(Dennis:MSc,
author="L. A. Dennis",
title="An Exploration of Semantic Resolution",
year=1994,
institution="Department of Artificial Intelligence, University of Edinburgh")
Last modified: Tue Jun 7 13:21:38 BST 2011