var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https%3A%2F%2Fautonomy-and-verification-uol.github.io%2Fpubs.bib&group0=year&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Fautonomy-and-verification-uol.github.io%2Fpubs.bib&group0=year&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Fautonomy-and-verification-uol.github.io%2Fpubs.bib&group0=year&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

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

To the site owner:

\n\n

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

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

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2020\n \n \n (15)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest.\n \n \n \n\n\n \n Cardoso, R. C.; Ferrando, A.; and Papacchini, F.\n\n\n \n\n\n\n In The Multi-Agent Programming Contest 2019, pages 31–58, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{Cardoso20d,\nauthor="Cardoso, Rafael C.\nand Ferrando, Angelo\nand Papacchini, Fabio",\ntitle="LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest",\nbooktitle="The Multi-Agent Programming Contest 2019",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="31--58",\nisbn="978-3-030-59299-8",\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent.\n \n \n \n\n\n \n Alves, G. V.; Dennis, L.; and Fisher, M.\n\n\n \n\n\n\n In Sekerinski, E.; Moreira, N.; Oliveira, J. N.; Ratiu, D.; Guidotti, R.; Farrell, M.; Luckcuck, M.; Marmsoler, D.; Campos, J.; Astarte, T.; Gonnord, L.; Cerone, A.; Couto, L.; Dongol, B.; Kutrib, M.; Monteiro, P.; and Delmas, D., editor(s), Formal Methods. FM 2019 International Workshops, pages 217–232, Cham, 2020. Springer International Publishing\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{10.1007/978-3-030-54994-7_16,\nauthor="Alves, Gleifer Vaz\nand Dennis, Louise\nand Fisher, Michael",\neditor="Sekerinski, Emil\nand Moreira, Nelma\nand Oliveira, Jos{\\'e} N.\nand Ratiu, Daniel\nand Guidotti, Riccardo\nand Farrell, Marie\nand Luckcuck, Matt\nand Marmsoler, Diego\nand Campos, Jos{\\'e}\nand Astarte, Troy\nand Gonnord, Laure\nand Cerone, Antonio\nand Couto, Luis\nand Dongol, Brijesh\nand Kutrib, Martin\nand Monteiro, Pedro\nand Delmas, David",\ntitle="Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent",\nbooktitle="Formal Methods. FM 2019 International Workshops",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="217--232",\nabstract="The design of autonomous vehicles includes obstacle detection and avoidance, route planning, speed control, etc. However, there is a lack of an explicitely representation of the rules of the road on an autonomous vehicle. Additionally, it is necessary to understand the behaviour of an autonomous vehicle in order to check whether or not it works according to the rules of the road. Here, we propose an agent-based architecture to embed the rules of the road into an agent representing the behaviour of an autonomous vehicle. We use temporal logic to formally represent the rules of the road in a way it should be possible to capture when and how a given rule of the road can be applied. Our contributions include: i. suggestion of changes in the rules of the road; ii. representation of rules in a suitable way for an autonomous vehicle agent; iii. dealing with indeterminate terms in the Highway Code.",\nisbn="978-3-030-54994-7",\nnote = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Computational Goals, Values and Decision-Making.\n \n \n \n \n\n\n \n Dennis, L. A.\n\n\n \n\n\n\n Science and Engineering Ethics. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"ComputationalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{dennis_see_2020,\n\tAbstract = {Considering the popular framing of an artificial intelligence as a rational agent that always seeks to maximise its expected utility, referred to as its goal, one of the features attributed to such rational agents is that they will never select an action which will change their goal. Therefore, if such an agent is to be friendly towards humanity, one argument goes, we must understand how to specify this friendliness in terms of a utility function. Wolfhart Totschnig (Fully Autonomous AI, Science and Engineering Ethics, 2020), argues in contrast that a fully autonomous agent will have the ability to change its utility function and will do so guided by its values. This commentary examines computational accounts of goals, values and decision-making. It rejects the idea that a rational agent will never select an action that changes its goal but also argues that an artificial intelligence is unlikely to be purely rational in terms of always acting to maximise a utility function. It nevertheless also challenges the idea that an agent which does not change its goal cannot be considered fully autonomous. It does agree that values are an important component of decision-making and explores a number of reasons why.},\n\tAuthor = {Dennis, Louise A. },\n\tDa = {2020/08/04},\n\tDate-Added = {2020-08-06 13:39:55 +0100},\n\tDate-Modified = {2020-08-06 13:39:55 +0100},\n\tDoi = {10.1007/s11948-020-00244-y},\n\tId = {Dennis2020},\n\tIsbn = {1471-5546},\n\tJournal = {Science and Engineering Ethics},\n\tTitle = {Computational Goals, Values and Decision-Making},\n\tTy = {JOUR},\n\tUrl = {https://doi.org/10.1007/s11948-020-00244-y},\n\tYear = {2020},\n\tBdsk-Url-1 = {https://doi.org/10.1007/s11948-020-00244-y}}\n  \n
\n
\n\n\n
\n Considering the popular framing of an artificial intelligence as a rational agent that always seeks to maximise its expected utility, referred to as its goal, one of the features attributed to such rational agents is that they will never select an action which will change their goal. Therefore, if such an agent is to be friendly towards humanity, one argument goes, we must understand how to specify this friendliness in terms of a utility function. Wolfhart Totschnig (Fully Autonomous AI, Science and Engineering Ethics, 2020), argues in contrast that a fully autonomous agent will have the ability to change its utility function and will do so guided by its values. This commentary examines computational accounts of goals, values and decision-making. It rejects the idea that a rational agent will never select an action that changes its goal but also argues that an artificial intelligence is unlikely to be purely rational in terms of always acting to maximise a utility function. It nevertheless also challenges the idea that an agent which does not change its goal cannot be considered fully autonomous. It does agree that values are an important component of decision-making and explores a number of reasons why.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Ethical Governor Systems viewed as a Multi-Agent Problem.\n \n \n \n \n\n\n \n Cardoso, R. C.; Ene, D.; Evans, T.; and Dennis, L. A.\n\n\n \n\n\n\n In Nallur, V., editor(s), Second Workshop on Implementing Machine Ethics, June 2020. Zenodo\n [RAIN]\n\n\n\n
\n\n\n\n \n \n \"EthicalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{cardosoime,\n  author = {Rafael C. Cardoso and Daniel Ene and Tom Evans and Louise A. Dennis},\n  title = {Ethical Governor Systems viewed as a Multi-Agent Problem},\n  editor       = {Vivek Nallur},\n  booktitle        = {Second Workshop on Implementing Machine Ethics},\n  month        = jun,\n  year         = 2020,\n  publisher    = {Zenodo},\n  doi          = {10.5281/zenodo.3938851},\n  url          = {https://doi.org/10.5281/zenodo.3938851},\n  note = {[<span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n First Steps towards an Ethical Agent for checking decision and behaviour for an Autonomous Vehicle on the Rules of the Road.\n \n \n \n \n\n\n \n Alves, G. V.; Dennis, L.; and Fisher, M.\n\n\n \n\n\n\n In Nallur, V., editor(s), Second Workshop on Implementing Machine Ethics, June 2020. Zenodo\n \n\n\n\n
\n\n\n\n \n \n \"FirstPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{alvesime,\n  author = {Gleifer Vaz Alves and Louise Dennis and Michael Fisher},\n  title = {First Steps towards an Ethical Agent for checking decision and behaviour for an Autonomous Vehicle on the Rules of the Road},\n  editor       = {Vivek Nallur},\n  booktitle        = {Second Workshop on Implementing Machine Ethics},\n  month        = jun,\n  year         = 2020,\n  publisher    = {Zenodo},\n  doi          = {10.5281/zenodo.3938851},\n  url          = {https://doi.org/10.5281/zenodo.3938851}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Adaptable and Verifiable BDI Reasoning.\n \n \n \n\n\n \n Stringer, P.; Cardoso, R. C.; Huang, X.; and Dennis, L. A.\n\n\n \n\n\n\n In Workshop on Agents and Robots for reliable Engineered Autonomy (AREA), 2020. \n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Stringer20a,\n  author    = {Stringer, P. and Cardoso, R. C. and Huang, X. and Dennis, L. A.},\n  title     = {Adaptable and Verifiable BDI Reasoning},\n  booktitle = {Workshop on Agents and Robots for reliable Engineered Autonomy (AREA)},\n  year      = {2020},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verification and Validation for Space Robotics.\n \n \n \n\n\n \n Cardoso, R. C.; Farrell, M.; Kourtis, G.; Webster, M.; Dennis, L. A.; Dixon, C.; Fisher, M.; and Lisitsa, A.\n\n\n \n\n\n\n 2020.\n Poster presented at the Opportunities and Challenges in Space Robotics Workshop held with ICRA 2020. [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@unpublished{Cardoso20c,\n  author    = {Cardoso, R. C. and Farrell, M. and Kourtis, G. and Webster, M. and Dennis, L. A. and Dixon, C. and Fisher, M. and Lisitsa, A.},\n  title     = {Verification and Validation for Space Robotics},\n  year      = {2020},\n  note = {Poster presented at the Opportunities and Challenges in Space Robotics Workshop held with ICRA 2020. [<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n ROSMonitoring: a Runtime Verification Framework for ROS.\n \n \n \n\n\n \n Ferrando, A.; Cardoso, R. C.; Fisher, M.; Ancona, D.; Franceschini, L.; and Mascardi, V.\n\n\n \n\n\n\n In Towards Autonomous Robotic Systems Conference (TAROS), 2020. \n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 15 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Ferrando20a,\n  author    = {Ferrando, A. and Cardoso, R. C. and Fisher, M. and Ancona, D. and Franceschini, L. and Mascardi, V.},\n  title     = {ROSMonitoring: a Runtime Verification Framework for ROS},\n  booktitle = {Towards Autonomous Robotic Systems Conference (TAROS)},\n  year      = {2020},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifiable Self-Aware Agent-Based Autonomous Systems.\n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n Proceedings of the IEEE special issue on Self-Aware Autonomous Systems,1011-1026. 2020.\n [Verifiable Autonomy, FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{dennis_ieee20,\n  author={Louise A. Dennis and Michael Fisher},\n  title ={Verifiable Self-Aware Agent-Based Autonomous Systems},\n  journal={Proceedings of the IEEE special issue on Self-Aware Autonomous Systems},\n  pages={1011-1026},\n  doi={10.1109/JPROC.2020.2991262},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]},\nyear=2020}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Model-Checking Information Diffusion in Social Networks with PRISM.\n \n \n \n\n\n \n Dennis, L. A.; and Slavkovik, M.\n\n\n \n\n\n\n In Bassiliades, N.; Chalkiadakis, G.; and de Jonge, D., editor(s), Multi-Agent Systems and Agreement Technologies, pages 475–492, Cham, 2020. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Dennis20,\n  author="Dennis, Louise A.\nand Slavkovik, Marija",\neditor="Bassiliades, Nick\nand Chalkiadakis, Georgios\nand de Jonge, Dave",\ntitle="Model-Checking Information Diffusion in Social Networks with PRISM",\nbooktitle="Multi-Agent Systems and Agreement Technologies",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="475--492",\nabstract="In this paper we present an agent-based approach to formalising information diffusion using Markov models which attempts to account for the internal informational state of the agent and investigate the use of probabilistic model-checking for analysing these models. We model information diffusion as both continuous and discrete time Markov chains, using the latter to provide an agent-centred perspective. We present a negative result - we conclude that current model-checking technology is inadequate for analysing such systems in an interesting way.",\nisbn="978-3-030-66412-1"\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Interface for Programming Verifiable Autonomous Agents in ROS.\n \n \n \n\n\n \n \n\n\n \n\n\n\n In null, editor(s), Multi-Agent Systems and Agreement Technologies, pages 191–205, Cham, 2020. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Heterogeneous Verification of an Autonomous Curiosity Rover.\n \n \n \n\n\n \n Cardoso, R. C.; Farrell, M.; Luckcuck, M.; Ferrando, A.; and Fisher, M.\n\n\n \n\n\n\n In NASA Formal Methods Symposium (NFM), 2020. \n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Cardoso20a,\n  author    = {Cardoso, R. C. and Farrell, M. and Luckcuck, M. and Ferrando, A. and Fisher, M.},\n  title     = {Heterogeneous Verification of an Autonomous Curiosity Rover},\n  booktitle = {NASA Formal Methods Symposium (NFM)},\n  year      = {2020},\n  note = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Reliable Decision-Making in Autonomous Vehicles.\n \n \n \n \n\n\n \n Alves, G. V.; Dennis, L.; Fernandes, L.; and Fisher, M.\n\n\n \n\n\n\n In Leitner, A.; Watzenig, D.; and Ibanez-Guzman, J., editor(s), Validation and Verification of Automated Systems: Results of the ENABLE-S3 Project, pages 105–117. Springer International Publishing, Cham, 2020.\n \n\n\n\n
\n\n\n\n \n \n \"ReliablePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 9 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{Alves2020,\nauthor="Alves, Gleifer Vaz\nand Dennis, Louise\nand Fernandes, Lucas\nand Fisher, Michael",\neditor="Leitner, Andrea\nand Watzenig, Daniel\nand Ibanez-Guzman, Javier",\ntitle="Reliable Decision-Making in Autonomous Vehicles",\nbookTitle="Validation and Verification of Automated Systems: Results of the ENABLE-S3 Project",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="105--117",\nabstract="The use of Autonomous Vehicles (AVs) on our streets is soon to be a reality; increasingly, interacting with such AVs will be part of our daily routine. However, we will certainly need to assure the reliable behaviour of an AV, especially when some unexpected scenarios (e.g. harsh environments, obstacles, emergencies) are taken into account. In this article we use an intelligent agent approach to capture the high-level decision-making process within an AV and then use formal verification techniques to automatically, and strongly, analyse the required behaviours. Specifically, we use the MCAPL framework, wherein our core agent is implemented using the GWENDOLEN agent programming language, and to which we can apply model checking via the AJPF model checker. By performing such formal verification on our agent, we are able to prove that the AV's decision-making process, embedded within the GWENDOLEN agent plans, matches our requirements. As examples, we will verify (formal) properties in order to determine whether the agent behaves in a reliable manner through three different levels of emergency displayed in a simple urban traffic environment.",\nisbn="978-3-030-14628-3",\ndoi="10.1007/978-3-030-14628-3_10",\nurl="https://doi.org/10.1007/978-3-030-14628-3_10"\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The ``Why Did You Do That?'' Button: Answering Why-Questions for End Users of Robotic Systems.\n \n \n \n\n\n \n Koeman, V. J.; Dennis, L. A.; Webster, M.; Fisher, M.; and Hindriks, K.\n\n\n \n\n\n\n In Dennis, L. A.; Bordini, R. H.; and Lespérance, Y., editor(s), Engineering Multi-Agent Systems, pages 152–172, Cham, 2020. Springer International Publishing\n [ORCA, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Koeman19EMAS,\nauthor="Koeman, Vincent J.\nand Dennis, Louise A.\nand Webster, Matt\nand Fisher, Michael\nand Hindriks, Koen",\neditor="Dennis, Louise A.\nand Bordini, Rafael H.\nand Lesp{\\'e}rance, Yves",\ntitle="The ``Why Did You Do That?'' Button: Answering Why-Questions for End Users of Robotic Systems",\nbooktitle="Engineering Multi-Agent Systems",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="152--172",\nabstract="The issue of explainability for autonomous systems is becoming increasingly prominent. Several researchers and organisations have advocated the provision of a ``Why did you do that?'' button which allows a user to interrogate a robot about its choices and actions. We take previous work on debugging cognitive agent programs and apply it to the question of supplying explanations to end users in the form of answers to why-questions. These previous approaches are based on the generation of a trace of events in the execution of the program and then answering why-questions using the trace. We implemented this framework in the agent infrastructure layer and, in particular, the Gwendolen programming language it supports -- extending it in the process to handle the generation of applicable plans and multiple intentions. In order to make the answers to why-questions comprehensible to end users we advocate a two step process in which first a representation of an explanation is created and this is subsequently converted into natural language in a way which abstracts away from some events in the trace and employs application specific predicate dictionaries in order to translate the first-order logic presentation of concepts within the cognitive agent program in natural language. A prototype implementation of these ideas is provided.",\nisbn="978-3-030-51417-4",\n  note = {[<span class="orca">ORCA</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Plan Library Reconfigurability in BDI Agents.\n \n \n \n\n\n \n Cardoso, R. C.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Dennis, L. A.; Bordini, R. H.; and Lespérance, Y., editor(s), Engineering Multi-Agent Systems, pages 195–212, Cham, 2020. Springer International Publishing\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Cardoso19EMAS,\nauthor="Cardoso, Rafael C.\nand Dennis, Louise A.\nand Fisher, Michael",\neditor="Dennis, Louise A.\nand Bordini, Rafael H.\nand Lesp{\\'e}rance, Yves",\ntitle="Plan Library Reconfigurability in BDI Agents",\nbooktitle="Engineering Multi-Agent Systems",\nyear="2020",\npublisher="Springer International Publishing",\naddress="Cham",\npages="195--212",\nabstract="One of the major advantages of modular architectures in robotic systems is the ability to add or replace nodes, without needing to rearrange the whole system. In this type of system, autonomous agents can aid in the decision making and high-level control of the robot. For example, a robot may have a module for each of the effectors and sensors that it has and an agent with a plan library containing high-level plans to aid in the decision making within these modules. However, when autonomously replacing a node it can be difficult to reconfigure plans in the agent's plan library while retaining correctness. In this paper, we exploit the formal concept of capabilities in Belief-Desire-Intention agents and describe how agents can reason about these capabilities in order to reconfigure their plan library while retaining overall correctness constraints. To validate our approach, we show the implementation of our framework and an experiment using a practical example in the Mars rover scenario.",\nisbn="978-3-030-51417-4",\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (12)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Analysis of Autonomous Mobile Collectives in Complex Physical Environments (Dagstuhl Seminar 19432).\n \n \n \n \n\n\n \n Gleirscher, M.; Haxthausen, A. E.; Leucker, M.; and Linker, S.\n\n\n \n\n\n\n Dagstuhl Reports, 9(10): 95–116. 2019.\n [S4]\n\n\n\n
\n\n\n\n \n \n \"AnalysisPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Linker2019b,\n  author    = {Mario Gleirscher and\n               Anne E. Haxthausen and\n               Martin Leucker and\n               Sven Linker},\n  title     = {Analysis of Autonomous Mobile Collectives in Complex Physical Environments\n               (Dagstuhl Seminar 19432)},\n  journal   = {Dagstuhl Reports},\n  volume    = {9},\n  number    = {10},\n  pages     = {95--116},\n  year      = {2019},\n  url       = {https://doi.org/10.4230/DagRep.9.10.95},\n  doi       = {10.4230/DagRep.9.10.95},\n  note = {[<span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Target counting with Presburger constraints and its application in sensor networks.\n \n \n \n \n\n\n \n Linker, S.; and Sevegnani, M.\n\n\n \n\n\n\n Proceedings of the Royal Society A, 475(2231). 2019.\n [S4]\n\n\n\n
\n\n\n\n \n \n \"TargetPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Linker2019a,\nauthor = {Sven Linker and Michele Sevegnani},\ntitle = {Target counting with Presburger constraints and its application in sensor networks},\njournal = {Proceedings of the Royal Society A},\nvolume = {475},\nnumber = {2231},\nyear = {2019},\nurl = {https://doi.org/10.1098/rspa.2019.0278},\ndoi = {10.1098/rspa.2019.0278},\n  note = {[<span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Modular Verification of Autonomous Space Robotics.\n \n \n \n\n\n \n Farrell, M.; Cardoso, R. C.; Dennis, L.; Dixon, C.; Fisher, M.; Kourtis, G.; Lisitsa, A.; Luckcuck, M.; and Webster, M\n\n\n \n\n\n\n In Assurance of Autonomy for Robotic Space Missions Workshop, 2019. \n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Farrell2019b,\n  author    = {Farrell, M. and Cardoso, R. C. and Dennis, L. and Dixon, C. and Fisher, M. and Kourtis, G. and Lisitsa, A. and Luckcuck, M. and Webster, M},\n  title     = {Modular Verification of Autonomous Space Robotics},\n  booktitle = {Assurance of Autonomy for Robotic Space Missions Workshop},\n  year      = {2019},\n  note = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages.\n \n \n \n\n\n \n Farrell, M.; Bradbury, M.; Fisher, M.; Dennis, L. A.; Dixon, C.; Yuan, H.; and Maple, C.\n\n\n \n\n\n\n In Ölveczky, P. C.; and Salaün, G., editor(s), Software Engineering and Formal Methods, pages 471–490, Cham, 2019. Springer International Publishing\n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{Farrell2019,\nauthor="Farrell, Marie\nand Bradbury, Matthew\nand Fisher, Michael\nand Dennis, Louise A.\nand Dixon, Clare\nand Yuan, Hu\nand Maple, Carsten",\neditor="{\\"O}lveczky, Peter Csaba\nand Sala{\\"u}n, Gwen",\ntitle="Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages",\nbooktitle="Software Engineering and Formal Methods",\nyear="2019",\npublisher="Springer International Publishing",\naddress="Cham",\npages="471--490",\nabstract="Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.",\nisbn="978-3-030-30446-1",\nnote = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Summary of Formal Specification and Verification of Autonomous Robotic Systems.\n \n \n \n\n\n \n Luckcuck, M.; Farrell, M.; Dennis, L. A.; Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n In Ahrendt, W.; and Tapia Tarifa, S. L., editor(s), Integrated Formal Methods, pages 538–541, Cham, 2019. Springer International Publishing\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{Luckcuck2019Summary,\nauthor="Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael",\neditor="Ahrendt, Wolfgang and Tapia Tarifa, Silvia Lizeth",\ntitle="A Summary of Formal Specification and Verification of Autonomous Robotic Systems",\nbooktitle="Integrated Formal Methods",\nyear="2019",\npublisher="Springer International Publishing",\naddress="Cham",\ndoi = {10.1007/978-3-030-34968-4_33},\npages="538--541",\nabstract="Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions published in [5], which surveys the state-of-the-art in formal specification and verification for autonomous robotics.",\nisbn="978-3-030-34968-4",\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Specification and Verification of Autonomous Robotic Systems: A Survey.\n \n \n \n \n\n\n \n Luckcuck, M.; Farrell, M.; Dennis, L. A.; Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n ACM Comput. Surv., 52(5): 1–41. sep 2019.\n [FAIR-SPACE, RAIN, ORCA]\n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Luckcuck2019,\ntitle = {{Formal Specification and Verification of Autonomous Robotic Systems: A Survey}},\nauthor = {Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael},\ndoi = {10.1145/3342355},\neprint = {1807.00048},\nissn = {03600300},\njournal = {ACM Comput. Surv.},\nmonth = {sep},\nnumber = {5},\npages = {1--41},\nurl = {https://arxiv.org/abs/1807.00048 http://dl.acm.org/citation.cfm?doid=3362097.3342355},\nvolume = {52},\nyear = {2019},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Probabilistic Model Checking of Robots Deployed in Extreme Environments.\n \n \n \n \n\n\n \n Zhao, X.; Robu, V.; Flynn, D.; Dinmohammadi, F.; Fisher, M.; and Webster, M.\n\n\n \n\n\n\n In Proc. 23rd AAAI Conference on Artificial Intelligence, pages 8066–8074, 2019. AAAI Press\n [ORCA]\n\n\n\n
\n\n\n\n \n \n \"ProbabilisticPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ZhaoRFD0W19,\n  author    = {Xingyu Zhao and\n               Valentin Robu and\n               David Flynn and\n               Fateme Dinmohammadi and\n               Michael Fisher and\n               Matt Webster},\n  title     = {Probabilistic Model Checking of Robots Deployed in Extreme Environments},\n  booktitle = {Proc. 23rd {AAAI} Conference on Artificial Intelligence},\n  pages     = {8066--8074},\n  year      = {2019},\n  publisher = {{AAAI} Press},\n  url       = {https://www.aaai.org/Library/AAAI/aaai19contents.php},\n  note = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards a Methodology to Test UAVs in Hazardous Environments.\n \n \n \n \n\n\n \n Page, V.; Webster, M.; Fisher, M.; and Jump, M.\n\n\n \n\n\n\n In ICAS 2019, The Fifteenth International Conference on Autonomic and Autonomous Systems, pages 38–45, June 2019. \n \n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{Page19ICAS,\n  author    = {Page, Vincent and Webster, Matt and Fisher, Michael and Jump, Mike},\n  title     = {Towards a {Methodology} to {Test} {UAVs} in {Hazardous} {Environments}},\n  booktitle = {ICAS 2019, The Fifteenth International Conference on Autonomic and Autonomous Systems},\n  year      = {2019},\n  pages     = {38--45},\n  month     = jun,\n  isbn      = {978-1-61208-712-2},\n  url       = {http://www.thinkmind.org/index.php?view=article&articleid=icas_2019_3_20_28007},\n  urldate   = {2019-06-12},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Enactability of Agent Interaction Protocols: Towards a Unified Approach.\n \n \n \n\n\n \n Ferrando, A.; Winikoff, M.; Cranefield, S.; Dignum, F.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. of the 7th International Workshop on Engineering Multi-Agent Systems (EMAS), 2019. \n [ORCA, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Ferrando19EMAS,\n  author    = {Angelo Ferrando and Michael Winikoff and Stephen Cranefield and Frank Dignum and Viviana Mascardi},\n  title     = {On Enactability of Agent Interaction Protocols: Towards a Unified Approach},\n  booktitle = {Proc. of the 7th International Workshop on Engineering Multi-Agent Systems (EMAS)},\n  year      = {2019},\n  note = {[<span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Proactive, Transparent, and Verifiable Ethical Reasoning for Robots.\n \n \n \n\n\n \n Bremner, P.; Dennis, L. A.; Fisher, M.; and Winfield, A. F.\n\n\n \n\n\n\n Proceedings of the IEEE,1-21. 2019.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@ARTICLE{BremnerDFW19,\nauthor={P. {Bremner} and L. A. {Dennis} and M. {Fisher} and A. F. {Winfield}},\njournal={Proceedings of the IEEE},\ntitle={On Proactive, Transparent, and Verifiable Ethical Reasoning for Robots},\nyear={2019},\nvolume={},\nnumber={},\npages={1-21},\nkeywords={Robots;Cognition;Ethics;Predictive models;Safety;Standards;Computer architecture;Ethics;formal verification;intelligent robots;software architecture.},\ndoi={10.1109/JPROC.2019.2898267},\nISSN={0018-9219},\nmonth={},\nnote = {[<span  class="va">Verifiable Autonomy</span>]}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Decentralised Planning for Multi-Agent Programming Platforms.\n \n \n \n\n\n \n Cardoso, R. C.; and Bordini, R. H.\n\n\n \n\n\n\n In Proc. of the 18th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), 2019. \n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Cardoso19AAMAS,\n  author    = {Rafael C. Cardoso and Rafael H. Bordini},\n  title     = {Decentralised Planning for Multi-Agent Programming Platforms},\n  booktitle = {Proc. of the 18th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS)},\n  year      = {2019},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Slicing Agent Programs for more Efficient Verification.\n \n \n \n\n\n \n Winikoff, M.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In Weyns, D.; Mascardi, V.; and Ricci, A., editor(s), Proc. 6th International Workshop in Engineering Multi-Agent Systems, volume 11375, of Lecture Notes in Computer Science, pages 139-157, Stockholm, Sweden, 2019. \n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{WinikoffDF:EMAS18,\n   author = {Michael Winikoff and Louise A. Dennis and Michael Fisher},\n   title = "{Slicing Agent Programs for more Efficient Verification}",\nbooktitle = {Proc. 6th International Workshop in Engineering Multi-Agent Systems},\nyear = {2019},\nvolume={11375},\npages={139-157},\neditor={D. Weyns and V. Mascardi and A. Ricci},\nseries={Lecture Notes in Computer Science},\naddress = {Stockholm, Sweden},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (22)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Verifiable Self-Certifying Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Collins, E.; Dennis, L. A.; Luckcuck, M.; Webster, M.; Jump, M.; Page, V.; Patchett, C.; Dinmohammadi, F.; Flynn, D.; Robu, V.; and Zhao, X.\n\n\n \n\n\n\n In 2018 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pages 341-348, Oct 2018. \n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{8539217,\n  author    = {Michael Fisher and Emily Collins and Louise A. Dennis and Matt Luckcuck and Matthew Webster and Michael Jump and Vincent Page and Charles Patchett and Fateme Dinmohammadi\n            and David Flynn and Valentin Robu and Xingu Zhao},\n  title     = {Verifiable Self-Certifying Autonomous Systems},\n  booktitle = {2018 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)},\n  year      = {2018},\n  pages     = {341-348},\n  month     = {Oct},\n  doi       = {10.1109/ISSREW.2018.00028},\n  note = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments.\n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In 2018. Springer\n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{NalonHD18,\nauthor = {Cl\\'audia Nalon and Ullrich Hustadt and Clare Dixon},\ntitle = "{KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments}",\njournal = {Journal of Automated Reasoning},\nyear = {2018},\n  volume    = {},\npublisher = {Springer},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks.\n \n \n \n\n\n \n Webster, M.; Breza, M.; Dixon, C.; Fisher, M.; and McCann, J.\n\n\n \n\n\n\n Electronic Communications of the EASST. 2018.\n [FAIR-SPACE, ORCA, RAIN]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{WebsterBDFM18,\n  author    =  {Matthew Webster and Michael Breza and Clare Dixon and Michael Fisher and Julie McCann},\n  title     = {Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks},\n  journal   = {Electronic Communications of the EASST},\n  volume    = {},\n  year      = {2018},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Making Sense of the World: Framing Models for Trustworthy Sensor-Driven Systems.\n \n \n \n\n\n \n Calder, M.; Dobson, S.; Fisher, M.; and McCann, J. A.\n\n\n \n\n\n\n Computers, 7(4): 62. 2018.\n [S4]\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{CalderDFM18,\n  author    = {Muffy Calder and\n               Simon Dobson and\n               Michael Fisher and\n               Julie A. McCann},\n  title     = "{Making Sense of the World: Framing Models for Trustworthy Sensor-Driven\n               Systems}",\n  journal   = {Computers},\n  volume    = {7},\n  number    = {4},\n  pages     = {62},\n  year      = {2018},\n  doi       = {10.3390/computers7040062},\n  note = {[<span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics.\n \n \n \n \n\n\n \n Hustadt, U.; Nalon, C.; and Dixon, C.\n\n\n \n\n\n\n In Konev, B.; Urban, J.; and Rümmer, P., editor(s), Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR), of CEUR Workshop Proceedings, pages 34–48, Aachen, 2018. \n [FAIR-SPACE, RAIN]\n\n\n\n
\n\n\n\n \n \n \"EvaluatingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{HustadtEtAl:PAAR2018,\nauthor = {Ullrich Hustadt and Cl\\'audia Nalon and Clare Dixon},\ntitle = "{Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics}",\nbooktitle = {Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)},\nyear = {2018},\npages = {34--48},\neditor = {Boris Konev and Josef Urban and Philipp R\\"ummer},\nnumber = 2162,\nseries = {CEUR Workshop Proceedings},\naddress = {Aachen},\nissn = {1613-0073},\nurl = {http://ceur-ws.org/Vol-2162/#paper-04},\nvenue = {Oxford, UK},\neventdate = {2018-07-19},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Machines That Know Right And Cannot Do Wrong: The Theory and Practice of Machine Ethics.\n \n \n \n \n\n\n \n Dennis, L. A.; and Slavkovik, M.\n\n\n \n\n\n\n IEEE Intelligent Informatics Bulletin, 19(1). 2018.\n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"MachinesPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{dennis18iib,\n  author = {Louise A. Dennis and Marija Slavkovik},\n  title = {Machines That Know Right And Cannot Do Wrong: The Theory and Practice of Machine Ethics},\n  journal = {IEEE Intelligent Informatics Bulletin},\n  volume = 19,\n  number = 1,\n  year = 2018,\n  url = {http://www.comp.hkbu.edu.hk/~cib/2018/Aug/article2/iib_vol19no1_article2.pdf},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifying and Validating Autonomous Systems: an Integrated Approach.\n \n \n \n\n\n \n Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. 8th IEEE International Conference on Runtime Verification (RV), 2018. \n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{Ferrando:RV18,\n   author = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi},\n    title = "{Verifying and Validating Autonomous Systems: an Integrated Approach}",\nbooktitle = {Proc. 8th IEEE International Conference on Runtime\n                  Verification (RV)},\nyear = {2018},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Robotics and Integrated Formal Methods: Necessity Meets Opportunity.\n \n \n \n \n\n\n \n Farrell, M.; Luckcuck, M.; and Fisher, M.\n\n\n \n\n\n\n In Furia, C. A.; and Winter, K., editor(s), Proc. 14th International Conference on Integrated Formal Methods (iFM), volume 11023, of Lecture Notes in Computer Science, pages 161-171, 2018. Springer\n [FAIR-SPACE, ORCA, RAIN]\n\n\n\n
\n\n\n\n \n \n \"RoboticsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{FarrellLF:IFM018,\n  author    = {Marie Farrell and Matt Luckcuck and Michael Fisher},\n  editor    = {Carlo A. Furia and Kirsten Winter},\n  title     = {Robotics and Integrated Formal Methods: Necessity Meets Opportunity},\n  booktitle = {Proc. 14th International Conference on Integrated\n               Formal Methods (iFM)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {11023},\n  pages     = {161-171},\n  publisher = {Springer},\n  year      = {2018},\n  url       = {https://doi.org/10.1007/978-3-319-98938-9_10},\n  doi       = {10.1007/978-3-319-98938-9_10},\n  biburl    = {https://dblp.org/rec/bib/conf/ifm/FarrellL018},\nnote = {[<span class="fs">FAIR-SPACE</span>, <span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Clarification of Ambiguity for the Simple Authentication and Security Layer.\n \n \n \n \n\n\n \n Al-Shareefi, F.; Lisitsa, A.; and Dixon, C.\n\n\n \n\n\n\n In Butler, M. J.; Raschke, A.; Hoang, T. S.; and Reichl, K., editor(s), Proc. 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ), volume 10817, of Lecture Notes in Computer Science, pages 189-203, 2018. Springer\n [FAIR-SPACE]\n\n\n\n
\n\n\n\n \n \n \"ClarificationPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{AlShareefiLD:ABZ18,\n  author    = {Farah Al{-}Shareefi and\n               Alexei Lisitsa and Clare Dixon},\n  editor    = {Michael J. Butler and\n               Alexander Raschke and\n               Thai Son Hoang and\n               Klaus Reichl},\n  title     = "{Clarification of Ambiguity for the Simple Authentication\n                and Security  Layer}",\n  booktitle = {Proc. 6th International Conference on Abstract\n               State Machines, Alloy, B, TLA, VDM, and {Z} (ABZ)},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {10817},\n  pages     = {189-203},\n  publisher = {Springer},\n  year      = {2018},\n  url       = {https://doi.org/10.1007/978-3-319-91271-4\\_13},\n  doi       = {10.1007/978-3-319-91271-4\\_13},\n  biburl    = {https://dblp.org/rec/bib/conf/asm/Al-ShareefiLD18},\n  note = {[<span class="fs">FAIR-SPACE</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifiable Self-Certifying Autonomous Systems.\n \n \n \n\n\n \n Fisher, M.; Collins, E.; Dennis, L. A.; Luckcuck, M.; Webster, M.; Jump, M.; Page, V.; Patchett, C.; Dinmohammadi, F.; Flynn, D.; Robu, V.; and Zhao, X.\n\n\n \n\n\n\n In Proc. 8th IEEE International Workshop on Software Certification (WoSoCer), Memphis, USA, 2018. \n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{Fisher:WoSoCer18,\n   author = {Michael Fisher and Emily Collins and Louise A. Dennis and Matt Luckcuck and Matthew Webster and Michael Jump and Vincent Page and Charles Patchett and Fateme Dinmohammadi\n            and David Flynn and Valentin Robu and Xingu Zhao},\n    title = "{Verifiable Self-Certifying Autonomous Systems}",\nbooktitle = {Proc. 8th IEEE International Workshop on Software Certification (WoSoCer)},\nyear = {2018},\naddress = {Memphis, USA},\nnote = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Certification of Safe and Trusted Robotic Inspection of Assets.\n \n \n \n\n\n \n Dinmohammadi, F.; Flynn, D.; Fisher, M.; Jump, M.; Page, V.; Robu, V.; Patchett, C.; Tang, W.; and Webster, M.\n\n\n \n\n\n\n In Proc. Prognostics and System Health Management Conference (PHM-Chongqing), Chongqing, China, 2018. IEEE\n [ORCA]\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@INPROCEEDINGS{Dinmohammadi:PHM18,\nauthor={Fateme Dinmohammadi and David Flynn and Michael Fisher and Michael Jump and Vincent Page and Valentin Robu and Charles Patchett and Wenshuo Tang and Matthew Webster},\nbooktitle={Proc. Prognostics and System Health Management\n     Conference (PHM-Chongqing)},\ntitle="{Certification of Safe and Trusted Robotic Inspection of Assets}",\nyear={2018},\nvolume={},\nnumber={},\naddress = {Chongqing, China},\npages={},\npublisher = {IEEE},\nnote = {[<span class="orca">ORCA</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Recognising Assumption Violations in Autonomous Systems Verification.\n \n \n \n \n\n\n \n Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; and Mascardi, V.\n\n\n \n\n\n\n In Proc. 17th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), pages 1933–1935, 2018. IFAAMAS/ACM\n [FAIR-SPACE, RAIN, Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"RecognisingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{FerrandoDA0M18,\n  author    = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi},\n  title     = "{Recognising Assumption Violations in Autonomous Systems Verification}",\n  booktitle = {Proc. 17th International Conference on Autonomous Agents\n               and MultiAgent Systems (AAMAS)},\n  pages     = {1933--1935},\n  year      = {2018},\n  publisher = {IFAAMAS/ACM},\n  url       = {http://dl.acm.org/citation.cfm?id=3238028},\n  timestamp = {Mon, 16 Jul 2018 09:21:17 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/atal/FerrandoDA0M18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time.\n \n \n \n \n\n\n \n Kamali, M.; Linker, S.; and Fisher, M.\n\n\n \n\n\n\n In Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2018. \n [FAIR-SPACE,S4,Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"ModularPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{KamaliLF:FTSCS18,\n  author    = {Maryam Kamali and Sven Linker and Michael Fisher},\n  title     = "{Modular Verification of Vehicle Platooning with Respect to Decisions,\n               Space and Time}",\n  booktitle = {Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1804.06647},\n  note = {[<span class="fs">FAIR-SPACE</span>,<span class="s4">S4</span>,<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators.\n \n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n In Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings, pages 160–176, 2018. \n [S4]\n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icfem/GainerLDH018,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption\n               in Networks of Pulse-Coupled Oscillators},\n  booktitle = {Formal Methods and Software Engineering - 20th International Conference\n               on Formal Engineering Methods, {ICFEM} 2018, Gold Coast, QLD, Australia,\n               November 12-16, 2018, Proceedings},\n  pages     = {160--176},\n  year      = {2018},\n  crossref  = {DBLP:conf/icfem/2018},\n  url       = {https://doi.org/10.1007/978-3-030-02450-5\\_10},\n  doi       = {10.1007/978-3-030-02450-5\\_10},\n  timestamp = {Mon, 05 Nov 2018 11:04:23 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/icfem/GainerLDH018},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Multi-Scale Verification of Distributed Synchronisation.\n \n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n CoRR, abs/1809.10655. 2018.\n [S4]\n\n\n\n
\n\n\n\n \n \n \"Multi-ScalePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-1809-10655,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {Multi-Scale Verification of Distributed Synchronisation},\n  journal   = {CoRR},\n  volume    = {abs/1809.10655},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1809.10655},\n  archivePrefix = {arXiv},\n  eprint    = {1809.10655},\n  timestamp = {Fri, 05 Oct 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1809-10655},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The MCAPL Framework including the Agent Infrastructure Layer an Agent Java Pathfinder.\n \n \n \n \n\n\n \n Dennis, L. A.\n\n\n \n\n\n\n J. Open Source Software, 3(24): 617. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/jossw/Dennis18,\n  author    = {Louise A. Dennis},\n  title     = {The {MCAPL} Framework including the Agent Infrastructure Layer an\n               Agent Java Pathfinder},\n  journal   = {J. Open Source Software},\n  volume    = {3},\n  number    = {24},\n  pages     = {617},\n  year      = {2018},\n  url       = {https://doi.org/10.21105/joss.00617},\n  doi       = {10.21105/joss.00617},\n  timestamp = {Tue, 13 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/jossw/Dennis18},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Two-stage agent program verification.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; and Webster, M.\n\n\n \n\n\n\n J. Log. Comput., 28(3): 499–523. 2018.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"Two-stagePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/logcom/Dennis0W18,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Matt Webster},\n  title     = {Two-stage agent program verification},\n  journal   = {J. Log. Comput.},\n  volume    = {28},\n  number    = {3},\n  pages     = {499--523},\n  year      = {2018},\n  url       = {https://doi.org/10.1093/logcom/exv002},\n  doi       = {10.1093/logcom/exv002},\n  timestamp = {Mon, 07 May 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/logcom/Dennis0W18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Practical Challenges in Explicit Ethical Machine Reasoning.\n \n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2018, Fort Lauderdale, Florida, USA, January 3-5, 2018., 2018. \n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"PracticalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/isaim/F18,\n  author    = {Louise A. Dennis and\n               Michael Fisher},\n  title     = {Practical Challenges in Explicit Ethical Machine Reasoning},\n  booktitle = {International Symposium on Artificial Intelligence and Mathematics,\n               {ISAIM} 2018, Fort Lauderdale, Florida, USA, January 3-5, 2018.},\n  year      = {2018},\n  crossref  = {DBLP:conf/isaim/2018},\n  url       = {http://isaim2018.cs.virginia.edu/papers/ISAIM2018\\_Ethics\\_Dennis\\_Fischer.pdf},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/isaim/DennisF18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Making Sense of the World: Models for Reliable Sensor-Driven Systems.\n \n \n \n \n\n\n \n \n\n\n \n\n\n\n CoRR, abs/1803.10478. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"MakingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time.\n \n \n \n \n\n\n \n Kamali, M.; Linker, S.; and Fisher, M.\n\n\n \n\n\n\n CoRR, abs/1804.06647. 2018.\n [Verifiable Autonomy, S4]\n\n\n\n
\n\n\n\n \n \n \"ModularPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-1804-06647,\n  author    = {Maryam Kamali and\n               Sven Linker and\n               Michael Fisher},\n  title     = {Modular Verification of Vehicle Platooning with Respect to Decisions,\n               Space and Time},\n  journal   = {CoRR},\n  volume    = {abs/1804.06647},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1804.06647},\n  archivePrefix = {arXiv},\n  eprint    = {1804.06647},\n  timestamp = {Mon, 13 Aug 2018 16:48:43 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1804-06647},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Sequent Calculus for Euler Diagrams.\n \n \n \n \n\n\n \n Linker, S.\n\n\n \n\n\n\n In Diagrammatic Representation and Inference - 10th International Conference, Diagrams 2018, Edinburgh, UK, June 18-22, 2018, Proceedings, pages 399–407, 2018. \n [S4]\n\n\n\n
\n\n\n\n \n \n \"SequentPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/diagrams/Linker18,\n  author    = {Sven Linker},\n  title     = {Sequent Calculus for Euler Diagrams},\n  booktitle = {Diagrammatic Representation and Inference - 10th International Conference,\n               Diagrams 2018, Edinburgh, UK, June 18-22, 2018, Proceedings},\n  pages     = {399--407},\n  year      = {2018},\n  crossref  = {DBLP:conf/diagrams/2018},\n  url       = {https://doi.org/10.1007/978-3-319-91376-6\\_37},\n  doi       = {10.1007/978-3-319-91376-6\\_37},\n  timestamp = {Tue, 10 Jul 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/diagrams/Linker18},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n SCAV'18: Report of the 2nd International Workshop on Safe Control of Autonomous Vehicles.\n \n \n \n \n\n\n \n Gleirscher, M.; Linker, S.; and Kugele, S.\n\n\n \n\n\n\n CoRR, abs/1811.01774. 2018.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"SCAV'18:Paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-1811-01774,\n  author    = {Mario Gleirscher and\n               Sven Linker and\n               Stefan Kugele},\n  title     = {SCAV'18: Report of the 2nd International Workshop on Safe Control\n               of Autonomous Vehicles},\n  journal   = {CoRR},\n  volume    = {abs/1811.01774},\n  year      = {2018},\n  url       = {http://arxiv.org/abs/1811.01774},\n  archivePrefix = {arXiv},\n  eprint    = {1811.01774},\n  timestamp = {Thu, 22 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1811-01774},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (15)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Theorem Proving for Metric Temporal Logic over the Naturals.\n \n \n \n \n\n\n \n Hustadt, U.; Ozaki, A.; and Dixon, C.\n\n\n \n\n\n\n In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pages 326–343, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"TheoremPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/cade/HustadtOD17,\n  author    = {Ullrich Hustadt and\n               Ana Ozaki and\n               Clare Dixon},\n  title     = {Theorem Proving for Metric Temporal Logic over the Naturals},\n  booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on\n               Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},\n  pages     = {326--343},\n  year      = {2017},\n  crossref  = {DBLP:conf/cade/2017},\n  url       = {https://doi.org/10.1007/978-3-319-63046-5\\_20},\n  doi       = {10.1007/978-3-319-63046-5\\_20},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/cade/HustadtOD17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n CRutoN: Automatic Verification of a Robotic Assistant's Behaviours.\n \n \n \n \n\n\n \n Gainer, P.; Dixon, C.; Dautenhahn, K.; Fisher, M.; Hustadt, U.; Saunders, J.; and Webster, M.\n\n\n \n\n\n\n In Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20, 2017, Proceedings, pages 119–133, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"CRutoN:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/fmics/GainerDDFHSW17,\n  author    = {Paul Gainer and\n               Clare Dixon and\n               Kerstin Dautenhahn and\n               Michael Fisher and\n               Ullrich Hustadt and\n               Joe Saunders and\n               Matt Webster},\n  title     = {CRutoN: Automatic Verification of a Robotic Assistant's Behaviours},\n  booktitle = {Critical Systems: Formal Methods and Automated Verification - Joint\n               22nd International Workshop on Formal Methods for Industrial Critical\n               Systems - and - 17th International Workshop on Automated Verification\n               of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20,\n               2017, Proceedings},\n  pages     = {119--133},\n  year      = {2017},\n  crossref  = {DBLP:conf/fmics/2017},\n  url       = {https://doi.org/10.1007/978-3-319-67113-0\\_8},\n  doi       = {10.1007/978-3-319-67113-0\\_8},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/fmics/GainerDDFHSW17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n KSP: A Resolution-based Prover for Multimodal K, Abridged Report.\n \n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 4919–4923, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"KSP:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ijcai/NalonHD17,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Ullrich Hustadt and\n               Clare Dixon},\n  title     = {{KSP:} {A} Resolution-based Prover for Multimodal K, Abridged Report},\n  booktitle = {Proceedings of the Twenty-Sixth International Joint Conference on\n               Artificial Intelligence, {IJCAI} 2017, Melbourne, Australia, August\n               19-25, 2017},\n  pages     = {4919--4923},\n  year      = {2017},\n  crossref  = {DBLP:conf/ijcai/2017},\n  url       = {https://doi.org/10.24963/ijcai.2017/694},\n  doi       = {10.24963/ijcai.2017/694},\n  timestamp = {Wed, 27 Jun 2018 12:24:11 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/ijcai/NalonHD17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking.\n \n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n In Quantitative Evaluation of Systems - 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings, pages 224–239, 2017. \n [S4]\n\n\n\n
\n\n\n\n \n \n \"InvestigatingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/qest/GainerLDHF17,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {Investigating Parametric Influence on Discrete Synchronisation Protocols\n               Using Quantitative Model Checking},\n  booktitle = {Quantitative Evaluation of Systems - 14th International Conference,\n               {QEST} 2017, Berlin, Germany, September 5-7, 2017, Proceedings},\n  pages     = {224--239},\n  year      = {2017},\n  crossref  = {DBLP:conf/qest/2017},\n  url       = {https://doi.org/10.1007/978-3-319-66335-7\\_14},\n  doi       = {10.1007/978-3-319-66335-7\\_14},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/qest/GainerLDHF17},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Abstract State Machines and System Theoretic Process Analysis for Safety-Critical Systems.\n \n \n \n \n\n\n \n Al-Shareefi, F.; Lisitsa, A.; and Dixon, C.\n\n\n \n\n\n\n In Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings, pages 15–32, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"AbstractPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sbmf/Al-ShareefiLD17,\n  author    = {Farah Al{-}Shareefi and\n               Alexei Lisitsa and\n               Clare Dixon},\n  title     = {Abstract State Machines and System Theoretic Process Analysis for\n               Safety-Critical Systems},\n  booktitle = {Formal Methods: Foundations and Applications - 20th Brazilian Symposium,\n               {SBMF} 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings},\n  pages     = {15--32},\n  year      = {2017},\n  crossref  = {DBLP:conf/sbmf/2017},\n  url       = {https://doi.org/10.1007/978-3-319-70848-5\\_3},\n  doi       = {10.1007/978-3-319-70848-5\\_3},\n  timestamp = {Fri, 17 Nov 2017 14:28:29 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/sbmf/Al-ShareefiLD17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings.\n \n \n \n \n\n\n \n Dixon, C.; and Finger, M.,\n editors.\n \n\n\n \n\n\n\n Volume 10483, of Lecture Notes in Computer Science.Springer. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"FrontiersPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@proceedings{DBLP:conf/frocos/2017,\n  editor    = {Clare Dixon and\n               Marcelo Finger},\n  title     = {Frontiers of Combining Systems - 11th International Symposium, FroCoS\n               2017, Bras{\\'{\\i}}lia, Brazil, September 27-29, 2017, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {10483},\n  publisher = {Springer},\n  year      = {2017},\n  url       = {https://doi.org/10.1007/978-3-319-66167-4},\n  doi       = {10.1007/978-3-319-66167-4},\n  isbn      = {978-3-319-66166-7},\n  timestamp = {Tue, 05 Sep 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/frocos/2017},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators.\n \n \n \n \n\n\n \n Gainer, P.; Linker, S.; Dixon, C.; Hustadt, U.; and Fisher, M.\n\n\n \n\n\n\n CoRR, abs/1709.04385. 2017.\n [S4]\n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-1709-04385,\n  author    = {Paul Gainer and\n               Sven Linker and\n               Clare Dixon and\n               Ullrich Hustadt and\n               Michael Fisher},\n  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption\n               in Networks of Pulse-Coupled Oscillators},\n  journal   = {CoRR},\n  volume    = {abs/1709.04385},\n  year      = {2017},\n  url       = {http://arxiv.org/abs/1709.04385},\n  archivePrefix = {arXiv},\n  eprint    = {1709.04385},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-04385},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal verification of autonomous vehicle platooning.\n \n \n \n \n\n\n \n Kamali, M.; Dennis, L. A.; McAree, O.; Fisher, M.; and Veres, S. M.\n\n\n \n\n\n\n Sci. Comput. Program., 148: 88–106. 2017.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/scp/KamaliDMFV17,\n  author    = {Maryam Kamali and\n               Louise A. Dennis and\n               Owen McAree and\n               Michael Fisher and\n               Sandor M. Veres},\n  title     = {Formal verification of autonomous vehicle platooning},\n  journal   = {Sci. Comput. Program.},\n  volume    = {148},\n  pages     = {88--106},\n  year      = {2017},\n  url       = {https://doi.org/10.1016/j.scico.2017.05.006},\n  doi       = {10.1016/j.scico.2017.05.006},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/scp/KamaliDMFV17},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards Moral Autonomous Systems.\n \n \n \n \n\n\n \n Charisi, V.; Dennis, L. A.; Fisher, M.; Lieck, R.; Matthias, A.; Slavkovik, M.; Sombetzki, J.; Winfield, A. F. T.; and Yampolskiy, R.\n\n\n \n\n\n\n CoRR, abs/1703.04741. 2017.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/CharisiDFLMSSWY17,\n  author    = {Vicky Charisi and\n               Louise A. Dennis and\n               Michael Fisher and\n               Robert Lieck and\n               Andreas Matthias and\n               Marija Slavkovik and\n               Janina Sombetzki and\n               Alan F. T. Winfield and\n               Roman Yampolskiy},\n  title     = {Towards Moral Autonomous Systems},\n  journal   = {CoRR},\n  volume    = {abs/1703.04741},\n  year      = {2017},\n  url       = {http://arxiv.org/abs/1703.04741},\n  archivePrefix = {arXiv},\n  eprint    = {1703.04741},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/CharisiDFLMSSWY17},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification.\n \n \n \n \n\n\n \n Fernandes, L. E. R.; Custodio, V.; Alves, G. V.; and Fisher, M.\n\n\n \n\n\n\n In Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@iFM 2017, Turin, Italy, 19th September 2017., pages 35–42, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:journals/corr/abs-1709-02557,\n  author    = {Lucas E. R. Fernandes and\n               Vinicius Custodio and\n               Gleifer V. Alves and\n               Michael Fisher},\n  title     = {A Rational Agent Controlling an Autonomous Vehicle: Implementation\n               and Formal Verification},\n  booktitle = {Proceedings First Workshop on Formal Verification of Autonomous Vehicles,\n               FVAV@iFM 2017, Turin, Italy, 19th September 2017.},\n  pages     = {35--42},\n  year      = {2017},\n  url       = {https://doi.org/10.4204/EPTCS.257.5},\n  doi       = {10.4204/EPTCS.257.5},\n  timestamp = {Fri, 02 Nov 2018 09:30:18 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-02557},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finding Maximum Expected Termination Time of Probabilistic Timed Automata Models with Cyclic behavior.\n \n \n \n \n\n\n \n Al-Bataineh, O. I.; Fisher, M.; and Rosenblum, D.\n\n\n \n\n\n\n CoRR, abs/1709.07171. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"FindingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-1709-07171,\n  author    = {Omar I. Al{-}Bataineh and\n               Michael Fisher and\n               David Rosenblum},\n  title     = {Finding Maximum Expected Termination Time of Probabilistic Timed Automata\n               Models with Cyclic behavior},\n  journal   = {CoRR},\n  volume    = {abs/1709.07171},\n  year      = {2017},\n  url       = {http://arxiv.org/abs/1709.07171},\n  archivePrefix = {arXiv},\n  eprint    = {1709.07171},\n  timestamp = {Mon, 13 Aug 2018 16:48:50 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-07171},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Hybrid Multi-Lane Spatial Logic.\n \n \n \n \n\n\n \n Linker, S.\n\n\n \n\n\n\n Archive of Formal Proofs. 2017.\n [Verifiable Autonomy, S4]\n\n\n\n
\n\n\n\n \n \n \"HybridPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Linker17,\n  author    = {Sven Linker},\n  title     = {Hybrid Multi-Lane Spatial Logic},\n  journal   = {Archive of Formal Proofs},\n  year      = {2017},\n  url       = {https://www.isa-afp.org/entries/Hybrid\\_Multi\\_Lane\\_Spatial\\_Logic.html},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesizing and verifying controllers for multi-lane traffic maneuvers.\n \n \n \n \n\n\n \n von Bochmann, G.; Hilscher, M.; Linker, S.; and Olderog, E.\n\n\n \n\n\n\n Formal Asp. Comput., 29(4): 583–600. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"SynthesizingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/fac/BochmannHLO17,\n  author    = {Gregor von Bochmann and\n               Martin Hilscher and\n               Sven Linker and\n               Ernst{-}R{\\"{u}}diger Olderog},\n  title     = {Synthesizing and verifying controllers for multi-lane traffic maneuvers},\n  journal   = {Formal Asp. Comput.},\n  volume    = {29},\n  number    = {4},\n  pages     = {583--600},\n  year      = {2017},\n  url       = {https://doi.org/10.1007/s00165-017-0424-4},\n  doi       = {10.1007/s00165-017-0424-4},\n  timestamp = {Wed, 26 Jul 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/fac/BochmannHLO17},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL.\n \n \n \n \n\n\n \n Linker, S.\n\n\n \n\n\n\n In Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings, pages 34–49, 2017. \n [Verifiable Autonomy, S4]\n\n\n\n
\n\n\n\n \n \n \"SpatialPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ifm/Linker17,\n  author    = {Sven Linker},\n  title     = {Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL},\n  booktitle = {Integrated Formal Methods - 13th International Conference, {IFM} 2017,\n               Turin, Italy, September 20-22, 2017, Proceedings},\n  pages     = {34--49},\n  year      = {2017},\n  crossref  = {DBLP:conf/ifm/2017},\n  url       = {https://doi.org/10.1007/978-3-319-66845-1\\_3},\n  doi       = {10.1007/978-3-319-66845-1\\_3},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/ifm/Linker17},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formalising Sensor Topologies for Target Counting.\n \n \n \n \n\n\n \n Linker, S.; and Sevegnani, M.\n\n\n \n\n\n\n In Proceedings First Workshop on Architectures, Languages and Paradigms for IoT, ALP4IoT@iFM 2017, Turin, Italy, September 18, 2017., pages 43–57, 2017. \n [S4]\n\n\n\n
\n\n\n\n \n \n \"FormalisingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:journals/corr/abs-1802-01791,\n  author    = {Sven Linker and\n               Michele Sevegnani},\n  title     = {Formalising Sensor Topologies for Target Counting},\n  booktitle = {Proceedings First Workshop on Architectures, Languages and Paradigms\n               for IoT, ALP4IoT@iFM 2017, Turin, Italy, September 18, 2017.},\n  pages     = {43--57},\n  year      = {2017},\n  crossref  = {DBLP:journals/corr/abs-1802-00976},\n  url       = {https://doi.org/10.4204/EPTCS.264.5},\n  doi       = {10.4204/EPTCS.264.5},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1802-01791},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="s4">S4</span>]}\n}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (10)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study.\n \n \n \n \n\n\n \n Webster, M.; Dixon, C.; Fisher, M.; Salem, M.; Saunders, J.; Koay, K. L.; Dautenhahn, K.; and Saez-Pons, J.\n\n\n \n\n\n\n IEEE Trans. Human-Machine Systems, 46(2): 186–196. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"TowardPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/thms/WebsterDFSSKDS16,\n  author    = {Matt Webster and\n               Clare Dixon and\n               Michael Fisher and\n               Maha Salem and\n               Joe Saunders and\n               Kheng Lee Koay and\n               Kerstin Dautenhahn and\n               Joan Saez{-}Pons},\n  title     = {Toward Reliable Autonomous Robotic Assistants Through Formal Verification:\n               {A} Case Study},\n  journal   = {{IEEE} Trans. Human-Machine Systems},\n  volume    = {46},\n  number    = {2},\n  pages     = {186--196},\n  year      = {2016},\n  url       = {https://doi.org/10.1109/THMS.2015.2425139},\n  doi       = {10.1109/THMS.2015.2425139},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/thms/WebsterDFSSKDS16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n : A Resolution-Based Prover for Multimodal K.\n \n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, pages 406–415, 2016. \n \n\n\n\n
\n\n\n\n \n \n \":Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/cade/NalonHD16,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Ullrich Hustadt and\n               Clare Dixon},\n  title     = {: {A} Resolution-Based Prover for Multimodal {K}},\n  booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}\n               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},\n  pages     = {406--415},\n  year      = {2016},\n  crossref  = {DBLP:conf/cade/2016},\n  url       = {https://doi.org/10.1007/978-3-319-40229-1\\_28},\n  doi       = {10.1007/978-3-319-40229-1\\_28},\n  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/cade/NalonHD16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Probabilistic Model Checking of Ant-Based Positionless Swarming.\n \n \n \n \n\n\n \n Gainer, P.; Dixon, C.; and Hustadt, U.\n\n\n \n\n\n\n In Towards Autonomous Robotic Systems - 17th Annual Conference, TAROS 2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings, pages 127–138, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"ProbabilisticPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/taros/GainerDH16,\n  author    = {Paul Gainer and\n               Clare Dixon and\n               Ullrich Hustadt},\n  title     = {Probabilistic Model Checking of Ant-Based Positionless Swarming},\n  booktitle = {Towards Autonomous Robotic Systems - 17th Annual Conference, {TAROS}\n               2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings},\n  pages     = {127--138},\n  year      = {2016},\n  crossref  = {DBLP:conf/taros/2016},\n  url       = {https://doi.org/10.1007/978-3-319-40379-3\\_13},\n  doi       = {10.1007/978-3-319-40379-3\\_13},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/taros/GainerDH16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An Assurance-based Approach to Verification and Validation of Human-Robot Teams.\n \n \n \n \n\n\n \n Webster, M.; Western, D.; Araiza-Illan, D.; Dixon, C.; Eder, K.; Fisher, M.; and Pipe, A. G.\n\n\n \n\n\n\n CoRR, abs/1608.07403. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/WebsterWADEFP16,\n  author    = {Matt Webster and\n               David Western and\n               Dejanira Araiza{-}Illan and\n               Clare Dixon and\n               Kerstin Eder and\n               Michael Fisher and\n               Anthony G. Pipe},\n  title     = {An Assurance-based Approach to Verification and Validation of Human-Robot\n               Teams},\n  journal   = {CoRR},\n  volume    = {abs/1608.07403},\n  year      = {2016},\n  url       = {http://arxiv.org/abs/1608.07403},\n  archivePrefix = {arXiv},\n  eprint    = {1608.07403},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/WebsterWADEFP16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Practical verification of decision-making in agent-based autonomous systems.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; Lincoln, N.; Lisitsa, A.; and Veres, S. M.\n\n\n \n\n\n\n Autom. Softw. Eng., 23(3): 305–359. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"PracticalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/ase/DennisFLLV16,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Nicholas Lincoln and\n               Alexei Lisitsa and\n               Sandor M. Veres},\n  title     = {Practical verification of decision-making in agent-based autonomous\n               systems},\n  journal   = {Autom. Softw. Eng.},\n  volume    = {23},\n  number    = {3},\n  pages     = {305--359},\n  year      = {2016},\n  url       = {https://doi.org/10.1007/s10515-014-0168-9},\n  doi       = {10.1007/s10515-014-0168-9},\n  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/ase/DennisFLLV16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal verification of ethical choices in autonomous systems.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; Slavkovik, M.; and Webster, M.\n\n\n \n\n\n\n Robotics and Autonomous Systems, 77: 1–14. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/ras/DennisFSW16,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Marija Slavkovik and\n               Matt Webster},\n  title     = {Formal verification of ethical choices in autonomous systems},\n  journal   = {Robotics and Autonomous Systems},\n  volume    = {77},\n  pages     = {1--14},\n  year      = {2016},\n  url       = {https://doi.org/10.1016/j.robot.2015.11.012},\n  doi       = {10.1016/j.robot.2015.11.012},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/ras/DennisFSW16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n \"How Did They Know?\" - Model-Checking for Analysis of Information Leakage in Social Networks.\n \n \n \n \n\n\n \n Dennis, L. A.; Slavkovik, M.; and Fisher, M.\n\n\n \n\n\n\n In Coordination, Organizations, Institutions, and Norms in Agent Systems XII - COIN 2016 International Workshops, COIN@AAMAS, Singapore, Singapore, May 9, 2016, COIN@ECAI, The Hague, The Netherlands, August 30, 2016, Revised Selected Papers, pages 42–59, 2016. \n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \""HowPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/atal/DennisSF16,\n  author    = {Louise A. Dennis and\n               Marija Slavkovik and\n               Michael Fisher},\n  title     = {"How Did They Know?" - Model-Checking for Analysis of Information\n               Leakage in Social Networks},\n  booktitle = {Coordination, Organizations, Institutions, and Norms in Agent Systems\n               {XII} - {COIN} 2016 International Workshops, COIN@AAMAS, Singapore,\n               Singapore, May 9, 2016, COIN@ECAI, The Hague, The Netherlands, August\n               30, 2016, Revised Selected Papers},\n  pages     = {42--59},\n  year      = {2016},\n  crossref  = {DBLP:conf/atal/2016coin},\n  url       = {https://doi.org/10.1007/978-3-319-66595-5\\_3},\n  doi       = {10.1007/978-3-319-66595-5\\_3},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/atal/DennisSF16},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Agent-Based Autonomous Systems and Abstraction Engines: Theory Meets Practice.\n \n \n \n \n\n\n \n Dennis, L. A.; Aitken, J. M.; Collenette, J.; Cucco, E.; Kamali, M.; McAree, O.; Shaukat, A.; Atkinson, K.; Gao, Y.; Veres, S. M.; and Fisher, M.\n\n\n \n\n\n\n In Towards Autonomous Robotic Systems - 17th Annual Conference, TAROS 2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings, pages 75–86, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"Agent-BasedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/taros/DennisACCKMSAGV16,\n  author    = {Louise A. Dennis and\n               Jonathan M. Aitken and\n               Joe Collenette and\n               Elisa Cucco and\n               Maryam Kamali and\n               Owen McAree and\n               Affan Shaukat and\n               Katie Atkinson and\n               Yang Gao and\n               Sandor M. Veres and\n               Michael Fisher},\n  title     = {Agent-Based Autonomous Systems and Abstraction Engines: Theory Meets\n               Practice},\n  booktitle = {Towards Autonomous Robotic Systems - 17th Annual Conference, {TAROS}\n               2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings},\n  pages     = {75--86},\n  year      = {2016},\n  crossref  = {DBLP:conf/taros/2016},\n  url       = {https://doi.org/10.1007/978-3-319-40379-3\\_8},\n  doi       = {10.1007/978-3-319-40379-3\\_8},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/taros/DennisACCKMSAGV16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Verification of Autonomous Vehicle Platooning.\n \n \n \n \n\n\n \n Kamali, M.; Dennis, L. A.; McAree, O.; Fisher, M.; and Veres, S. M.\n\n\n \n\n\n\n CoRR, abs/1602.01718. 2016.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/KamaliDMFV16,\n  author    = {Maryam Kamali and\n               Louise A. Dennis and\n               Owen McAree and\n               Michael Fisher and\n               Sandor M. Veres},\n  title     = {Formal Verification of Autonomous Vehicle Platooning},\n  journal   = {CoRR},\n  volume    = {abs/1602.01718},\n  year      = {2016},\n  url       = {http://arxiv.org/abs/1602.01718},\n  archivePrefix = {arXiv},\n  eprint    = {1602.01718},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/KamaliDMFV16},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Engineering Moral Agents - from Human Morality to Artificial Morality (Dagstuhl Seminar 16222).\n \n \n \n \n\n\n \n Fisher, M.; List, C.; Slavkovik, M.; and Winfield, A. F. T.\n\n\n \n\n\n\n Dagstuhl Reports, 6(5): 114–137. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"EngineeringPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/dagstuhl-reports/FisherLSW16,\n  author    = {Michael Fisher and\n               Christian List and\n               Marija Slavkovik and\n               Alan F. T. Winfield},\n  title     = {Engineering Moral Agents - from Human Morality to Artificial Morality\n               (Dagstuhl Seminar 16222)},\n  journal   = {Dagstuhl Reports},\n  volume    = {6},\n  number    = {5},\n  pages     = {114--137},\n  year      = {2016},\n  url       = {https://doi.org/10.4230/DagRep.6.5.114},\n  doi       = {10.4230/DagRep.6.5.114},\n  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/dagstuhl-reports/FisherLSW16},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Predicting \"springback\" using 3D surface representation techniques: A case study in sheet metal forming.\n \n \n \n \n\n\n \n El-Salhi, S.; Coenen, F.; Dixon, C.; and Khan, M. S.\n\n\n \n\n\n\n Expert Syst. Appl., 42(1): 79–93. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"PredictingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/eswa/El-SalhiCDK15,\n  author    = {Subhieh El{-}Salhi and\n               Frans Coenen and\n               Clare Dixon and\n               M. Sulaiman Khan},\n  title     = {Predicting "springback" using 3D surface representation techniques:\n               {A} case study in sheet metal forming},\n  journal   = {Expert Syst. Appl.},\n  volume    = {42},\n  number    = {1},\n  pages     = {79--93},\n  year      = {2015},\n  url       = {https://doi.org/10.1016/j.eswa.2014.07.041},\n  doi       = {10.1016/j.eswa.2014.07.041},\n  timestamp = {Fri, 26 May 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/eswa/El-SalhiCDK15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Ordered Resolution for Coalition Logic.\n \n \n \n \n\n\n \n Hustadt, U.; Gainer, P.; Dixon, C.; Nalon, C.; and Zhang, L.\n\n\n \n\n\n\n In Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21-24, 2015. Proceedings, pages 169–184, 2015. \n \n\n\n\n
\n\n\n\n \n \n \"OrderedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/tableaux/HustadtGDNZ15,\n  author    = {Ullrich Hustadt and\n               Paul Gainer and\n               Clare Dixon and\n               Cl{\\'{a}}udia Nalon and\n               Lan Zhang},\n  title     = {Ordered Resolution for Coalition Logic},\n  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th\n               International Conference, {TABLEAUX} 2015, Wroc{\\l}aw, Poland, September\n               21-24, 2015. Proceedings},\n  pages     = {169--184},\n  year      = {2015},\n  crossref  = {DBLP:conf/tableaux/2015},\n  url       = {https://doi.org/10.1007/978-3-319-24312-2\\_12},\n  doi       = {10.1007/978-3-319-24312-2\\_12},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/tableaux/HustadtGDNZ15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Modal-Layered Resolution Calculus for K.\n \n \n \n \n\n\n \n Nalon, C.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n In Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21-24, 2015. Proceedings, pages 185–200, 2015. \n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/tableaux/NalonHD15,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Ullrich Hustadt and\n               Clare Dixon},\n  title     = {A Modal-Layered Resolution Calculus for {K}},\n  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th\n               International Conference, {TABLEAUX} 2015, Wroc{\\l}aw, Poland, September\n               21-24, 2015. Proceedings},\n  pages     = {185--200},\n  year      = {2015},\n  crossref  = {DBLP:conf/tableaux/2015},\n  url       = {https://doi.org/10.1007/978-3-319-24312-2\\_13},\n  doi       = {10.1007/978-3-319-24312-2\\_13},\n  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/tableaux/NalonHD15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards Autonomous Robotic Systems - 16th Annual Conference, TAROS 2015, Liverpool, UK, September 8-10, 2015, Proceedings.\n \n \n \n \n\n\n \n Dixon, C.; and Tuyls, K.,\n editors.\n \n\n\n \n\n\n\n Volume 9287, of Lecture Notes in Computer Science.Springer. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@proceedings{DBLP:conf/taros/2015,\n  editor    = {Clare Dixon and\n               Karl Tuyls},\n  title     = {Towards Autonomous Robotic Systems - 16th Annual Conference, {TAROS}\n               2015, Liverpool, UK, September 8-10, 2015, Proceedings},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {9287},\n  publisher = {Springer},\n  year      = {2015},\n  url       = {https://doi.org/10.1007/978-3-319-22416-9},\n  doi       = {10.1007/978-3-319-22416-9},\n  isbn      = {978-3-319-22415-2},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/taros/2015},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An abstract formal basis for digital crowds.\n \n \n \n \n\n\n \n Slavkovik, M.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n Distributed and Parallel Databases, 33(1): 3–31. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/dpd/SlavkovikDF15,\n  author    = {Marija Slavkovik and\n               Louise A. Dennis and\n               Michael Fisher},\n  title     = {An abstract formal basis for digital crowds},\n  journal   = {Distributed and Parallel Databases},\n  volume    = {33},\n  number    = {1},\n  pages     = {3--31},\n  year      = {2015},\n  url       = {https://doi.org/10.1007/s10619-014-7161-y},\n  doi       = {10.1007/s10619-014-7161-y},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/dpd/SlavkovikDF15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards Verifiably Ethical Robot Behaviour.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; and Winfield, A. F. T.\n\n\n \n\n\n\n In Artificial Intelligence and Ethics, Papers from the 2015 AAAI Workshop, Austin, Texas, USA, January 25, 2015., 2015. \n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/aaai/DennisFW15,\n  author    = {Louise Abigail Dennis and\n               Michael Fisher and\n               Alan F. T. Winfield},\n  title     = {Towards Verifiably Ethical Robot Behaviour},\n  booktitle = {Artificial Intelligence and Ethics, Papers from the 2015 {AAAI} Workshop,\n               Austin, Texas, USA, January 25, 2015.},\n  year      = {2015},\n  crossref  = {DBLP:conf/aaai/2015ethics},\n  url       = {http://aaai.org/ocs/index.php/WS/AAAIW15/paper/view/10119},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/aaai/DennisFW15},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Semantic Framework for Socially Adaptive Agents: Towards strong norm compliance.\n \n \n \n \n\n\n \n van Riemsdijk, M. B.; Dennis, L. A.; Fisher, M.; and Hindriks, K. V.\n\n\n \n\n\n\n In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015, pages 423–432, 2015. \n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/atal/RiemsdijkDFH15,\n  author    = {M. Birna van Riemsdijk and\n               Louise A. Dennis and\n               Michael Fisher and\n               Koen V. Hindriks},\n  title     = {A Semantic Framework for Socially Adaptive Agents: Towards strong\n               norm compliance},\n  booktitle = {Proceedings of the 2015 International Conference on Autonomous Agents\n               and Multiagent Systems, {AAMAS} 2015, Istanbul, Turkey, May 4-8, 2015},\n  pages     = {423--432},\n  year      = {2015},\n  crossref  = {DBLP:conf/atal/2015},\n  url       = {http://dl.acm.org/citation.cfm?id=2772935},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/atal/RiemsdijkDFH15},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards Verifiably Ethical Robot Behaviour.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; and Winfield, A. F. T.\n\n\n \n\n\n\n CoRR, abs/1504.03592. 2015.\n [Verifiable Autonomy]\n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/DennisFW15,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Alan F. T. Winfield},\n  title     = {Towards Verifiably Ethical Robot Behaviour},\n  journal   = {CoRR},\n  volume    = {abs/1504.03592},\n  year      = {2015},\n  url       = {http://arxiv.org/abs/1504.03592},\n  archivePrefix = {arXiv},\n  eprint    = {1504.03592},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/DennisFW15},\n  bibsource = {dblp computer science bibliography, https://dblp.org},\n  note = {[<span class="va">Verifiable Autonomy</span>]}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A roadmap to pervasive systems verification.\n \n \n \n \n\n\n \n Konur, S.; and Fisher, M.\n\n\n \n\n\n\n Knowledge Eng. Review, 30(3): 324–341. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/ker/KonurF15,\n  author    = {Savas Konur and\n               Michael Fisher},\n  title     = {A roadmap to pervasive systems verification},\n  journal   = {Knowledge Eng. Review},\n  volume    = {30},\n  number    = {3},\n  pages     = {324--341},\n  year      = {2015},\n  url       = {https://doi.org/10.1017/S0269888914000228},\n  doi       = {10.1017/S0269888914000228},\n  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/ker/KonurF15},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (14)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A resolution-based calculus for Coalition Logic.\n \n \n \n \n\n\n \n Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U.\n\n\n \n\n\n\n J. Log. Comput., 24(4): 883–917. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/logcom/NalonZDH14,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Lan Zhang and\n               Clare Dixon and\n               Ullrich Hustadt},\n  title     = {A resolution-based calculus for Coalition Logic},\n  journal   = {J. Log. Comput.},\n  volume    = {24},\n  number    = {4},\n  pages     = {883--917},\n  year      = {2014},\n  url       = {https://doi.org/10.1093/logcom/ext074},\n  doi       = {10.1093/logcom/ext074},\n  timestamp = {Wed, 17 May 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/logcom/NalonZDH14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A resolution calculus for the branching-time temporal logic CTL.\n \n \n \n \n\n\n \n Zhang, L.; Hustadt, U.; and Dixon, C.\n\n\n \n\n\n\n ACM Trans. Comput. Log., 15(1): 10:1–10:38. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/tocl/ZhangHD14,\n  author    = {Lan Zhang and\n               Ullrich Hustadt and\n               Clare Dixon},\n  title     = {A resolution calculus for the branching-time temporal logic {CTL}},\n  journal   = {{ACM} Trans. Comput. Log.},\n  volume    = {15},\n  number    = {1},\n  pages     = {10:1--10:38},\n  year      = {2014},\n  url       = {https://doi.org/10.1145/2529993},\n  doi       = {10.1145/2529993},\n  timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/tocl/ZhangHD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Verification of an Autonomous Personal Robotic Assistant.\n \n \n \n \n\n\n \n Webster, M.; Dixon, C.; Fisher, M.; Salem, M.; Saunders, J.; Koay, K. L.; and Dautenhahn, K.\n\n\n \n\n\n\n In 2014 AAAI Spring Symposia, Stanford University, Palo Alto, California, USA, March 24-26, 2014, 2014. \n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/aaaiss/WebsterD0SSKD14,\n  author    = {Matt Webster and\n               Clare Dixon and\n               Michael Fisher and\n               Maha Salem and\n               Joe Saunders and\n               Kheng Lee Koay and\n               Kerstin Dautenhahn},\n  title     = {Formal Verification of an Autonomous Personal Robotic Assistant},\n  booktitle = {2014 {AAAI} Spring Symposia, Stanford University, Palo Alto, California,\n               USA, March 24-26, 2014},\n  year      = {2014},\n  crossref  = {DBLP:conf/aaaiss/2014},\n  url       = {http://www.aaai.org/ocs/index.php/SSS/SSS14/paper/view/7734},\n  timestamp = {Wed, 14 Nov 2018 14:23:12 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/aaaiss/WebsterD0SSKD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Clausal Resolution for Modal Logics of Confluence.\n \n \n \n \n\n\n \n Nalon, C.; Marcos, J.; and Dixon, C.\n\n\n \n\n\n\n In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, pages 322–336, 2014. \n \n\n\n\n
\n\n\n\n \n \n \"ClausalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/cade/NalonMD14,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Jo{\\~{a}}o Marcos and\n               Clare Dixon},\n  title     = {Clausal Resolution for Modal Logics of Confluence},\n  booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR}\n               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,\n               Austria, July 19-22, 2014. Proceedings},\n  pages     = {322--336},\n  year      = {2014},\n  crossref  = {DBLP:conf/cade/2014},\n  url       = {https://doi.org/10.1007/978-3-319-08587-6\\_24},\n  doi       = {10.1007/978-3-319-08587-6\\_24},\n  timestamp = {Sun, 21 May 2017 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/conf/cade/NalonMD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n \"The Fridge Door is Open\"-Temporal Verification of a Robotic Assistant's Behaviours.\n \n \n \n \n\n\n \n Dixon, C.; Webster, M. P.; Saunders, J.; Fisher, M.; and Dautenhahn, K.\n\n\n \n\n\n\n In Advances in Autonomous Robotics Systems - 15th Annual Conference, TAROS 2014, Birmingham, UK, September 1-3, 2014. Proceedings, pages 97–108, 2014. \n \n\n\n\n
\n\n\n\n \n \n \""ThePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/taros/DixonWSFD14,\n  author    = {Clare Dixon and\n               Matthew P. Webster and\n               Joe Saunders and\n               Michael Fisher and\n               Kerstin Dautenhahn},\n  title     = {"The Fridge Door is Open"-Temporal Verification of a Robotic Assistant's\n               Behaviours},\n  booktitle = {Advances in Autonomous Robotics Systems - 15th Annual Conference,\n               {TAROS} 2014, Birmingham, UK, September 1-3, 2014. Proceedings},\n  pages     = {97--108},\n  year      = {2014},\n  crossref  = {DBLP:conf/taros/2014},\n  url       = {https://doi.org/10.1007/978-3-319-10401-0\\_9},\n  doi       = {10.1007/978-3-319-10401-0\\_9},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/taros/DixonWSFD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Resolution Prover for Coalition Logic.\n \n \n \n \n\n\n \n Nalon, C.; Zhang, L.; Dixon, C.; and Hustadt, U.\n\n\n \n\n\n\n In Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014., pages 65–73, 2014. \n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:journals/corr/NalonZDH14,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Lan Zhang and\n               Clare Dixon and\n               Ullrich Hustadt},\n  title     = {A Resolution Prover for Coalition Logic},\n  booktitle = {Proceedings 2nd International Workshop on Strategic Reasoning, {SR}\n               2014, Grenoble, France, April 5-6, 2014.},\n  pages     = {65--73},\n  year      = {2014},\n  crossref  = {DBLP:journals/corr/MogaveroMV14},\n  url       = {https://doi.org/10.4204/EPTCS.146.9},\n  doi       = {10.4204/EPTCS.146.9},\n  timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/NalonZDH14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On and On the Temporal Way.\n \n \n \n \n\n\n \n Dixon, C.; and Fisher, M.\n\n\n \n\n\n\n In HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, pages 85–111. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{DBLP:conf/birthday/DixonF14,\n  author    = {Clare Dixon and\n               Michael Fisher},\n  title     = {On and On the Temporal Way},\n  booktitle = {{HOWARD-60:} {A} Festschrift on the Occasion of Howard Barringer's\n               60th Birthday},\n  pages     = {85--111},\n  year      = {2014},\n  crossref  = {DBLP:conf/birthday/2014howard},\n  url       = {http://www.easychair.org/publications/?page=2015413951},\n  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/birthday/DixonF14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Clausal Resolution for Modal Logics of Confluence.\n \n \n \n \n\n\n \n Nalon, C.; Marcos, J.; and Dixon, C.\n\n\n \n\n\n\n CoRR, abs/1405.0293. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"ClausalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/NalonMD14,\n  author    = {Cl{\\'{a}}udia Nalon and\n               Jo{\\~{a}}o Marcos and\n               Clare Dixon},\n  title     = {Clausal Resolution for Modal Logics of Confluence},\n  journal   = {CoRR},\n  volume    = {abs/1405.0293},\n  year      = {2014},\n  url       = {http://arxiv.org/abs/1405.0293},\n  archivePrefix = {arXiv},\n  eprint    = {1405.0293},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/NalonMD14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Reconfigurable Autonomy.\n \n \n \n \n\n\n \n Dennis, L. A.; Fisher, M.; Aitken, J. M.; Veres, S. M.; Gao, Y.; Shaukat, A.; and Burroughes, G.\n\n\n \n\n\n\n KI, 28(3): 199–207. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"ReconfigurablePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/ki/DennisFAVGSB14,\n  author    = {Louise A. Dennis and\n               Michael Fisher and\n               Jonathan M. Aitken and\n               Sandor M. Veres and\n               Yang Gao and\n               Affan Shaukat and\n               Guy Burroughes},\n  title     = {Reconfigurable Autonomy},\n  journal   = {{KI}},\n  volume    = {28},\n  number    = {3},\n  pages     = {199--207},\n  year      = {2014},\n  url       = {https://doi.org/10.1007/s13218-014-0308-1},\n  doi       = {10.1007/s13218-014-0308-1},\n  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/ki/DennisFAVGSB14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Actions with Durations and Failures in BDI Languages.\n \n \n \n \n\n\n \n Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n In ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014), pages 995–996, 2014. \n \n\n\n\n
\n\n\n\n \n \n \"ActionsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ecai/DennisF14,\n  author    = {Louise A. Dennis and\n               Michael Fisher},\n  title     = {Actions with Durations and Failures in {BDI} Languages},\n  booktitle = {{ECAI} 2014 - 21st European Conference on Artificial Intelligence,\n               18-22 August 2014, Prague, Czech Republic - Including Prestigious\n               Applications of Intelligent Systems {(PAIS} 2014)},\n  pages     = {995--996},\n  year      = {2014},\n  crossref  = {DBLP:conf/ecai/2014},\n  url       = {https://doi.org/10.3233/978-1-61499-419-0-995},\n  doi       = {10.3233/978-1-61499-419-0-995},\n  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/ecai/DennisF14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An Abstract Formal Basis for Digital Crowds.\n \n \n \n \n\n\n \n Slavkovik, M.; Dennis, L. A.; and Fisher, M.\n\n\n \n\n\n\n CoRR, abs/1408.1592. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/SlavkovikDF14,\n  author    = {Marija Slavkovik and\n               Louise A. Dennis and\n               Michael Fisher},\n  title     = {An Abstract Formal Basis for Digital Crowds},\n  journal   = {CoRR},\n  volume    = {abs/1408.1592},\n  year      = {2014},\n  url       = {http://arxiv.org/abs/1408.1592},\n  archivePrefix = {arXiv},\n  eprint    = {1408.1592},\n  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},\n  biburl    = {https://dblp.org/rec/bib/journals/corr/SlavkovikDF14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal verification of a pervasive messaging system.\n \n \n \n \n\n\n \n Konur, S.; Fisher, M.; Dobson, S.; and Knox, S.\n\n\n \n\n\n\n Formal Asp. Comput., 26(4): 677–694. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/fac/KonurFDK14,\n  author    = {Savas Konur and\n               Michael Fisher and\n               Simon Dobson and\n               Stephen Knox},\n  title     = {Formal verification of a pervasive messaging system},\n  journal   = {Formal Asp. Comput.},\n  volume    = {26},\n  number    = {4},\n  pages     = {677--694},\n  year      = {2014},\n  url       = {https://doi.org/10.1007/s00165-013-0277-4},\n  doi       = {10.1007/s00165-013-0277-4},\n  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/fac/KonurFDK14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation.\n \n \n \n \n\n\n \n Webster, M. P.; Cameron, N.; Fisher, M.; and Jump, M.\n\n\n \n\n\n\n J. Aerospace Inf. Sys., 11(5): 258–279. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"GeneratingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/jacic/WebsterCFJ14,\n  author    = {Matthew P. Webster and\n               Neil Cameron and\n               Michael Fisher and\n               Mike Jump},\n  title     = {Generating Certification Evidence for Autonomous Unmanned Aircraft\n               Using Model Checking and Simulation},\n  journal   = {J. Aerospace Inf. Sys.},\n  volume    = {11},\n  number    = {5},\n  pages     = {258--279},\n  year      = {2014},\n  url       = {https://doi.org/10.2514/1.I010096},\n  doi       = {10.2514/1.I010096},\n  timestamp = {Fri, 02 Nov 2018 09:33:11 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/jacic/WebsterCFJ14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Preface to the Special Issue on Computational Logic in Multi-Agent Systems (CLIMA XIII).\n \n \n \n \n\n\n \n Fisher, M.; van der Torre, L. W. N.; Dastani, M.; and Governatori, G.\n\n\n \n\n\n\n J. Log. Comput., 24(6): 1251–1252. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"PrefacePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/logcom/FisherTDG14,\n  author    = {Michael Fisher and\n               Leendert W. N. van der Torre and\n               Mehdi Dastani and\n               Guido Governatori},\n  title     = {Preface to the Special Issue on Computational Logic in Multi-Agent\n               Systems {(CLIMA} {XIII)}},\n  journal   = {J. Log. Comput.},\n  volume    = {24},\n  number    = {6},\n  pages     = {1251--1252},\n  year      = {2014},\n  url       = {https://doi.org/10.1093/logcom/ext075},\n  doi       = {10.1093/logcom/ext075},\n  timestamp = {Wed, 14 Nov 2018 10:17:07 +0100},\n  biburl    = {https://dblp.org/rec/bib/journals/logcom/FisherTDG14},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);