DSpace Community:
http://hdl.handle.net/2381/316
20170118T10:56:09Z

Temperature aware online algorithms for minimizing flow time
http://hdl.handle.net/2381/39199
Title: Temperature aware online algorithms for minimizing flow time
Authors: Birks, Martin; Fung, Stanley P. Y.
Abstract: We consider the problem of minimizing the total flow time of a set of unit sized jobs in a discrete time model, subject to a temperature threshold. Each job has its release time and its heat contribution. At each time step the temperature of the processor is determined by its temperature at the previous time step, the job scheduled at this time step and a cooling factor. We show a number of lower bound results, including the case when the heat contributions of jobs are only marginally larger than a trivial threshold. Then we consider a form of resource augmentation by giving the online algorithm a higher temperature threshold, and show that the Hottest First algorithm can be made 1competitive, while other common algorithms like Coolest First cannot. Finally we give some results in the offline case.
Description: A preliminary version of this paper appeared in the 10th Annual Conference on the Theory and Applications of Models of Computation (TAMC), 2013.
20170118T10:06:37Z

VOML: A Framework for Modelling Virtual Organizations and Virtual Breeding Environment
http://hdl.handle.net/2381/39111
Title: VOML: A Framework for Modelling Virtual Organizations and Virtual Breeding Environment
Authors: Rajper, N. J.; ReiffMarganiec, Stephan
Abstract: This paper presents the VOML (Virtual Organization Modelling Language) framework. VOML is a formal approach for specifying VOs (Virtual Organizations) and their VBEs (Virtual Breeding Environments).The VOML framework allows domain users to model a system in terms of their domain terminology and from that domain specific model IT community can derive a complete operational model closer to underlying execution environment. The framework is a collection of three sublanguages, each covering different aspects which are considered paramount at a particular level of VO representation. We present VOML and its underlying methodological approach in detail and demonstrate how to model VOs. Our focus will be on the methodological approach that VOML supports and on the language primitives that VOML offers for modelling VOs.
20170110T10:15:54Z

Relating two automatabased models of orchestration and choreography
http://hdl.handle.net/2381/39062
Title: Relating two automatabased models of orchestration and choreography
Authors: Basile, D.; Degano, P.; Ferrari, G. L.; Tuosto, E.
Abstract: We investigate the relations between two automatabased models for describing and studying distributed services, called contract automata and communicating machines. In the first model, distributed services are abstracted away as automata – oblivious of their partners – that coordinate with each other through an orchestrator. The second one is concerned with the interactions occurring between distributed services, that are represented by channelbased asynchronous communications; then services are coordinated through choreography.
We define a notion of strong agreement on contract automata; exhibit a natural mapping from this model to communicating machines with a synchronous semantics; and give conditions to ensure that strong agreement corresponds to wellformed choreography. Then these results are extended to a more liberal notion of agreement and to a fully asynchronous semantics of communicating machines.
20170104T16:46:32Z

Which Models of the Past Are Relevant to the Present? A software effort estimation approach to exploiting useful past models
http://hdl.handle.net/2381/39042
Title: Which Models of the Past Are Relevant to the Present? A software effort estimation approach to exploiting useful past models
Authors: Minku, Leandro L.; Yao, X.
Abstract: Software Effort Estimation (SEE) models can be used for decisionsupport by software managers to determine the effort required to develop a software project. They are created based on data describing projects completed in the past. Such data could include past projects from within the company that we are interested in (WC projects) and/or from other companies (crosscompany, i.e., CC projects). In particular, the use of CC data has been investigated in an attempt to overcome limitations caused by the typically small size of WC datasets. However, software companies operate in nonstationary environments, where changes may affect the typical effort required to develop software projects. Our previous work showed that both WC and CC models of the past can become more or less useful over time, i.e., they can sometimes be helpful and sometimes misleading. So, how can we know if and when a model created based on past data represents well the current projects being estimated? We propose an approach called Dynamic Crosscompany Learning (DCL) to dynamically identify which WC or CC past models are most useful for making predictions to a given company at the present. DCL automatically emphasizes the predictions given by these models in order to improve predictive performance. Our experiments comparing DCL against existing WC and CC approaches show that DCL is successful in improving SEE by emphasizing the most useful past models. A thorough analysis of DCL’s behaviour is provided, strengthening its external validity.
20170104T10:11:16Z

Uncovering Sustainability Concerns in Software Product Lines
http://hdl.handle.net/2381/39032
Title: Uncovering Sustainability Concerns in Software Product Lines
Authors: Chitchyan, Ruzanna; Groher, I.; Noppen, J.
Abstract: Sustainable living, i.e., living within the bounds of the available environmental, social, and economic
resources, is the focus of many presentday social and scientific discussions. But what does sustainability
mean within the context of Software Engineering? In this paper we undertake a comprehensive analysis
of 8 case studies to address this question within the context of a specific SE approach, Software Product
Line Engineering (SPLE). We identify the sustainabilityrelated characteristics that arise in presentday
studies that apply SPLE. We conclude that technical and economic sustainability are in prime focus on the
present SPLE practice, with social sustainability issues, where they relate to organisations, also addressed
to a good degree. On the other hand, the issues related to the personal sustainability are less prominent, and
environmental considerations are nearly completely amiss. We present feature models and crossrelations
that result from our analysis as a starting point for sustainability engineering through SPLE, suggesting
that any new development should consider how these models would be instantiated and expanded for the
intended sociotechnical system. The good representation of sustainability features in these models is also
validated with two additional case studies
Description: 12 months embargo
20170103T14:19:40Z

Nominal lambda calculus: An internal language for FMcartesian closed categories
http://hdl.handle.net/2381/38996
Title: Nominal lambda calculus: An internal language for FMcartesian closed categories
Authors: Crole, Roy L.; Nebel, Frank
Abstract: Reasoning about atoms (names) is difficult. The last decade has seen the development of numerous novel techniques. For equational reasoning, Clouston and Pitts introduced Nominal Equational Logic (NEL), which provides judgements of equality and freshness of atoms. Just as Equational Logic (EL) can be enriched with function types to yield the lambdacalculus (LC), we introduce NLC by enriching NEL with (atomdependent) function types and abstraction types. We establish metatheoretic properties of NLC; define cartesian closed categories, hence a categorical semantics for NLC; and prove soundness & completeness by way of NLCclassifying categories. A corollary of these results is that NLC is an internal language for cccs. A key feature of NLC is that it provides a novel way of encoding freshness via dependent types, and a new vehicle for studying the interaction of freshness and higher order types. © 2013 Elsevier B.V.
20161216T15:17:17Z

A low cost workload generation approach through the cloud for capacity planning in ServiceOriented Systems
http://hdl.handle.net/2381/38890
Title: A low cost workload generation approach through the cloud for capacity planning in ServiceOriented Systems
Authors: Ferreira, C. H. G.; Estrella, J. C.; Nunes, L. H.; ReiffMarganiec, Stephan; Batista, B. G.; Nakamura, L. H. V.; Leite, D.; Peixoto, M.; Libardi, R. M. D. O.
Abstract: This paper presents a cloud approach for low cost capacity
planning evaluations. To perform these evaluations we
have to specify and measure the workload on the target system
to discover issues and make the necessary adjustments.
However, due to high costs, these evaluations are usually
done using simulations, which does not consider stochastic
effects. We propose to use a tool named PEESOS, a generic
and flexible approach to apply real workloads and measure
used resources on these real systems. As a proof of concept,
our case study use a real ticket sales service to evaluate the
influence of scalability in the resource provisioning to show
how PEESOS can lower the cost of such real evaluations.
The results show the efficiency and savings that we can obtain
using PEESOS for largescale capacity planning evaluations
before the real services are deployed. This approach
can avoid several problems that real services faces when they
launch.
20161209T16:15:42Z

Towards a Distributed Runtime Monitor for ICS/SCADA Systems
http://hdl.handle.net/2381/38889
Title: Towards a Distributed Runtime Monitor for ICS/SCADA Systems
Authors: Wain, Andrew; ReiffMarganiec, Stephan; Janicke, H.; Jones, K.
Abstract: Industrial Control Systems (ICS) and SCADA (Supervisory Control and Data Acquisition) systems are
typically used in industries such as electricity generation and supply, gas supply, logistics, manufacturing
and hospitals and are considered critical national infrastructure. The evolution of these systems from
isolated environments into internet connected ones, in combination with their long service life and realtime
nature have raised severe security concerns in the event of a cyberattack. In this paper, we review
the current literature surrounding the threats, vulnerabilities, exploits and existing approaches to securing
vulnerable SCADA systems. We then focus specifically on the development of a distributed online runtime
monitor to detect violations of safety properties. We conclude with suggestions for further research needed
to progress the state of the art in the area of distributed online runtime verification of SCADA systems.
Description: Licence checked at http://www.bcs.org/upload/pdf/ewiclicence.pdf
20161209T16:10:14Z

Towards a Gamified Approach for Enhancing the VBE Preparedness for Establishing Virtual Collaborations
http://hdl.handle.net/2381/38888
Title: Towards a Gamified Approach for Enhancing the VBE Preparedness for Establishing Virtual Collaborations
Authors: Rajper, N.; ReiffMarganiec, Stephan; Nizamani, Q.
Abstract: Formation of collaborative settings (virtual organizations, collaborative network organizations, etcetera) is hindered by the lack of trust between unfamiliar but potential partners. Gamification is the application of game design principles to non game environments. We claim that incorporating the concepts of gamification into Virtual Organisation Breeding Environments (VBEs) leads to building trust between VBE members, as well as motivating them to be proactive members of the VBEs that contribute towards the flourishing of VBEs. This paper explores a novel gamified approach, supported by a suitable methodology, to address the relatively neglected concept of ‘preparedness’ of VBEs.
20161209T16:00:00Z

Towards a software framework for the autonomous internet of things
http://hdl.handle.net/2381/38887
Title: Towards a software framework for the autonomous internet of things
Authors: Hernandez, M. E. P.; ReiffMarganiec, Stephan
Abstract: IoT promises a world where Smart Objects (SO) are able to autonomously communicate and work together to make the (human) user's life easier. Popular approaches for development of IoT applications take for granted that onobject resources are evenly constrained. As consequence, we observe a trend towards a datafeeder architecture in which "smart objects" are simple data gatherers and senders. Raw data is stored and processed in cloud platforms feeding Web applications and services. The autonomy of SOs is then compromised as they are not able to operate without these platforms. We propose a framework and architecture for the development of IoT applications where smart objects exhibit autonomy in regards to platforms and human users. We completed the successful evaluation of our proposal with the implementation of a prototype and the execution of a use case for physical resources provisioning.
20161209T15:48:55Z

PEESOSCloud: a workloadaware architecture for performance evaluation in serviceoriented systems
http://hdl.handle.net/2381/38886
Title: PEESOSCloud: a workloadaware architecture for performance evaluation in serviceoriented systems
Authors: Ferreira, C. H. G.; Nunes, L. H.; Pereira Jr., L. A.; Nakamura, L. H.; Estrella, J. C.; ReiffMarganiec, Stephan
Abstract: It is a challenging task to ensure quality in serviceoriented systems deployed in cloud computing owing to the dynamicity of its environment. Many approaches have been adopted to identify and evaluate bottlenecks and problems in performance. The most common scenario consists of distributed systems that use a workload capable of enabling clients to exploit the target system in different operational conditions. However, one requirement that tends to be overlooked is to determine how the workload is executed, as software and hardware faults can lead to its mischaracterization. In this paper, a number of problems in the workload generation have been identified and summarized. A new architecture, called PEESOSCloud, is proposed which allows these services to be evaluated as well as to improve the ability of the workload so that it conforms with its described characteristics. Experiments in a cloud environment were conducted to show how PEESOSCloud works and validate its capabilities. Our experiment also showed that the mischaracterization of the workload leads to poor results, whereas an workloadaware implementation leads to a better performance evaluation.
20161209T15:40:29Z

Increasing Energy Efficiency on Smartphones through Data forecashing
http://hdl.handle.net/2381/38885
Title: Increasing Energy Efficiency on Smartphones through Data forecashing
Authors: Xu, J.; Yang, D.; Wang, J.; Guan, C.; ReiffMarganiec, Stephan; Shen, H.
Abstract: Smartphones are widely used in daily life to access
services and various functions require continuous communication,
which leads to increased energy consumption. However,
the development of battery and related energy saving technology
can not meet the demand for energy consumption. Much
of current research work focuses on energy models caring
much about energy consumption of every single application.
In this paper, we propose a data forecastingbased strategy for
increasing energy efficiency on smartphones based on the predictability
of data to be accessed. To achieve this, a combination
of Collaborative filtering with the kmeans algorithm categorize
users with similar user groups and speculate use increased for
the data users will access. With this model, we also adopt data
prestoring model and dynamic updating model. The simulation
results illustrate that our approach is leading to energy saving.
20161209T15:34:13Z

Cloud Simulator: A Cost Model Simulator Module for Cloudsim
http://hdl.handle.net/2381/38884
Title: Cloud Simulator: A Cost Model Simulator Module for Cloudsim
Authors: Alves, D. C.; Batista, B. G.; Macahdo, D. L.; ReiffMarganiec, Stephan; Kuehne, B. T.
Abstract: The vast cloud computing environment holds out good prospects for researchers in the computing technology field. However, with several Cloud providers offering different pricing models, the evaluation and modeling of Cloud environments and applications are getting harder because there is a lack of tools for this task. We propose the CM Cloud Simulator to fill this gap since it provides a comprehensive and dynamic simulation of applications with various deployment configurations and incurs the cost it would require when implemented in a Cloud Provider, according to the cost model of any service provider. The CM Cloud Simulator also provides custombuilt cost models through the XML file.
Description: Support information as well as the
CM Cloud Simulator code is available at
https://github.com/diegoca80/CloudModule.
20161209T15:25:27Z

Optimized Composite Service Transactions through Execution Results Prediction
http://hdl.handle.net/2381/38883
Title: Optimized Composite Service Transactions through Execution Results Prediction
Authors: Xu, J.; Li, Z.; Chi, H.; Wang, M.; Guan, C.; ReiffMarganiec, Stephan; Shen, H.
Abstract: Abstract:
Traditional web services transaction processing mechanism handle exception by forward recovery and backward recovery. These compensation mechanisms often lead to waste of resources and time. In this paper, we propose a framework for predicting outcomes of service executions as part of service compositions which allows to choose service instances that are likely to lead to a successful result in the first instance and thus reduces the need for invoking costly recovery mechanisms. The framework makes use of watchdogs to maintain an awareness of service availability and a precoordinator which has oversight of the whole composite Web service and acts as a control center. An analysis of a scenario shows that we cannot only provide users with a more satisfactory result, but also can reduce the overhead costs of resources and waste.
20161209T15:16:56Z

Towards an Offthecloud IoT data processing Architecture via a Smart Car Parking Example
http://hdl.handle.net/2381/38881
Title: Towards an Offthecloud IoT data processing Architecture via a Smart Car Parking Example
Authors: Alturki, Badraddin; ReiffMarganiec, Stephan
Abstract: Nowadays, it is obvious that technology has revolutionised our
lives by supporting us to do complicated jobs. The Internet of
Things (IoT) is one of the emerging technologies. One of the most
significant current research topics in the IoT is smart city. The
smart city includes several applications such assmart home, smart
industry and smart mobility. The smart car parking system is an
aspect of smart mobility and an important application in smart
city projects, because of the rapidly increasing number of cars in
urban areas. However, most of the current proposals in smart car
parking systems manage the data on the cloud side which is a
problem since the system needs to send the raw data from sensor
to cloud and receive instructions back: this is expensive in terms
of energy and data transmission cost. To tackle this issue we
present a proposal to save energy and to reduce the amount of data
that is transmitted over the network to cloud by processing closer
to source in this paper. The architecture is demonstrated through
a case study.
20161209T14:38:33Z

Characterizing word problems of groups
http://hdl.handle.net/2381/38806
Title: Characterizing word problems of groups
Authors: Jones, S. A. M.; Thomas, Richard M.
Abstract: The word problem of a finitely generated group is a fundamental notion in group theory; it can be defined as the set of all the words in the generators of the group that represent the identity element of the group. This definition allows us to consider a word problem as a formal language and a rich topic of research concerns the connection between the complexity of this language and the algebraic structure of the corresponding group.
Another interesting problem is that of characterizing which languages are word problems of groups. There is a known necessary and sufficient criterion for a language to be a word problem of a group; however a natural question is what other characterizations there are. In this paper we investigate this question, using sentences expressed in firstorder logic where the relations we consider are membership of the language in question and concatenation of words. We choose some natural conditions that apply to word problems and then characterize which sets of these conditions are sufficient to guarantee that the language in question really is the word problem of a group. We finish by investigating the decidability of these conditions for the families of regular and onecounter languages.
20161202T12:39:07Z

Relation lifting, a survey
http://hdl.handle.net/2381/38793
Title: Relation lifting, a survey
Authors: Kurz, Alexander; Velebil, J.
Abstract: We survey work in category theory and coalgebra on how to extend a functor from maps to relations. This relation lifting has a universal property, which is presented in some detail and guides us to generalisations to monotone and manyvalued relations. As applications, it is shown how different notions of bisimulation, simulation and modal logics do arise.
20161201T15:46:25Z

Foreword: special issue on coalgebraic logic
http://hdl.handle.net/2381/38792
Title: Foreword: special issue on coalgebraic logic
Authors: DOBERKAT, E. E.; KURZ, ALEXANDER
Abstract: The second Dagstuhl seminar on coalgebraic logics took place from October 7–12, 2012, in the Leibniz Forschungszentrum Schloss Dagstuhl, following a successful earlier one in December 2009. From the 44 researchers who attended and the 30 talks presented, this collection highlights some of the progress that has been made in the field. We are grateful to Giuseppe Longo and his interest in a special issue in Mathematical Structures in Computer Science.
20161201T15:42:55Z

Compact Dynamic Rewriteable (CDRW) Arrays
http://hdl.handle.net/2381/38769
Title: Compact Dynamic Rewriteable (CDRW) Arrays
Authors: Poyias, A.; Puglisi, S. J.; Raman, Rajeev
Abstract: In this paper we consider the problem of compactly representing
a rewritable array of bitstrings. The operations
supported are: create(N, k), which creates a new array of
size N, where each entry is of size at most k bits and equal
to 0; set(i, v), which sets A[i] to v, provided that v is at
most k bits long and get(i) which returns the value of A[i].
Our aim is to approach the minimum possible space bound
of S =
PN−1
i=0 A[i], where A[i] ≥ 1 is the length in bits of
the number in A[i], while simultaneously supporting operations
in O(1) time. We call such a data structure a Compact
Dynamic Rewriteable Array (CDRW) array.
On the word RAM model with word size w, for n < 2
w
and k ≤ w, we give practical solutions based on compact
hashing that achieve O(1/ ) expected time for get and set
and use (1 + )S + O(N) bits, for any constant > 0.
Experimental evaluation of our (preliminary, only somewhat
optimized) implementations shows excellent performance in
terms of both space and time, particularly when heuristics
are added to our base algorithms.
20161201T10:12:12Z

Asymptotically Optimal Encodings for Range Selection and Topk Queries
http://hdl.handle.net/2381/38768
Title: Asymptotically Optimal Encodings for Range Selection and Topk Queries
Authors: Grossi, R.; Iacono, J.; Navarro, G.; Raman, Rajeev; Satti, S. R.
Abstract: Given an array A[1, n] of elements with a total order, we consider the problem of building a
data structure that solves two queries: (a) selection queries receive a range [i, j] and an integer
k and return the position of the kth largest element in A[i, j]; (b) topk queries receive [i, j] and
k and return the positions of the k largest elements in A[i, j]. These problems can be solved in
optimal time, O(1 + lg k/ lg lg n) and O(k), respectively, using linearspace data structures.
We provide the first study of the encoding data structures for the above problems, where A
cannot be accessed at query time. Several applications are interested in the relative order of the
entries of A, and their positions, rather their actual values, and thus we do not need to keep A
at query time. In those cases, encodings save storage space: we first show that any encoding
answering such queries requires n lg k − O(n + k lg k) bits of space; then, we design encodings
using O(n lg k) bits, that is, asymptotically optimal up to constant factors, while preserving
optimal query time.
20161201T09:47:09Z

Foundations of session types and behavioural contracts
http://hdl.handle.net/2381/38761
Title: Foundations of session types and behavioural contracts
Authors: Hüttel, H.; Lanese, I.; Vasconcelos, V. T.; Caires, L.; Carbone, M.; Deniélou, P. M.; Mostrous, D.; Padovani, L.; Nióravara, A.; Tuosto, Emilio; Vieira, H. T.; Zavattaro, G.
Abstract: Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This article surveys the main accomplishments of the last 20 years within these two approaches.
Description: Categories and Subject Descriptors: F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs;
D.3.3 [Programming Languages]: Language Constructs and Features; D.2.4 [Software Engineering]:
Software/Program Verification
20161129T15:45:36Z

The Effect of Dyadic Interactions on Learning Rotate Gesture for TechnologyNaïve Older Adults
http://hdl.handle.net/2381/38756
Title: The Effect of Dyadic Interactions on Learning Rotate Gesture for TechnologyNaïve Older Adults
Authors: Mihajlov, M.; Law, Effie LaiChong; Springett, M.
Abstract: Older adults having limited experience with modern
computing technology may find it difficult to learn touch
gestures, especially the more complex rotate gesture. Social
interactions, as implied by social constructivism, are
assumed to be powerful in enabling older adults to acquire
the skill of touch gestures. The social effect can be reinforced
with the motivational effect of digital games. To verify the
assumption, we conducted empirical studies with 59 older
adults, who were divided into two groups: 17 Singles and 21
Dyads. They were asked to play a set of digital games on a
multitouch tabletop. Results show that on average Dyads
have spent significantly longer time in the games and have
performed a significantly higher number of correct rotate
gestures than Singles. Future work focuses on analyzing the
emotional aspect of social interactions and identifying
further applications of social gaming to other ageing issues.
20161129T12:13:45Z

Compressed bit vectors based on variabletofixed encodings
http://hdl.handle.net/2381/38749
Title: Compressed bit vectors based on variabletofixed encodings
Authors: Jo, S.; Joannou, Stelios; Okanohara, D.; Raman, Rajeev; Satti, S. R.
Abstract: We consider practical implementations of compressed bitvectors, which support rank and select
operations on a given bitstring, while storing the bitstring in compressed form. Our approach
relies on variabletofixed encodings of the bitstring, an approach that has not yet been considered
systematically for practical encodings of bitvectors. We show that this approach leads to fast
practical implementations with low redundancy (i.e., the space used by the bitvector in addition
to the compressed representation of the bitstring), and is a flexible and promising solution to
the problem of supporting rank and select on moderately compressible bitstrings, such as those
encountered in realworld applications.
Description: Also Conference Paper in Proceedings of the Data Compression Conference March 2014 DOI: 10.1109/DCC.2014.85
20161129T11:01:01Z

BTR: training asynchronous Boolean models using singlecell expression data.
http://hdl.handle.net/2381/38718
Title: BTR: training asynchronous Boolean models using singlecell expression data.
Authors: Lim, C. Y.; Wang, H.; Woodhouse, S.; Piterman, Nir; Wernisch, L.; Fisher, J.; Göttgens, B.
Abstract: BACKGROUND: Rapid technological innovation for the generation of singlecell genomics data presents new challenges and opportunities for bioinformatics analysis. One such area lies in the development of new ways to train gene regulatory networks. The use of singlecell expression profiling technique allows the profiling of the expression states of hundreds of cells, but these expression states are typically noisier due to the presence of technical artefacts such as dropouts. While many algorithms exist to infer a gene regulatory network, very few of them are able to harness the extra expression states present in singlecell expression data without getting adversely affected by the substantial technical noise present. RESULTS: Here we introduce BTR, an algorithm for training asynchronous Boolean models with singlecell expression data using a novel Boolean state space scoring function. BTR is capable of refining existing Boolean models and reconstructing new Boolean models by improving the match between model prediction and expression data. We demonstrate that the Boolean scoring function performed favourably against the BIC scoring function for Bayesian networks. In addition, we show that BTR outperforms many other network inference algorithms in both bulk and singlecell synthetic expression data. Lastly, we introduce two case studies, in which we use BTR to improve published Boolean models in order to generate potentially new biological insights. CONCLUSIONS: BTR provides a novel way to refine or reconstruct Boolean models using singlecell expression data. Boolean model is particularly useful for network reconstruction using singlecell data because it is more robust to the effect of dropouts. In addition, BTR does not assume any relationship in the expression states among cells, it is useful for reconstructing a gene regulatory network with as few assumptions as possible. Given the simplicity of Boolean models and the rapid adoption of singlecell genomics by biologists, BTR has the potential to make an impact across many fields of biomedical research.
Description: The haematopoietic data, which include two Boolean models [38, 39] and the two datasets [10] are included in the BTR package, and are also available in their respective publications. BTR is available as an R package on CRAN and also on Github [https://github.com/cheeyeelim/btr] [49]. All data and scripts that are used to generate results in this paper are available either as part of the BTR package or at [https://github.com/cheeyeelim/btr_resultscripts] [50].
20161125T09:48:49Z

Diversifying Software Architecture for Sustainability: A Valuebased Perspective
http://hdl.handle.net/2381/38708
Title: Diversifying Software Architecture for Sustainability: A Valuebased Perspective
Authors: Sobhy, D.; Bahsoon, R.; Minku, Leandro; Kazman, R.
Abstract: We use real options theory to evaluate the options of diversity
in design by looking at the tradeoffs between the cost and longterm
value of different architectural strategies under uncertainty, given a set
of scenarios of interest. As part of our approach, we extend one of the
widely used architecture tradeoffs analysis methods (CostBenefit Analysis
Method) to incorporate diversification. We also use a case study
to demonstrate how decision makers and architects can reason about
sustainability using a diversified costvalue approach.
20161123T17:09:55Z

SIGACT News Online Algorithms Column 28: Online Matching on the Line, Part 2
http://hdl.handle.net/2381/38659
Title: SIGACT News Online Algorithms Column 28: Online Matching on the Line, Part 2
Authors: Van Stee, Rob
Abstract: In the online matching problem on the line, requests (points in R) arrive one by one to be
served by a given set of servers. Each server can be used only once. This is a variant of the kserver
problem restricted to the real line. Although easy to state, this problem is stil wide open. The best
known lower bound is 9.001 [2], showing that this problem is really different from the wellknown
cow path problem. Antoniadis et al. [1] recently presented a sublinearly competitive algorithm.
In this column, I present some results by Elias Koutsoupias and Akash Nanavati on this problem
with kind permission of the authors. The column is based on Akash’ PhD thesis [4], which contains
an extended version of their joint WAOA 2003 paper [3] which has never appeared in a journal. I
have expanded the proofs and slightly reorganized the presentation.
The previous column (see SIGACT News 47(1):99111) contains a proof of a linear upper bound
for the generalized work function algorithm and a logarithmic lower bound for the algorithm. This
column gives a more detailed analysis of this algorithm, leading to a different (but again linear)
upper bound. The techniques used here may potentially be helpful to show a sublinear upper bound
for γwfa. I conjecture that this algorithm in fact has a logarithmic competitive ratio (which would
match the known lower bound for it), but this very much remains an open question.
Description: The final published version is available through the links above.
20161121T16:27:44Z

The Effects of Relative Importance of User Constraints in Cloud of Things Resource Discovery: A Case Study
http://hdl.handle.net/2381/38618
Title: The Effects of Relative Importance of User Constraints in Cloud of Things Resource Discovery: A Case Study
Authors: Nunes, L. H.; Estrella, J. C.; Perera, C.; ReiffMarganiec, Stephan; Delbem, A. N.
Abstract: Over the last few years, the number of smart objects
connected to the Internet has grown exponentially in comparison
to the number of services and applications. The integration
between Cloud Computing and Internet of Things, named as
Cloud of Things, plays a key role in managing the connected
things, their data and services. One of the main challenges in
Cloud of Things is the resource discovery of the smart objects
and their reuse in different contexts. Most of the existent work
uses some kind of multicriteria decision analysis algorithm to
perform the resource discovery, but do not evaluate the impact
that the user constraints has in the final solution. In this paper,
we analyse the behaviour of the SAW, TOPSIS and VIKOR
multiobjective decision analyses algorithms and the impact
of user constraints on them. We evaluated the quality of the
proposed solutions using the Paretooptimality concept.
Description: 12 month embargo from publication
20161118T09:18:07Z

Multicriteria IoT Resource Discovery: A Comparative Analysis
http://hdl.handle.net/2381/38617
Title: Multicriteria IoT Resource Discovery: A Comparative Analysis
Authors: Nunes, L. H.; Estrella, J. C.; Perera, C.; ReiffMarganiec, Stephan; Delbem, A. N.
Abstract: The growth of real world objects with embedded and globally networked sensors allows to consolidate
the Internet of Things paradigm and increase the number of applications in the domains of ubiquitous and
contextaware computing. The merging between Cloud Computing and Internet of Things named Cloud of
Things will be the key to handle thousands of sensors and their data. One of the main challenges in the Cloud
of Things is contextaware sensor search and selection. Typically, sensors require to be searched using two
or more conflicting context properties. Most of the existing work uses some kind of multicriteria decision
analysis to perform the sensor search and selection, but does not show any concern for the quality of the
selection presented by these methods. In this paper, we analyse the behaviour of the SAW, TOPSIS and
VIKOR multiobjective decision methods and their quality of selection comparing them with the Paretooptimality
solutions. The gathered results allow to analyse and compare these algorithms regarding their
behaviour, the number of optimal solutions and redundancy.
Description: 12 months embargo from publication
20161118T09:09:25Z

An Abstract Semantics of the Global View of Choreographies
http://hdl.handle.net/2381/38559
Title: An Abstract Semantics of the Global View of Choreographies
Authors: Guanciale, R.; Tuosto, Emilio
Abstract: We introduce an abstract semantics of the global view of choreographies. Our semantics is given in terms of preorders and can accommodate different lower level semantics. We discuss the adequacy of our model by considering its relation with communicating machines, that we use to formalise the local view. Interestingly, our framework seems to be more expressive than others where semantics of global views have been considered. This will be illustrated by discussing some interesting examples.
Description: In Proceedings ICE 2016, arXiv:1608.03131
20161115T14:45:30Z

On undefined and meaningless in Lambda definability
http://hdl.handle.net/2381/38557
Title: On undefined and meaningless in Lambda definability
Authors: De Vries, FerJan
Abstract: We distinguish between undefined terms as used in lambda definability of partial recursive functions and meaningless terms as used in infinite lambda calculus for the infinitary terms models that generalise the Böhm model. While there are uncountable many known sets of meaningless terms, there are four known sets of undefined terms. Two of these four are sets of meaningless terms. In this paper we first present set of sufficient conditions for a set of lambda terms to serve as set of undefined terms in lambda definability of partial functions. The four known sets of undefined terms satisfy these conditions. Next we locate the smallest set of meaningless terms satisfying these conditions. This set sits very low in the lattice of all sets of meaningless terms. Any larger set of meaningless terms than this smallest set is a set of undefined terms. Thus we find uncountably many new sets of undefined terms. As an unexpected bonus of our careful analysis of lambda definability we obtain a natural modification, strict lambdadefinability, which allows for a Barendregt style of proof in which the representation of composition is truly the composition of representations.
Description: 1998 ACM Subject Classification F.4.1 [Mathematical Logic] lambda calculus and related systems
20161115T14:35:59Z

Engineering Requirements for Social Sustainability
http://hdl.handle.net/2381/38328
Title: Engineering Requirements for Social Sustainability
Authors: Al Hinai, Maryam; Chitchyan, Ruzanna
Abstract: Software is no longer a passive tool, but is an active agent in shaping modern communities. Yet, to date, software engineers do not endeavour to explicitly state requirements which a software system must fulfil if it is to positively contribute to the wellbeing (that is the social sustainability) of its user community. This paper presents a proposal on how to bridge this gap. It notes that social sustainability requirements stem from key societal values, such as equity, security, education, which can be elicited into value patterns. Such patterns can then serve as templates for software requirements specification. The viability of this proposal is demonstrated through formation of equity value patterns, which are instantiated as requirements to 6 sample studies. We observe that while each organisation and subcommunity will have own diverse cultural and traditional values with respective requirements, the fundamental notions (such as equity, security, freedom) that serve as the core of social sustainability remain relatively stable. It is such values that we propose to elicit into patterns for requirements specification.
20161103T10:29:17Z

A Search Based Approach for StressTesting Integrated Circuits
http://hdl.handle.net/2381/38327
Title: A Search Based Approach for StressTesting Integrated Circuits
Authors: Eljuse, Basil; Walkinshaw, Neil
Abstract: In order to reduce software complexity and be power efficient, hardware platforms are increasingly incorporating functionality that was traditionally administered at a softwarelevel (such as cache management). This functionality is often complex, incorporating multiple processors along with a multitude of design parameters. Such devices can only be reliably tested at a ‘system’ level, which presents various testing challenges; behaviour is often nondeterministic (from a software perspective), and finding suitable test sets to ‘stress’ the system adequately is often an inefficient, manual activity that yields fixed test sets that can rarely be reused. In this paper we investigate this problem with respect to ARM’s Cache Coherent Interconnect (CCI) Unit. We present an automated searchbased testing approach that combines a parameterised testgeneration framework with the hillclimbing heuristic to find test sets that maximally ‘stress’ the CCI by producing much larger numbers of data stall cycles than the corresponding manual test sets.
20161103T10:10:09Z

A Distributed Sensor Data Search Platform for Internet of Things Environments
http://hdl.handle.net/2381/38324
Title: A Distributed Sensor Data Search Platform for Internet of Things Environments
Authors: Nunes, Luiz H.; Estrella, Júlio C.; Nakamura, Luis H. V.; Libardi, Rafael M. de O.; Ferreira, Carlos H. G.; Jorge, Liuri L. R.; Perera, Charith; ReiffMarganiec, Stephan
Abstract: Recently, the number of devices has grown increasingly and it is hoped that, between 2015 and 2016, 20 billion devices will be connected to the Internet and this market will move around 91.5 billion dollars. The Internet of Things (IoT) is composed of small sensors and actuators embedded in objects with Internet access and will play a key role in solving many challenges faced in today's society. However, the real capacity of IoT concepts is constrained as the current sensor networks usually do not exchange information with other sources. In this paper, we propose the Visual Search for Internet of Things (ViSIoT) platform to help technical and nontechnical users to discover and use sensors as a service for different application purposes. As a proof of concept, a real case study is used to generate weather condition reports to support rheumatism patients. This case study was executed in a working prototype and a performance evaluation is presented.
20161102T16:43:01Z

Proof Transformation via Interpretation Functions: Results, Problems and Applications
http://hdl.handle.net/2381/38301
Title: Proof Transformation via Interpretation Functions: Results, Problems and Applications
Authors: Kosiuczenko, Piotr
Abstract: Change is a constant factor in Software Engineering process. Redesign of a class structure requires transformation of the corresponding OCL constraints. In a previous paper we have shown how to use, what we call, interpretation functions for transformation of constraints. In this paper we discuss recently obtained results concerning proof transformations via such functions. In particular we detail the fact that they preserve proofs in equational logic, as well as proofs in other logical systems like propositional logic with modus ponens or proofs using resolution rule. Those results have direct applications to redesign of UML State Machines and Sequence Diagrams. If states in a State Machine are interpreted by State Invariants, then the topological relations between its states can be interpreted as logical relations between the corresponding formulas. Preservation of the consequence relation can bee seen as preservation of the topology of State Machines. We indicate also an unsolved problem and discuss the mining of its positive solution.
20161031T15:15:55Z

Resamplingbased ensemble methods for online class imbalance learning
http://hdl.handle.net/2381/38239
Title: Resamplingbased ensemble methods for online class imbalance learning
Authors: Wang, Shuo; Minku, Leandro L.; Yao, Xin
Abstract: Online class imbalance learning is a new learning problem that combines the challenges of both online learning and class imbalance learning. It deals with data streams having very skewed class distributions. This type of problems commonly exists in realworld applications, such as fault diagnosis of realtime control monitoring systems and intrusion detection in computer networks. In our earlier work, we defined class imbalance online, and proposed two learning algorithms OOB and UOB that build an ensemble model overcoming class imbalance in real time through resampling and timedecayed metrics. In this paper, we further improve the resampling strategy inside OOB and UOB, and look into their performance in both static and dynamic data streams. We give the first comprehensive analysis of class imbalance in data streams, in terms of data distributions, imbalance rates and changes in class imbalance status. We find that UOB is better at recognizing minorityclass examples in static data streams, and OOB is more robust against dynamic changes in class imbalance status. The data distribution is a major factor affecting their performance. Based on the insight gained, we then propose two new ensemble methods that maintain both OOB and UOB with adaptive weights for final predictions, called WEOB1 and WEOB2. They are shown to possess the strength of OOB and UOB with good accuracy and robustness.
20161024T15:38:20Z

Inferring Computational State Machine Models from Program Executions
http://hdl.handle.net/2381/38231
Title: Inferring Computational State Machine Models from Program Executions
Authors: Walkinshaw, Neil; Hall, Msthew
Abstract: The challenge of inferring state machines from log
data or execution traces is wellestablished, and has led to the
development of several powerful techniques. Current approaches
tend to focus on the inference of conventional finite state machines
or, in few cases, state machines with guards. However, these ma
chines are ultimately only partial, because they fail to model how
any underlying variables are computed during the course of an
execution; they are not
computational
. In this paper we introduce
a technique based upon Genetic Programming to infer these
data transformation functions, which in turn render inferred
automata fully computational. Instead of merely determining
whether or not a sequence is possible, they can be simulated, and
be used to compute the variable values throughout the course of
an execution. We demonstrate the approach by using a Cross
Validation study to reverseengineer complete (computational)
EFSMs from traces of established implementations.
20161024T13:30:50Z

Online and Verification Problems under Uncertainty
http://hdl.handle.net/2381/38096
Title: Online and Verification Problems under Uncertainty
Authors: Charalambous, George
Abstract: In the under uncertainty setting we study problems with imprecise input data for which precise data can be obtained. There exists an underlying problem with a feasible solution, but is computable only if the input is precise enough. We are interested in measuring how much of the imprecise input data has to be updated in order to be precise enough. We look at the problem for both the online and the offline (verification) cases. In the verification under uncertainty setting an algorithm is given imprecise input data and also an assumed set of precise input data. The aim of the algorithm is to update the smallest number of input data such that if the updated input data is the same as the corresponding assumed input data (i.e. verified), a solution for the underlying problem can be calculated. In the online adaptive under uncertainty setting the task is similar except the assumed set of precise data is not given to the algorithm, and the performance of the algorithm is measured by comparing the number of input data that have been updated against the result obtained in the verification setting of the same problem.
We have studied these settings for a few geometric and graph problems and found interesting results. Geometric problems include several variations of the maximal points problem where, in its classical form, given a set of points in the plane we want to compute the set of all points that are maximal. The uncertain element here is the actual location of each point. Graph problems include a few variations of the graph diameter problem where, in its classical form, given a graph we want to calculate a farthest pair of vertices. The uncertain element is the weight of each edge.
20160926T11:40:14Z

DirectionReversible SelfTimed Cellular Automata for DelayInsensitive Circuits
http://hdl.handle.net/2381/38087
Title: DirectionReversible SelfTimed Cellular Automata for DelayInsensitive Circuits
Authors: Ulidowski, Irek; Morrison, Daniel
Abstract: We introduce a new SelfTimed Cellular Automaton capable of simulating reversible delayinsensitive circuits. In addition to a number of reversibility and determinism properties, our STCA exhibits directionreversibility, where reversing the direction of a signal and running a circuit forwards is equivalent to running the circuit in reverse. We define also several extensions of the STCA which allow us to realise three larger classes of delayinsensitive circuits, including parallel circuits. We then show which of the reversibility, determinism and directionreversibility properties hold for these classes of circuits
20160916T14:24:29Z

Reordering Buffer Management with Advice
http://hdl.handle.net/2381/38076
Title: Reordering Buffer Management with Advice
Authors: Van Stee, Rob; Rosen, Adi; Adamaszek, Anna; Renault, Marc. P.
Abstract: In the reordering buffer management problem, a sequence of colored items arrives at a service station to be processed. Each color change between two consecutively processed items generates some cost. A reordering buffer of capacity k items can be used to preprocess the input sequence in order to decrease the number of color changes. The goal is to find a scheduling strategy that, using the reordering buffer, minimizes the number of color changes in the given sequence of items. We consider the problem in the setting of online computation with advice. In this model, the color of an item becomes known only at the time when the item enters the reordering buffer. Additionally, together with each item entering the buffer, we get a fixed number of advice bits, which can be seen as information about the future or as information about an optimal solution (or an approximation thereof) for the whole input sequence. We show that for any ε>0 there is a (1+ε)competitive algorithm for the problem which uses only a constant (depending on ε) number of advice bits per input item. This also immediately implies a (1+ε)approximation algorithm which has 2O(nlog1/ε) running time (this should be compared to the trivial optimal algorithm which has a running time of kO(n)). We complement the above result by presenting a lower bound of Ω(logk) bits of advice per request for any 1competitive algorithm.
Description: Following the embargo period the above license applies.
20160914T13:15:12Z

Collaborative annotation, search and categorisation
http://hdl.handle.net/2381/38032
Title: Collaborative annotation, search and categorisation
Authors: Hong, Yi
Abstract: The purpose of this research is to develop a collaborative framework for annotation,
search and categorisation. The basis of this research is to define an ontologybased data
model that allows users to create semantic tags, establish relationships among tags
and provide contextual information by hierarchical concepts and properties structure
derived from a lexical knowledge base. A computational model is introduced to record
uncertainty, establish user credibility and compute the truthfulness or reliability of the
statements, which can then be used for ranking search results. A method to transform
a relational database to the ontologybased repository is developed to populate the
proposed data model. The second stage of the research is to develop an expressive yet
intuitive querying technique for searching semantically annotated data. There are many
questions that arise when querying complex datasets. For example, how to help average
nontech users to write queries without excessive reliance on external technical support?
How to utilise a rich knowledge base and how to enable members of a collaborative
team to construct queries collectively, considering their opinions on the importance of
searching criteria? Traditional keywordbased or formbased approaches fail to address
these issues due to lack of expressive power or flexibility. A visual querying technique is
presented for the collaborative team, based on graph pattern matching. This method
allows members of a collaborative team to collectively construct complex queries in
a more convenient manner. Then the possibility of applying various categorisation
techniques to help sort annotated objects is investigated. A new workflow model is
proposed that help a collaborative team build a universallyaccepted categorisation
system and develop a systematic way for team members to create a training data
set, taking into account various criteria and degrees of uncertainty in human decisionmaking.
Eventually, a modified Naive Bayes classifier was built for storing a large
number of objects. In the end, in collaboration with members of an archaeological
research team, a series of experiments was conducted to evaluate our methodologies.
20160909T10:59:24Z

Activation Network Problems
http://hdl.handle.net/2381/37966
Title: Activation Network Problems
Authors: Alqahtani, Hasna Mohsen H.
Abstract: Network design problems traditionally are modelled by a graph where each edge (or node) has a fixed cost. We investigate optimization problems in a realistic model for wireless network design called activation network. The activation network setting can be defined as follows. We are given a directed or undirected graph G = (V, E) together with a family {fuv : (u, v) E E} of monotone nondecreasing activation functions from D² to {0, 1}, where D is a constantsize subset of the nonnegative real numbers, such that the activation of an edge depends on the chosen values from the domain D at its endpoints. An edge (u, v) E E is activated for chosen values xᵤ and xᵥ if fᵤᵥ(xᵤ, xᵥ) = 1, and the activation function fᵤᵥ is called monotone nondecreasing if fᵤᵥ (xᵤ, xᵥ) = 1 implies fᵤᵥ (yᵤ, yᵥ) = 1 for any yᵤ ≥ xᵤ, yᵥ ≥ xᵥ. The objective of activation network problems is to find activation values xᵥ E E for all v E V such that the total activation cost ∑ᵥEᵥ xᵥ is minimized and the activated set of edges satisfies some connectivity requirements. We give a 1:5approximation algorithm for the minimum activation cost of k nodedisjoint stpaths (stMANDP) when k = 2. We also show that a papproximation algorithm for the stMANDP problem implies a papproximation algorithm for solving the minimum activation cost of k edgedisjoint stpaths (stMAEDP) problem when k = 2. We propose polynomial time algorithms that optimally solve the stMANDP, stMAEDP, minimum activation Steiner tree and the problem of finding minimum activation cost nodedisjoint paths between k disjoint terminal pairs for graphs with treewidth bounded by a constant. We also study the stMANDP, stMAEDP, minimum spanning activation tree and minimum activation arborescence problems for the special case where D = 2 and all edges have the same activation function.
20160815T15:39:46Z

Discovering "unknown known" security requirements
http://hdl.handle.net/2381/37936
Title: Discovering "unknown known" security requirements
Authors: Rashid, Awais; Naqvi, Syed Asad Ali; Ramdhany, Rajiv; Edwards, Matthew; Chitchyan, Ruzanna; Babar, M. Ali
Abstract: Security is one of the biggest challenges facing organisations in the modern hyperconnected world. A number of theoretical security models are available that provide best practice security guidelines and are widely utilised as a basis to identify and operationalise security requirements. Such models often capture highlevel security concepts (e.g., whitelisting, secure configurations, wireless access control, data recovery, etc.), strategies for operationalising such concepts through specific security controls, and relationships between the various concepts and controls. The threat landscape, however, evolves leading to new tacit knowledge that is embedded in or across a variety of security incidents. These unknown knowns alter, or at least demand reconsideration of the theoretical security models underpinning security requirements. In this paper, we present an approach to discover such unknown knowns through multiincident analysis. The approach is based on a novel combination of grounded theory and incident fault trees. We demonstrate the effectiveness of the approach through its application to identify revisions to a theoretical security model widely used in industry.
20160809T13:41:42Z

Requirements: The Key to Sustainability
http://hdl.handle.net/2381/37935
Title: Requirements: The Key to Sustainability
Authors: Becker, Christoph; Betz, Stefanie; Chitchyan, Ruzanna; Duboc, Leticia; Easterbrook, Steve M.; Penzenstadler, Birgit; Seyff, Norbert; Venters, Colin C.
Abstract: Software's critical role in society demands a paradigm shift in the software engineering mindset. This shift's focus begins in requirements engineering. This article is part of a special issue on the Future of Software Engineering.
20160809T13:13:22Z

Generalised distributivity and the logic of metric spaces
http://hdl.handle.net/2381/37701
Title: Generalised distributivity and the logic of metric spaces
Authors: Babus, Octavian Vladut
Abstract: The aim of the thesis is to work towards a manyvalued logic over a commutative unital quantale and, at the same time, towards a generalisation of coalgebraic logic enriched over a commutative unital quantale Ω. This is done by noticing that the contravariant powerset adjunction can be generalised to categories enriched over a commutative unital quantale. From here we define categorical algebras for the monad generated by this adjunction. We finish by showing that these categorical algebras are algebras over Set with operations and equations, and show that in some cases we can restrict the arity of those operations to be finite.
20160608T09:27:55Z

Descriptions of Groups using Formal Language Theory
http://hdl.handle.net/2381/37684
Title: Descriptions of Groups using Formal Language Theory
Authors: Rino Nesin, Gabriela Asli
Abstract: This work treats word problems of finitely generated groups and variations thereof, such as word problems of pairs of groups and irreducible word problems of groups. These problems can be seen as formal languages on the generators of the group and as such they can be members of certain wellknown language classes, such as the class of regular, onecounter, contextfree, recursively enumerable or recursive languages, or less well known ones such as the class of terminal Petri net languages. We investigate what effect the class of these various problems has on the algebraic structure of the relevant group or groups.
We first generalize some results on pairs of groups, which were previously proven for contextfree pairs of groups only. We then proceed to look at irreducible word problems, where our main contribution is the fact that a group for which all irreducible word problems are recursively enumerable must necessarily have solvable word problem. We then investigate groups for which membership of the irreducible word problem in the class of recursively enumerable languages is not independent of generating set. Lastly, we prove that groups whose word problem is a terminal Petri net language are exactly the virtually abelian groups.
20160602T12:13:04Z

Digital Educational Games: Methodologies for Evaluating the Impact of Game Type
http://hdl.handle.net/2381/37613
Title: Digital Educational Games: Methodologies for Evaluating the Impact of Game Type
Authors: Heintz, Stephanie Alexandra
Abstract: The main research question addressed in this thesis is how the choice of game type influences the success of digital educational games (DEG), where success is defined as significant knowledge gain in combination with positive player experience. Games differ in type if they differ at least by one game feature.
As a first step we identified a comprehensive set of unique game features, summarised in the Game ElementsAttributes Model (GEAM), where elements are the defining components that all games share (e.g. Challenges) and attributes are their possible implementation (e.g. time pressure).
To deepen the understanding of relationships amongst game features, we conducted a survey based on the GEAM and received 321 responses. Using hierarchical clustering, we grouped 67 games, selected by the survey respondents, in terms of similarity and mapped the identified clusters on a 2D space to visualise their difference in distance from each other. On the resulting Game Genre Map, five main areas were detected, which proved to conform mostly to a selection of existing game genres. By specifying their GEAM attributes, we redefined these genres: Minigame, Action, Adventure, Resource, and Roleplay.
Based on the aforementioned groundwork, two empirical studies were conducted. Study 1 compared three DEGs of the Minigame genre, differing in a single GEAM attribute  time pressure vs. puzzle solving and abstract vs. realistic graphics. Study 2 compared DEGs of different genres which vary in the implementation of several GEAM attributes. For both studies, statistically significant differences were found in learning outcome, for Study 2 also in the player experience dimensions: Flow, Tension, Challenge, and Negative Affect. However, the influences of the covariates  learning and play preconditions, learning style, and personality traits  were not confirmed. Further research based on the methodological frameworks developed is needed.
20160519T15:22:27Z

Data Collection in Wireless Sensor Networks
http://hdl.handle.net/2381/37606
Title: Data Collection in Wireless Sensor Networks
Authors: Rasul, Aram Mohammed
Abstract: This thesis is principally concerned with effcient energy consumption in wireless
sensor networks from two distinct aspects from a theoretical point of view.
The thesis addresses the issue of reducing idle listening states in a restricted tree
topology to minimise energy consumption by proposing an optimisation technique:
the extrabit technique. This thesis also focuses on showing lower bounds on the
optimal schedule length, which are derived for some special cases of the tree, such as
a single chain, balanced chains, imbalanced chains, three and four level kary trees
and Rhizome trees. Then, we propose an algorithm which can exactly match the
lower bound for a single chain, balanced chains and Rhizome trees individually and
which is a few steps away from the optimal solution for imbalanced chains. Finally,
we propose the use of two frequencies to further save energy and minimize latency.
Recent research has shown that significant energy improvements can be achieved
in WSNs by exploiting a mobile sink for data collection via single hop communications. A mobile sink approaches the transmission range of sensors to receive their
data and deposit the data at the base station. The thesis, as a second problem,
focuses on the design issues of an energy efficient restricted tour construction for
sink mobility. We propose two different techniques. The first one is heuristic and
uses a criterion based on maximum coverage and minimum energy consumption
called the "maxratio". Although its time complexity is polynomial, this heuristic
algorithm cannot always produce a good solution. As a result, we propose the sec
ond algorithm. Despite the time complexity of the second algorithm being pseudo
polynomial, the optimal solution can be found if one exists. For each algorithm men
tioned, two scenarios are taken into account with regard to the transmission. In the
first scenario, one assumes that there is no upper bound on the transmission range
while in the second setting the nodes can adjust their transmission range between 0
and the maximum range. The algorithms have been implemented and simulated in
Matlab.
20160519T12:03:50Z

Complexities of Computation: A Survey Report
http://hdl.handle.net/2381/37604
Title: Complexities of Computation: A Survey Report
Authors: Jain, A. K.; Jain, Nitin Kumar
Abstract: Computation of real numbers has been a challenging task for many years. Because of its unique nature of infinity, it is considered as a very good area of research. This paper tries to convey the nature of the real numbers and the difficulty to compute them i.e. to approximate the value and some respective development processes related to the real numbers. While making a general calculation the approximation can go on and on, this still doesn’t give the exact value. Computer system’s memory is finite. Goal is to approximate the real numbers but the problem arises where to stop and which basis they are subjected for approximation on.
20160519T10:59:37Z

Interaction Models and Automated Control under Partial Observable Environments
http://hdl.handle.net/2381/37602
Title: Interaction Models and Automated Control under Partial Observable Environments
Authors: Braberman, Victor; D'Ippolito, Nicolas; Piterman, Nir; Uchitel, Sebastian; Ciolek, Daniel
Abstract: The problem of automatically constructing a software component such that when executed in a given environment satisfies a goal, is recurrent in software engineering. Controller synthesis is a field which fits into this vision. In this paper we study controller synthesis for partially observable LTS models. We exploit the link between partially observable control and nondeterminism and show that, unlike fully observable LTS or Kripke structure control problems, in this setting the existence of a solution depends on the interaction model between the controllertobe and its environment. We identify two interaction models, namely Interface Automata and Weak Interface Automata, define appropriate control problems and describe synthesis algorithms for each of them.
20160518T15:21:12Z

T2: Temporal Property Verification
http://hdl.handle.net/2381/37601
Title: T2: Temporal Property Verification
Authors: Brockschmidt, Mark; Cook, Byron; Ishtiaq, Samin; Khlaaf, Heidy; Piterman, Nir
Abstract: We present the opensource tool T2, the first public release from the TERMINATOR project. T2 has been extended over the past decade to support automatic temporallogic proving techniques and to handle a general class of userprovided liveness and safety properties. Input can be provided in a native format and in C, via the support of the LLVM compiler framework. We briefly discuss T2's architecture, its underlying techniques, and conclude with an experimental illustration of its competitiveness and directions for future extensions.
Description: This is an extended version of a paper presented at the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems and published in the Proceedings as Brockschmidt, M., Cook, B. et. al., T2: Temporal Property Verification, Lecture Notes in Computer Science, 2016, 9636, pp 387393.
20160518T14:45:25Z