No description available.

No description available.

No description available.

This research work is focused on understanding the effects of inhomogeneity on traffic flow by theoretical analysis and computer simulations. Traffic has been observed at almost all levels of natural and manmade systems (e.g., from microscopic protein motors to macroscopic objects like cars). For these various traffic, basic and emer- gent phenomena, modelling methods, theoretical analysis and physical meanings are normally concerned. Inhomogeneity like bottlenecks may cause traffic congestions or motor protein crowding. The crowded protein motors may lead to some human diseases. The congested traffic patterns have not been understood well so far. The modelling method in this research is based on totally asymmetric simple exclusion process (TASEP). The following TASEP models are developed: TASEP with single inhomogeneity, TASEP with zoned inhomogeneity, TASEP with junction, TASEP with site sharing and different boundary conditions. These models are motivated by vehicular traffic, pedestrian trafficc, ant traffic, protein motor traffic and/or Internet traffic. Theoretical solutions for the proposed models are obtained and verified by Monte Carlo simulations. These theoretical results can be used as a base for further developments. The emergent properties such as phase transitions, phase separations and spontaneous symmetry breaking are observed and discussed. This study has contributed to a deeper understanding of generic traffic dynamics, particularly, in the presence of inhomogeneity, and has important implications for explanation or guidance of future traffic studies.

One of the established strengths of human tutors is their ability to recognise and adapt to the emotions of students. This is a skill that has traditionally been lacking from Intelligent Tutoring Systems (ITSs); despite their ability to intelligently model and adapt to aspects of the student’s cognitive state, ITSs are generally completely unable to detect or adapt to aspects of the student’s affective state. In response to this shortcoming, this thesis explores the pioneering development of an emotion-sensitive ITS. With the empathy of effective human tutors as our blueprint, we investigate how an artificial tutor should adapt to the affective state of students, and develop an original affective tutoring strategies method. As a validation of the feasibility of an emotion-sensitive tutoring system, we implement and test our method in a functional Affective Tutoring System (ATS) for counting and addition, Easy with Eve, featuring an empathetic animated pedagogical agent, Eve. Eve is able to detect student affect using an in-house real time facial expression analysis system. To inform the system’s adaptation to student affect, the novel method for student modelling and emotion-sensitive tutoring strategies has been developed using a fuzzy, case-based reasoning approach. This approach is used to mine data about human tutor adaptations to student affect that was generated by an observational study of human tutors that was carried out in a local primary school. To test the impact of emotion detection and the presence of the animated agent, four different versions of the ATS were tested in local primary schools with a total of 59 participants. The findings from the study indicate that adding the detection of facial expressions to the student model did not improve student short-term performance, but there was mixed evidence that the presence of the animated agent Eve may cause students to perceive the system slightly more positively (a persona effect). This effect was marginally greater when the animated agent was enabled to detect and adapt to the affective state of students, which tentatively shows that emotion detection in an ATS may have a positive effect on student motivation.

The LEGO® MINDSTORMS® toolkit can be used to help students learn basic programming and engineering concepts. Software that is widely used with LEGO MINDSTORMS is ROBOLAB, developed by Professor Chris Rogers from Tufts University, Boston, United States. It has been adopted in about 10,000 schools in the United States and other countries. It is used to program LEGO MINDSTORMS robotics in its icon-based programming environment. However, this software does not provide debug features for LEGO MINDSTORMS programs. Users cannot test the program before downloading it into LEGO robotics hardware. In this project, we develop a simulator for LEGO MINDSTORMS to simulate the motions of LEGO robotics in a virtual 3D environment. We use ODE (Open Dynamic Engine) and OpenGL, combined with ROBOLAB. The simulator allows users to test their ROBOLAB program before downloading it into the LEGO MINDSTORMS hardware. For users who do not have the hardware, they may use the simulator to learn ROBOLAB programming skills which may be tested and debugged using the simulator. The simulator can track and display program execution as the simulation runs. This helps users to learn and understand basic robotics programming concepts. An introduction to the overall structure and architecture of the simulator is given and is followed by a detailed description of each component in the system. This presents the techniques that are used to implement each feature of the simulator. The discussions based on several test results are then given. This leads to the conclusion that the simulator is able to accurately represent the actions of robots under certain assumptions and conditions.

This thesis investigates a method for tackling the verification of parametric systems, systems whose behaviour may depend on the value of one or more parameters. The range of allowable values for such parameters may, in general, be large or unknown. This results in a large number of instances of a system that require verification, one instance for each allowable combination of parameter values. When one or more parameters are unbounded, the family of systems that require verification becomes infinite. Computer protocols are one example of such parametric systems. They may have parameters such as the maximum sequence number or the maximum number of retransmissions. Traditional protocol verification approaches usually only analyse and verify properties of a parametric system for a small range of parameter values. It is impossible to verify in this way every concrete instance of an infinite family of systems. Also, the number of reachable states tends to increase dramatically with increasing parameter values, and thus the well known state explosion phenomenon also limits the range of parameters for which the system can be analysed. In this thesis, we concentrate on the parametric verification of the Stop-and-Wait Protocol (SWP), an elementary flow control protocol. We have used Coloured Petri Nets (CPNs) to model the SWP, operating over an in-order but lossy medium, with two unbounded parameters: the maximum sequence number; and the maximum number of retransmissions. A novel method has been used for symbolically representing the parametric reachability graph of our parametric SWP CPN model. This parametric reachability graph captures exactly the infinite family of reachability graphs resulting from the infinite family of SWP CPNs. The parametric reachability graph is represented symbolically as a set of closed-form algebraic expressions for the nodes and arcs of the reachability graph, expressed in terms of the two parameters. By analysing the reachability graphs of the SWP CPN model for small parameter values, structural regularities in the reachability graphs were identified and exploited to develop the appropriate algebraic expressions for the parametric reachability graph. These expressions can be analysed and manipulated directly, thus the properties that are verified from these expressions are verified for all instances of the system. Several properties of the SWP that are able to be verified directly from the parametric reachability graph have been identified. These include a proof of the size of the parametric reachability graph in terms of both parameters, absence of deadlocks (undesired terminal states), absence of livelocks (undesirable cycles of behaviour from which the protocol cannot escape), absence of dead transitions (actions that can never occur) and the upper bounds on the content of the underlying communication channel. These are verified from the algebraic expressions and thus hold for all parameter values. Significantly, language analysis is also carried out on the parametric SWP. The parametric reachability graph is translated into a parametric Finite State Automaton (FSA), capturing symbolically the infinite set of protocol languages (i.e. sequences of user observable events) by means of similar algebraic expressions to those of the parametric reachability graph. Standard FSA reduction techniques were applied in a symbolic fashion directly to the parametric FSA, firstly to obtain a deterministic representation of the parametric FSA, then to obtain an equivalent minimised FSA. It was found that the determinisation procedure removed the effect of the maximum number of retransmissions parameter, and the minimisation procedure removed the effect of the maximum sequence number parameter. Conformance of all instances of the SWP over both parameters to its desired service language is proved. The development of algebraic expressions to represent the infinite class of Stop-and-Wait Protocols, and the verification of properties (including language analysis) directly from these algebraic expressions, has demonstrated the potential of this method for the verification of more general parametric systems. This thesis provides a significant contribution toward the development of a general parametric verification methodology.

Fusion Motion Capture (FMC), a wearable motion capture system was developed, and applied to the optimisation of athlete performance in alpine ski racing. In what may be a world first, the three-dimensional movements of a skilled athlete (with less than 20 FIS1 points) skiing through a complete training giant slalom racecourse were analysed. FMC consists of multiple light weight sensors attached to the athlete including inertial measurement units (IMUs), pressure sensitive insoles and a global position system (GPS) receiver. The IMUs contain accelerometers, gyroscopes, and magnetometers. Limb orientation and location are obtained by mathematically combining the most reliable data from each sensor using fusion algorithms developed by the author. FMC fuses the signals from the IMUs and GPS without the need for the post filtering, usually applied to motion capture data, and therefore, maintains maximum bandwidth. The FMC results were stable and relatively independent of motion type and duration unlike other inertial systems available in 2005, when the research was initiated. Analysis of data collected from an athlete skiing giant slalom contradict the traditional „going straight turning short? race strategy. The shortest path may not always be the fastest. Instead each gate has a different optimum approach arc. Optimum turn radius increases with both increasing speed and increasing terrain slope. The results also contradict laboratory measurements of ski/snow sliding friction and suggest that snow resistance in giant slalom is of similar importance to wind drag. In addition to gravity, the athlete increased speed using the techniques of „lateral projection? and „pumping?. Race performance was determined from the analysis of the athlete skiing through the entire course. FMC proved, therefore, to be more suitable than traditional optical systems that are practically limited to capturing small sections of a race course. The athlete experienced high and rapidly fluctuating torques about all three axes of the lower joints. This information could be useful in designing training programmes racecourses and equipment to reduce knee injuries. Data driven animations and colour coded force vector diagrams were developed to enhance athlete feedback. Inline skating data was also analysed.