Although there have been numerous attempts to build and evaluate adaptive e-learning systems, they tend to be limited in scope, and suffer from a lack of carefully designed and controlled experimental evaluations of their effectiveness and usability. This thesis addresses these issues through the implementation of an adaptive e-learning system and its experimental validation. The design of an adaptive framework and the specific instantiation of its components into a configurable adaptive e-learning system are presented. The domain model of the system deals with computer security. The learner model incorporates the information perception dimension of the Felder-Silverman model of learning style and also knowledge level. The adaptation model generates personalised learning paths and offers adaptive guidance and recommendation. The thesis also provides an empirical evaluation through three controlled experiments to investigate the effect of different forms of adaptation. Rigorous experimental design, careful investigation and precise reporting of results are taken into account in all the three experiments. The findings indicate that matching the sequence of learning objects to the information perception learning style yields significantly better learning outcome and learner satisfaction than non-matching sequences. They also indicate that adaptation based on the combination of the information perception learning style and knowledge level yields significantly better learning outcome (both in the short- and long-term) and learner satisfaction than adaptation based on either of these learner characteristics alone; this combination is also marked by a significantly higher level of perceived usability compared to a non-adaptive version of the e-learning system.

The thesis presents verification of biometric authentication protocols. ProVerif is used as the verification tool for verifying and analysing the protocols. The protocol are analysed in ProVerif model. Various attacks to the protocols are generated in order to verify whether the protocols hold their intended properties. We have selected three biometric authentication protocols and proposed a remote biometric authentication protocol for on-line banking. Each of which has different intended purposes and properties. The first protocol is generic authentication using biometric data. This protocol provides three properties of the protocol: effectiveness, correctness, and privacy of biometric data. In addition, the protocol is clarified in order to verify the property of effectiveness. Details in chapter 3 show that without this clarification, the property of effectiveness would not hold. The second protocol is a biometric authentication protocol for a signature creation application. This is a specific purpose protocol that requires successfully biometric authentication in order to proceed the user's request, signing a document. The two properties of the protocol are verified: privacy of biometric data and intensional authentication. This protocol is used for signing a document using a user's private key. Hence, extension of the protocol is required so that the intensional authentication property can be verified. This property demonstrates that the legitimate user signs only the document that he intends to sign. A detailed description of this work can be found in chapter 4. The thesis further considers a remote biometric authentication protocol. Chapter 5 presents the protocol and verification of its desirable properties. This chapter shows analysis of the two properties of the protocol: privacy of biometric data and authenticity. Next, the thesis proposes a remote biometric authentication protocol for on-line banking in chapter 6. The protocol promises three intended properties: privacy of the biometric data, liveness of biometric data and intensional authentication. The protocol is illustrated in detail and desirable properties of the protocol are verified. Finally, chapter 7 concludes this study by briefly comparing properties that each protocol hold. Furthermore, we have identified the limitations of this thesis and possible areas for further research.

Many problems in the real world are multi-objective by nature, this means that many times there is the need to satisfy a problem with more than one goal in mind. These type of problems have been studied by economists, mathematicians, between many more, and recently computer scientists. Computer scientists have been developing novel methods to solve this type of problems with the help of evolutionary computation. Particle Swarm Optimisation (PSO) is a relatively new heuristic that shares some similarities with evolutionary computation techniques, and that recently has been successfully modified to solve multi-objective optimisation problems. In this thesis we first review some of the most relevant work done in the area of PSO and multi-objective optimisation, and then we proceed to develop an heuristic capable to solve this type of problems. An heuristic, which probes to be very competitive when tested over synthetic benchmark functions taken from the specialised literature, and compared against state-of-the-art techniques developed up to this day; we then further extended this heuristic to make it more competitive. Almost at the end of this work we incursion into the area of dynamic multi-objective optimisation, by testing the capabilities and analysing the behaviour of our technique in dynamic environments.

In operating systems such as Unix, processes can interact via signals. Signal handling resembles both exception handling and concurrent interleaving of processes. The handlers can be installed dynamically by the main program, but signals arrive non-deterministically; therefore, a handler may interrupt a program at any point. However, the interleaving of actions is not symmetric, in that the handler interrupts the main program, but not conversely. This thesis presents operational semantics and program logic for an idealized form of signal handling. To make signal handling logically tractable, we define handling to be block-structured. To reason about the interleaving of signal handlers, we adopt the idea of binary relations on states from rely-guarantee logics, imposing rely conditions on handlers. Given the one-way interleaving of signal handlers, the logic is less symmetric than rely-guarantee. We combine signal and exception handlers in the same language to investigate their interactions, specifically whether a handler can run more than once or is linearly used. We prove soundness of the program logic relative to a big-step operational semantics for signal handling. Then, we introduce and discuss reentrancy in various domains. Finally, we present our work towards logic with Reentrancy Linear Type System.

This thesis proposes a novel method for allocating multi-attribute computational resources via competing marketplaces. Trading agents, working on behalf of resource consumers and providers, choose to trade in resource markets where the resources being traded best align with their preferences and constraints. Market-exchange agents, in competition with each other, attempt to provide resource markets that attract traders, with the goal of maximising their profit. Because exchanges can only partially observe global supply and demand schedules, novel strategies are required to automate their search for market niches. By applying a novel methodology, which is also used to explore, for the first time, the generalisation ability of market mechanisms, novel attribute-level selection (ALS) strategies are analysed in competitive market environments. Results from simulation studies suggest that using these ALS strategies, market-exchanges can seek out market niches under a variety of environmental conditions. In order to facilitate traders' selection between dynamic competing marketplaces, this thesis explores the application of a reputation system, and simulation results suggest reputation-based market-selection signals can lead to more efficient global resource allocations in dynamic environments. Further, a subjective reputation system, grounded in Bayesian statistics, allows traders to identify and ignore the opinions of those attempting to falsely damage or bolster marketplace reputation.

Classical supervised learning from a training set of labelled examples assumes that the labels are correct. But in reality labelling errors may originate, for example, from human mistakes, diverging human opinions, or errors of the measuring instruments. In such cases the training set is misleading and in consequence the learning may suffer. In this thesis we consider probabilistic modelling of random label noise. The goal of this research is two-fold. First, to develop new improved algorithms and architectures from a principled footing which are able to detect and bypass the unwanted effects of mislabelling. Second, to study the performance of such methods both empirically and theoretically. We build upon two classical probabilistic classifiers, the normal discriminant analysis and the logistic regression and introduce the label-noise robust versions of these classifiers. We also develop useful extensions such as a sparse extension and a kernel extension in order to broaden applicability of the robust classifiers. Finally, we devise an ensemble of the robust classifiers in order to understand how the robust models perform collectively. Theoretical and empirical analysis of the proposed models show that the new robust models are superior to the traditional approaches in terms of parameter estimation and classification performance.

Many real-world optimization problems have multiple objectives that have to be optimized simultaneously. Although a great deal of effort has been devoted to solve multi-objective optimization problems, the problem is still open and the related issues still attract significant research efforts. Quantum-behaved Particle Swarm Optimization (QPSO) is a recently proposed population based metaheuristic that relies on quantum mechanics principles. Since its inception, much effort has been devoted to develop improved versions of QPSO designed for single objective optimization. However, many of its advantages are not yet available for multi-objective optimization. In this thesis, we develop a new framework for multi-objective problems using QPSO. The contribution of the work is threefold. First a hybrid leader selection method has been developed to compute the attractor of a given particle. Second, an archiving strategy has been proposed to control the growth of the archive size. Third, the developed framework has been further extended to handle constrained optimization problems. A comprehensive investigation of the developed framework has been carried out under different selection, archiving and constraint handling strategies. The developed framework is found to be a competitive technique to tackle this type of problems when compared against the state-of-the-art methods in multi-objective optimization.

It investigates systematically the reservoir construction of Echo State Network (ESN). This thesis proposes two very simple deterministic ESN organisation (Simple Cycle reservoir (SCR)) and Cycle Reservoir with Jumps (CRJ). Simple Cycle reservoir (SCR) is sufficient to obtain performances comparable to those of the classical ESN. While Cycle Reservoir with Jumps (CRJ) significantly outperform the those of the classical ESN. This thesis also studies and discusses three reservoir characterisations - short-term memory capacity (MC), eigen-spectrum of the reservoir weight matrix and Lyapunov Exponent with their relation to the ESN performance. It also designs and utilises an ensemble of ESNs with diverse reservoirs whose collective readout is obtained through Negative Correlation Learning (NCL) of ensemble of Multi-Layer Perceptrons (MLP), where each individual MPL realises the readout from a single ESN. Finally, this thesis investigates the relation between two quantitative measures characterising short term memory in input driven dynamical systems, namely the short term memory capacity (MC), and the Fisher memory curve (FMC).

This thesis presents two novel algorithms for monitoring plan execution in stochastic partially observable environments. The problems can be formulated as partially-observable Markov decision processes (POMDPs). Exact solutions of POMDP problems are difficult to find due to the computational complexity, so many approximate solutions are proposed instead. These POMDP solvers tend to generate an approximate policy at planning time and execute the policy without any change at run time. Our approaches will monitor the execution of the initial approximate policy and perform plan modification procedure to improve the policy’s quality at run time. This thesis considers two approximate POMDP solvers. One is a translation-based POMDP solver which converts a subclass of POMDP, called quasi-deterministic POMDP (QDET-POMDP) problems into classical planning problems or Markov decision processes (MDPs). The resulting approximate solution is either a contingency plan or an MDP policy that requires full observability of the world at run time. The other is a point-based POMDP solver which generates an approximate policy by utilizing sampling techniques. Study of the algorithms in simulation has shown that our execution monitoring approaches can improve the approximate POMDP solvers overall performance in terms of plan quality, plan generation time and plan execution time.

Traditionally, semantic trees have played an important role in proof theory for validating the unsatisfiability of sets of clauses. More recently, they have also been used to implement more practical tools for verifying the unsatisfiability of clause sets in first-order predicate logic. The method ultimately relies on the Herbrand Base, a set used in building the semantic tree. The Herbrand Base is used together with the Herbrand Universe, which stems from the initial clause set in a particular theorem. When searching for a closed semantic tree, the selection of suitable atoms from the Herbrand Base is very important and should be carried out carefully by educated guesses in order to avoid building a tree using atoms which are irrelevant for the proof. In an effort to circumvent the creation of irrelevant ground instances, a novel approach is investigated in this dissertation. As opposed to creating the ground instances of the clauses in S in a strict syntactic order, the values will be established through calculations which are based on relevance for the problem at hand. This idea has been applied and accordingly tested with the use of the Smart Semantic Tree Theorem Prover (SSTTP), which provides an algorithm for choos- ing prominent atoms from the Herbrand Base for utilisation in the generation of closed semantic trees. Part of this study is an empirical investigation of this prover performance on first-order problems without equality, as well as whether or not it is able to compete with modern theorem provers in certain niches. The results of the SSTTP are promising in terms of finding proofs in less time than some of the state-of-the-art provers. However, it can not compete with them in terms of the total number of the solved problems.