purplecat: Hand Drawn picture of a Toy Cat (Default)
Model-Checking for Analysis of Information Leakage in Social Networks has been accepted into the post-proceedings volume of the conference it was given at. The acceptance is notable, in particular, for the referees' comments which amount in all cases to "have dealt with previous comments more than sufficiently, nothing more to do" which is good in the light of how much time I don't have between now and the camera ready deadline.
purplecat: (academia)

We are pleased to inform you that your paper

"How Did They Know?" - Model-Checking for Analysis of Information Leakage in Social Networks

has been accepted for presentation at COIN@ECAI.


Matryoshka, the Boss, and I cooked up the idea for this paper while at Dagstuhl based, more or less, on the fact that I was going to be going to ECAI (European Conference on Artificial Intelligence) anyway (for an IEEE meeting on Robot Ethics) and so thought I would also attend the associated COIN workshop (which is about organisations of software agents). All that being the case it seemed a shame not to submit something to the workshop. We therefore took some previous work of ours on modelling groups of agents as further agents which we had applied to Digital Crowds, and Matryoshka's interest in "fixing the Internet", dumped it in a probabilistic model-checker and came up with some numbers for how likely messages were to reach unwanted parties via forwarding through social networks.

It needs a lot of further work, but it feels like it has some potential and the referees seem to have felt so too. In fact I'm not sure I've ever seen such unanimity towards "accept" among a set of reviews.
purplecat: (lego robots)
We are pleased to confirm that your paper:

Agent-based Autonomous Systems and Abstraction Engines: Theory meets Practice

has been accepted as a full paper at TAROS 2016, the 17th Towards Autonomous Robotic Systems conference.


This paper is more a set of system descriptions covering work on autonomous robot arms (done as part of the Reconfigurable Autonomy project I was working on until a couple of years ago), work on autonomous vehicle platoons (done as part of the Verifiable Autonomy project I'm currently working on) and the Lego Rovers work - and noting some incremental changes the practice of building these systems has had on the theory behind them.

However since we spend quite a lot of time system/demo building and they are really hard to write up and get published I'm quite pleased to get this published, even as a minor conference paper. It also helps maintain the link to research in the Lego Rovers work which I think is good in principle, and will help with any putative impact case.
purplecat: Hand Drawn picture of a Toy Cat (Default)
From an email received by Matryoshka who has been masterminding everything:

I am pleased to confirm that your paper "Formal Verification of Ethical Choices in Autonomous Systems" has been accepted for publication in Robotics and Autonomous Systems.

This was originally a journal special issue version of our 2013 TAROS paper: Ethical Choice in Unforeseen Circumstances, but via a long and tortuous story its become more of a standalone extension of the work in its own right.
purplecat: Hand Drawn picture of a Toy Cat (agents)
A slightly delayed announcement because the referee's comments required a lot of work, but this will be in AAMAS 2015 (Autonomous Agents and Multi-agent systems). It's a follow up to our 2013 paper Agent Reasoning for Norm Compliance: A Semantic Approach. Once again Birna took the lead, but I helped with a lot of the proofs and we did most of the work while she was on a two week visit to Liverpool in the Autumn.

In our last paper we allowed an agent to comply with a set of social (or other) norms by simply doing nothing. In this paper we tackle situations where "doing nothing" isn't actually appropriate. The up shot is that we can't guarantee than some agent can obey all social norms, but we do manage to define some norm set that any agent should be able to follow.
purplecat: Hand Drawn picture of a Toy Cat (agents)

I am pleased to inform you that your paper:

Towards Verifiably Ethical Robot Behaviour:

Has been accepted to be presented as a talk at the AAAI-15 workshop
on AI and Ethics.

We had a large number of submissions and the acceptance rate was
under 40%.


Nicely high level comments in the review as well which should be fairly easy to incorporate into the paper.

This is our attempt (together with Alan Winfield) to convert the work he describes here into a form were we can prove stuff about it. In short the previous work developed a framework that could integrate with whatever mechanism a robot was using to decide what to do and filter options down to those that were "most ethical" - the example used was a robot that normally would not collide with humans but, in the event that a human was about to walk into a hole in the ground, the robot would collide with the human in order to prevent them doing so. We converted this into a framework where we could prove that it was doing the filtering correctly in a very abstract description of the scenario and also generate some probabilistic results about likely outcomes in more concrete versions of the scenario.

We're also experimenting with something called Open Notebook Science and so have an Open Notebook for the work in the paper - I personally think the notebook is very dull but then the point isn't to be interesting so much as transparent.
purplecat: (academia)

we are pleased to inform you that your manuscript:

Two-Stage Agent Program Verification

has been accepted to the CLIMA XIV Special Issue on the Journal of Logic and Computation, subject to minor revision.


This is an updated version of Using Agent JPF to Build Models for Other Model Checkers and I'm really pleased its been accepted for the Journal special issue since I didn't really have aspirations for it beyond the workshop.
purplecat: (academia)
We have received the reports from our advisors on your manuscript, "A Formal Basis for Digital Crowds", which you submitted to Distributed and Parallel Databases.

Based on the advice received, the Editor feels that your manuscript could be accepted for publication should you be prepared to incorporate minor revisions.


As one of my co-authors notes, having read the reviews, "We have until july 31st to get proficient at the last 15 years in communication protocols"
purplecat: Hand Drawn picture of a Toy Cat (Default)
I am pleased to inform you that your paper

Title: Actions with Durations and Failures in BDI Languages

has been accepted for poster presentation at ECAI'14 and a two-page publication
in its proceedings.


I actually received this notification a while back but I was sulking about the "two-page publication" part, wrestling with the childcare issues attending the conference was going to raise and generally not feeling particularly celebratory about it. However the original 8 pages have been brutally hacked down to 2, though I personally think it will be be a bit of a miracle if they are comprehensible to someone in that form and the original 8 have been issued instead as a University technical report so if anyone really wants to know what we were on about they can find out.

One of the reasons we went the technical report route was I realised while I was hacking how much I dislike discovering a reference is actually two page short paper from ECAI (European Conference on Artificial Intelligence) or IJCAI (International Joint Conference on Artificial Intelligence) because at that length the content is generally high-level hand waving or densely technical with no context or motivation. As a result of the compromise between my boss and I about what should go in our 2 page version, I have high hopes it manages to combine both high-level hand waving (boss's preference) and poorly motivated densely technical stuff (my preference).

For those actually interested in the content, we realised that sometimes doing stuff (e.g., moving from point A to point B) takes time, and sometimes it goes wrong while you are doing it, and that the existing rational agent programming languages didn't handle this very well. So we outlined in a general way how it should be handled. One of the referees thought it was an interesting problem but our solution was "a bit trivial". I resisted the temptation to write "well of course the solution looks obvious now" in my author's response.
purplecat: (academia)
We have received the reports from our advisors on your manuscript, "Practical Verification of Decision-Making in Agent-Based Autonomous Systems", which you submitted to Automated Software Engineering.

Based on the advice received, your manuscript could be accepted for publication should you be prepared to incorporate minor revisions.


This paper hasn't quite had the legs of the albatross paper (actually it hasn't even come close to being the burden the albatross paper was), but it has certainly done the rounds involving major rewrites and considerable extra implementation effort. Bits of it have also ended up in other publications (most notably the Communications of the ACM article) and that's always a bit worrying. I didn't want to end up in a situation where the actual nitty-gritty technical detail was rendered unpublishable because the high-level view had appeared elsewhere. One of the referees even flags this up and has asked for some clarifications about what has appeared elsewhere, but thankfully agrees there is sufficient novel work left to make it publishable.
purplecat: Hand Drawn picture of a Toy Cat (agents)
I was going to start this post with the words "It is very strangeā€¦" but I suspect in the modern age it isn't strange at all, it merely hasn't happened to me before.

At any rate, when I woke up this morning it was to find I had been tweeted (or, at least, mentioned in a tweet)1 by a complete stranger. This alerted me to the fact I had an article in a magazine - Space Safety Magazine in fact2.

To be fair, I did know there was going to be an article in Space Safety Magazine. I even wrote it. I just wasn't really aware that it was imminently due to appear.

Here it is - it appears to be publicly available and is aimed at a more or less general audience: Safe Autonomous Space Software.

1. I'm sorry, I really haven't grasped twitter. I think I was just mentioned, but maybe he was tweeting at me.

2. No, this is really a thing, and presumably not just invented for the opportunity to appear as a guest publication on Have I Got News For You.
purplecat: Hand Drawn picture of a Toy Cat (Default)
It turns out that our Communications of the ACM article is available open access - I have no recollection whether this is journal policy, we paid for it to be open access, or it's just open access for a while. However if you're interested in reading one of my papers which aims to be at least a little accessible (aimed at computery folk rather than computational logicians specifically, for instance) then this is probably your opportunity.
purplecat: Hand Drawn picture of a Toy Cat (Default)
Thank you very much for submitting a paper to CLIMA XIV. We are delighted to let
you know that your paper "Using Agent JPF to Build Models for Other Model Checkers" is accepted for presentation and inclusion in the Springer LNAI Proceedings.


Yay! That is my fifth paper acceptance this year which considering the publication deserts that were 2012 and 2011 is a welcome relief.

Agent JPF is a model checking tool for so called rational agent programming languages that I built on top of NASA's Java Pathfinder as part of the project before last. I've been tweaking it ever since and grappling slightly with the fact that, out of the box, JPF only checks there are no deadlocks or exceptions in a Java program where most model checkers have fairly sophisticated languages for describing properties based on temporal logics.

Hunter et al. recently published an interesting paper in which they used JPF to create a model of an agent program written in the Brahms language (which is a human-agent interaction modelling language used by NASA) but then shipped the model off to the Spin model checker for actual verification. I knew about this work in advance since they worked with my (very nearly almost graduated) PhD student and he brought one of the authors, Franco Raimondi up to Liverpool to give a talk, and then I picked his brains about how it all worked. At some point during the conversation I had one of those why didn't I think of this? moments because it is a very elegant and simple idea and I was within a hair's breadth of implementing it myself - I just hadn't realised the fact.

So I quickly adapted AJPF to do the same. Outputting models to Spin proved to be a doddle, but I was really interested in outputting stuff to a model checker called PRISM which can verify probabilistic properties - e.g., "if the aircraft's sensors are correct 90% of a time and the risk of an aircraft appearing on a collision course is 10% then the chance that the aircraft collides with another is less than 1%" because I really didn't want to implement algorithms for reasoning about probabilities over Java programs.

It was all implemented and written up in something of a rush, so I'm pleased it got accepted, though slightly alarmed by the fact that all the reviewers have commented on how well written the paper is. Maybe I should write more papers in a frantic hurry!
purplecat: Hand Drawn picture of a Toy Cat (agents)
We have now received the review reports on your paper entitled "Autonomous Asteroid Exploration[Improvements of Agent Based Control for Autonomous Spacecraft in Complex Environments]" submitted to the IEEE CIM Special Issue on Intelligent Space Systems and Operations. I am pleased to inform you that your paper has been CONDITIONALLY ACCEPTED subject to minor revisions in response to the editor/reviewers' comments (attached at the back of this email).


This is one of two journal papers planned from the Engineering Autonomous Space Software project. It's basically the engineering paper - describing what the project achieved from the engineering perspective and focusing on an asteroid exploration case study. The Computer Science paper which is intended to focus on verification is... umm... in small pieces all over my hard drive having been rejected by both JAIR (Journal of Artificial Intelligence Research) and AIJ (Artificial Intelligence Journal) and pending updated results and possibly a new case study based on autonomous cruise control in cars.
purplecat: (academia)
It is my pleasure to inform you that the contribution referenced above, for which you are listed as the corresponding author, has been accepted for publication in the Proceedings of the 14th Towards Autonomous Robotic Systems (TAROS 2013) In Springer Lecture Notes in Artificial Intelligence series.

Matryoshka has been working with our group for the past year on a variety of topics including ethical reasoning. She did most of the theory for this paper while I did the implementation. The basic idea is to provide constraints on agent decision-making in a situation where no pre-existing behaviours are available. In this situation an agent can call a planning system but we wanted to reject plans that were `unethical' or at least select the most ethical choice - e.g., if an unmanned aircraft is about to crash we want it to, where possible, select the crash site that will minimize the loss of life.

We cunningly bypass a couple of millennia of philosophical debate by assuming someone has already come up with a functioning ethical framework and we merely consider how an agent can make sure its choices comply with the framework.

We have a follow up paper planned, which reminds me that I'm supposed to be reading the draft and deciding if it is implementable.
purplecat: Hand Drawn picture of a Toy Cat (Default)

It is a pleasure to accept your manuscript entitled "Verifying Autonomous Systems" in its current form for publication in Communications of the ACM. The comments of the reviewer(s) who reviewed your manuscript are included at the foot of this letter.

Thank you for your fine contribution. On behalf of the Editors of the Communications of the ACM, we look forward to your continued contributions to the magazine. You will hear from us in a few months, when the paper is slated for production.


Communications of the ACM is a magazine style publication, rather than an academic journal though our paper was still peer reviewed. However it was written more as an overview/survey style paper describing our approach to the verification of autonomous systems. In it my boss basically pulled together a description of the verification work we did during the Engineering Autonomous Space Systems project and another project he had running on the Certification of Unmanned Aerial Vehicles. It's a three author paper by my boss, myself and the RA on the UAV project.

I'm really pleased to have had two paper acceptances in such a short space of time. I didn't get any papers published in 2012 and the papers I published in 2011 were mostly "legacy" papers from previous project rather than current work. Mind you when I expressed concern about this in my PDR, my boss just teased me gently and pointed out that I preferred the programming aspect of my job to churning out papers just because. He also said he wasn't worried about it and observed that we had a lot of papers submitted or in preparation at the time and so things were likely to pick up. It looks like he was right.
purplecat: Hand Drawn picture of a Toy Cat (Default)

We are pleased to inform you that your paper #671
Title: Agent Reasoning for Norm Compliance: A Semantic Approach
has been accepted for full publication and oral presentation in the proceedings of the Twelfth International Conference on Autonomous Agents and Multiagent Systems (AAMAS2013).





Explanation under the Cut )
purplecat: Hand Drawn picture of a Toy Cat (Default)
We are pleased to inform you that your paper

24 : Verification of Brahms Human-Robot Teamwork Models

has been accepted for presentation and publication in the proceedings of the 13th European Conference on Logics in Artificial Intelligence JELIA 2012. Congratulations!


This is another paper primarily by my PhD student and is mostly about how we verified some simple examples of an "intelligent house" system that is supposed to assist a confused elderly person living on their own. The actual example is just a simple case study, most of the work has been the infrastructure to allow programs in the Brahms language (which is designed to simulate examples of humans and robots working together) to actually be verified.
purplecat: (academia)
It is our pleasure to inform you that your abstract entitled "Agent
Control of Cooperating Satellites" submitted to the AI in Space:
Intelligence beyond planet earth, has been accepted for an oral
presentation.


The exciting thing about this paper is that we only had to submit an abstract, but are now required to produce a full paper by the 1st July - I forsee much frantic scribbling in the next month or so. The paper describes the current case study we are working on which is the exploration of asteroid clusters using multiple satellites.

Thank you very much for submitting a paper to CLIMA XII. We are delighted to let
you know that your paper is accepted for presentation and inclusion in the
Springer LNAI Proceedings.


This paper is "A Formal Semantics for Brahms" and is really the baby of my PhD Student (using the phrase "my PhD Student" here to refer to someone for whom I'm tenuously 3rd supervisor in a vague "the university admin can't cope with RA's supervising PhD students" kind of way). I did do a little polishing on the paper so I'm not too embarrased by the author credit. Brahms is an agent programming language used by NASA to model human-robot interaction. We want to do some model checking (verification) of these models but that means we needed a semantics for the language first which said PhD student had been diligently working on for about a year now.

This entry was originally posted at http://purplecat.dreamwidth.org/41470.html.
purplecat: (academia)
It is our pleasure to inform you that your abstract entitled "Agent
Control of Cooperating Satellites" submitted to the AI in Space:
Intelligence beyond planet earth, has been accepted for an oral
presentation.


The exciting thing about this paper is that we only had to submit an abstract, but are now required to produce a full paper by the 1st July - I forsee much frantic scribbling in the next month or so. The paper describes the current case study we are working on which is the exploration of asteroid clusters using multiple satellites.

Thank you very much for submitting a paper to CLIMA XII. We are delighted to let
you know that your paper is accepted for presentation and inclusion in the
Springer LNAI Proceedings.


This paper is "A Formal Semantics for Brahms" and is really the baby of my PhD Student (using the phrase "my PhD Student" here to refer to someone for whom I'm tenuously 3rd supervisor in a vague "the university admin can't cope with RA's supervising PhD students" kind of way). I did do a little polishing on the paper so I'm not too embarrased by the author credit. Brahms is an agent programming language used by NASA to model human-robot interaction. We want to do some model checking (verification) of these models but that means we needed a semantics for the language first which said PhD student had been diligently working on for about a year now.

Profile

purplecat: Hand Drawn picture of a Toy Cat (Default)
purplecat

August 2017

S M T W T F S
   1 2 3 4 5
67 89101112
13 1415161718 19
20212223242526
2728293031  

Syndicate

RSS Atom

Tags

Style Credit

Expand Cut Tags

No cut tags