What's on in Computing Science?

Date: Friday, 28 March, 2008
Time: 14:00
Location: Sir Alwyn Williams Building, 423 Seminar Room
Scottish Theorem Proving
Alan Bundy, Muffy Calder, Ewen Maclean, Christopher Power

Directions

From city center, take underground (Buchanan or St Enoch's station) exit Hillhead.

Exit Hillhead station, turn right.

First right onto Great George Street.

Second right onto Lillybank Gardens.

Sir Alwyn Williams building on the left after terrace houses.



Alan Bundy - Ontology Evolution in Physics (2:00 - 2:40)

Abstract: We investigate the problem of automatically repairing inconsistent representations in ontologies when an existing theory conflicts with some acquired evidence. To address this problem of ontology evolution, we introduce novel strategies for fault diagnosis and for representation repair and compose them into repair plans, which can be executed by software agents. Two such plans have been developed to repair ontologies that disagree over the value and the dependence of a function respectively. As ontology evolution is analogous to the change of physicists' view of the world, these plans were evaluated using different versions of ontologies representing various concepts in physics. These ontologies also help justify the modifications made by the repair plans between successive versions.

Muffy Calder - Solving parameterised model checking for degenerative systems (2:40 - 3:20)

Abstract:Model checking allows automated reasoning over a finite model. Often, we want to reason over a parameterised model, for example, we want to reason about a distributed system where the parameter is the number of components or the communication topology (or both!). But like all good things, this is unattainable because it is unsolvable. However, also like all good things, we can find classes that are solvable. Here, we consider degenerative systems – systems that have the property that a model of a system over a communication graph eventually behaves like a system over a reduced communication graph. We define an induction schema for degenerative systems (non-probabilistic and probabilistic), based on the idea of relating an ordering on communication graphs to an ordering on models. This allows us to derive results for arbitrary LTL properties, provided base cases are proven (e.g. by model checking).

Ewen Maclean(to appear) (3.40 - 4.20)

Christopher Power - Prism2Promela: a tool for debugging Prism models (4.20-5.00)

Abstract:The model checker, PRISM, is a tool that facilitates the formal modelling and analysis of systems that exhibit random or probabilistic behaviour. One area where PRISM lacks is the provision of methods for model debugging. To help alleviate this problem, a tool for translating PRISM into Promela models is presented. Once in this form the SPIN model checker can be utilised in debugging the Promela model, providing insights to where the bug lies in the original PRISM model.

Contact: Mr Christopher Power (power@dcs.gla.ac.uk)

Add to my calendar