Logic and Computation Group
Seminars 2009/10
The Logic and Computation group hosts regular seminars, given by group members or guest speakers. The seminars take place every Thursday from 1-2pm in the meeting room (Room 1.01), first floor, Ashton Building.
LoCo seminars in previous years: 2008-09
Semester 1, 2009-2010: |
|||
|---|---|---|---|
| Date | Speaker | Title | |
| 22 October 2009 | Louise Dennis | An Architecture for Hybrid BDI Continuous Agents for Space Software | |
| 29 October 2009 | Alexei Lisitsa | Reachability as Deducibility, Finite Countermodels and Verification | |
| 12 November 2009 | Michael Fisher | Analysis and verification of pervasive/ubiquitous systems | |
Abstracts of the Talks: |
|||
An Architecture for Hybrid BDI Continuous Agents for Space Software
Abstract
Current approaches to the engineering of space software such as satellite control systems are based around the development of feedback controllers using packages such as MatLab's Simulink toolbox. These provide powerful tools for engineering real time systems that adapt to changes in the environment but are limited when the controller itself needs to be adapted.
We are investigating ways in which ideas from temporal logics and agent programming can be integrated with the use of such control systems to provide a more powerful layer of autonomous decision making. This talk will discuss our initial approaches to the engineering of such systems.
Reachability as Deducibility and Verification
Abstract
I propose a simple, generic and powerful approach to the verification of infinite state and parameterized systems. The approach is based on modeling the reachability between (parameterized) states as deducibility between suitable encodings of states by formulae of first-order logic. To establish a safety property, that is non-reachability of unsafe states, the finite model finder is used to find a finite countermodel, the witness for non-deducibility.
Analysis and verification of pervasive/ubiquitous systems
Abstract
In this talk I will give a brief overview of the work several members of the group are doing concerning the formalization, programming, and verification of "pervasive" (or "ubiquitous") systems. The main problems here are handling context-awareness, multiple logical dimensions, and human-agent teamwork.
The work described involves (at least) Savas, Louise, Sven, Anthony, and Richard.