DSpace Collection:
http://hdl.handle.net/2381/1116
20170227T16:34:12Z

UncertaintyDriven BlackBox Test Data Generation
http://hdl.handle.net/2381/39377
Title: UncertaintyDriven BlackBox Test Data Generation
Authors: Walkinshaw, Neil; Fraser, Gordon
Abstract: We can never be certain that a software system is correct simply by testing it, but with every additional successful test we become less uncertain about its correctness. In absence of source code or elaborate specifications and models, tests are usually generated or chosen randomly. However, rather than randomly choosing tests, it would be preferable to choose those tests that decrease our uncertainty about correctness the most. In order to guide test generation, we apply what is referred to in Machine Learning as "Query Strategy Framework": We infer a behavioural model of the system under test and select those tests which the inferred model is "least certain" about. Running these tests on the system under test thus directly targets those parts about which tests so far have failed to inform the model. We provide an implementation that uses a genetic programming engine for model inference in order to enable an uncertainty sampling technique known as "query by committee", and evaluate it on eight subject systems from the Apache Commons Math framework and JodaTime. The results indicate that test generation using uncertainty sampling outperforms conventional and Adaptive Random Testing.
20170224T15:26:35Z

Improved Lower Bounds for Online Hypercube Packing
http://hdl.handle.net/2381/39372
Title: Improved Lower Bounds for Online Hypercube Packing
Authors: Heydrich, Sandy; van Stee, Rob
Abstract: Packing a given sequence of items into as few bins as possible in an online fashion is a widely studied problem. We improve lower bounds for packing hypercubes into bins in two or more dimensions, once for general algorithms (in two dimensions) and once for an important subclass, socalled Harmonictype algorithms (in two or more dimensions). Lastly, we show that two adaptions of the ideas from the best known onedimensional packing algorithm to square packing also do not help to break the barrier of 2.
20170224T15:00:05Z

Online bin stretching with three bins
http://hdl.handle.net/2381/39336
Title: Online bin stretching with three bins
Authors: Böhm, Martin; Sgall, Jiri; van Stee, Rob; Veselý, Pavel
Abstract: Online Bin Stretching is a semionline variant of bin packing in which the
algorithm has to use the same number of bins as an optimal packing, but is allowed to slightly
overpack the bins. The goal is to minimize the amount of overpacking, i.e., the maximum
size packed into any bin.
We give an algorithm for Online Bin Stretching with a stretching factor of 11/8 = 1.375
for three bins. Additionally, we present a lower bound of 45/33 = 1.36 for Online Bin
Stretching on three bins and a lower bound of 19/14 for four and five bins that were
discovered using a computer search.
Description: The file associated with this record is embargoed until 12 months after the date of publication. The final published version may be available through the links above. Following the embargo period the above license applies.
20170206T16:50:54Z

Ensemble learning for data stream analysis: a survey
http://hdl.handle.net/2381/39321
Title: Ensemble learning for data stream analysis: a survey
Authors: Krawczyk, Bartosz; Minku, Leandro L.; Gama, Joao; Stefanowski, Jerzy; Wozniak, Michal
Abstract: x
Description: The file associated with this record is embargoed until 18 months after the date of publication. The final published version may be available through the links above. Following the embargo period the above license applies.
20170202T15:35:45Z

Emergent stem cell homeostasis in the C. elegans germline is revealed by hybrid modeling.
http://hdl.handle.net/2381/39247
Title: Emergent stem cell homeostasis in the C. elegans germline is revealed by hybrid modeling.
Authors: Hall, B. A.; Piterman, Nir; Hajnal, A.; Fisher, J.
Abstract: The establishment of homeostasis among cell growth, differentiation, and apoptosis is of key importance for organogenesis. Stem cells respond to temporally and spatially regulated signals by switching from mitotic proliferation to asymmetric cell division and differentiation. Executable computer models of signaling pathways can accurately reproduce a wide range of biological phenomena by reducing detailed chemical kinetics to a discrete, finite form. Moreover, coordinated cell movements and physical cellcell interactions are required for the formation of threedimensional structures that are the building blocks of organs. To capture all these aspects, we have developed a hybrid executable/physical model describing stem cell proliferation, differentiation, and homeostasis in the Caenorhabditis elegans germline. Using this hybrid model, we are able to track cell lineages and dynamic cell movements during germ cell differentiation. We further show how apoptosis regulates germ cell homeostasis in the gonad, and propose a role for intercellular pressure in developmental control. Finally, we use the model to demonstrate how an executable model can be developed from the hybrid system, identifying a mechanism that ensures invariance in fate patterns in the presence of instability.
Description: One figure and two movies are available at http://www.biophysj.org/biophysj/supplemental/S00063495(15)005895.
20170120T16:59:18Z

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

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

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

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

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

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

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

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

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

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

Two Dimensional Range Minimum Queries and Fibonacci Lattices
http://hdl.handle.net/2381/37491
Title: Two Dimensional Range Minimum Queries and Fibonacci Lattices
Authors: Brodal, Gerth Stølting; Davoodi, Pooya; Lewenstein, Moshe; Raman, Rajeev; Srinivasa Rao, Satti
Abstract: Given a matrix of size N , two dimensional range minimum queries (2DRMQs) ask for the position of the minimum element in a rectangular range within the matrix. We study tradeoffs between the query time and the additional space used by indexing data structures that support 2DRMQs. Using a novel technique—the discrepancy properties of Fibonacci lattices—we give an indexing data structure for 2DRMQs that uses O(N/c) bits additional space with O(clog c(log log c) ²) query time, for any parameter c , 4≤c≤N. Also, when the entries of the input matrix are from {0,1}, we show that the query time can be improved to O(clog c) with the same space usage.
Description: The file associated with this record is under a 24month embargo from publication in accordance with the publisher's selfarchiving policy. The full text may be available through the publisher links provided above.
20160506T09:25:06Z

Bin packing in multiple dimensions
http://hdl.handle.net/2381/37457
Title: Bin packing in multiple dimensions
Authors: van Stee, Rob
Abstract: I mentioned in a previous column [22] that the best known lower bound for the twodimensional
online bin packing problem is 1.907 by Blitz, van Vliet, Woeginger [2], which is an unpublished
(and now lost [24]) manuscript. I have realized since then that even the penultimate result, 1.856,
was published only in Andre van Vliet's Ph.D. thesis [23] and is not readily available. It therefore
seems like a good idea to describe his methods here, though not in full detail. This will include
a discussion of the threedimensional case. I will also survey other results in multidimensional
packing, that were left out in my previous column.
20160427T13:54:43Z

Online algorithms with advice for bin packing and scheduling problems
http://hdl.handle.net/2381/37456
Title: Online algorithms with advice for bin packing and scheduling problems
Authors: Renault, Marc P.; Rosén, Adi; van Stee, Rob
Abstract: We consider the setting of online computation with advice and study the bin packing problem and a number of scheduling problems. We show that it is possible, for any of these problems, to arbitrarily approach a competitive ratio of 1 with only a constant number of bits of advice per request. For the bin packing problem, we give an online algorithm with advice that is (1+ε)competitive and uses O(1εlog 1ε) bits of advice per request. For scheduling on m identical machines, with the objective function of any of makespan, machine covering and the minimization of the ℓ<inf>p</inf> norm, p>1, we give similar results. We give online algorithms with advice which are (1+ε)competitive ((1/(1ε))competitive for machine covering) and also use O(1εlog 1ε) bits of advice per request. We complement our results by giving a lower bound that shows that for any online algorithm with advice to be optimal, for any of the above scheduling problems, a nonconstant number (namely, at least (12mn)log m, where n is the number of jobs and m is the number of machines) of bits of advice per request is needed.
20160427T13:45:14Z

The cost of selfishness for maximizing the minimum load on uniformly related machines
http://hdl.handle.net/2381/37390
Title: The cost of selfishness for maximizing the minimum load on uniformly related machines
Authors: Epstein, L.; Kleiman, E.; Van Stee, Rob
Abstract: Consider the following scheduling game. A set of jobs, each controlled by a selfish agent, are to be assigned to m uniformly related machines. The cost of a job is defined as the total load of the machine that its job is assigned to. A job is interested in minimizing its cost, while the social objective is maximizing the minimum load (the value of the cover) over the machines. This goal is different from the regular makespan minimization goal, which was extensively studied in a game theoretic context. We study the price of anarchy (poa) and the price of stability (pos) for uniformly related machines. The results are expressed in terms of s, which is the maximum speed ratio between any two machines. For uniformly related machines, we prove that the pos is unbounded for s>2, and the poa is unbounded for s≥2. For the remaining cases we show that while the poa grows to infinity as s tends to 2, the pos is at most 2 for any s≤2. © 2012 Springer Science+Business Media New York.
20160420T09:17:00Z

SIGACT news online algorithms column 23
http://hdl.handle.net/2381/37389
Title: SIGACT news online algorithms column 23
Authors: van Stee, Rob
Description: timestamp: Sun, 04 May 2014 01:00:00 +0200 biburl: http://dblp.unitrier.de/rec/bib/journals/sigact/Stee14 bibsource: dblp computer science bibliography, http://dblp.org
20160420T09:13:06Z

Dividing connected chores fairly
http://hdl.handle.net/2381/37387
Title: Dividing connected chores fairly
Authors: Heydrich, S.; van Stee, Rob
Abstract: In this paper we consider the fair division of chores (tasks that need to be performed by agents, with negative utility for them), and study the loss in social welfare due to fairness. Previous work has been done on this socalled price of fairness, concerning fair division of cakes and chores with nonconnected pieces and of cakes with connected pieces. In this paper, we consider situations where each player has to receive one connected piece of the chores. We provide tight or nearly tight bounds on the price of fairness with respect to the three main fairness criteria proportionality, envyfreeness and equitability and for utilitarian and egalitarian welfare. We also give the first proof of the existence of equitable divisions for chores with connected pieces.
Description: The file associated with this record is under a 24month embargo from publication in accordance with the publisher's selfarchiving policy. The full text may be available through the publisher links provided above.
20160420T09:04:38Z

SIGACT News Online Algorithms Column 27: Online Matching on the Line, Part 1
http://hdl.handle.net/2381/37327
Title: SIGACT News Online Algorithms Column 27: Online Matching on the Line, Part 1
Authors: Van Stee, Rob
20160418T09:47:02Z

A Unified Approach to Truthful Scheduling on Related Machines
http://hdl.handle.net/2381/37326
Title: A Unified Approach to Truthful Scheduling on Related Machines
Authors: Van Stee, Rob; Epstein, L.; Levin, A.
Abstract: We present a unified framework for designing deterministic monotone polynomial time approximation schemes (PTASs) for a wide class of scheduling problems on uniformly related machines. This class includes (among others) minimizing the makespan, maximizing the minimum load, and minimizing the pnorm of the machine loads vector. Previously, this kind of result was only known for the makespan objective. Monotone algorithms have the property that an increase in the speed of a machine cannot decrease the amount of work assigned to it. Our results imply the existence of a truthful mechanism that can be implemented in polynomial time, where the social goal is approximated within arbitrary precision.
Description: The file associated with this record is under a 12month embargo from publication in accordance with the publisher's selfarchiving policy. The full text may be available through the publisher links provided above.
20160418T09:33:53Z

RunTime Resolution of Service Property Conflicts in Web Service Composition
http://hdl.handle.net/2381/37275
Title: RunTime Resolution of Service Property Conflicts in Web Service Composition
Authors: Xu, J.; Ning, X.; ReiffMarganiec, Stephan; Duan, Q.; Zheng, Z.
Abstract: Service composition has become a common approach to realising complex business processes. The large number of services developed and deployed independently by various providers can lead to undesirable interactions between properties of different services which are a serious obstacle for service composition to meet users' requirements. While some property conflicts can be prevented during design, many occur during execution based on runtime data. In this paper, we propose a solution for the problem of runtime resolution of service property conflicts. We formulate the conflict resolution problem as biobjective optimisation model based on user's revenue. Solving the optimisation model provides a set of Pareto solutions which are ranked to identify the optimal one for resolving a service property conflict. The proposed scheme is implemented in a prototype for experimental performance evaluation. The experimental results indicate that our scheme is effective and efficient in resolving service property conflicts at runtime.
20160413T08:38:30Z

A TwoPhase Algorithm for Bin Stretching with Stretching Factor 1.5
http://hdl.handle.net/2381/37201
Title: A TwoPhase Algorithm for Bin Stretching with Stretching Factor 1.5
Authors: Böhm, M.; Sgall, J.; Van Stee, Rob; Veselý, P.
Abstract: Online Bin Stretching is a semionline variant of bin packing in which the algorithm has to use the same number of bins as an optimal packing, but is allowed to slightly overpack the bins. The goal is to minimize the amount of overpacking, i.e., the maximum size packed into any bin. We give an algorithm for Online Bin Stretching with a stretching factor of $1.5$ for any number of bins. We build on previous algorithms and use a twophase approach. We also show that this approach cannot give better results by proving a matching lower bound.
Description: Preprint of a journal version. The conference version can be found at arXiv:1404.5569
20160408T09:22:21Z

Dynamic Selection of Evolutionary Operators Based on Online Learning and Fitness Landscape Analysis
http://hdl.handle.net/2381/37186
Title: Dynamic Selection of Evolutionary Operators Based on Online Learning and Fitness Landscape Analysis
Authors: Consoli, P. A.; Mei, Y.; Minku, Leandro Lei; Yao, X.
Abstract: Selfadaptive mechanisms for the identification of the most suitable variation operator in evolutionary algorithms rely almost exclusively on the measurement of the fitness of the offspring, which may not be sufficient to assess the optimality of an operator (e.g., in a landscape with an high degree of neutrality). This paper proposes a novel adaptive operator selection mechanism which uses a set of four fitness landscape analysis techniques and an online learning algorithm, dynamic weighted majority, to provide more detailed information about the search space to better determine the most suitable crossover operator. Experimental analysis on the capacitated arc routing problem has demonstrated that different crossover operators behave differently during the search process, and selecting the proper one adaptively can lead to more promising results.
20160407T10:51:27Z

Honesty by typing
http://hdl.handle.net/2381/37180
Title: Honesty by typing
Authors: Bartoletti, M.; Scalas, A.; Tuosto, Emilio; Zunino, R.
Abstract: We propose a type system for a calculus of contracting processes. Processes may stipulate contracts, and then either behave honestly, by keeping the promises made, or not. Type safety guarantees that a typeable process is honest  that is, the process abides by the contract it has stipulated in all possible contexts, even those containing dishonest adversaries. © 2013 IFIP International Federation for Information Processing.
20160407T10:15:59Z

From orchestration to choreography through contract automata
http://hdl.handle.net/2381/37178
Title: From orchestration to choreography through contract automata
Authors: Basile, D.; Degano, P.; Ferrari, GL.; Tuosto, Emilio
Abstract: We study the relations between a contract automata and an interaction model. In the former model, distributed services are abstracted away as automata  oblivious of their partners  that coordinate with each other through an orchestrator. The interaction model relies on channelbased asynchronous communication and choreography to coordinate distributed services. We define a notion of strong agreement on the contract model, exhibit a natural mapping from the contract model to the interaction model, and give conditions to ensure that strong agreement corresponds to wellformed choreography.
20160407T09:40:52Z

Communicating machines as a dynamic binding mechanism of services
http://hdl.handle.net/2381/37177
Title: Communicating machines as a dynamic binding mechanism of services
Authors: Vissani, I.; Pombo, C. G. L.; Tuosto, Emilio
Abstract: Distributed software is becoming more and more dynamic to support applications able to respond and adapt to the changes of their execution environment. For instance, serviceoriented computing (SOC) envisages applications as services running over globally available computational resources where discovery and binding between them is transparently performed by a middleware. Asynchronous Relational Networks (ARNs) is a wellknown formal orchestration model, based on hypergraphs, for the description of serviceoriented software artefacts. Choreography and orchestration are the two main design principles for the development of distributed software. In this work, we propose Communicating Relational Networks (CRNs), which is a variant of ARNs, but relies on choreographies for the characterisation of the communicational aspects of a software artefact, and for making their automated analysis more efficient.
20160407T09:08:49Z

ChoreographyBased Analysis of Distributed Message Passing Programs
http://hdl.handle.net/2381/37150
Title: ChoreographyBased Analysis of Distributed Message Passing Programs
Authors: Taylor, R.; Tuosto, E.; Walkinshaw, Neil; Derrick, J.
Abstract: x
20160406T08:45:42Z

Data Mining for Software Engineering and Humans in the Loop
http://hdl.handle.net/2381/37102
Title: Data Mining for Software Engineering and Humans in the Loop
Authors: Minku, Leandro L.; Mendes, E.; Turhan, B.
Abstract: The field of data mining for software engineering has been growing
over the last decade. This field is concerned with the use of data mining
to provide useful insights into how to improve software engineering processes
and software itself, supporting decision making. For that, data produced by
software engineering processes and products during and after software development
is used. Despite promising results, there is frequently a lack of discussion
on the role of software engineering practitioners amidst the data mining approaches.
This makes adoption of data mining by software engineering practitioners
difficult. Moreover, the fact that experts’ knowledge is frequently
ignored by data mining approaches, together with the lack of transparency
of such approaches, can hinder the acceptability of data mining by software
engineering practitioners. In order to overcome these problems, this position
paper provides a discussion of the role of software engineering experts when
adopting data mining approaches. It also argues that this role can be extended
in order to increase experts’ involvement in the process of building data mining
models. We believe that such extended involvement is not only likely to
increase software engineers’ acceptability of the resulting models, but also improve
the models themselves. We also provide some recommendations aimed
at increasing the success of experts involvement and model acceptability.
20160331T08:54:54Z

Online Ensemble Learning of Data Streams with Gradually Evolved Classes
http://hdl.handle.net/2381/36721
Title: Online Ensemble Learning of Data Streams with Gradually Evolved Classes
Authors: Sun, Y.; Tang, K.; Minku, Leandro Lei; Wang, S.; Yao, X.
Abstract: Class evolution, the phenomenon of class emergence and disappearance, is an important research topic for data stream mining. All previous studies implicitly regard class evolution as a transient change, which is not true for many realworld problems. This paper concerns the scenario where classes emerge or disappear gradually. A classbased ensemble approach, namely ClassBased ensemble for Class Evolution (CBCE), is proposed. By maintaining a base learner for each class and dynamically updating the base learners with new data, CBCE can rapidly adjust to class evolution. A novel undersampling method for the base learners is also proposed to handle the dynamic classimbalance problem caused by the gradual evolution of classes. Empirical studies demonstrate the effectiveness of CBCE in various class evolution scenarios in comparison to existing class evolution adaptation methods.
20160216T11:35:26Z

Quasivarieties and varieties of ordered algebras : Regularity and exactness
http://hdl.handle.net/2381/36716
Title: Quasivarieties and varieties of ordered algebras : Regularity and exactness
Authors: Kurz, Alexander Herbert; Velebil, J.
Abstract: We characterise quasivarieties and varieties of ordered algebras categorically in terms of regularity, exactness and the existence of a suitable generator. The notions of regularity and exactness need to be understood in the sense of category theory enriched over posets. We also prove that finitary varieties of ordered algebras are cocompletions of their theories under sifted colimits (again, in the enriched sense).
Description: The file associated with this record is under a 6month embargo from publication in accordance with the publisher's selfarchiving policy. The full text may be available through the publisher links provided above.
20160215T11:57:40Z

Multitype display calculus for propositional dynamic logic
http://hdl.handle.net/2381/36715
Title: Multitype display calculus for propositional dynamic logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander Herbert; Palmigiano, A.
Abstract: We introduce a multitype display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnapstyle cutelimination and subformula property.
20160215T11:50:32Z

Positive Fragments Of Coalgebraic Logics
http://hdl.handle.net/2381/36575
Title: Positive Fragments Of Coalgebraic Logics
Authors: Balan, A.; Kurz, Alexander Herbert; Velebil, J.
Abstract: Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn's result from Kripke frames to coalgebras for weakpullback preserving functors. To facilitate this analysis we prove a number of category theoretic results on functors on the categories $mathsf{Set}$ of sets and $mathsf{Pos}$ of posets: Every functor $mathsf{Set} to mathsf{Pos}$ has a $mathsf{Pos}$enriched left Kan extension $mathsf{Pos} to mathsf{Pos}$. Functors arising in this way are said to have a presentation in discrete arities. In the case that $mathsf{Set} to mathsf{Pos}$ is actually $mathsf{Set}$valued, we call the corresponding left Kan extension $mathsf{Pos} to mathsf{Pos}$ its posetification. A $mathsf{Set}$functor preserves weak pullbacks if and only if its posetification preserves exact squares. A $mathsf{Pos}$functor with a presentation in discrete arities preserves surjections. The inclusion $mathsf{Set} to mathsf{Pos}$ is dense. A functor $mathsf{Pos} to mathsf{Pos}$ has a presentation in discrete arities if and only if it preserves coinserters of `truncated nerves of posets'. A functor $mathsf{Pos} to mathsf{Pos}$ is a posetification if and only if it preserves coinserters of truncated nerves of posets and discrete posets. A locally monotone endofunctor of an ordered variety has a presentation by monotone operations and equations if and only if it preserves $mathsf{Pos}$enriched sifted colimits.
20160204T12:46:07Z

Presenting Distributive Laws
http://hdl.handle.net/2381/36574
Title: Presenting Distributive Laws
Authors: Bonsangue, M. M.; Hansen, H. H.; Kurz, Alexander Herbert; Rot, J.
Abstract: Distributive laws of a monad T over a functor F are categorical tools for specifying algebracoalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of wellbehaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation from a distributive law for the underlying free monad. We apply this result to show the equivalence between two different representations of contextfree languages.
20160204T12:43:36Z