|
Please consult our research directory and individual staff members' web pages to learn about their research interests. Some supervisors are affiliated with more than one institute, and so the institute placement for some proposals is arbitrary.
In a few cases, there is a scholarship providing financial support for PhD study on the indicated topic. Other sources of funding may be available to support study on other topics, and scholarships earmarked for specific areas of study may become available at short notice. But the vast majority of our scholarships are allocated to the best applicants, without regard to topic of study, subject to eligibility rules.
Theoretical and empirical study of brain processes and artificial learning systems, drawing on neuroscience, cognitive science, computer science, computational science, mathematics and statistics. For informal enquiries regarding PhD study in ANC, please see the ANC PhD pages.
Research in ANC in bioinformatics currently occurs in the areas of modelling protein and genetic networks, mapping structure to function in the nervous system and building biological databases. Further details are available on the Bioinformatics in ANC research pages, and the Bioinformatics in Edinburgh pages.
Machine learning research currently occurs in the areas of time
sequence analysis, image analysis, graphical models, deep structure
learning, fMRI, Gaussian processes, neural networks, unsupervised
learning, astroinformatics and machine learning applications. Further
details are available on the Machine learning in IANC research pages and the Edinburgh Machine Learning Group pages.
A Microsoft Research European PhD Scholarship in Learning and Inference in Highly Structured Continuous-Time Stochastic Systems is available. Click here for further information.
Current research topics in the field of neuroinformatics include models of neural computation, computational neuroscience, modelling of the visual system and the basal ganglia, modelling of developmental neuroanatomy, cognitive modelling, and development of software tools for computational neuroanatomy, computational modelling and computational neuroscience. Further details are available from the Neuroinformatics in ANC pages, the Neuroinformatics in Edinburgh pages and the Neuroinformatics Doctoral Training Centre.
Basic and applied research and development in knowledge representation and reasoning. Through its Artificial Intelligence Applications Institute (AIAI) it works with others to deploy the technologies associated with this research.
Interactive proof systems provide machine assistance for the development of large corpora of theorems and their proofs, sometimes running into thousands of proofs. To manage a large corpus of proofs, it is necessary to impose structure on it and to provide tools to browse and manipulate it. For instance, each proof step depends on previously proved theorems, axioms, rules of inference, definitions, etc. After many thousands of proofs, the user may realise that a slightly different definition or axiom would have and will make his/her job much easier. Unfortunately, implementing the consequences of even a minor change is a daunting undertaking, so that the user is forced either to live with the non-optimal corpus or restart the development: neither of which is an attractive option. The proof management tool envisaged here would keep track of the dependencies in the corpus, calculate the consequences of any change, automate the implementation of those changes as much as possible, and identify any residual changes for interactive manipulation. Look here for more details, and related project suggestions.
Most computational models of reasoning assume a fixed representation of knowledge, i.e. facts and rules remaining unchanged during inference. These are called 'ontologies'. However, observations of human reasoning show that representations of knowledge are fluid and evolve in response to attacks on arguments, to changing goals and to a changing world. It is not just beliefs that change, but also the 'signature' of the ontology, i.e. the functions and predicates in a logic representation, and their arities and types. My research group has pioneered techniques for identifying the need for representational change, including ontological change, and techniques for evolving the representation over time. We have applied these techniques to the semantic web, law and physics. Look here for more details, and related project suggestions.
Theorem provers are computer tools supporting the stating and checking of formal mathematical arguments. One aim is make them useful to mathematics students and to mathematically-oriented researchers. Typically the language used for expressing mathematical concepts is restricted to allow the automation of reasoning about the well-formedness of mathematical phrases: this reasoning is too tedious to leave to the theorem prover user. Restrictions include making strong distinctions between values and types (collections of values) and placing rigid constraints on the allowable types. These restrictions make it hard to naturally translate mathematical concepts and arguments from textbooks and research papers. The aim of the project is to devise an improved language along with suitable automatic support for the well-formedness reasoning. The project might start with a study of one of the current best languages, that of the Mizar system and involve experiments with the Isabelle/ZF prover. This project may also be of interest to PhD students in LFCS.
Agents are programs that possess a high level of autonomy and adaptiveness - being able to interact with other agents in ways that obey principles of rationality drawn from observing human society. In systems without clear boundaries, like the Internet, the loose software coupling associated with multi-agent design is an attractive way to construct large, resilient software systems. The openness of the Internet, however, raises a fundamental question: how do agents conform to the social norms of new situations that they encounter? To answer this question we must tackle a range of issues: specification of social norms; mechanisms for their enforcement in a de-centralised way; analysis of potential behaviours pre-deployment; resilience of social structures when agents fail or the environment changes. A convincing answer to this question, encompassing the range of associated issues, is one way of establishing the foundations of large-scale multi-agent reasoning systems and, perhaps, a more robust Semantic Web. We have established a major European project (www.openk.org) and a group of interacting PhD projects in this area.
Game theory provides a rigorous mathematical foundation upon which distributed rational decision making can be modelled and analysed. Although game-theoretic work in economics has analysed the significance of communication in strategic interactions between multiple agents, a full decision-theoretic underpinning for the high-level complex communication that is used by agents in multiagent systems research is still amiss. The development of game-theoretic semantics for agent communication languages and interaction protocols would allow for integrating communication activity into more general models of rational action.
In open decentralised systems, such as agent-based Semantic Web applications, developing a shared understanding of concepts used in communication is a necessary prerequisite to achieving coordinated interaction. When ontology conflicts arise due to misunderstandings, negotiating a common view of the concepts necessary to perform the task in question is a viable (yet underdeveloped) approach. However, from the standpoint of an individual agent it is not clear why ontological views of the other party should be accepted, and in fact, changing one's ontology may have a serious long-term impact on future interactions. The essential question becomes what kinds of argumentation strategies could be used to convince the other agent of modifying its ontology, and what computational models of such argumentation-based negotiation should be.
Many mechanisms for multiagent coordination have been proposed so far, but the application of methods used to manage the long-term, large-scale systems of interaction in human societies have been largely overlooked so far. What makes political coordination mechanisms particularly interesting is that the medium of social exchange is power (rather than, say, money in economic coordination or personal commitment in mechanisms based on social commitment). In other words, agents who participate in a political (e.g. democratic) system of power re-distribution agree to give up some part of their autonomy in the long-term for the benefit of assigning certain tasks to specialistists. However, this loss of autonomy is not irrevocable as political systems may have participative elements (lobbyism, campaigning, etc.), so that time is a major issue when deciding how to get involved in global decision making. Also, it remains to be explored for what kind of multiagent system functionality this type of coordination mechanism might be appropriate.
While recent advances in the areas of Semantic Web, Web Service and Grid technologies indicate that a paradigm shift toward the adoption of service-oriented architectures is imminent in many areas of mainstream software development, these developments have largely focused on providing the necessary infrastructure and standards for large-scale, networked, open systems until now. However, not many applications exist in which these technoloogies are used by "intelligent" software agents capable of flexible autonomous action and interaction. The goal of this project is to develop an agent-based framework that utilises AI technologies such as reasoning, planning, and learning within these semantically rich and knowledge-intensive service-oriented environments and to build software agents that make intelligent use of these new technologies.
The project will explore Artificial Intelligence technology to support team work orientated towards achieving joint objectives. The technology will include multi-agent systems, teamwork, semantic web use, agent presence and status notification, intelligent planning, coordination, task execution and monitoring, and the use of virtual worlds. The human and system agents, sensors and computational services will exchange task and planning information in the form of the <I-N-C-A> ontology - a shared model for plans, processes, and process products (the results of carrying out tasks). The I-X intelligent systems framework will form the core of the architecture.
Basic and applied study of communication among humans and between humans and machines using text, speech, and graphics for interactive dialog.
In several aspects of linguistic analysis, it is natural to think of some form of concurrent processing, not least because the brain is a massively concurrent system. This is particularly true in phonology and phonetics, and descriptions such as feature analyses, and especially autosegmental phonology, go some way to recognizing this. Although there has been some work on rigorous formal models of such descriptions, there has been little if any application of the extensive body of research in theoretical computer science on concurrent processes. Such a project has the potential to give better linguistic understanding of synchronic and diachronic aspects of phonology and perhaps syntax, and even to improve speech generation and recognition, by adding formal underpinning and improvement to the existing agent-based approaches.
Recently significant progress has been made in natural language processing (NLP) through the use of lexicalized grammars. Some classes of these grammars have been shown to be expressive enough for many NLP tasks while maintaining a polynomial worst case complexity necessary for efficient use. Given the parallels between the NLP tasks of parsing and generation and reasoning about physical action in the form of plan recognition and planning, the project seeks to make critical use of these lexicalized grammar formalisms for reasoning in multiple applications including plan recognition and planning.
Current large scale control systems use multiple methods to build complex assessments of the current state of the world and a controlled system. These hypothesis are often based on current sensor information with little or no high level information about previous world and/or system state. As a result these systems often build up very large databases of timestamped sensor information and high level hypothesis over very small windows of time that can be mutually contradictory. The project seeks algorithms that develop over arching hypothesis about the actual past course of events in the system.
Natural language is full of partially redundant cues to structure (e.g., a word's position in a sentence and its morphological form are both cues to its syntactic class). This project investigates how a language learner can effectively combine these cues to reduce uncertainty about the correct form of the learned grammar. The work will involve implementing Bayesian probabilistic models of language learning, and examining the consequences of considering different sources of information. Optionally, this project could also involve a human experimental component.
Eyetracking corpora contain naturally occurring text that has been read by a number of experimental participants while their eyemovements were recorded. Such corpora provide a rich source of information about human language processing, e.g., processing difficulty manifests itself as elevated fixation times or re-inspection of words. The aim of this project is to make eyetracking corpora accessible to psycholinguistic research, either by devising ways of extracting measures from existing corpora that meet the need for experimental control and counterbalancing in psycholinguistics, or by developing ways of collecting new corpora that are sufficiently controlled, without resorting to the artificial materials that are often used in psycholinguistics.
The human parsing mechanism is highly accurate and extremely robust: humans are able to recover a correct syntactic structure even from noisy text or speech. However, this fact is not reflected in current computational models of human parsing. This challenge can be addressed by applying probabilistic modeling techniques from computational linguistics to develop realistic models of human parsing. Cognitive plausibility is a prime concern here, i.e., memory limitations, incrementality, parsing strategies need to be modeled in line with psycholinguistic findings.
The visual world paradigm is an important new way of studying how humans process language. In this approach, experimental participants watch a visual scene while listening to a speech stimulus describing the scene. Their eye-movement patterns reveal that linguistic processing and visual processing is closely timelocked, which presents an interesting modeling challenge. A computational model needs to be developed that integrates visual and linguistic processing, and explains how humans extract relevant features from both the speech signal and the visual scene to direct their eye-movements.
Hidden Markov models (HMMs) are the current model of choice for automatic speech recognition (ASR). Although they are seemingly very simple models, in fact they require a complex system of context-dependent models, parameter sharing and adaptation algorithms to achieve the best performance. HMMs are a member of a wider family of models - dynamic Bayesian networks (DBNs). There are an infinite variety of other DBNs waiting to be tried for ASR. DBNS can be formulated to reflect our understanding of the speech signal; one example of this would be multi-streamed DBNs (such as the factorial HMM) in which the factors have explicit linguistic interpretations - the factors might represent aspects of the speech production process. Dependencies can be introduced between these hidden factors, creating ever richer model structures at the cost of increased computational complexity. The goal is to find model structures that improve recognition accuracy whilst remaining computationally feasible. We have already started exploring various forms of DBN, but there is still a lot of scope for exciting and original research in this area. The tools and compute power are now available to work with models that were intractable until recently. It may be that some of the techniques developed for HMMs can be transferred to DBNs, or we could build things like parameter tying, pronunciation variation, language modelling and adaptation into the model structure itself.
Natural Language Generation (NLG) is an important field within Natural Language Processing (NLP) that enables systems to communicate with their users through both spoken and written language. Until recently, NLG relied solely on symbolic techniques. However, the requirements of new applications (e.g., text summarization, question answering and machine translation) pose a number of challenges for traditional NLG, with respect to robustness and coverage. Previous work has developed statistical methods mainly for surface realization and lexical choice. Interesting directions for future research include reranking models for automatically generated texts, probabilistic models for content and sentence planning, and developing metrics for assessing text quality.
An emerging area of research in the field of Natural Language Processing (NLP) is text-to-text generation. Text-to-text generation takes naturally occurring texts as input and transforms them into new texts satisfying constraints such as length or style. Examples of applications that require text-to-text generation are single- and multidocument summarization, text simplification, sentence compression, and question answering. At the heart of methods developed for text-to-text generation lies the ability to identify and generate paraphrases, i.e., alternative ways to convey the same information either at the sentence or at the document level.
The aim of this PhD project is to investigate text-rewriting and develop models that capture alternative ways to convey the same information. The aim is to adopt a data intensive approach where meaning equivalences will be learned directly from text samples by exploiting what is observable in the data rather than manually specified rules, or elaborate semantic representations. Such an approach can deal with different text genres and domains, it is robust, and relatively inexpensive as it assumes that crucial semantic information can be discovered by analysing the linguistic environment as approximated by large corpora.
While shallow parsers are sufficiently fast and robust to process large volumes of text, they don't tend to support conventional semantic representations. But these are useful for a number of NLP applications, such as question answering, machine translation and summarisation. The aim of this project is to design, implement and evaluate a system for constructing semantic representations that meets the following critieria: it has broad coverage; it supports various levels of syntactic and semantic analysis ranging from chunk parsing to parsing with grammars; and it is reusable, in the sense that the rules for semantic construction can be applied to the output of several different parsers of varying depth (in the presence or absence of a grammar). The project will use layered modal logics to make the connection between syntax and semantics in a modular, declarative manner, and it will be implemented via well-known theorem proving techniques.
This project addresses the problems of acquiring rich semantic information for a language which lacks sophisticated and deep linguistic processing tools. The overall aim is to exploit parallel corpora and machine learning to acquire a model of semantics for such languages. The particular aim of this project is to project logical forms from a source language to a target language in a parallel corpus, to obtain automatically a (noisy) corpus labelled with logical forms, from which one can learn a mapping from target langauge strings to their logical forms (but this learning task is not part of this project).
We will use a corpus of English-German scheduling dialogues, for which the English portion has been hand-labelled with its preferred derivation, and associated logical form, as provided by a hand-crafted deep grammar (the English Resource Grammar). To project these logical forms onto the target sentences, we will use a combination of an existing model of word alignment (Giza++), POS taggers for the source and target langauges for which we will provide semantic components, and shallow symbolic modelling. Word alignments and the POS taggers are used to estimate changes to lexical predicate symbols during projection. Shallow modelling, which encapsulates knowledge of the target language concerning closed class words, verb alternations and the like, is used to edit the results. The system will be evaluated against the output from an existing hand-crafted German grammar, which derives logical forms in the same framework as the English Resource Grammar.
Any adequate model of dialogue interpretation must account for how the understanding of a dialogue and its content is grounded by its participants. In spite of the interest that grounding has attracted, two types of grounding has proved difficult to model: one is to do with implicit grounding; and the other with grounding in contexts where a dispute or disagreement has taken place. The aim of this project is to exploit the dynamics in dynamic semantics to model how grounding evolves as the dialogue proceeds. Standard contexts of evaluation (i.e., world assignment pairs) are to be replaced with contexts that represent the public commitments of each dialogue participant, and grounding amounts to the joint entailments among those commitments. This brings together work in dynamic semantics of natural language---and particularly dynamic theories of anaphora resolution and speech acts---with dynamic logics of public announcement. As part of this work, the student would need to develop novel logics that link public commitment with other attitudes, such as intentions, preferences and belief.
People use their whole bodies to communicate. Many people who study gesture have argued that gesture should combine with its synchronous speech within the grammar, producing a single derivation tree. This assumption is necessary both to predict the fine-grained temporal synchrony betwen speech and gesture, and to capture distinctive constraints on coreference and other semantic relations that apply to units of speech and gesture in coordination (e.g. the content of a gesture and its synchronous speech cannot be combined with disjunction).
The aim of this project is to develop a grammar of situated language: i.e., of speech and gesture combined. The starting point will be Combinatory Categorial Grammar (CCG), a grammar that already combines language with intonation, in particular providing a formal model of how pitch accents and boundary tones affect semantics. We will extend this grammar with a syntactic and compositional semantic analysis of deictic and iconic gestures. The resulting model should make predictions about the co-temporality of speech and gesture in syntax---the timing of a gesture is affected by pitch accents as well as syntactic constituency---and predictions about which gestures are semantically consistent with its synchronous speech and which are incoherent.
Speech-based dialogue systems have reached levels of performance where they can be of practical use, but they still suffer from brittleness and often require many hand-coded rules. This project uses machine learning and statistical methods to address these two shortcomings. Machine learning allows many aspects of a dialogue system to be learnt automatically from data, thereby avoiding the need for many hand-coded rules. A statistical approach allows uncertainty within and between the different modules of a dialogue system to be treated in a systematic way, thereby addressing brittleness. For instance, when the speech recogniser or parser are uncertain about what has been said, the dialogue manager can consider all the hypotheses in parallel. This work will be done using a probabilistic model called Partially Observable Markov Decision Processes (POMDPs).
Organisations such as the World Health Organization need to issue health documentation in a number of languages, all of which need human translators. This can be expensive. An alternative would be to accelerate the translation task using Statistical Machine Translation. Challenges include: dealing with complex terms, the need to obtain good results using little training data and integration of existing static knowledge sources such as ontologies and databases.
Rather than requiring users to wear microphones for speech recognition to operate, we are interested in using microphone arrays attached to walls or tables. Microphone array beamforming for localization and enhancement is a well studied, using microphone arrays for speech recognition, less so. We are interested in approaches in which the parameters used to combine the signals from the different microphones are treated as parameters of the speech recognition acoustic model, and optimized along with the rest of the system. Interesting research issues arise when talkers are moving, and when multiple talkers overlap.
Large vocabulary speech recognition is largely based on language models in which the probability of the current word is estimated conditional on the previous words spoken (the history). However in multiparty conversations, there is not a single, linear stream of words, and it is not always obvious what the closest history is. This project aims to develop statistical models that integrate history information from both the talker in question, as well as other talkers, while remaining computationally feasible.
This project is concerned with building speech analysis and recognition models that respect the constraints of speech production. Although speech production data may be available when training data is collected (if a specialised recording facility is used) it is not available in the general case. The aim of this project is to use observed articulatory data to construct a hidden space. When unseen acoustic data is presented this hidden space is inferred from the data, and can be used as a constraint for speech recognition. The advantage is that inference of the hidden space of articulation must respect the constraints learned from observed articulatory data.
It is now feasible to make recordings of human communication (eg multiparty meetings) using mutiple cameras and microphones, along with other sensors. At the present time, state of the art statistical modelling and machine learning approaches are based on approaches such as hidden Markov models (HMMs), Gaussian mixture models (GMMs), decision trees, and feed-forward neural networks. These approaches have proven successful for many problems: in particular they scale well to very large data sets. However, they do not provide a rich structural representation. For example, HMMs are a standard approach to modelling complex time series (eg speech), but they are not well suited to representing multiple, asynchronous streams of data. Likewise, GMMs are excellent models for general unknown probability distributions, but are not well suited to situations with more than a flat structure. We are primarily interested in two approaches to the problem of modelling multiple streams of data with a hidden structure: dynamic Bayesian networks (DBNs) and latent variable models. DBNs may be viewed as a generalization of HMMs, and are well suited to learning multistream models with a structured state space. Latent variable models assume that the observed data is generated from a lower dimensional hidden or latent space. These models are particularly appropriate for multimodal and multistream situations, since an underlying assumption is that the multiple streams of data are (partially) caused by the same underlying process.
Lifelike conversational agents, behaving like humans with facial animation and gesture, and making speech conversations with humans, are one of the next-generation human-interface. Much efforts have been made so far to make the agents natural, especially controlling mouth/lip movement, and eye movement. On the other hand, controlling the movement of the agent's head including facial expression has not been studied that much, even though head movement sometimes plays a more important role in naturalness and intelligibility than mouths and eyes. The purpose of the project is to develop a mechanism for controlling the head movement of photo-realistic lifelike agents when the agents are in various modes; idling, listening, speaking and singing. One of the outstanding features of the project is that it aims to imitate the manner of head motion of an existing person to give the agents virtual personalities with the help of machine learning techniques and methods used for text-to-speech synthesis.
State-of-the-art automatic speech recognition systems employ the phone as the basic acoustic unit for recognition, because of its compactness and easier trainability than larger units such as syllables. However, it seems that recognitions accuracies, especially for spontaneous speech where people speak rather quickly and not clearly enough, have saturated for these years despite the great efforts that have been taken to improve phone-based models. The project explores larger units of acoustic models that would resolve ambiguities caused by phone-based models. To that end, the project tackles the data-sparseness training problem of acoustic models of larger units by incorporating hierarchical tying (sharing) and adaptation techniques, where unit selection and model training are treated in a framework of optimization problems.
Currently, wide-coverage parsers have reached asymptote at around 90% recovery on all measures relevant to interpretation. The main reason is the shortage of human-annotated training data for supervised learning. The project seeks to generalize a radically lexicalized grammar learned from annotated data using large amounts of unlabelled text on the basis of evidence that the original lexicon includes instances of all grammatical lexical types.
When uttering the sentence "Marcel proved completeness", we "sing" it to a different "tune" in answer to the question "Who proved completeness?" than as an answer to "What did Marcel prove?" It is important to get intonational tunes right in spoken dialogue applications. The project seeks to formalize the meaning of such intonational tunes and apply them in spoken dialogue generation.
The grammatical systems of tense, mood, and aspect convey a number of causal and intentional relations between states and events, as well as purely temporal relations. The project seeks to provide a complete semantics for such relations, drawing on linguistic, computational, and knowledge-representational theories in application to domains such as meeting summarization.
Hidden Markov Model (HMM)-based language models are widely used in speech recognition, and lie behind all speech recognition technology. The project investigates use of higher-level grammatical information in language models.
The project seeks to apply the techniques of computational linguistics to the analysis of music, and in particular those aspects of harmonic and rhythmical structure that are reflected in a musical score and an expressive peformance.
When http: URIs are used to refer to things as opposed to web pages, ambiguity arises on the Web. Both humans and machines need to solve the question of what some person is actually referring to when they use an http: URI, especially if that URI can be used both to refer to a web page and a thing that is not on the Web. We have a preliminary solution based on the ability of humans to verify the results of a search engine request. We call our solution ``Web Proper Names'' -- it provides a distributed approach to creating and sharing Web names for things, allows use of Web names for non-Web things to be easily distinguished from the use of URIs to address web pages and achieves interoperability of names.
The approach can be used to create canonical HTML RDDL files for things recording the results of search and human assessments. There is a very topical and exciting research challenge here -- how to exploit this technique to enable a probabilistic/statistical approach to achieving the information synergy goals of the Semantic Web.
A common strategy used in presenting new information is to do so in comparison with something else, e.g.
"Unlike the old-line cosmetics houses, Unilever and P&G both have enormous research and development bases to draw on for new products."
"A call option is similar to a put, except that it gives its owner the right to buy shares at a stated price until expiration."
"As with many other goods, the American share of Japan's PC market is far below that in the rest of the world."
These comparisons are multi-functional, and languages possess a wide variety of constructions for presenting them (usually outside of a clause's main predicate-argument structure). This project will involve developing methods for extracting comparative information from large corpora and using it to produce more informative answers. It will complement other work being done locally on information fusion for QA and on answering difference questions.
A hefty amount of tedious manual labor is usually needed to create the kind of annotated corpora that support advances in discourse, dialogue and text processing. Following work on "annotation projection" from parallel corpora by Philip Resnik and his students in the area of parsing, we want to investigate whether a similar approach can be used to project annotation relevant to discourse, dialogue and/or text, thereby reducing the amount of manual effort required.
Architecture and engineering of future computing systems: performance and scalability; innovative algorithms, architectures, compilers, languages and protocols, networks and communications.
More data is available digitally than ever before. The increasing mountain of data poses interesting challanges. How best to integrate data from several sources, perhaps from different scientific disciplines? It is vital to create a robust path from data to knowledge via data integration and mining. For example, what happens to the data mining processes if one of the data sources significantly changes? Challenges include the automatic integration of multiple database schemas, the design of a data to knowledge system via integration and mining and the application of advanced data mining algorithms in a specific domain.Successful candidates will be based in the National e-Science Centre.
Grid computing is a popular approach to share computational and data resources on a global scale. Its aim is to make computing as easily accessible as the power grid does for electricity. Although many computing grids are in operation today, various issues remain to be solved. Security and authentication of the users of a grid need to be handled at various sites. Resources need to be utilised to their maximum potential by effective scheduling. Data is often required near the computational processes while transporting it can be costly. Users of grids expect different ways of interaction, some may prefer a command-line interface, while others may expect to use a custom build portal. Projects in this area are often in collaboration with other disciplines that make use of the grid, such as physics, astronomy, bioinformatics and computational chemistry.Successful candidates will be based in the National e-Science Centre.
The objective of this research is to investigate the use of speculative multithreading to improve single-application and multiprogramming performance, and to increase fault-tolerance and reliability. This investigation follows three main lines of research. The first is the development of a compilation environment to generate efficient speculative parallel code, including speculative parallelization and speculative helper threads. The second line of research involves the development of optimized thread-level speculative architectures. Finally, the third line of research is expected to cover novel uses of speculative multithreading, such as fault-tolerance. For more details, please consult the VESPA project web page.
This new architectural approach is likely to replace current monolithic superscalar microprocessors in the future. The objective of this research is to investigate the use of single chip multiprocessor architectures based on the replication of very simple processor-memory "cells". This investigation follows two main lines of research. The first is the development of novel compilation techniques to extract larger degrees of TLP from traditionally hard to parallelise applications. The second is the development of improved architectures through the systematic study of architectural design alternatives under various performance, complexity, and power dissipation constraints. For more details, please consult the Cellular Multiprocessors project web page.
The skeletal approach to parallel programming advocates the use of program forming constructs which abstract commonly occuring patterns of parallel computation and interaction. In effect, these constructs define a co-ordination language into which fragments of lower level (either sequential or explicitly parallel) code can be inserted. There is a range of opportunities for developments in this area:
There is widespread expectation that future micro-electronic circuits will be unreliable: some of the transistors will not be operational or there will be large variations in their properties, or transient errors could occur unexpectedly somewhere in a circuit. In this scenario, the current hardware design style, which relies on all components working 100% correctly, will be unusable. This project will investigate novel micro-architectural techniques for designing computing systems using un-reliable circuits.
It is a well known fact that the energy consumption of a processing unit depends on the actual values of the data being processed. Surprisingly, this principle is not, generally, being used to influence the design of such units. Byte-slicing well-known circuits and applying shortcuts when the corresponding operand bytes contain all zeroes or all ones is the only direction that has been seriously pursued. This work will investigate alternative designs for processing units, by looking at different algorithms, data-representations and organisations. For example, self-timed, iterative implementations could be used instead of the common combinatorial ones. An important part of this project would be to analyse typical data values used in real applications, by profiling or other means.
The Semiconductor Industry Association predicts that technologies will become very "noisy" in the near future. Current noise mitigation approaches will become inefficient to cope with the large number of potential trouble spots, thus leaving noise tolerance as the preferred alternative. Asynchronous circuits, especially delay-insensitive ones, claim insensitivity or, at least, considerable robustness with regard to delay variation, but are they tolerant with respect to noise from sources such as crosstalk, supply voltage bounce etc.? This work will initially quantify the noise-tolerance of known implementations of asynchronous building blocks and propose alternative more robust implementations. At a second stage, (micro-)architectural approaches to noise-tolerance will be considered, taking advantage of the inherent timing flexibility of the asynchronous design framework.
Syntax-directed synthesis for self-timed circuits, where a high-level description of a circuit, using a hardware description language, is automatically converted into a gate-level netlist, allows complex circuits to be designed seemingly effortlessly. One of the main features absent in these design flows is testing, i.e. how to ensure that a fabricated chip has no manufacturing defects, and design for testability (DfT), i.e. adding extra circuits to aid testing. This project will investigate how to test circuits generated by syntax-directed synthesis methods. In contrast with traditional test-related tools, which work on a low-level circuit netlist, this project will use the high-level, handshake-component network generated by syntax-directed synthesis as the starting point for determining the best test strategy to follow. This representation provides more information about the functionality and structure of a circuit than a gate-level netlist and should help achieve better test-coverage results and/or lower DfT overheads. Finally a test analysis phase could be investigated which helps the synthesis engine to decide the most testable implementation when multiple alternatives exist.
Self-timed circuit design is gaining traction because of the increasingly harder timing closure problems faced by the conventional, synchronous design style. One of the challenges of self-timed circuit design is testability, i.e. how to ensure that a fabricated chip has no manufacturing defects. With the shift to submicron feature sizes of CMOS technology, the standard stuck-at fault model is not capable of capturing all possible manufacturing defects, therefore a more detailed, delay fault model is needed. This is even more important in self-timed circuits as delay faults could break local timing assumptions and can cause the circuit to malfunction.
This project will explore new and novel approaches to detecting delay faults in self-timed circuits. These techniques can take advantage of the fact that self-timed circuits halt when a handshake protocol is violated due to a fault. Moreover, conventional approaches based on insertion of DfT circuits to control/observe faults will also be investigated. Using the invented techniques, this investigation aims to develop a test methodology supported by custom tools that will be of practical help to designers and test engineers.
In any modern architecture, the cache hierarchy occupies a significant fraction of the total chip area and thus consumes a large amount of energy. It is also the first point in any multi-core system where threads will interact with each other. The differing requirements of these threads can be lead to sub-optimal cache performance and energy consumption. This project will focus on the use of the compiler and runtime solutions to optimise the cache hierarchy for power reduction and thermal management.
Traditional approach to utilize radio spectrum for wireless communication has been to statically partition and allocate the spectrum to different parties through auctioning. It is widely recognized that this approach not only leads to inefficient spectrum use, but also creates interoperability issues among networks using different parts of the spectrum. The advent of programmable/software radios and multi-radio platforms has made dynamic spectrum access/sharing a viable and promising alternative. The objective of this research is to study architectures and techniques that enable dynamic spectrum access and provide significant gains in spectrum efficiency while meeting quality-of-service requirements of end-user applications.in the context of wireless network environments with diverse applications and heterogeneous wireless technologies/devices.
Scalability/performance and reliability have been the two main issues of focus of the wireless networking research community. Several new approaches such as packet-level (network) coding and cooperative communication have emerged recently. These approaches when put together have the potential to better address the aforementioned two issues. The goal of this research is to understand interactions among these new approaches and capabilities at various layers of the protocol stack as well as to develop cross-layer techniques that exploit such interactions. A related research topic is to develop a general framework for monitoring network and channel state information necessary to trigger such cross-layer adaptation.
The use of information and communications technologies in developing regions has already shown that it can have a tremendous positive impact on variety of areas including education and healthcare. It also comes with a unique set of challenges that are tied to the cost constraints, absence of reliable infrastructure, environment and cultural issues in these regions. The objective of this research is to develop low-cost and robust networking solutions for such environments. A complementary line of research is to explore novel applications that are enabled by such network and sensor deployments.
The aim of this project is to develop advanced compiler technology that can take emerging applications and automatically map them on to the next generation multi-core processors such as the IBM Cell. This PhD will involve new research into discovering parallelism within multimedia and streaming applications going beyond standard data parallel analysis. The project will also investigate cost-effective mapping of parallelism to processors which may include dynamic or adaptive compilation.
The overall objective of this project is to develop a compiler framework that can automatically learn how to optimise programs. Rather than hard-coding a compiler strategy for each platform, we aim to develop a novel portable compiler approach that can automatically tune itself to any fixed hardware and can improve its performance over time. This is achieved by employing machine learning approaches to optimisation, where the machine learning algorithm first learns the optimisation space and then automatically derives a compilation strategy that attempts to generate the ``best'' optimised version of any user program. Such an approach, if successful, will have a wide range of applications. It will allow portability and performance of compilers across platforms, eliminating the human compiler-development bottleneck.
Future embedded systems will have the capacity to deploy many CPUs in a single chip. There are a large number of variables in the complex process of optimising the design of such multi-core systems. Automated design space exploration is therefore becoming an important area of research for future embedded systems. The PhD candidate selected to work on this project will focus on investigating new ways to explore the design space of multi-core low power scalable architectures suitable for mobile embedded devices.
Current trends toward chip-multiprocessors with increasing number of processors and the comparatively smaller increase in on-chip cache sizes place increasing pressure on the cache hierarchy. Reconfigurable cache hierarchies allow the system to dynamically adapt to the workload to maximise the effectiveness of caching. The PhD candidate will investigate reconfigurable cache designs to provide scalable high-performance configurations for future multi-core systems.
Efficient implementation is critical for embedded systems. Current optimising compiler approaches based on static analysis fail to deliver performance as they rely on a hardwired idealised model of the processor. This project is concerned with using feedback directed search techniques which can dramatically outperform standard approaches. This project will investigate the use of automatically generated performance predictors based on machine learning to act as proxies for the machine. This will allow extremely rapid determination of good optimisations and allow greater coverage of the optimisation space.
As on-chip transistors shrink, the contribution of inter-gate wiring delays to the overall timing and power consumption of logic circuits becomes more pronounced. This will have a profound effect on the design of future microprocessors, and on the ways in which automated design methodologies model the delay and power consumption. For example, the inaccuracies of statistical wire-load models becomes so severe below 0.18μm that they are of little practical use. The alternative, which is to use some form of physical synthesis, is too computationally expensive to use in the kinds of iterative design-space exploration where hundreds or thousands of competing hardware structures must be evaluated. The aim of this project is to investigate ways in which physically accurate wire length models can be constructed from high level hardware specifications.
Multi-threading is an established technique for time-slicing the micro- architectural structures in a deeply-pipelined processor. It allows the hardware resources to achieve better utilisation, yielding higher overall processor throughput, and for real-time computing it offers a good solution for guaranteed response times. However, the replication of resources and the provision of hardware thread schedulers, typically leads to complex processor designs that are physically large and consume lots of energy. The aim of this project is to explore the possibilities for low-power multi-threaded architectures, particularly those aimed at real-time embedded micro-controller applications.
One of the defining characteristics of computationally-demanding embedded computations, such as high definition video codecs, is the large quantities of data parallelism in many of their algorithms. The aim of this project is to explore the characteristics of a range of data-parallel algorithms, from typical embedded computations, and identify new and novel ways to provide reconfigurable micro- architectural structures to exploit the available data parallelism. The goal will be to search for reconfigurable structures that do not rely on relatively inefficient Field Programmable Gate Arrays.
Why are some combinatorial problems harder to solve than others? What characteristics determine how difficult a problem is. What is the best way of matching the characteristics of several algorithms to the problem instances you want to solve? These questions form a basis for many challenges surrounding combinatorial problems such as graph colouring, satisfiability, travelling salesman, vehicle routing, and many more. The algorithm that solve these problems are computationally intensive, and solving many of them to understand a problems characteristic makes this several times worse. Using grid computing we now have access to massive parallel computing resources required to gain this understanding. Successful candidates will be based in the National e-Science Centre.
We have several projects where we are investigating computer vision methods for understanding what people are doing based on video sequence data. It is becoming possible to represent models of simple behaviours and recognise those behaviours. However, people switch behaviours over time, for example, when people change from a window-shopping/browsing behaviour into a enter/select/purchase/exit behaviour. This project will investigate how to represent and recognise multiple sequential behaviours.
Many approaches to recognising humans behaviour from video data are based on person tracking. While tracking performance is improving, it seems unlikely that near-perfect tracking will be possible in the near future (given the variety of scene conditions that cause problems for trackers). This project will investigate methods for recognising behaviours based on incomplete fragments of tracked data, which most current trackers are capable of producing.
We will soon have a dense 3D shape capture system observing data at 500 frames per second. This project will investigate how to acquire accurate dynamic models of quickly changing shapes, based on data from this new sensor. For example, it can be applied tobats observed in flight.
We are working on several projects to produce robot systems that closely copy insect behavioural capabilities. This ranges from novel sensing devices (e.g. auditory systems, specialised visual processing hardware, hair sensors) to detailed neural network controllers and mechanisms of learning; it could also include insect-like locomotion (walking, flying robots). Potential students should have good programming skills, an interest in biology and neuroscience, and ideally some knowledge of robot hardware issues.
Developing and applying foundational understanding of computation and communication: formal models, mathematical theories, and software tools.
The Proof General project is concerned with constructing tools to help people use interactive theorem provers. Theorem provers are applied in the development of high integrity hardware and software systems and in the efforts to construct a body of mechanically verified mathematics. Interactive proof development focuses on the construction of proof texts which have much in common with program texts. What we would like to do is to apply techniques used in software engineering to the development and maintenance of proof scripts.For example, refactoring tools would be invaluable in proof development, as proof scripts become larger and more complex. Research is needed into the development of these techniques and understanding how they can be supported by theorem provers. As a vehicle to support the research, we are developing a new version of the Proof General environment based on the extensible Eclipse IDE.
Independence-friendly logics are logics in which, in a certain sense, the truth of formulae in one location must be established independently of the truth of formulae in another location. (More precisely, values for existential variables may require to be chosen independently of previous values for universal variables.) There has been some work on the natural idea of applying these logics to distributed or concurrent systems, but much work remains to be done. Some particular questions are: satisfiability, complexity etc. of IF temporal logics; application to software design; relationship to true concurrency. More practically, there are no tools available even for the most basic use of IF logics.
The modal mu-calculus is a logic that combines fixpoint operators (think of finite or infinite looping in a program) with modal logic. Much of its theory is well understood, but there are several outstanding problems. The main problem is the complexity of evaluating formulae, known to be NP and co-NP, but not known to be Ptime. A related, but probably easier, question is that of semantic alternation depth, that is, determining the "hardness", in a certain technical sense, of a formula.
Many scientific databases have the properties that they are accretive (new information is added, but relatively little is deleted) and that updates to existing data are relatively infrequent. Keeping archives of such databases is essential for accuracy in scientific citation. We present an archiving system with the following properties:
The system relies on the fact that scientific databases are typically hierarchical and have a hierarchical key structure. It can also use "diff" files when no such key is available.
It is increasingly common to use XML to represent data currently residing in databases. With this comes the need for a full treatment of integrity constraints for XML such as key, foreign key, functional, inclusion and inverse constraints, which are commonly found in databases to convey an essential part of the semantics of the data. The goal of this project is to develop XML specifications with constraints, to advance understanding of consistency and implication of XML constraints, as well as to explore applications of constraints in XML data transformations and integration such as information preservation, constraint propagation and normalization of XML specifications. In pursuit of this goal, methods for specifying and reasoning about XML constraints are being developed, and transformation techniques and tools in the XML context are being implemented and evaluated. Results from the project are expected to yield insight into integrity constraints for hierarchically structured data, including but not limited to XML.
This is a subset, but an important subset, of our work on integrity constraints for XML. Keys are essential in the design of relational databases, and they are also important in XML documents where they are closely connected with "digital identifiers" and "deep citations" in digital libraries. Unlike their relational counterparts, keys in XML have a hierarchical structure, which makes defining them and reasoning about them a non-trivial exercise.
One of the assumptions underlying much of curation is that the objects we are "curating" are fixed. For many people who call themselves curators, this assumption is false. Consider a standard reference work such as a dictionary, compendium, or catalogue. The chances are that it is now an on-line database. It is such databases that are no driving, for example, much research in biology; and unlike their cellulose predecessors, the period between new editions is measured not in decades, but in days or hours. Worse, because our knowledge is changing so rapidly, both the structure and content of these databases can undergo quite radical changes. The value of these databases lies in the way they organise and annotate existing data - data extracted from other databases. Current database technology is ill-equipped to deal with such databases. In particular recording where data comes from - its provenance - is a non-trivial problem. Provenance is often classified into two kinds: coarse-grained, in which one simply logs the transactions, and fine-grained, in which one tries to give an account of how and why individual data items were copied and annotated. The latter is a challenging problem and calls for new models of both data and query languages.
A fundamental concern of information integration in an XML context is the ability to embed one or more source documents in a target document so that (a) the target document conforms to a target DTD schema and (b) the information in the source document(s) is preserved. Given a mapping f from instances of a source XML DTD to instances of a target XML DTD, one often wants the mapping to preserve the information of source documents T by ensuring (a) invertibility: the source T can be recovered from the target document f(T); and (b) query preservation: all queries (in a certain XML query language) on the source T can also be answered on the target document f(T). To this end, we will investigate schema-mapping techniques to ensure information preservation, including various embedding mechanisms, transformation rules and propagation of constraints. The topic requires a solid background in logics, complexity theory, algorithms and database systems.
Most current implementations of XQuery are either "toy" - they break on large documents or they are "fake" - they are SQL masquerading as XQuery. We shall describe some recent work on a native XML store and an interpreter for a useful subset of XQuery that scales in the way one would expect of a database query language. Preliminary results on a large-ish (80GB) data set show that the techniques produce performance which is comparable with well-tuned SQL queries running on the same data in a commercial RDBMS. The technique is based on a combination of two existing ideas. The first is to extend a very old idea of using column-based storage of tabular data to the storage of XML. An XML document is separated into a "skeleton", which describes the structure of the document and a set of "vectors", which are the sequences of data values appearing under all paths bearing a given sequence of tag names. The second idea is to generate a query-friendly compressed version of the skeleton.
In the SAT problem we are given a Boolean expression (typically in conjunctive normal form), and the goal is to find an assignment to its propositional variables that makes the entire expression evaluate to true. This problem is fundamental both in theory and practice, because SAT is very generic and thus many algorithmic problems can be reduced to SAT directly. However, SAT is a "hard" computational problem. That is, no algorithm is known to solve all problem instances efficiently. Interestingly, among the "hardest" instances for common SAT solvers are randomly generated inputs. Therefore, the goal of this project is to understand why random SAT formulae are "hard", and if/how they can be solved efficiently via new algorithmic ideas. In fact, recently an exciting new approach to this problem has been put forward by statistical physicists. Hence, one of the aims will be a rigorous study of these new ideas to understand both their algorithmic impact and their limitations. The topic is particularly well suited for a student with an interest in probability theory.
Think about some kind of (probably-irregular) polytope in a real high-dimensional space, and imagine the set of lattice points (integer-valued points) which lie inside the polytope. The problem of developing algorithms to approximately count the number of lattice points inside a given input polytope (in some appropriate mathematical description) in polynomial-time is a challenging problem in theoretical computer science. It has been solved for certain classes of polytopes, but there are some interesting classes of polytope for which the problem remains open. Most, if not all, of the polynomial-time algorithms that have been created to approximately count lattice points are randomized algorithms (which can use "random bits"). The goal of this project is to design a polynomial-time algorithm to approximately count the lattice points of a given transportation polytope (also known as a contingency tables polytope). There have been algorithms developed for restricted subclasses of transportation polytopes, but the general problem has resisted solution so far. The project would be exciting for a student with an interest in combinatorics, computational complexity, or probability theory.
Very few combinatorial enumeration problems are computationally feasible, at least if we insist on exact solutions. This empirical observation motivates the study of approximation algorithms for counting problems. In the past decade, considerable progress has been made in classifying counting problems according to whether they are efficiently approximable or not. This progress has been mostly in the positive direction, where the Markov chain simulation has proved a powerful tool for constructing efficient algorithms. Nevertheless, the complexity-theoretic status of many counting problems is still unresolved. Many of these problems are presumably hard to approximate, but our techniques for providing evidence for this are quite primitive. This area would suit a student with an interest in combinatorics, computational complexity, or probability theory.
Modelling is becoming a necessity in studying biological signalling pathways, because the combinatorial complexity of such systems rapidly overwhelms intuitive and qualitative forms of reasoning. Yet, this same combinatorial explosion makes the traditional modelling paradigm based on systems of differential equations impractical. In contrast, agent-based or concurrent languages describe biological interactions in terms of rules, thereby avoiding the combinatorial explosion besetting differential equations. An exciting aspect of the agent-based approach is that it naturally lends itself to the identification and analysis of the causal structures that deeply shape the dynamical, and perhaps even evolutionary, characteristics of complex distributed biological systems. A broad set of topics needs investigation from the integration of static and dynamic spatial structures, to the design of languages for the manipulation of models and their properties using causal/temporal logics, and the elaboration of the foundations of stochastic rewriting systems.
Recursive Markov Chains (RMCs), a new and natural abstract model of procedural probabilistic programs and related systems involving recursion and probability, are a probabilistic version of Recursive State Machines (RSMs), and strictly generalize stochastic context-free grammars and related stochastic processes. There are already several useful non-probabilistic program analysis and verification tools based on variants of RSMs and related models like pushdown systems. Systems that combine probability and recursion are pervasive in many programming and other systems contexts, but until now both the proper theoretical framework and the tools and algorithms to analyse and verify such systems have been lacking. In order to efficiently verify and "model check" RMCs and extensions of RMCs against formally specified properties, a number of often deep algorithmic questions will need to be addressed; this work has begun but is at a preliminary stage. Developing practical implementations of such algorithms will require a great deal of optimization, combining numerical, algebraic, and logical techniques. This project has two components, suited for students with different research inclinations:
XML has become the prime standard for data exchange on the Web. With this comes the need for XML publishing, i.e., mapping data currently residing in relational databases to an XML format. In practice a community or industry typically agrees on a schema (DTD), and subsequently all members of the community exchange their data with respect to the predefined schema. This is referred to as schema-directed publishing, in which the target XML document (view) is required to conform to a given schema. This is rather nontrivial: the presence of recursion and/or nondeterminism in an XML schema introduces difficulties in defining schema-conformant mappings. The aim of this project is to study and implement a DTD-directed framework for publishing relational data in XML. The framework provides a language for guiding the user toward the definition of an XML view that is guaranteed to conform to a given target DTD, as well as middleware for efficiently computing these views. It is based on the novel notion of attribute transformation grammars (ATGs), which extend a DTD by associating semantic rules defined in terms of SQL queries.
The prevalent use of XML highlights the important issue of ensuring the selective exposure of XML content to different user groups based on their access privileges. The problem of securing XML querying is to ensure that, given a user query Q over an XML database T, the evaluation of Q returns only information in T that the user is allowed to access. This calls for 1) an expressive language for specifying access policies for multiple user groups at various levels of granularity; 2) efficient techniques to enforce access policies during XML query evaluation; and 3) the ability to derive and provide a view schema for each group of users, characterizing their accessible data in order to facilitate query formulation and optimization. Previous proposals and standards for XML security are to specify and enforce access policies at a physical level by either annotating data nodes or materializing XML views. This is costly for large XML databases, and worse still, is error-prone when the underlying data or access policies are updated. Furthermore, none of these models supports schema availability. The aim of this project is to investigate and develop an XML security model that both specifies and enforces XML access control at a conceptual (schema) level.
As the W3C standard for navigating XML documents, XPath has been widely used for specifying (e.g., XML Schema) and querying (e.g., XQuery, XSLT) XML data. In contrast to its regular-expression counterpart, a number of fundamental questions are open for XPath: for an XPath fragment commonly used in practice, is there a logic characterizing its expressive power? Is there a rewrite (or axiom) system for determining equivalence of XPath expressions? Is a fragment closed under Boolean operations (closure properties under intersection, complementation)? Is there a normal form for a fragment? This project is to answer these questions. Results expected from the project are useful for, e.g., XML query optimization.
When overlapping or redundant information from multiple sources is integrated, inconsistencies or conflicts in the data may emerge as violations of integrity constraints on the integrated data. The constraint repair problem attempts to find ``low cost'' changes that, when applied, will cause the constraints to be satisfied.
This project aims to develop techniques to clean (integrated) data, including:
Schema mapping is to find a data transformation that, given an instance of a source schema, will produce an instance that conforms to a target schema while preserving the appropriate information content of the source. Finding schema mappings is a common task in a wide variety of data exchange and integration scenarios.
Schema matching is to find a pairing of attributes (or groups of attributes) from the source schema and attributes of the target schema such that pairs are likely to be semantically related. In many systems finding such a schema matching is an early step in building a schema mapping.
A fundamental concern of information integration is the ability to embed instances of one or more source schemas in an instance of a target schema so that the information in the source instances is preserved. This calls for a notion of schema embedding that enables a source schema to be effectively matched to (or, embedded in) a target schema with larger "information capacity". This notion should allow for powerful schema-restructuring transformations that capture data-structuring variants (e.g. different hierarchical element groupings) commonly encountered in practice, while ensuring lossless instance mappings and effective translation of source queries over the target.
Partial evaluation (a.k.a. program specialization) has been studied in the context of programming languages as a general optimization technique. Intuitively, given a function f(s, d) and part of its input s, partial evaluation is to specialize f(s, d) with respect to the known input s. That is, it performs the part of f's computation that depends only on s, and generates a partial answer, i.e. a (residual) function f' that depends on the as yet unavailable input d.
This project is to develop this idea for the evaluation of XML queries over a tree that is fragmented, both horizontally and vertically over a number of sites. The key idea is to send the whole query to each site which partially evaluates, in parallel, the query and sends the results as compact residual functions to a coordinator which combines these to obtain the result.
This project is not only to explore the usefulness and potential of partial evaluation in distributed systems, but is also expected to yield effective techniques for centralized XML stores to evaluate XML queries and beyond.
The PEPA project began in Edinburgh in 1991 and has developed a modelling language and associated tools to predict the performance of software and hardware systems. The PEPA language (Performance Evaluation Process Algebra) is a compact modelling language which models systems as compositions of sequential components which perform timed activities either individually or in cooperation with other components. PEPA models are analysed by compilation into Continuous-time Markov Chains (CTMCs) or other formalisms. Research projects on the language include extending the software tools which support it, and improving their analysis capabilities, and applying the language to modelling real-world performance problems in hardware and software systems.
Stochastic process algebras are used in the new research area of Systems Biology to provide a component-based modelling approach which can be applied to increase our systems-level understanding of cellular processes. Languages such as the Stochastic pi-calculus and PEPA have been used to model signalling pathways in cells. Much work remains to be done in this area to produce formal languages which give a satisfactory account of the biological processes at work and which stand as working languages which can be used both by computer scientists and biologists. Formal treatments of the biological concepts of inhibition, stoichiometry and compartments have only been attempted and are examples of areas where significant research innovation and application is required. Similarly, mapping stochastic process algebras to ordinary differential equations in order to bridge between the working language of computer scientists and the working language of biologists has begun but much more needs to be done here.
Process calculi have traditionally been discrete-state modelling tools. These give precise characterisations of systems with a small number of abstractly-described components but cannot scale to large numbers of closely-described components. An alternative semantics which is based on continuous-state representations can scale to describe large populations of components but this comes at the cost of using an approximation to the true (discrete) behaviour. One process calculus which has been provided with a continuous-state semantics, the PEPA language, has already found many applications in theoretical computer science and systems biology. Much remains still to be done to understand and exploit further the great potential afforded by a continuous-state semantics. This project would investigate both the theoretical and the practical concerns of this theme, developing and using software tools to apply the research ideas to real-world examples.
Computer models are invaluable for analysing properties of systems. In model checking we explore the state spaces of systems exhaustively and can provide formal guarantees of system correctness. Model checking is used at Microsoft to check device drivers and at Intel to verify microprocessor designs. Abstraction and divide-and-conquer strategies help address the challenge of state space sizes which grow exponentially with system size. The aim of this project is to use a theorem prover to manage and enhance these strategies. Theorem provers are computer tools for rigorously checking mathematical arguments. They are harder to use than model checkers, but offer richer specification languages and a fuller range of reasoning techniques. One option with this project is to address models that include timed and stochastic aspects. This project may also be of interest to PhD students in CISA and ICSA.
Data exchange is one of the oldest data management problems. It arises every time when two or more legacy databases need to exchange information while their schemas cannot be changed. The main technical challenges are in building target database instances that correctly represent information from the source data, and in evaluating queries on such databases in a semantically correct manner. The goal of this project is to develop solid foundations for data exchange, concentrating on such critical issues as managing inherent incompleteness of information in data exchange and using it in query answering for both relational and XML databases.
The basic settings of the fields of database querying and verification/model-checking are very similar: in both cases one evaluates a logical formula on a finite structure (a query on a relational database, or a temporal formula on a Kripke structure). Both fields have invested heavily in developing logical formalisms and efficient algorithms for query evaluation and model checking, but despite this, there are very few direct connections between them (for example, we now know how temporal logics and navigation in XML documents are related). There are many more potential connections that have not received the attention they deserve: e.g., between streaming XML and verification of pushdown specifications or between database querying and verifying data-driven web services. One of my goals is to study these connections, with the ultimate goal of bringing the fields closer together. I am interested in students with good theoretical background (logic, automata, algorithms); knowledge of databases and verification is obviously a plus.
Computational Effects play a major role in programming languages, e.g., exceptions, side-effects, interactive input/output and probabilistic and ordinary nondeterminism. Recently an algebraic theory emphasising the operators that generate the effects has been developed. In another, but related direction, the Logic of Programs is in a fragmentary state with, e.g., LCF, Hoare logic and temporal logic being major but unrelated such logics. The proposed thesis will investigate a proposed unified logic of programs based on adding operators for effects to LCF, and a related general modal calculus for effects. There is a wide variety of possible research varying from theoretical to practical, and reasonably straightforward to very uncharted territory.
Many of the components needed for a complete, general and coherent theory of specification and formal development of modular software systems have emerged over the past decades. These include an understanding of: the structure of specifications and how this relates to the modular structure of programs; behavioural equivalence and its role in the implementation of data abstractions; stepwise refinement and implementation of specifications; parameterisation of specifications and program modules; proof in the context of structured specifications; and the degree to which such a theory can be made independent of the particular logical system used to write specifications. One missing component of this well-developed theory is a satisfactory treatment of behavioural equivalence in the context of (higher-order) parameterised program modules; other gaps concern the development of practical calculi for reasoning about correctness of such modules.
"Proof carrying code" (PCC) is an approach to security of mobile code whereby the downloaded code is equipped with an efficiently checkable certificate, in the form of a condensed mathematical proof, describing aspects of its behaviour. Advantages of PCC include the fact that it certifies intrinsic properties of code rather than merely its origin, and that it does not rely on a centralized certification authority. Mobile code is perfect for scientific computation on a distributed platform such as the Grid, where it is feasible to ship application code (say, 100KB) to the data (say, one of the multi-terabyte databases in the AstroGrid) but not vice versa. Work done on PCC for resource certification is being extended to the Grid context, by adapting it to Java-style object-oriented programming, and the resulting framework assessed by applying it to case studies in Grid-based scientific computation. See the Mobility + Security group's web page.
Portable devices with the capability to download code from remote sites are becoming commonplace, with examples including mobile phones, PDAs, and smart cards. This situation presents huge security challenges, and indeed the first mobile phone viruses have already appeared. "Proof carrying code" (PCC) is an approach to security of downloaded code whereby it is equipped with an efficiently checkable certificate, in the form of a condensed mathematical proof, describing aspects of its behaviour. Research on PCC has brought it to the point where it is ripe for serious experiments on portable devices. That is the objective of this project, together with work to extend the framework to cope with the deficiencies which such experiments are likely to expose. See the Mobility + Security group's web page.
Topology is well known as a subject with applications in many areas of mainstream mathematics. It is less known that the core concepts of topology can be given direct computational readings, leading to a topological analysis of computational phenomena (for example, computation on infinite data, such as data streams or real numbers, is necessarily continuous). At LFCS, we are studying the kinds of topological space that are appropriate for modelling computational behaviour, and the constructions on them that are needed to model computational notions such as: probabilistic choice, general computational effects (side effects, nondeterminism, continuations, ...), exact real-number computation, polymorphism, strictness, recursion, references, etc. The project currently involves Alex Simpson, Matthias Schröder and Ingo Battenfeld, and also has connections with the research interests of John Longley, Gordon Plotkin and John Power.
Constructive set theories provide one type of foundation for "constructive mathematics", a form of mathematics in which mathematical statements and proofs have built-in algorithmic content. In computer science, constructive set theories can be used as a tool for specification, synthesis and verification in formal program development. They can also be used to facilitate reasoning about programming features such as recursion and polymorphism. My research in this area includes: axiomatizing constructive set theories, realizability and category-theoretic models of constructive set theories (especially "algebraic set theory"), applications to programming language properties (especially via "synthetic domain theory"). Possible applications in pure mathematics (e.g. the "internalization" of arguments from the theory of fibrations) may also be interesting to investigate.
Formal verification of properties of programs, processes, systems, etc. is often based on unwieldy (though powerful) axiomatizations or rule systms formalized within (over-)expressive meta-logics, embedded within industrial-scale proof assistants or theorem provers. In some interesting cases, however, the structural techniques of proof theory can be applied to obtain elegant proof systems, with good meta-theoretic properties, tailored towards supporting a natural reasoning style for verification. Particular topics of interest in this area include: cyclic proof systems for induction and coinduction (avoiding explicit induction and counduction rules); proof systems for well-behaved (e.g. decidable) fragments of first- or higher-order logics (e.g. modal, monadic or guarded fragments); and modal logics for parallel processes, especially logics for name generation and mobility (this topic connects with the research interests of Ian Stark). I am also interested in the mathematical and philospohical foundations of proof theory, especially in the semantics of proof and in proof-theoretic accounts of logical meaning.
The various (irreversible) actions that take place during computation (e.g. side effects, nondeterminism, probabilistic choice, input/output, jumps) are known collectively as "computational effects". Such effects can be incorporated within the otherwise effect-free world of declarative programming (such as functional programming) via the use of type systems that distinguish between "effectful" and effect-free computation. The idea of using "computational monads" as a basis for such type systems was first proposed in the late 1980s by Eugenio Moggi (then at LFCS), an idea that has since been incorporated into the functional programming language Haskell by Phil Wadler (now at LFCS). In this area, I am particularly interested in type theories for investigating combinations of effects with explicit polymorphism (including parametricity), linearity (for expressing usage constraints on effects), recursion and dependent types. Other LFCS researchers interested in related topics include: John Longley, Gordon Plotkin, John Power, Ian Stark and Phil Wadler.
This project investigates fundamental models for concurrent and mobile computation; addressing in particular features that arise from the identity, distribution and mobility of both data and code. These kinds of computation are readily expressed in formal systems like CCS and the pi-calculus; and in programming languages and libraries inspired by them. Going beneath the syntax and concrete implementation, the project task is to build mathematical spaces of behaviour, and then interpret each process as an element in this space. This opens the possibility of more powerful analysis and investigation of what mobile processes can do, what what they cannot do, and what we can prove about them. This approach of denotational semantics is well established for sequential programming languages, but less so in the world of mobile computation and "programming the internet". For the specific case of the pi-calculus, there are already fully-abstract denotational models, based on indexed structures that capture the dynamically-changing configuration of processes. However, these are closely tied to that single calculus: what we need now is to take what has been learnt and apply it to other systems that take a different view on mobility and interaction. A first target is the join calculus: whose distinctive approach to wide-area concurrency has recently found its way into Microsoft's C-omega language.
Many convenient features of modern programming languages involve some notion of generativity: the idea that an entity (e.g. identifier, reference, object, exception, thread, channel, etc.) may be freshly created, distinct from all others. Such dynamic creations occur at a variety of levels, from the run-time behaviour of Lisp's "gensym", to resolving questions of scope during program linking. For sound design and correct implementation, it is essential to develop an appropriate abstract understanding of what it means to be new. The aim of this project is to study modal logics for the creation of new names; investigating possible definitions, semantics and proof theory. The work will draw on existing research at Edinburgh on models for names in programming languages and process calculi; systems like the nu-calculus and pi-calculus; and novel type theories for reasoning about names and binding.
"Bad smells" are informally defined attributes of a code base which suggest that the code may benefit from refactoring, such as code duplication, switch statements, and parallel class hierarchies. An obvious question is whether bad smells can be recognised automatically and even whether the code can be automatically refactored to eliminate the smells. The jCOSMO tool from CWI recognises certain bad smells automatically. However, in independent work Mantyla, Vanhanen and Lassenius found that there was poor correlation between bad smells as recognised by human developers and as recognised by their tools, even for smells chosen because they should be easy to recognise automatically. This intriguing finding suggests that the existence of a "bad smell" is more complex than at first appears. It raises, in turn, the question of whether bad smells do indeed indicate problem areas in code, and what the best combination of human and automatic inspection is. This project should investigate these issues systematically, and possibly go on to propose tool and/or methodology improvements. A promising arena is the collection of open source software held at sourceforge, and its developers.
Formal two-player games have a long history in computer science and outside. They have been applied in the verification of systems, where the players aim respectively to demonstrate a flaw in a system and to demonstrate that the system works as specified. In order to make calculations with such games feasible, it is essential to be able to use abstractions of the games: for example, one considers a large (perhaps infinite) class of game positions all together, until such time as distinctions between the positions force one to treat parts of the class differently. There is a considerable body of such work, which underpins some impressive tools. However, the field still lacks a principled, clean account of how games and their abstractions may be combined. This project should develop such an account.
Higher-order grammars and higher-order pushdown automata offer mechanisms for generating families of languages and families of infinite trees. Recent work has shown that model-checking, that is determining whether temporal properties are true of such structures, is decidable. However, equivalence questions for the deterministic case, whether two grammars or pushdown automata generate the same language or tree are open.
In January 2003 consumer spending on the web exceeded one billion pounds per month in Britain. Yet web programming remains an immature art, expensive and error prone. A web programmer must master a myriad of languages: the logic is written in a mixture of Java, Python, and Perl; the forms in HTML, XML, Javascript, and Flash; and the queries are written in SQL or XQuery. There is no easy way to link these - to be sure that a form in HTML or a query in SQL produces data of a type that the logic in Java expects. Links, a new language for web programming, use a single source for code to run on all three tiers. It compile into SQL or XQuery to run on back ends, and into Javascript, Flash, or Java to run on clients. It incorporates ideas from the functional languages Erlang, Haskell, Kleisli, ML, Scheme, and Xduce, applying today's theory to improve tomorrow's practice.
|
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 650 2690, Fax: +44 131 651 1426, E-mail: hod@inf.ed.ac.uk Please contact our webadmin with any comments or corrections. Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh |
