Sunday, October 2, 2011

UKZN/Meraka KRR MAIS '11

So last week I spent a week among computer scientists at the UKZN/Meraka KRR Masters Artificial Intelligence Spring School 2011.

I was initially a bit apprehensive, I was almost certainly going to be the only non-computer scientist among them. Although I'm in cognitive science/philosophy (both of which have quite strong ties to computer science on their best days) I was concerned that my lack of a more advanced background in theoretical computer science and logic would be a hindrance and that I would be stuck staring blankly at pages of formulae that made as much sense to me as ancient Sanskrit.
Thankfully, that wasn't the case.

The primary coursework for the week was Allesandro Artale's "Formal Methods" - which was firmly based in Formal Logic - more specifically, the course deals with "model checking" - which is the process of checking whether some or other property holds over a model of some system. The system in question could really be anything that's able to be modelled formally, but the focus was on modelling software systems.
The course is meant to be - I think - run over a number of weeks, so the pace was quite brisk and I could have used a little more time to digest some of the concepts - but I learned a hell of a lot. The highlight of the course, for me, was the discussions of the syntax and semantics of a number of temporal logics, which I have only barely touched on before. Temporal logic is really just a species of modal logic, so if you've done the latter the former will be easily digestible. Specifically, we looked at Linear Temporal Logic (LTL), Computational Tree Logic (CTL), and CTL* (which is a superset of LTL and CTL). Once we had a decent grasp on the semantics of these Logics we moved on to verifying whether particular kinds of properties help over models described in these languages.
We also did a little practical on specifying models and checking properties using the application NuSMV ... I'd like to see how this is used in industry (if it is) because we really only looked at toy examples.

The Formal Methods course ran across the whole week, from 9-12 every morning. In the afternoons there were tutorials (one on Hyper-heuristics, and another on "SAT and efficient boolean reasoning" that I had to miss because of work). Other than that there were presentations of various hons, Msc, and PhD projects being done at UKZN and Meraka's KRR group.


Oh, and if anyone from the Spring School reads this, thank you so much for letting me sit in - I'll most certainly be back next year.