purplecat

Several people now have told me these posts are entirely jibberish however I want to document the progress of our thought on the project. It's all under the cut but I don't suggest you read it unless you are actually interested in agents, programming and/or model checking.


To recap, the purpose of the MCAPL project is to provide a uniform framework in which programs written in a variety of Agent Programming Languages can be verified using a technique called model checking.

Our first idea was to create a "compilation language" that we could model check. The intention was that programs written in other languages would be "compiled down" to AIL (as opposed to machine code, or java bytecode, or whatever) and we would then create an optimised model checker for this language. After a year pursuing this idea we decided it needed changing about six weeks ago.

There are two things needed to understand why we reached this decision. Firstly agents (or at least the so-called "rational" or BDI style agents that we are interested in) operate a "reasoning cycle" fixed by the language - we had designed what we hoped was a sufficiently generic reasoning cycle for AIL, but the Durham end of the project, who were trying to write a compiler, were having difficulties adapting to even our generic reasoning cycle. Secondly we were (and still are) proposing to adapt an existing model checker (called Java Pathfinder (JPF)) for our purposes but as it stands it takes too long to model check a good sized program. Model checking works by examining all the states a program can be in as it runs - for even small Java programs that is a lot of states. Our advantage here was that, when talking about agents, there were only a few states we were actually interested in (most of the states of the underlying program were irrelevant to us). In fact, we were largely uninterested in what was going on while the agent was reasoning and only really interested in the state it was in after every turn of the reasoning cycle. JPF came with a handy module (called the Model Java Interface (MJI)) which allegedly could be used to hide states and improve efficiency.

So our thought was - why have an AIL reasoning cycle at all? why not put the original reasoning cycle of whatever language we are interested in into "MJI" and then provide tools so we could model check what was happening after each turn of this reasoning cycle. In Java terms this meant defining an interface (which is kind of like a set of requirements a program must satisfy) and then providing tools for model checking any program that implemented this interface. This was all pretty easy and I'd got the framework for this implemented by the time I wrote this post - what I didn't do was hide anything in MJI, considering that to be Durham's problem. However, I did then do some reading up on MJI and realised that "hiding" things in it was not entirely, or even at all, straightforward. I reported this and my boss, M., was surprisingly relieved, "it all seemed too much like magic", he said.

So, on to plan C, in this AIL is no longer a language but a toolkit for implementing languages. In particular it no longer has a fixed reasoning cycle but a framework of bits of reasoning cycle which you can plug together in whatever order suits you. We've kept the interface idea for the model checking which means that we can still model check any program that satisfies the interface but the whole "hiding states" idea goes out of the window if you do that. On the other hand we, or at least Durham, are working on ways of hiding as many of AIL's states as possible (i.e., we will go to all the effort of hiding bits of AIL in MJI) so that any language implemented using AIL's building blocks should model check better (or at least quicker) than one implemented without.

The current state of play is that I have the AIL toolkit up and running, and a toy language, named after G. (if this kind of behaviour is good enough for theorem provers then I reckon its OK for programming languages, and I was gettting tired of acronyms and puns) implemented using it. I have a program written in this toy language (in which a single agent convinces itself that it has picked something up) and I can model check that whenever the program is run it "Eventuallly believes it has picked something up" - the program runs in the blink of any eye, but it takes four minutes to model check it, waiting for those efficiency gains from Durham...

At the moment, due to the way I've implemented the model checking, I can't nest my "temporal quantifiers". Essentially this means I can say "P is true for the entire time the program runs" and "P will eventually become true whenever the program runs" but I can't say "When the program runs there eventually comes a point after which P is true for the rest of the run" - or in logical notation I can say (<>P) and ([]P) but not (<>[]P). I think I can fix this but it involves lots of complicated fiddling with the JPF virtual machine which M. thinks isn't worth my time.

I'm quite proud of the progress here and am revising my opinion of Java. The sort of pull everything apart and plug back together again in a new way that I've been doing for the past six weeks seems to be vastly easier in an object-oriented fashion than in the logic programming language I previously used (although, as B. has pointed out, a decent development environment and debugger haven't hurt either).


On hearing that a programming language was named after her G. immediately asked if she could program in it. I baulked a bit since its a long way off being anything approaching a sensible teaching language. In the end I said she could once she could program, confident in the knowledge this is probably several years away. With some satisfaction, a few days later when we attended a Curriculum Morning a the school, B. pointed out the note that listed "programming" in the IT curriculum for the summer term this year...