This document contains topics for medium-length projects suitable for honours students and as shorter variants for summer scholars, Erasmus Mundus and other similar projects, as well as PhD thesis projects which take 3 years to complete. The list of PhD topics is incomplete: it is best to discuss the possible PhD thesis topics with the individual researchers by first contacting them by email.
If you want to start PhD studies you have to follow the ANU application procedures and contact a potential supervisor to write a research plan.
After the success of Binary Decision Diagrams (BDD) in computer-aided verification and many other areas, there has been a lot of interest in identifying other normal forms of propositional formulas (Boolean functions) for which efficient (polynomial time) algorithms exist for the basic operations required in these applications. Research in the last 8 years have led to the identification of Decomposable Negation Normal Form DNNF which is more compact but allows a slightly more narrow set of efficient (polynomial-time) operations.
In the standard framework of Boolean function representations based on the connectives for Disjunction, Conjunction and Negation, the least restrictive form is that of general NNF (Negation Normal Form). This normal form always leads to at least as succinct representations as BDD or DNNF.
A practically interesting problem is the identification of more efficient but not necessarily polynomial-time algorithms for the manipulation of general NNF formulas. In comparison to BDD or DNNF, NNF are sometimes exponentially more succint. The seemingly efficient operations on BDD or DNNF could be simply a result of these normal forms being less succinct: a non-polynomial operation on NNF could conceivably be in absolute terms more efficient than a polynomial operation on the exponentially bigger BDD or NNF.
This project is an investigation of operations on NNF that are in absolute terms equally or more efficient than the operations on the equivalent BDD or DNNF. We know that such operations exist, because one way of implementing these operations is to first translate the functions to BDD or DNNF and then use
the corresponding BDD or DNNF operations.
The goal of the work is the development of practically useful alternatives to BDD and DNNF representations that are based on the more succinct NNF.
Contact:
Dr. Jussi Rintanen
This project consists in picking up one (or more, depending on project time frame, problem difficulty, etc) of the commonly used planning benchmark domains that encode optimisation problems, and attack the underlying problem using whatever methods/tools seem most suitable, including for example LP/MILP, CSP/COP/SAT, local search methods, or anything else. The aim is to obtain a better understanding of the problems that underlie planning benchmarks -- how hard are they, in a practical, rather than complexity-theoretical, sense, and what instance parameters determine that hardness? how well do domain-independent planning systems compare, in terms of effectiveness and solution quality, to a domain-specific solution? -- but also to learn something about the different combinatorial optimisation technologies -- how difficult are they to apply to a given problem? which is more suited to what kind of problem?
Contact:
Dr. Patrik Haslum
Declarative (or partly declarative) representation of application knowledge in IT systems is an area of intense research. The goal is to reduce the need for tedious low-level programming in the delivery of complex IT systems. The means for achieving this goal are: high-level declarative representation of application knowledge, powerful algorithms for reasoning about this knowledge and using it in driving the procedures in the core of the IT system.
Existing Business Process Management Systems (BPMS) and Business Rule Management Systems (BRMS) are steps in this direction, but still cannot provide a highly automated and robust path from high-level knowledge and requirements to end-user applications.
The goal of the project is to investigate the declarative representation of the delivery of services in a chosen public sector application area (for example immigration (visas), taxation, social security) as well as the automatic derivation of procedures for delivering these services through the Internet or in desktop applications. The work is based on ideas similar to ones embodied in existing BRMS and BPMS, but takes them substantially further in terms of automation in the implementation end. The implementation of the procedures are based on combinatorial search algorithms that synthesize task sequences and business processes. A further goal is to generate processes that are provably optimal in the sense that the expected number of steps they require is the lowest possible.
Prequisites: basic knowledge of Knowledge Representation, Logic, Automated Reasoning, and Planning.
Contact:
Dr. Jussi Rintanen
Diagnosis is determining what happens on a system (car, plane,
telecommunication network, water supply network, etc.) from observations
on this system. This is an important task for monitoring and
maintenance of expensive or critical systems. The main difficulty is
usually to manage complexity. Discrete-event systems is a modeling of
dynamic systems based on discrete (i.e. not continuous) variables.
Satisfiability is the problem of determining if the variables of a given
Boolean formula can be assigned in such a way as to make the specified
formula evaluate to TRUE. This 50-years-old problem is still very
active and attracts a lot of attention as many problems in Computer
Science can be translated into SAT.
The possibilities of SAT solvers for diagnosis have not completely been
investigated. Extensions of the recent results in order to improve both
efficiency and expressiveness of this approach include:
A. Grastien, Anbulagan, J. Rintanen and E. Kelareva, Diagnosis of
discrete-event systems using satisfiability algorithms, Proceedings of
the 22nd AAAI Conference on Artificial Intelligence (AAAI-07), AAAI
Press, 2007
J. Rintanen and A. Grastien, Diagnosability testing with satisfiability
algorithms, in M. Veloso, ed., Proceedings of the 20th International
Joint Conference on Artificial Intelligence, pages 532-537, AAAI Press,
2007.
Contact: Dr. Alban Grastien
Symbolic techniques, and in particular BDD, were proved very efficient to solve many AI problems, and in particular the diagnosis. However, little was proposed on the topic of diagnosability using symbolic techniques. The goal of this project is to investigate this subject.
To start the project, the student will have to investigate the existing BDD packages. Then, the student will implement an existing BDD-based algorithm and test its efficient with respect to other algorithms. Many possible improvements will need to be investigated. When the student is more familiar with the topic, he will be ask to propose his own ideas. This subject is wide enough for a Ph.D topic.
References:
[Pen04] Y. Pencole. Diagnosability analysis of distributed discrete event systems. In European Conference on Artificial Intelligence (ECAI'04), pages 173178, 2004.
[Schu07] A. Schumann, Y. Pencole, and S. Thiebaux. A Spectrum of Symbolic On-line Diagnosis Approaches. 22nd American National Conference on Artificial Intelligence (AAAI-07), AAAI Press, Vancouver (Canada), July 2007.
Contact: Dr. Alban Grastien
Within the area of AI planning, a wide variety of projects are possible,
ranging from highly theoretical to practical, implementation-oriented,
and anywhere in between. For example:
Contact:
Dr. Patrik Haslum
Planning is the problem of finding a sequence of actions that reach a goal starting from a given initial state. Factored planning is a relatively new family of decomposition approaches which are useful when a problem is too large to be solved as one piece and has an appropriate structure.
There are many possible factored planning methods, and many ways of improving their performance. The project will consist in helping in the design and implementation of one such method.
We expect the applicants to have good programming and problem-solving skills and an interest in artificial intelligence. Joining this project is an excellent opportunity to learn about planning. Opportunities exits for further collaboration, for instance as an honours or PhD student.
Contact:
Dr. Adi Botea
Diagnosis and planning are two techniques at the core of the AI component of an immobot.
Diagnosis processes sensor data and makes inferences about the system status.
When a fault is detected, planning tells how to automatically reconfigure the system
back to a normal state.
The goal of the project is to design and implement a model that integrates planning and diagnosis.
The applicants should have good Java programming skills.
The project can be extended into an honours and/or PhD program.
Contact:
Dr. Adi Botea,
Dr. Alban Grastien
If the number of nodes in a graph is high, like tens of thousands or millions, and the graph is dense, then representing all the edges explicitly one at a time leads to very inefficient processing of the data. By recognizing regularities in the graph and utilizing the regularity to represent the graph more compactly, big improvements in efficiency can be obtained. One regularity in many big and dense graphs is the presence of complete bipartite subgraphs N,M in which there is an edge between every node in N and every node in M. Each such subgraph could be represented simply by representing N and M, without enumerating all the |N| X |M| edges explicitly. Another regularity, complete subgraphs (cliques), can be compactly represented in terms of bipartite subgraphs too.
The goal of the research is to develop efficient algorithms for compressing the representation of graphs by identifying complete bipartite subgraphs in them. Finding the maximal bipartite subgraph of a graph is an NP-hard problem. Some polynomial time approximation algorithms with approximation guarantees exist, but it seems that they are not very practical for graphs consisting of tens of thousands or millions of nodes.
The work will proceed by implementing and comparing existing approximation algorithms with and without approximation guarantees, and developing improvements to the existing algorithms and identifying heuristics for improving them.
Contact: Dr. Jussi Rintanen
Problems in many areas of AI and computer science can be reduced to SAT. Although SAT is NP-complete, problem instances arising from real-world applications often have special structure allowing them to be solved efficiently. Current SAT solvers are frequently able to solve instances with over a million variables.
This project will involve a review of the latest SAT technology, particularly a class of algorithms known as clause learning, followed by an attempt to advance the state of the art by proposing new algorithms or improvements to existing algorithms. The final product could be either an extension of an existing SAT solver or an entirely new solver, which may then be considered for entry into the next International SAT Competition.
Contact: Dr. Jinbo Huang
Desirable properties of a package repository include, for example, upgradeability, which ensures that the user can always upgrade a package to a newer version without having to remove previously installed packages that they need to use, although it may require the installation, upgrade, or replacement of other packages.
For large repositories and complex dependencies, such analysis can be a challenge. Some of these tasks are now well understood in formal terms. For example, package installability is known to be NP-complete and an encoding to SAT is known. The aim of this project is to extend the scope of this knowledge by formulating additional queries and properties encountered in package management in formal logic, and studying their theoretical complexity as well as practical solution methods.
Contact: Dr. Jinbo Huang
The goal of the project is to implement a very efficient planner
based on SAT/CSP technology by integrating the constraint solver
with the problem representation that is specific to planning problems.
This way it is possible to utilize constraint reasoning techniques
for planning more efficiently while still benefiting from powerful
inferences sanctioned by techniques like constraint propagation
and clause-learning.
Contact: Dr. Jussi Rintanen
Chronicles Recognition [Dousson, 2002] is a diagnosis technique that has
been successfully applied to several domains including the diagnosis of
telecommunication networks and the diagnosis of cardiac arrhytmia (see
for instance [Fromont et al., 2003]). Basically, a chronicle is a list
of temporally-constrainted events. A chronicle is recognised when an
instance of each event is found in the flow of observations that
satisfies the constraints. The chronicle are usually made ``by hand''.=20
Automatic generation of chronicles is challenging, although it has been
investigated for Petri-Nets-modelled system [Guerraz--Dousson, 2004] or
cardiac arrythmias (through Machine Learning techniques).
In this project, we propose to automatically generate chronicle-like
patterns from a finite-state-machine-based model. This task is
difficult as it must avoid ambiguities and false recognitions. The work
will be theoretical but also applied to the monitoring of mail servers.
References:
Elisa Fromont, Marie-Odile Cordier, Ren=E9 Quiniou, and Alfredo Hernandez:
Kardio and Calicot: a comparison of two cardiac arrhythmia classifiers ,
AIME'03 Workshop: Qualitative and Model-based Reasoning in Biomedicine
Christophe Dousson :
Extending and unifying chronicle representation with event counters, ECAI'02
Bruno Guerraz and Christophe Dousson
Chronicles Construction Starting from the Fault Model of the System to
Diagnose, DX'04
Contact:
Dr. Alban Grastien
The project is an investigation of implementation techniques for network-oriented
planning. The basis is a planning language which is based on a modal logic
for expressing network properties. The goal is the development of an efficient
planning system for this language by using heuristic search and the state space
representation of the planning problem.
The main goal of the project is an implemented planning system, but the topic
provides ample possibilities for more theoretical/analytical excursions
to more fundamental questions about network-oriented planning.
Contact:
Dr. Jussi Rintanen
The main problem of the MBD is the complexity of the task which is usually exponential in the number of components. It is possible to simplify the diagnosis task by reducing the accuracy of the diagnosis. Existing works includes determining the sub-system that is sufficient to ensure diagnosability. The basic technique to simplify the task is to reduce the quantity of information used by the diagnoser.
These works are still pretty limited and this proposal aims at addressing these limitations. We consider the detection of a single fault. Improvements include:
[P et al. 06] Y. Pencole, D. Kamenetsky, A. Schumann Towards low-cost diagnosis of component-based systems, 6th IFAC Symposium on Fault Detection, Supervision and Safety of Technical Process (SAFEPROCESS), Beijing, P.R. China August 29-September 1 ,2006
Contact: Dr. Alban Grastien
The classical model-based diagnosis technique is called /First Principles/ [Rei87]. It relies on the comparison of the expected output of a model of the system behaviour and the actual output of the system. If the outputs do not match, conflicts are computed and the diagnoses (possible sets of faults) are refined.
Discrete-event systems are dynamic system which can be modeled in a discrete manner, basically automata. A large literature exists for the diagnosis of discrete-event systems. The basic technique computes all the behaviours of the model that match the output of the system, and determine whether these behaviours are faulty.
For some historical reasons, the first principles were never used for diagnosis of discrete-event systems. However, current techniques show their limits as the increasing complexity of the systems makes it impossible to compute all behaviours consistent with the output.
In this project, we propose to investigate the use of first principles for diagnosis of discrete-event systems. This approach would allow to compute a limited number of behaviours, which was already proved successful for the SAT-based approach [GARK07]. This unification will provide clarification on how different are classical diagnosis and diagnosis of discrete-event systems. The notion of conflicts will also probably need to be extended.
[GARK07] A. Grastien, Anbulagan, J. Rintanen and E. Kelareva, Diagnosis of discrete-event systems using satisfiability algorithms, Proceedings of the 22nd AAAI Conference on Artificial Intelligence (AAAI-07), AAAI Press, 2007
[Rei87] R. Reiter, A theory of diagnosis from first principles, Artificial Intelligence Journal (AIJ), vol. 32, n 1, p. 57-95, 1987.
[BT08] E. Benazera and L. Trave-Massuyes, Generating Diagnoses from Conflicting Component Sets with Continuous Extents. 19th International Workshop on Principles of Diagnosis (DX-08), p. 23-30.
Contact: Dr. Alban Grastien
Contact: Dr. Alban Grastien
The thesis research addresses the problem of automatically deriving
the processes and procedures behind corporate IT systems.
The goal of the PhD thesis is to contribute to the development of
rigorous approaches to corporate data processing. This includes
research in most of the following problems.
An ideal PhD candidate would have a strong theoretical background in the theory of computation, automated reasoning, and search algorithms
as well as strong practical skills to apply the research to real world problems.
Contact:
Dr. Jussi Rintanen
The goal of the PhD thesis is to cover all aspects of application-specific
control of SAT solvers. This includes
An ideal PhD candidate would have a strong theoretical background in computational logic and some of its spplications as well as strong practical skills in applying them to real world problems, and also strong programming skills.
Contact:
Dr. Jussi Rintanen
An important extension of the SAT problem, QBF, is a natural basis for
solving many extended reasoning tasks for which SAT is not expressive
enough. The algorithmic basis of QBF is similar to SAT but not as
well understood.
For both SAT and QBF there currently exist no theory why the CDCL+restarts
based solvers work so well.
The goal of the thesis is to investigate the proof systems and proof
procedures for SAT and QBF and potentially develop new and more
efficient ones for both. The focus of the work will be in QBF solving,
but understanding the state of the art in both areas it will be
necessary to first establish a better understanding of the functioning
of algorithms for solving SAT as well.
Specific questions to be asked and answered include the following.
An ideal candidate for this project has a deep interest in
analytic questions about fundamental problems in computer science,
including complexity theory and NP-hardness, proof systems and
algorithms, and also strong practical skills in applying
the analytic skills for solving challenging theoretical and
practical problems.
Contact:
Dr. Jussi Rintanen
Within the area of AI planning, a wide variety of projects are possible,
ranging from highly theoretical to practical, implementation-oriented,
and anywhere in between. For example:
Various Combinatorial Optimisation Problems
Project Code: S_02
Although research in AI planning aims to construct fully general, domain-independent, planning systems, systems are often evaluated and compared by testing them on a collection of benchmark domains, accumulated over time by the research community. Many of these benchmarks resemble well-known combinatorial optimisation problems, such scheduling/sequencing, allocation, etc., or at least contain parts that do, but each also has its own peculiarities and tweaks. For a majority of benchmark domains, it is known that finding optimal solutions is difficult (NP-hard or worse) while just finding any solution is relatively easy (there exists efficient, and often simple, domain-specific algorithms), providing further evidence that the underlying problems encoded in these benchmark domains are, at heart, about optimisation.
Supervisor: Dr. Patrik Haslum
Declarative Business Processes in Delivery of Public Services
Project Code: S_03
Supervisor: Dr. Jussi Rintanen
Diagnosis by SAT Algorithms
Project Code: S_04
Recent works on diagnosis of discrete-event systems propose the use of
satisfiability algorithms for efficient computation.
Supervisors: Dr. Alban Grastien,
Dr. Anbulagan
References:
BDD for diagnosis and diagnosability
Project Code: S_05
Diagnosis is the problem of finding what happened in a system given a description of the general behaviour of the machine and observations of the current behaviour. Diagnosability is the problem of determining whether the diagnosis can always be found without ambiguity (possibly after some delay). We are here interested in so called Discrete Event Systems.
Supervisor: Dr. Alban Grastien
Artificial Intelligence in Video Games
Project Code: S_06
Video games are an excellent testbed for artificial intelligence research. They model real-life features such as uncertainty and dynamic worlds, and are suitable for several AI areas such as planning, learning and heuristic search. Commercial games are a fast-growing multi-billion dollar industry. The contacts between industry and academia are more and more present, stimulated in part by the newly created AIIDE conference, meant to bridge the gaps between the two communities.
We offer an opportunity to work on such an exciting application and possibly engage in a longer collaboration. Here are a few more concrete project ideas to begin with:
Supervisor: Dr. Adi Botea
We expect the applicants to have strong C++ programming skills and an interest in artificial intelligence.
Links:
Contact:
Dr. Adi Botea
Projects in Automated Planning
Project Code: S_07
Planning is a branch of AI concerned with automating the reasoning
that goes on in formulating plans, in the sense of a series of steps to
be taken, each of which has some effect on the state of (a highly abstract
model of) the world, so as to bring about some desired end state.
As a prototypical example, one may take single-player games ("puzzles")
such as the Freecell card game or the old Rubik's Cube. Possible
applications of automated planning methods (aside from solving puzzles)
are many and diverse: examples include airport ground traffic control,
computing genome edit distances, testing protocols for logical flaws,
or controlling a printer.
The aim of research in planning, as in many other branches of AI, is
to construct domain-independent ("universal") solutions for this kind of
problem. That is, rather than solving each application problem
individually, a general AI planning system should be able to solve any
one of them, provided a formal specification of the problem as input.
Several approaches to achieving this have been tried, such as different
variations of search, or recasting the problem as another kind of general
reasoning (e.g., a CSP, or logical deduction). Yet, efficient general
automated planning remains a challenge.
Supervisor: Dr. Patrik Haslum
New projects based on student's ideas can of course also be considered.
This, however, is not the only way of organising the computation
of a solution. In particular, in the two-pass scheme it is often
the case that the amount of information that needs to be passed
between neighbour nodes grows very large. It is possible that
using more passes, with less information exchanged each time, may
be more efficient.
A possible project is to implement and compare such different
variants of the factored planning method. Existing software provides
a lot of the required infrastructure.
A possible project is to investigate these cases, with the
aim of formulating a new sufficient tractability condition that
covers them. My current idea is that this may be possible by looking
at the structure of automata (which are used to represent information
about parts of the problem), and the conditions under which the
size of the product of two automata is linearly bounded. I would be
particularly interested in seeing if this can be connected to the
idea of using graph grammars to define restricted classes of planning
problems (see my ICAPS 2008 paper).
Existing methods for answering this question are all based on
exhaustive search, in one form or another, that is, one tries,
systematically and exhaustively, in all ways to find a plan, and if
no plan is found one can conclude that none exists. Such methods are
somewhat unsatisfactory: they scale up very poorly (in particular,
the difficulty of proving plan non-existence this way is related to
the size of the problem, but not to how complicated the reason for
non-existence is) and they fail to provide a succinct and understandable
explanation for the failure to construct a plan.
As an alternative, I am looking at methods that explicitly search
for a proof of plan non-existence. While I have some ideas for how
this can be done, they have yet to be put into practice. Thus, this
is (at the current stage) mostly an algorithm design and implementation
project.
The focus of this project can be either on the theoretical questions,
or on implementation and experimentation, or both.
Factored Planning
Project Code: S_08
Supervisors: Dr. Adi Botea and Dr. Sylvie Thiebaux
Immobile Robots: Integrating Diagnosis and Planning
Project Code: S_09
An immobile robot (immobot) is a real-life system (e.g., a power grid)
enhanced with AI capabilities for self control and self configuration.
Supervisors: Dr. Adi Botea and Dr. Alban Grastien
Algorithms for Finding Complete Bipartite Subgraphs
Project Code: S_10
Many applications require the representation of data or knowledge in the form of a binary relation or a graph, like "X knows Y" or "location X has a road connection to location Y".
Supervisor: Dr. Jussi Rintanen
Advances in Practical SAT Solving
Project Code: S_11
Satisfiability (SAT) is the problem of determining whether a Boolean formula can evaluate to true (i.e., be satisfied) under some assignment of truth values to its variables. For example, the formula ((X or Y or (not Z)) and ((not X) or (not Y) or (not Z))) can be satisfied by assigning false to all three variables.
Supervisor: Dr. Jinbo Huang
Logical Analysis of Software Package Management
Project Code: S_12
In software package management a major task is to maintain dependencies among packages when installing or removing packages while at the same time retaining certain desirable properties of the package repository. For example, installing a package X may require the removal of an existing package Y, but Y may be depended on by another existing package Z which cannot be removed. A possible solution may then lie in the fact that Z actually depends on the disjunction of Y and some W (that is, Z can survive with either Y or W). Hence replacing Y with W will resolve the dilemma.
Supervisor: Dr. Jinbo Huang
Constraint-Based Planning
Project Code: S_13
SAT and CSP are general framework for solving arbitrary problems
that can be viewed as constraint satisfaction. Best algorithms
for SAT/CSP are able to solve very challenging problems from
application areas such as diagnosis, model-checking and planning.
However, the use of generic SAT/CSP solvers has the drawback that
the utilization of heuristics and reasoning techniques specific
to application areas is very difficult. Therefore in some cases
it is a more efficient to implement specialized constraint solvers
for a problem representation specific to the application.
Supervisor: Dr. Jussi Rintanen
Chronicle Construction from FSM Model
Project Code: S_14
Diagnosis is determining what happens on a system (car, plane,
telecommunication network, water supply network, etc.) from observations
on this system. This is an important task for monitoring and maintenance
of expensive or critical systems.
Supervisor: Dr. Alban Grastien
Planning in Networks
Project Code: S_15
Many planning problems are about transportation networks, power distribution
networks, water distribution networks or connections (a binary relation)
between nodes in a network in general.
Existing planning languages poorly support network-oriented planning, which
motivates the introduction of expressive and efficient languages for expressing
and solving such planning problems.
Supervisor: Dr. Jussi Rintanen
Fast and Optimal Pathfinding on Game Maps
Project Code: S_16
Description and Goals
Supervisors: Dr. Adi Botea
Pathfinding involves computing a route between two given locations on a map,
while avoiding all obstacles.
The problem is important in many real-life applications, including games,
robotics, and GSP navigation.
Pathfinding problems are usually solved by running a search algorithm, such as A*.
A* is able to compute cost-optimal solutions but it can require significant memory and time resources.
Recent approaches use hierarachical abstraction to greatly speed up the process,
at the cost of losing the solution optimality guarantees.
In this project, we aim at designing a new algorithm that combines the speed of hierarchical methods
and the solution optimality guarantees of standard A*.
We do this starting from the observation that many path fragments are equivalent, and therefore there is no need to explore all of them.
Requirements
Student's gain
Contact: Dr. Adi Botea
Observability for Diagnosability
Project Code: S_17
Model-Based Diagnosis (MDB) is the problem of finding what happened in a system given a description of the general behaviour of the machine and observations of the current behaviour. An important property that is usually required is the so-called diagnosability. This property simply states that the failure will always be identified (possibly after some delay).
Supervisor: Dr. Alban Grastien
Unifying Diagnosis of Discrete-Event Systems and First Principles
Project Code: S_18
Diagnosis is the problem of determining whether a fault (unexpected yet unavoidable behaviour) occurred on a system, and if so to identify which fault and isolate on which part of the system.
Supervisor: Dr. Alban Grastien
Observation Relaxations for Diagnosis of Discrete-Event Systems
Project Code: S_19
Model-Based Diagnosis (MDB) is the problem of finding what happened in a system given a description of the general behaviour of the machine and observations of the current behaviour. System designers are more and more aware of the importance of diagnosis and include many sensors/logs on their system behaviours. Although this profusion of information makes the diagnosis more accurate, it becomes prohibitive to process. In this project, we propose to investigate techniques to determine which observations on the system are relevant for the diagnosis.
Supervisor: Dr. Alban Grastien
PhD Thesis Projects
Here are some topics for PhD thesis projects. If you are interested
in doing a PhD in our group, you can choose any topic that matches
our research interests.
Automated Synthesis of Workflows and Business Processes
Project Code: P_01
In corporate IT systems, including ones in public sector (government) systems,
there is a strong move to formalizing and automating the processes by
which services are delivered inside and outside the organization.
The emergence of Business Process Management Systems in a strong indication
of the underlying need to have a formal approach to the development
of IT systems.
Supervisor: Dr. Jussi Rintanen
The thesis research will have both strong analytic and practical components.
Parts of the work involves deriving new algorithms for
workflow and business processes synthesis, and these algorithms are to
be empirically evaluated.
The algorithmic work is supported by analytic investigations on the properties of the algorithms and the synthesis problems solved by them.
Application-Specific Control of SAT Algorithms
Project Code: P_02
The propositional satisfiability problem SAT has proved to be a flexible
and efficient way of representing and solving a wide range of problems in AI
and other areas of computer science. Best implementations of algorithms
for SAT rely on powerful general-purpose inference rules and heuristics.
The use of control knowledge and heuristics derived from a specific
application is a new and very promising research area which may
make SAT algorithms applicable to much more challenging problems
and make them competitive with specialized algorithms on much wider
classes of problems.
Supervisor: Dr. Jussi Rintanen
The thesis research will have both strong analytic and practical components.
Large part of the work is in deriving novel algorithmic techniques for SAT and understanding the behavior of SAT algorithms and the general SAT problem both analytically and empirically.
An equally important part is understanding the behavior of SAT algorithms with respect to concrete real-world applications like model-checking and AI planning.
Proof Systems and Proof Procedures for SAT and QBF
Project Code: P_03
The satisfiability problem SAT of the classical propositional logic
is a basis of many automated tools in computer-aided verification and
related problems, including the planning problem in AI. Current best
algorithms are based on conflict-directed clause learning CDCL which
has been shown to be more powerful as a proof system than the restricted
form of resolution on which the traditional Davis-Putnam-Logemann-Loveland
procedure is based. CDCL is typically combined with a rapid-restart
strategy for increased performance.
Supervisor: Dr. Jussi Rintanen
Projects in Automated Planning
Project Code: P_04
Planning is a branch of AI concerned with automating the reasoning
that goes on in formulating plans, in the sense of a series of steps to
be taken, each of which has some effect on the state of (a highly abstract
model of) the world, so as to bring about some desired end state.
As a prototypical example, one may take single-player games ("puzzles")
such as the Freecell card game or the old Rubik's Cube. Possible
applications of automated planning methods (aside from solving puzzles)
are many and diverse: examples include airport ground traffic control,
computing genome edit distances, testing protocols for logical flaws,
or controlling a printer.
The aim of research in planning, as in many other branches of AI, is
to construct domain-independent ("universal") solutions for this kind of
problem. That is, rather than solving each application problem
individually, a general AI planning system should be able to solve any
one of them, provided a formal specification of the problem as input.
Several approaches to achieving this have been tried, such as different
variations of search, or recasting the problem as another kind of general
reasoning (e.g., a CSP, or logical deduction). Yet, efficient general
automated planning remains a challenge.
Supervisor: Dr. Patrik Haslum
New projects based on student's ideas can of course also be considered.
This, however, is not the only way of organising the computation
of a solution. In particular, in the two-pass scheme it is often
the case that the amount of information that needs to be passed
between neighbour nodes grows very large. It is possible that
using more passes, with less information exchanged each time, may
be more efficient.
A possible project is to implement and compare such different
variants of the factored planning method. Existing software provides
a lot of the required infrastructure.
A possible project is to investigate these cases, with the
aim of formulating a new sufficient tractability condition that
covers them. My current idea is that this may be possible by looking
at the structure of automata (which are used to represent information
about parts of the problem), and the conditions under which the
size of the product of two automata is linearly bounded. I would be
particularly interested in seeing if this can be connected to the
idea of using graph grammars to define restricted classes of planning
problems (see my ICAPS 2008 paper).
Existing methods for answering this question are all based on
exhaustive search, in one form or another, that is, one tries,
systematically and exhaustively, in all ways to find a plan, and if
no plan is found one can conclude that none exists. Such methods are
somewhat unsatisfactory: they scale up very poorly (in particular,
the difficulty of proving plan non-existence this way is related to
the size of the problem, but not to how complicated the reason for
non-existence is) and they fail to provide a succinct and understandable
explanation for the failure to construct a plan.
As an alternative, I am looking at methods that explicitly search
for a proof of plan non-existence. While I have some ideas for how
this can be done, they have yet to be put into practice. Thus, this
is (at the current stage) mostly an algorithm design and implementation
project.
The focus of this project can be either on the theoretical questions,
or on implementation and experimentation, or both.