Log in

No account? Create an account
30 June 2012 @ 04:11 pm
Paper Accepted: Verification of Brahms Human-Robot Teamwork Models  
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.

This entry was originally posted at http://purplecat.dreamwidth.org/71426.html.
parrot_knightparrot_knight on June 30th, 2012 03:25 pm (UTC)
Excellent, and a very good idea.
louisedennislouisedennis on June 30th, 2012 03:29 pm (UTC)
"Intelligent Houses" are a pretty big area of research at the moment, though a lot of the actual examples people come up with are pretty straightforward.
a_cubeda_cubed on July 1st, 2012 03:20 am (UTC)
I know one of the researchers at the Culture Lab in Newcastle who are doing much more serious work than many of the toy examples that people make. I've pointed her at this post, since it's not friends-locked. Let me know if you'd like an introdction (I've given her the same offer).
louisedennislouisedennis on July 1st, 2012 08:43 am (UTC)
It's a kind thought. What we really need are medium sized Brahms programs and, if they exist, NASA isn't releasing them. The big examples are all intractable given the current state of the verification machinery so we're left with constructing examples ourselves - hence toy systems involving intelligent houses and digital nurses. We're sending him to talk to both the Hertfordshire and Bristol robotics people to see if he can get some more realistic examples from them, even though he'll probably have to cast the examples into Brahms himself. If your contact has something suitable (i.e. a medium sized, realistic system, involving collaboration between humans and the system and (preferably) robots plus some safety aspects suitable for model checking) that would be great but our time scales are quite tight since he really needs to be submitted by December.

More generally though, our group has a general interest in the verification of pervasive systems, so if your contact at the Culture lab has a similar interest or at least interests where some kind of verification could be useful then we'd certainly be interested in a more general way in some kind of collaboration.
lukadreaminglukadreaming on June 30th, 2012 03:31 pm (UTC)
Kargicq: Neuromancerkargicq on June 30th, 2012 05:30 pm (UTC)
Well done!
fififolle: DF - racehorse rushfififolle on June 30th, 2012 10:23 pm (UTC)
Nice one!
bunnbunn on July 1st, 2012 07:37 am (UTC)
I'm glad to hear that research into Intelligent Houses is being done by one so versed in sci fi. Let's face it, Intelligent Houses always end up going mad and locking their owners inside themselves. I am sure you will be suitably wary about giving them central locking. :-D

(And, well done!)
louisedennislouisedennis on July 1st, 2012 08:47 am (UTC)
Well we're not so much interested in programming the houses as proving that they'll never lock anyone in - except, of course, when they're supposed to lock someone in.

My boss gave what I thought was a perfectly innocuous talk on Friday about verifying the reliability of autonomous systems, and we got this bizarre line of questioning from the audience all about how cats randomly decide to climb into boxes and how could we verify that? In the end I pointed out that you wouldn't let a cat fly an aeroplane and, in fact, the point of what we were doing was to prove that the system wouldn't randomly decide to do something totally unexpected - or in the case of cats and boxes apparently entirely expected but nevertheless random or something...
wellinghallwellinghall on July 1st, 2012 05:05 pm (UTC)
There was a school of thought in the 1950s that by the ?1980s, aeroplans would be so automated that the only crew would be a man and a dog. The man would be there to feed the dog, and the dog would be there to bite the man if he tried to touch any of the controls.
louisedennislouisedennis on July 1st, 2012 06:12 pm (UTC)
There is, I think some truth in this observation....
wellinghallwellinghall on July 1st, 2012 05:03 pm (UTC)
Well done!