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
Games are a computational model used in computer science, economics, biology, and social sciences to name a few. The motivation for the present project arises from the area of multi-agent planning in artificial intelligence, but the results are applicable to other areas.
Given a description of the possible states of the game, of the states that are considered as winning positions, and of the actions that agents can take in each state, the basic problem is to find a winning strategy for a given agent coalition (a set of agents). Such a strategy specifies the actions that the coalition agents must take in each state, and guarantees that the coalition will end up in a winning state, regardless of the actions taken by agents outside the coalition. In the project, we focus on a slightly different problem, where the coalition is not given. Instead, we want to find the smallest size coalition which has a winning strategy. This is a computationally hard problem, so we will be building efficient algorithms which attempt to perform well on average. Such algorithms will use symbolic representations of set of states based on binary decision diagrams, and will automatically derive heuristics to guide the search from the description of the input game.
The student will start from a basic algorithm idea, which (s)he will flesh out, implement and extend to more complex cases such as: 1) computing a coalition of minimal cost, given a specification of the cost of collaboration, 2) partially observable games (agent decisions are based on partial information about the current state of the game), 3) more complex objectives than just reaching a winning state.
Contact:
Dr. Sylvie Thiebaux
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
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.
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. New projects based on student's ideas can also be considered. Students interested in AI planning are encouraged to enquire.
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
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 (not Y)) and (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.
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.
On the practical side, the student will have access to an existing simple (yet competitive) SAT solver, written in C++, and will modify it and conduct experiments to explore the possibilities of improving its performance. The final product could be either an extension of the existing solver or an entirely new solver, which can then be entered into next year's International SAT Competition.
Contact: Dr. Jinbo Huang
This compilation-based approach has greatly improved the efficiency and scalability of probabilistic reasoning with Bayesian networks, which has much in common with probabilistic planning. We would therefore like to investigate the possibility of carrying this success over to probabilistic planning. The main challenge would be to design and implement new domain encoding methods, and new algorithms to work with these encodings, that can solve a given type of planning task (e.g.,
conformant planning, contingent planning, etc.). The compilation part will be accomplished using an existing state-of-the-art knowledge compiler. The new planner implemented can then be entered into the next International Planning Competition.
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
In the ROSACE project, a high-level mission is expanded into a set of goals which are allocated to the robots. The robots must act cooperatively to achieve these goals, and this might require explicitly delegating subgoals to other robots. Cooperatively synthesizing plans of actions is still a largely open problem. The student will design and implement a cooperative and distributed version of a standard planning algorithm, and which guarantees certain properties (termination, correctness, etc). This will require becoming familiar with automated planning, constraint satisfaction and distributed search methods.
This project is best suited to a student with interest and background in artificial intelligence, distributed algorithms, and with good programming skills.
Contact:
Dr. Sylvie Thiebaux
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 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
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, DPO Group (ANU) & Managing Complexity (NICTA)
Computing the Smallest Winning Coalition in a Multi-Agent Game
Project Code: S_03
This topic is proposed as part of the French-Australian Science and Technology cooperation project "Planning Approaches to Sofware Verification", whose partners are INRIA, ANU, and UWA.
Supervisor: Dr. Sylvie Thiebaux, DPO Group (ANU) & Managing Complexity (NICTA)
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, DPO Group (ANU) & Managing Complexity (NICTA)
Dr. Anbulagan, DPO Group (ANU) & Managing Complexity (NICTA)
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, DPO Group (ANU) & Managing Complexity (NICTA)
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, DPO Group (ANU) & Managing Complexity (NICTA)
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 of 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.
Supervisor: Dr. Patrik Haslum, DPO Group (ANU) & Managing Complexity (NICTA)
Factored Planning
Project Code: S_08
Supervisors: Dr. Adi Botea and Dr. Sylvie Thiebaux, DPO Group (ANU) & Managing Complexity (NICTA)
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, DPO Group (ANU) & Managing Complexity (NICTA)
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, DPO Group (ANU) & Managing Complexity (NICTA)
How to Beat the World's Best Satisfiability Solvers
Project Code: S_11
Supervisor: Dr. Jinbo Huang, DPO Group (ANU) & Managing Complexity (NICTA)
Knowledge Compilation for Probabilistic Planning
Project Code: S_12
Probabilistic planning is concerned with domains where the agent wishes to achieve a goal with high probability when its initial state and/or action effects are probabilistic. It is possible to encode probability distributions, as well as the entire probabilistic planning domain, using propositional logic. One can then compile the logic into a special form that allows efficient inference. The key
is that the compilation can often be very efficient as it exploits the structure of the planning domain.
Supervisor: Dr. Jinbo Huang, DPO Group (ANU) & Managing Complexity (NICTA)
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, DPO Group (ANU) & Managing Complexity (NICTA)
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, DPO Group (ANU) & Managing Complexity (NICTA)
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, DPO Group (ANU) & Managing Complexity (NICTA)
Distributed Planning
Project Code: S_16
This topic is proposed as part of a collaboration with CNRS in the framework of the ROSACE project funded by the French Scientific and Technological Research Network for Aeronautics and Space. ROSACE studies the design, specification, implementation and deployment of a fleet of mobile autonomous cooperating robots with well-established properties particularly in terms of safety, self-healability, ability to achieve a set of missions and self-adaptation in a dynamic environment.
Supervisor: Dr. Sylvie Thiebaux, DPO Group (ANU) & Managing Complexity (NICTA)
Fast and Optimal Pathfinding on Game Maps
Project Code: S_17
Description and Goals
Supervisors: Dr. Adi Botea, DPO Group (ANU) & Managing Complexity (NICTA)
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_18
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, DPO Group (ANU) & Managing Complexity (NICTA)
Unifying Diagnosis of Discrete-Event Systems and First Principles
Project Code: S_19
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, DPO Group (ANU) & Managing Complexity (NICTA)
Observation Relaxations for Diagnosis of Discrete-Event Systems
Project Code: S_20
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, DPO Group (ANU) & Managing Complexity (NICTA)
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.
Application-Specific Control of SAT Algorithms
Project Code: P_01
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, DPO Group (ANU) & Managing Complexity (NICTA)
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_02
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, DPO Group (ANU) & Managing Complexity (NICTA)