This thesis provides a powerful general-purpose proof technique for the verification of systems, whether finite or infinite. It extends the idea of finite local model-checking, which was introduced by Stirling and Walker: rather than traversing the entire state space of a model, as is done for model-checking in the sense of Emerson, Clarke et al. (checking whether a (finite) model satisfies a formula), local model-checking asks whether a particular state satisfies a formula, and only explores the nearby states far enough to answer that question. The technique used was a tableau method, constructing a tableau according to the formula and the local structure of the model. This tableau technique is here generalized to the infinite case by considering sets of states, rather than single states; because the logic used, the propositional modal mu-calculus, separates simple modal and boolean connectives from powerful fix-point operators (which make the logic more expressive than many other temporal logics), it is possible to give a relatively straightforward set of rules for constructing a tableau. Much of the subtlety is removed from the tableau itself, and put into a relation on the state space defined by the tableau-the success of the tableau then depends on the well-foundedness of this relation. This development occupies the second and third chapters: the second considers the modal mu-calculus, and explains its power, while the third develops the tableau technique itself The generalized tableau technique is exhibited on Petri nets, and various standard notions from net theory are shown to play a part in the use of the technique on nets-in particular, the invariant calculus has a major role. The requirement for a finite presentation of tableaux for infinite systems raises the question of the expressive power of the mu-calculus. This is studied in some detail, and it is shown that on reasonably powerful models of computation, such as Petri nets, the mu-calculus can express properties that are not merely undecidable, but not even arithmetical. The concluding chapter discusses some of the many questions still to be answered, such as the incorporation of formal reasoning within the tableau system, and the power required of such reasoning.

End-User privacy concerns surrounding use of Social Networks present new and complex problems for research. Specifically, a phenomenon known as “the Privacy Paradox” has been observed where end-users stated concerns, attitudes and intended behaviour are not consistent with the actual behaviour within the network. Numerous causes have been proposed as potentially being the root of the problem of this paradoxical phenomenon including a lack of user awareness of privacy issues, a low level skill in using technology or a lack of privacy salience within the social network itself. However, the role of the User Interface (UI) in contributing to, and potentially providing a solution to, poor privacy behaviour is under-explored. A potentially fruitful avenue of enquiry given that behaviour is considered to be a reaction to environmental stimulus and the UI provides the environment within which the user is interacting. This thesis implements a two phase approach to furthering understanding of privacy behaviour in social networks. First, a survey is implemented exploring the relationship of concepts within the privacy paradox identifying that users stated needs are not being met by their observable behaviour. Secondly, two experiments are implemented in order to explore this behaviour as an interaction with the network; these questions are answered to build a social network profile and can be grouped according to their potential sensitivity. A model of social psychology, the Theory of Planned Behaviour (TPB), is used to develop such experiments in order to examine the cognition behind these interactions. Each of the salient influencers defined by the TPB is used to inform a series of UI treatments and form the basis for experiment groups. An initial experiment explores the method and is used to inform the design of the second, which also introduces a factorial design to explore the relationships between treatments. These experiments show that participants within the treatment groups disclose less information than the control, with statistical significance. Within the first experiment this non-disclosure took place across all questions sensitivities, possibly due to limitations in the experimental method. However, participants in experiment two appear far more selective in their disclosure, choosing not to answer more sensitive questions suggesting that they thought of their privacy while interacting with the system. Findings within this thesis suggest that the UI plays an important role in influencing end-user behaviour as it can inform the context of the interaction as it happens.

Information Systems for complex situations often fail to adequately deliver quality and suitability. One reason for this failure is an inability to identify comprehensive user requirements. Seldom do all stakeholders, especially those „invisible‟ or „back room‟ system users, have a voice when systems are designed. If this is a global problem then it may impact on both the public and private sectors in terms of their ability to perform, produce and stay competitive. To improve upon this, system designers use rich pictures as a diagrammatic means of identifying differing world views with the aim of creating shared understanding of the organisation. Rich pictures have predominantly been used as freeform, unstructured tools with no commonly agreed syntax. This research has collated, analysed and documented a substantial collection of rich pictures into a single dataset. Attention has been focussed on three main research areas; how the rich picture is facilitated, how the rich picture is constructed and how to interpret the resultant pictures. This research highlights the importance of the rich picture tool and argues the value of adding levels of structure, in certain cases. It is shown that there are considerable benefits for both the interpreter and the creator by providing a pre-drawing session, a common key of symbols and a framework for icon understanding. In conclusion, it is suggested that there is some evidence that a framework which aims to support the process of the rich picture and aid interpretation is valuable.

This thesis asserts that modern developments in technology have not been used as extensively as they could to aid blind people in their learning objectives. The same could also be said of many aspects of other areas of their lives. In particular in many countries blind students are discouraged from learning mathematics because of the intrinsically visual nature of many of the topics and particularly geometry. For many young people mathematics is also not a subject that is easily or willingly tackled. The research presented here has thus sort to answer whether a playful haptic environment could be developed which would be attractive to blind users to learn and interact with geometric concepts. In the study a software tool using a haptic interface was developed with certain playful characteristics. The environment developed sought to give the blind users practice in interacting with three dimensional geometric shapes and the investigation of the size of these shapes and their cross-section. The playful elements were enhanced by adding elements of competition such as scores and time limits which promote competition between the users. The tests have shown that blind users can easily use the system to learn about three dimensional shapes and that practice increases their confidence in recognising shape and size of these objects.

Mobile notifications provide a unique mechanism for real-time information delivery systems to users in order to increase its effectiveness. However, real-time notification delivery to users via mobile phones does not always translate into users' awareness about the delivered information because these alerts might arrive at inappropriate times and situations. Moreover, notifications that demand users' attention at inopportune moments are more likely to have adverse effects and become a cause of potential disruption rather than proving beneficial to users. In order to address these challenges it is of paramount importance to devise intelligent notification mechanisms that monitor and learn users' behaviour for maximising their receptivity to the delivered information and adapt accordingly. The central goal of this dissertation is to build a framework for intelligent notifications that relies on the awareness of users' context and preferences. More specifically, we firstly investigate the impact of physical and cognitive contextual features on users' attentiveness and receptivity to notifications. Secondly, we construct and evaluate a series of models for predicting opportune moments to deliver notifications and mining users' notification delivery preferences in different situations. Finally, we design and evaluate a model for anticipating the right device notifications in cross-platform environments.

This thesis develops a new approach to evolving Binary Decision Diagrams, and uses it to study evolvability issues. For reasons that are not yet fully understood, current approaches to artificial evolution fail to exhibit the evolvability so readily exhibited in nature. To be able to apply evolvability to artificial evolution the field must first understand and characterise it; this will then lead to systems which are much more capable than they are currently. An experimental approach is taken. Carefully crafted, controlled experiments elucidate the mechanisms and properties that facilitate evolvability, focusing on the roles and interplay between neutrality, modularity, gradualism, robustness and diversity. Evolvability is found to emerge under gradual evolution as a biased distribution of functionality within the genotype-phenotype map, which serves to direct phenotypic variation. Neutrality facilitates fitness-conserving exploration, completely alleviating local optima. Population diversity, in conjunction with neutrality, is shown to facilitate the evolution of evolvability. The search is robust, scalable, and insensitive to the absence of initial diversity. The thesis concludes that gradual evolution in a search space that is free of local optima by way of neutrality can be a viable alternative to problematic evolution on multi-modal landscapes.

The topic of this thesis is users' models: the representations users may form of the computer system which they are interacting with. It has been proposed that user interfaces which support the construction of appropriate users' models facilitate learning and use of computer systems. Users' models have been a topic of research in human-computer interaction (HCI) since 1984, but to date, no knowledge exists which could be applied by designers of computer systems. The aim of the thesis is to address this problem and contribute to the development of an integrated and applicable body of knowledge on users' models. The thesis commences with an examination of the history and current state of the discipline of human-computer interaction to establish the context and determine the appropriate methods for conducting research on users' models. Since mental representations and mental models originate from the related disciplines of psychology and cognitive science, the review of the literature starts with an outline of the relevant theories, followed by a review of the theoretical and empirical work to date on users' model in HCI. The review concludes that more exploratory empirical work is required to obtain data from which evidence for, and descriptions of, users' models could be derived; however, suitable methods for eliciting and describing users' models have to be devised first. The second part of the thesis describes a series of five observational studies of users interacting with application software. The studies employed different scenarios, ranging from traditional experimental-style scenarios, with users working through a series of tasks, to constructive interaction scenarios, where users interacted with a co-investigator playing the role of a learner or co-learner. All studies were recorded on video, transcribed and analysed. Advantages and drawbacks of the scenarios for eliciting users' models are identified and discussed. The analysis of the tapes and transcripts provides some evidence of users' models; the conclusions of the thesis provide an outline of how theories regarding users' models can be formulated, and tested, using the data collected.

Automated decision support tools are designed to aid users and improve their performance in certain tasks by providing advice in the form of prompts, alarms, assessments, or recommendations. However, recent evidence suggests that sometimes use of such tools introduces decision errors that are not made without the tool. We refer to this phenomenon as “automation bias” (AB), resulting in a broader definition of this term than used by many authors. Sometimes, such automation-induced errors can even result in overall performance (in terms of correct decisions) which is actually worse with the tool than without it. Our literature review reveals an emphasis on mediators affecting automation bias and some mitigation strategies aimed at reducing it. However, there is a lack of research on the cognitive causal explanations for automation bias and on adaptive mitigation strategies that result in tools that adapt to the needs and characteristics of individual users. This thesis aims to address some of these gaps in the literature and focuses on systems consisting of a human and an automated tool which does not replace, but instead supports the human towards making a decision, with the overall responsibility lying with the human user. The overall goal of this thesis is to help reduce the rate of automation bias through a better understanding of its causes and the proposal of innovative, adaptive mitigation strategies. To achieve this, we begin with an extensive literature review on automation bias including examples, mediators, explanations, and mitigations while identifying areas for further research. This review is followed by the presentation of three experiments aimed at reducing the rate of AB in different ways: (1) an experiment to explore causal mechanisms of automation bias, the effect of the mere presence of tool advice before its presentation and the effect of the sequence of tool advice in a glaucoma risk calculator environment, (2) simulations that apply concepts of diversity to human + human systems to improve system performance in a breast cancer double reading programme, and (3) an experiment to study the possibility of improving system performance by tailoring tool setting (sensitivity / specificity combination) for groups of similarly skilled users and cases of similar difficulty level using a spellchecking tool. Results from the glaucoma experiment provide evidence of the effect of the presence of tool advice on user decisions - even before its presentation, as well as evidence of a newly introduced cognitive mechanism (users’ strategic change in decision threshold) which may account for some automation bias errors previously observed but unexplained in the literature. Results from the double reading experiment provide evidence of the benefits of diversity in improving system performance. Finally, results from the spell checker experiment provide evidence that groups of similarly skilled users perform better at different tool settings, that the same group of users perform better using a different tool setting in difficult versus easy tasks, and that use of simple models of user behaviour may allow the prediction, among a subset of tool settings for a certain tool, the tool setting that would be most appropriate for each user ability group and class of case difficulty.

Reduced Ordered Binary Decision Diagrams (ROBDDs) provide a dense and memory efficient representation of Boolean functions. When ROBDDs are applied in logic synthesis, the problem arises of detecting both classical and generalised symmetries. State-of-the-art in symmetry detection is represented by Mishchenko's algorithm. Mishchenko showed how to detect symmetries in ROBDDs without the need for checking equivalence of all co-factor pairs. This work resulted in a practical algorithm for detecting all classical symmetries in an ROBDD in O(|G|³) set operations where |G| is the number of nodes in the ROBDD. Mishchenko and his colleagues subsequently extended the algorithm to find generalised symmetries. The extended algorithm retains the same asymptotic complexity for each type of generalised symmetry. Both the classical and generalised symmetry detection algorithms are monolithic in the sense that they only return a meaningful answer when they are left to run to completion. In this thesis we present efficient anytime algorithms for detecting both classical and generalised symmetries, that output pairs of symmetric variables until a prescribed time bound is exceeded. These anytime algorithms are complete in that given sufficient time they are guaranteed to find all symmetric pairs. Theoretically these algorithms reside in O(n³+n|G|+|G|³) and O(n³+n²|G|+|G|³) respectively, where n is the number of variables, so that in practice the advantage of anytime generality is not gained at the expense of efficiency. In fact, the anytime approach requires only very modest data structure support and offers unique opportunities for optimisation so the resulting algorithms are very efficient. The thesis continues by considering another class of anytime algorithms for ROBDDs that is motivated by the dearth of work on approximating ROBDDs. The need for approximation arises because many ROBDD operations result in an ROBDD whose size is quadratic in the size of the inputs. Furthermore, if ROBDDs are used in abstract interpretation, the running time of the analysis is related not only to the complexity of the individual ROBDD operations but also the number of operations applied. The number of operations is, in turn, constrained by the number of times a Boolean function can be weakened before stability is achieved. This thesis proposes a widening that can be used to both constrain the size of an ROBDD and also ensure that the number of times that it is weakened is bounded by some given constant. The widening can be used to either systematically approximate an ROBDD from above (i.e. derive a weaker function) or below (i.e. infer a stronger function). The thesis also considers how randomised techniques may be deployed to improve the speed of computing an approximation by avoiding potentially expensive ROBDD manipulation.

The motivation for this thesis was the lack of any existing comprehensive framework or method to help developers with the evaluation or gathering of requirements and the evaluation or designing of technology solutions to accessible interactions between people, technology and objects, particularly in face-to-face situations involving people with disabilities. A Technology Enhanced Interaction Framework (TEIF) and TEIF Method for enhancing interactions with people, technology and objects through the use of technology was developed and successfully validated by three developer experts, three accessibility experts, and an HCI professor. The TEIF main components are people, objects, technology, interactions, time / place, and context while the TEIF Method involves requirement questions with multiple choice answers and technology suggestions, Interaction Diagrams and Use Case Diagrams. For evaluation of the TEIF Method, an example scenario involving a hearing impaired visitor to a Thai small local museum was developed along with corresponding requirement questions and answers, technology suggestions, technology solutions, an Interaction Diagram and a Use Case Diagram. While the TEIF has all the necessary components and sub components to be a general framework, the TEIF Method is focused on accessible interactions, and the content of the method used in this research was focused on people with hearing impairment because of time limitations. An experiment with 36 developers showed they were able to use the TEIF Method to evaluate requirements for technology solutions to problems involving interaction with hearing-impaired people better than the Other Methods. The TEIF Method helped developers select a best solution significantly more often than the Other Methods and rate the best solution significantly closer to expert ratings than the Other Methods. The TEIF Method also helped differentiation between solutions to be closer to experts’ differentiation than the Other Methods for some solutions and requirements. Questionnaire results showed that the developers thought that the TEIF Method helped to evaluate requirements and technology solutions to interaction problems involving hearing impaired people and would also help with gathering requirements and designing technology solutions for people with other disabilities. The developers also thought that the TEIF Method helped improve a developer’s awareness of interaction issues and understanding of how environment context affects interaction. Suggestions for future developments include extending the TEIF Method for other disabilities, including a more nuanced multi-level classification of how well different technologies meet different requirements and the use of the TEIF and TEIF Method as an index for case based solutions.