The Department of Computing Science and Mathematics presents the following seminars. Unless otherwise stated, seminars will take place in Room 4B94 of the Cottrell Building, University of Stirling from 15.00 to 16.00 on Friday afternoons during semester time.
If you would like to give a seminar to the department in future or if you need more information, please contact the seminar organiser Carron Shankland (Phone 01786-467-444, Email firstname.lastname@example.org).
Liara Aparecida dos Santos Leal, Mathematics Department-PUCRS, Brazil
Certainly a very important point in the computer systems design and analysis is concerning the computational complexity. Since the introduction of the NP-completeness theory due to Stephen Cook, in the early 1970s, a wide variety of problems from mathematics, computer science, operational research and general engineering are now known to be NP-complete. The fundamental "P=NP?" question, considered the most important problem to be solved in the next century, reduces to ascertaining the completeness.
When it comes to NP-hard optimization problems, there is also another parameter of interest. An optimization problem can be defined as the task to maximize or minimize some objective function, over a feasible solutions space. Generally these solutions can not be efficiently searched due to their too large number, in such way that finding an optimum solution results a computationally intractable problem. In many cases, a solution close to the exact solution can be satisfactory. However, in practice, optimization problems are used to presenting diverse behavior related to approximation degree, could be classified highly approximable until it is proved impossible to approximate.
This work presents a categorial approach to cope with some questions originally studied within Computational Complexity Theory, focalizing to those aspects which could be named "qualitatives" or "structurals". The Structural Complexity's goal is to classify the problems in such way that it obtains an hierarchy in relation to the intrinsic problem difficulty degree.
Keywords: Structural Complexity, Optimization Problems, Approximation Problems, Category Theory.
Dr Carron Shankland, University of Stirling
Formal methods allow us to reason about and predict dynamic system properties. Here we show how the probabilistic Guarded Command Language (pGCL) can be used to determine the likelihood of an algorithm terminating with a successful outcome within a given deadline, where the algorithm relies on a random choice.
We focus on a specific component of the IEEE~1394 `FireWire' standard: contention resolution in the network leader election protocol. The leader election protocol requires a set of asynchronous communicating nodes to elect a unique leader. In certain worst cases, when the timing parameters and computation speeds of all network nodes are identical, successful leader election relies on resolution of contention (in which two nodes have nominated the other as leader). At the core of the contention resolution algorithm is a choice based on a randomly generated Boolean. This choice may result in re-entering the contentious state, so it is not obvious that root contention will ever be resolved.
Exactly this problem is addressed by Stoelinga and Vaandrager, who prove that the root contention resolution algorithm is guaranteed to terminate successfully eventually. In practice, however, a time bounded solution is more useful; how long do we have to wait before a leader is elected? Here we formally derive a relationship between the number of attempts to resolve contention and the probability of a successful outcome. Moreover, we use the maximum time parameters of the amendment to the IEEE standard to determine the relation between the probability of successful contention resolution and the elapsed time.
Dr Savi Maharaj, University of Stirling
This talk describes joint work with Carron Shankland and Muffy Calder. The work is part of a larger project involving the development of a symbolic semantics for Full LOTOS (LOTOS with data), with the goal of making it practicable to reason about LOTOS specifications which involve the use of data. In the standard (non-symbolic) semantics, such specifications may give rise to infinite transition systems; the symbolic approach leads to smaller, and in many cases finite, transition systems which are more amenable to analysis on a machine.
I will describe one aspect of this project, involving the development of a logic for reasoning about Full LOTOS processes. The logic is designed to be "adequate" with respect to bisimulation (a naturally arising equivalence between processes), in the sense that bisimilar LOTOS processes have the same logical properties. The talk will explain the definitions of the logic and the bisimulation, and will sketch the proof of adequacy. A key factor in the development of the proof was the use of a mechanical proof checker, PVS.
Dr John Soraghan, University of Strathclyde
Richard Bland, University of Stirling
A Clinical Guidance Tree (CGT) is a way of representing medical information as a decision tree, in which the possible treatments for a disease, and their various outcomes, appear as nodes in a branching structure.
This talk will describe a project being undertaken by Stirling University staff from Nursing & Midwifery, the Forth Valley Primary Care Research Group, and Computing Science. We are developing a program to display information, in the form of a CGT, on two diseases. The hypothesis is that a GCT is particularly effective in conveying this sort of information to patients. The talk will concentrate on the development of the program and the conceptual extensions that we have made to the CGT model.
Mario Kolberg, University of Stirling.
The Telecommunications Industry has undergone major paradigm shifts in the previous years. One of these is the shift from circuit-switched networks towards packet-switched networks. There is hardly any doubt anymore that IP will be the ubiquitous transport protocol of the future.
At present the work towards Internet telephony has attracted a lot of attention. The Session Initiation Protocol (SIP) was standardised by the Internet Engineering Task Force (IETF) and can be used to establish telephony calls on IP networks. SIP supports third party services provisioning and even end-user defined services.
However, the rapid deployment of services on top of SIP is hindered by a well known problem - Feature Interactions. In a multi-service provider environment (such as SIP) the feature interaction problem is regarded to be an even more pressing issue. Services of different providers from a multitude of service creators are likely to interwork. This in turn leads to the fact that the ad-hoc approaches to service interaction handling commonly applied in the industry today will not be sufficient anymore.
In this talk, the technological changes in SIP compared to the traditional telephony network are highlighted as well as the impact of the changed business environment. The talk will focus on a new approach which addresses these changes.
Dr Stephen J McKenna, Department of Applied Computing University of Dundee
We are interested in developing computer vision systems for tracking and interpreting human activities in applications such as outdoor surveillance and monitoring, in-vehicle interfaces, gesture recognition for motor-impaired users and supportive environments for the elderly. This talk will describe computationally efficient methods for such systems. Scene segmentation is typically performed by building on-line foreground and background, probabilistic appearance models that adapt to cope with varying viewing conditions. Appearance-based models are used to enable multiple object tracking and disambiguation of quite severe occlusions despite rotations in depth, changes in lighting and shape deformation. Distance transforms are used to control model adaptation and to fit 2D geometric models. Certain actions and behavioural events can be recognised using these models. Results from several real-time systems are used to illustrate the talk.
Prof Iain Stewart, Department of Mathematics and Computer Science, University of Leicester
Finite model theory is concerned with the model theory of finite structures (such as graphs, strings etc.). It has strong connections with complexity theory and database theory. In particular, there are numerous results of the form: a problem is in some complexity class if, and only if, it can be defined in some logic. Infinite model theory has a strong mathematical tradition and there are established tools and techniques for proving undefinability results, some of which carry over to the finite setting. One hope is that these tools can be used to prove logical undefinability results which translate to complexity-theoretic lower bound results (like P is different from NP). Some of the mainstream logics of finite model theory actually arise in the more computational context of program schemes. In this talk, I will give a basic introduction to finite model theory and introduce some classes of program schemes and their relationship with some logics from finite model theory. This talk will be suitable for a broad audience and I will not assume much computer science or logic.
I will follow my seminar with an explanation of the joint EPSRC/LMS initiative MathFIT (Mathematics for Information Technology) of which I am Co-ordinator. The MathFIT web-pages currently reside at: http://www.mcs.le.ac.uk/~istewart/MathFIT/MathFIT.html.
Jose Juan Pazos Arias, University of Vigo, Spain.
In this talk I will present the work of the GRIS group (Network and Software Engineering Group) in the formal techniques field, both past work and current research.
Dave Marples, Telecordia and Honorary Professor at University of Stirling
Vendors and Network Operators are starting to see opportunities for massively distributed service execution platforms which help to avoid some of the scaling issues that the traditional telecom software industry with its largely centralised approaches to computation has suffered. These distributed and relatively open platforms do, however, bring with them some dangers, particularly in the field of multiple applications interacting with one another in an unintentional fashion. This can be viewed as the Feature Interaction problem taken to a whole new level. In this talk, an outline of the leading Open Services Platform as specified by the OSGi www.osgi.org will be presented, and three key questions for discussion will be offered.
For further technical detail, see the complete set of slides from Dave's talk.
Dr Lydia Plowman, Institute of Education, University of Stirling
Over the last few years there has been a dramatic growth in toys that use technology to give the appearance of interactivity. Toys such as Furby (Tiger), My Real Baby (Hasbro), the Microsoft family of Actimates (Arthur, DW, Barney) and 'robotic' dogs such as Poo-Chi (Tiger) respond to a child's attention by means of sensors and basic speech programs.
This convergence of high technology and children's toys provides the background to a new project funded by ESRC/EPSRC under its PACCIT (People at the Centre of Communication and Information Technology) programme. As the project has been running for less than a month I do not have research findings to share but I will discuss interface and interaction in this context and sketch out some of the ethical, social and educational issues arising from these toys.
For further details, see the complete set of slides from Dr Plowman's talk.
Dr Alice Miller, Department of Computing Science, University of Glasgow
We show how the SPIN model-checker is applied to analyse the behaviour of a real software artifact -- feature interaction in telecommunications services. We demonstrate how minimal abstraction techniques can greatly reduce the cost of model-checking, and how analysis can be performed automatically using scripts.
For further details, see the complete set of slides from Dr Miller's talk.
Dave Barton, Titan Corporation -- AverStar Group
The increasing capacity of Systems on Silicon (SoS) is demanding new design techniques, and new design languages, to meet the challenges presented by the increasing gap between our design capability and our production capability. Rosetta is a language defined to allow the designer to describe systems using models in multiple engineering domains and stating the constraints on the system rather than relying solely on describing its functional behavior. This talk will introduce the motivation, syntax, semantics, and use of Rosetta in describing very large systems.
For further technical detail, see the complete set of slides from Dave's talk.
Nhamoinesu Mtetwa, University of Stirling.
Noise is often treated as irrelevant interference in systems like radios and telephones and engineers have always sought means to minimise it. Surprisingly, during the last two decades researchers have found that background noise is sometimes useful. Many physical systems, from electronic circuits to nerve cells, work better in the presence of certain types of noise. This phenomenon is known as Stochastic Resonance (SR). In this talk, I will discuss SR and the role that it plays in neuronal systems. SR requires non-linear systems. Neurons (and hence also neuronal simulations) are non-linear. Neurons are also analogue and neuronal simulation emulates this. The simulation is usually done using floating-point arithmetic on conventional computers. We aim to show that we can get the same results in hardware using a Field Programmable Gate Array (FPGA) using only fixed point arithmetic.
Computing Science and Mathematics Seminars (Current Series)
To Computing Science and Mathematics Research
To Computing Science and Mathematics Home Page