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)
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!

Profile

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

July 2017

S M T W T F S
       1
23456 7 8
910 11 121314 15
16171819202122
23242526272829
3031     

Syndicate

RSS Atom

Tags

Style Credit

Expand Cut Tags

No cut tags