DSpace Collection:
http://hdl.handle.net/2381/1116
2018-01-20T09:06:07Z
2018-01-20T09:06:07Z
Features of Agent-based Models
Heckel, Reiko
Kurz, Alexander
Chattoe-Brown, Edmund
http://hdl.handle.net/2381/40910
2018-01-18T03:25:35Z
2018-01-17T10:10:47Z
Title: Features of Agent-based Models
Authors: Heckel, Reiko; Kurz, Alexander; Chattoe-Brown, Edmund
Abstract: The design of agent-based models (ABMs) is often ad-hoc when it comes to defining their scope. In order for the inclusion of features such as network structure, location, or dynamic change to be justified, their role in a model should be systematically analysed. We propose a mechanism to compare and assess the impact of such features. In particular we are using techniques from software engineering and semantics to support the development and assessment of ABMs, such as graph transformations as semantic representations for agent-based models, feature diagrams to identify ingredients under consideration, and extension relations between graph transformation systems to represent model fragments expressing features.
Description: In Proceedings GaM 2017, arXiv:1712.08345
2018-01-17T10:10:47Z
Semantics of global view of choreographies
Tuosto, Emilio
Guanciale, Roberto
http://hdl.handle.net/2381/40743
2018-01-09T03:30:07Z
2018-01-08T16:15:56Z
Title: Semantics of global view of choreographies
Authors: Tuosto, Emilio; Guanciale, Roberto
Abstract: We propose two abstract semantics of the global view of choreographies given in terms of partial orders. The first semantics is formalised as pomsets of communication events while the second one is based on hypergraphs of events. These semantics can accommodate different levels of abstractions. We discuss the adequacy of our models by considering their relation with communicating machines, that we use to formalise the local view. Our approach increases expressiveness and allows us to overcome some limitations that affect alternative semantics of global views. This will be illustrated by discussing some interesting examples. Finally, we show that the two semantics are equivalent and have different merits. More precisely, the semantics based on pomsets yields a more elegant presentation, but it is less suitable for implementation. The semantics based on hypergraphs instead is amenable to a straightforward implementation.
Description: The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2018-01-08T16:15:56Z
A Q-learning-based memetic algorithm for multi-objective dynamic software project scheduling
Shen, Xiao-Ning
Minku, Leandro L.
Marturi, Naresh
Guo, Yi-Nan
Han, Ying
http://hdl.handle.net/2381/40568
2017-11-22T03:25:04Z
2017-11-21T12:06:06Z
Title: A Q-learning-based memetic algorithm for multi-objective dynamic software project scheduling
Authors: Shen, Xiao-Ning; Minku, Leandro L.; Marturi, Naresh; Guo, Yi-Nan; Han, Ying
Abstract: Software project scheduling is the problem of allocating employees to tasks in a software project. Due to the large scale of current software projects, many studies have investigated the use of optimization algorithms to find good software project schedules. However, despite the importance of human factors to the success of software projects, existing work has considered only a limited number of human properties when formulating software project scheduling as an optimization problem. Moreover, the changing environments of software companies mean that software project scheduling is a dynamic optimization problem. However, there is a lack of effective dynamic scheduling approaches to solve this problem. This work proposes a more realistic mathematical model for the dynamic software project scheduling problem. This model considers that skill proficiency can improve over time and, different from previous work, it considers that such improvement is affected by the employees’ properties of motivation and learning ability, and by the skill difficulty. It also defines the objective of employees’ satisfaction with the allocation. It is considered together with the objectives of project duration, cost, robustness and stability under a variety of practical constraints. To adapt schedules to the dynamically changing software project environments, a multi-objective two-archive memetic algorithm based on Q-learning (MOTAMAQ) is proposed to solve the problem in a proactive-rescheduling way. Different from previous work, MOTAMAQ learns the most appropriate global and local search methods to be used for different software project environment states by using Q-learning. Extensive experiments on 18 dynamic benchmark instances and 3 instances derived from real-world software projects were performed. A comparison with seven other meta-heuristic algorithms shows that the strategies used by our novel approach are very effective in improving its convergence performance in dynamic environments, while maintaining a good distribution and spread of solutions. The Q-learning-based learning mechanism can choose appropriate search operators for the different scheduling environments. We also show how different trade-offs among the five objectives can provide software managers with a deeper insight into various compromises among many objectives, and enabling them to make informed decisions.
Description: The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2017-11-21T12:06:06Z
Optimal online two-way trading with bounded number of transactions
Fung, Stanley P. Y.
http://hdl.handle.net/2381/40517
2017-11-10T03:21:55Z
2017-11-09T14:26:29Z
Title: Optimal online two-way trading with bounded number of transactions
Authors: Fung, Stanley P. Y.
Abstract: We consider a two-way trading problem, where investors buy and sell a stock whose price moves within a certain range. Naturally they want to maximize their profit. Investors can perform up to k trades, where each trade must involve the full amount. We give optimal algorithms for three different models which differ in the knowledge of how the price fluctuates. In the first model, there are global minimum and maximum bounds m and M. We first show an optimal lower bound of φφ (where φ=M/mφ=M/m) on the competitive ratio for one trade, which is the bound achieved by trivial algorithms. Perhaps surprisingly, when we consider more than one trade, we can give a better algorithm that loses only a factor of φ2/3φ2/3 (rather than φφ) per additional trade. Specifically, for k trades the algorithm has competitive ratio φ(2k+1)/3φ(2k+1)/3. Furthermore we show that this ratio is the best possible by giving a matching lower bound. In the second model, m and M are not known in advance, and just φφ is known. We show that this only costs us an extra factor of φ1/3φ1/3, i.e., both upper and lower bounds become φ(2k+2)/3φ(2k+2)/3. Finally, we consider the bounded daily return model where instead of a global limit, the fluctuation from one day to the next is bounded, and again we give optimal algorithms, and interestingly one of them resembles common trading algorithms that involve stop loss limits.
2017-11-09T14:26:29Z
Predicting Postpartum Hemorrhage (PPH) during Cesarean Delivery Using the Leicester PPH Predict Tool: A Retrospective Cohort Study.
Dunkerton, Suzanna E.
Jeve, Yadava B.
Walkinshaw, Neil
Breslin, Eamonn
Singhal, Tanu
http://hdl.handle.net/2381/40427
2017-10-05T02:21:35Z
2017-10-04T13:52:45Z
Title: Predicting Postpartum Hemorrhage (PPH) during Cesarean Delivery Using the Leicester PPH Predict Tool: A Retrospective Cohort Study.
Authors: Dunkerton, Suzanna E.; Jeve, Yadava B.; Walkinshaw, Neil; Breslin, Eamonn; Singhal, Tanu
Abstract: Objective: The aim of the present study was to develop a toolkit combining various risk factors to predict the risk of developing a postpartum hemorrhage (PPH) during a cesarean delivery.
Study Design: A retrospective cohort study of 24,230 women who had cesarean delivery between January 2003 and December 2013 at a tertiary care teaching hospital within the United Kingdom serving a multiethnic population. Data were extracted from hospital databases, and risk factors for PPH were identified. Hothorn et al recursive partitioning algorithm was used to infer a conditional decision tree. For each of the identified combinations of risk factors, two probabilities were calculated: the probability of a patient producing ≥1,000 and ≥ 2,000 mL blood loss.
Results: The Leicester PPH predict score was then tested on the randomly selected remaining 25% (n = 6,095) of the data for internal validity. Reliability testing showed an intraclass correlation of 0.98 and mean absolute error of 239.8 mL with the actual outcome.
Conclusion: The proposed toolkit enables clinicians to predict the risk of postpartum hemorrhage. As a result, preventative measures for postpartum hemorrhage could be undertaken. Further external validation of the current toolkit is required.
Description: The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2017-10-04T13:52:45Z
Sound conformance testing for cyber-physical systems: Theory and implementation
Araujo, Hugo
Carvalhoa, Gustavo
Mohaqeqi, Morteza
Mousavi, Mohammad Reza
Sampaio, Augusto
http://hdl.handle.net/2381/40317
2017-09-05T02:23:43Z
2017-09-04T13:26:09Z
Title: Sound conformance testing for cyber-physical systems: Theory and implementation
Authors: Araujo, Hugo; Carvalhoa, Gustavo; Mohaqeqi, Morteza; Mousavi, Mohammad Reza; Sampaio, Augusto
Abstract: Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate. We use reachability analysis to find such bounds and implement the proposed approach using the CORA toolbox in Matlab. We apply the implemented approach on a case study from the automotive domain.
2017-09-04T13:26:09Z
Optimized Service Level Agreement Establishment in Cloud Computing
de Azevedo, Leonildo J. M.
Estrella, Julio C.
Nakamura, Luis H. V.
Santana, Marcos J.
Santana, Regina H. C.
Toledo, Claudio F. Motta
Batista, Bruno G.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/40300
2017-10-06T13:35:06Z
2017-08-31T14:48:34Z
Title: Optimized Service Level Agreement Establishment in Cloud Computing
Authors: de Azevedo, Leonildo J. M.; Estrella, Julio C.; Nakamura, Luis H. V.; Santana, Marcos J.; Santana, Regina H. C.; Toledo, Claudio F. Motta; Batista, Bruno G.; Reiff-Marganiec, Stephan
Abstract: Nowadays, the access to a cloud computing environment is provided on-demand,
offering transparent services to clients. Although the cloud allows an abstraction
of the behavior of the infrastructure in the service providers (involving logical
and physical resources), the Service Level Agreements (SLAs) fulfilment remains a
challenge, because depending on the service demand and the system configuration,
the providers may not be able to meet the clients requirements. In this
way, mechanisms that take account of load balancing and resource provisioning
algorithms to provide an efficient load distribution in the available resources
are necessary. However, the studies in the literature do not effectively address
the problem of the resource provisioning to meet clients requirements using
optimization techniques, restricting the analysis to a limited set of objectives. This
paper proposes algorithms to address the computational resource provisioning
problem using optimization techniques on-the-fly. The techniques optimize the use
of the resources available in the cloud infrastructure, aiming to fulfill the clients
requirements defined in the SLAs, and ensuring the efficient use of resources.
Description: The file associated with this record is under embargo until 24 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2017-08-31T14:48:34Z
Finding Clustering Configurations to Accurately Infer Packet Structures from Network Data
Esoul, Othman
Walkinshaw, Neil
http://hdl.handle.net/2381/40286
2017-08-31T02:24:15Z
2017-08-30T08:10:58Z
Title: Finding Clustering Configurations to Accurately Infer Packet Structures from Network Data
Authors: Esoul, Othman; Walkinshaw, Neil
Abstract: Clustering is often used for reverse engineering network protocols from captured network traces. The performance of clustering techniques is often contingent upon the selection of various parameters, which can have a severe impact on clustering quality. In this paper we experimentally investigate the effect of four different parameters with respect to network traces. We also determining the optimal parameter configuration with respect to traces from four different network protocols. Our results indicate that the choice of distance measure and the length of the message has the most substantial impact on cluster accuracy. Depending on the type of protocol, the $n$-gram length can also have a substantial impact.
2017-08-30T08:10:58Z
Honesty by Typing
Bartoletti, Massimo
Scalas, Alceste
Tuosto, Emilio
Zunino, Roberto
http://hdl.handle.net/2381/40092
2017-07-29T02:24:26Z
2017-07-28T08:41:20Z
Title: Honesty by Typing
Authors: Bartoletti, Massimo; Scalas, Alceste; Tuosto, Emilio; Zunino, Roberto
Abstract: We propose a type system for a calculus of contracting processes. Processes
can establish sessions by stipulating contracts, and then can interact either by keeping the
promises made, or not. Type safety guarantees that a typeable process is honest — that
is, it abides by the contracts it has stipulated in all possible contexts, even in presence of
dishonest adversaries. Type inference is decidable, and it allows to safely approximate the
honesty of processes using either synchronous or asynchronous communication.
2017-07-28T08:41:20Z
Honesty by Typing
Bartoletti, Massimo
Scalas, Alceste
Tuosto, Emilio
Zunino, Roberto
http://hdl.handle.net/2381/39781
2017-05-16T02:22:20Z
2017-05-15T11:12:55Z
Title: Honesty by Typing
Authors: Bartoletti, Massimo; Scalas, Alceste; Tuosto, Emilio; Zunino, Roberto
Abstract: We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by keeping the promises made, or not. Type safety guarantees that a typeable process is honest — that is, it abides by the contracts it has stipulated in all possible contexts, even in presence of dishonest adversaries. Type inference is decidable, and it allows to safely approximate the honesty of processes using either synchronous or asynchronous communication.
2017-05-15T11:12:55Z
On preventive blood pressure self-monitoring at home
Verdezoto, Nervo
Grönvall, Erik
http://hdl.handle.net/2381/39770
2017-05-13T03:13:50Z
2017-05-12T13:57:21Z
Title: On preventive blood pressure self-monitoring at home
Authors: Verdezoto, Nervo; Grönvall, Erik
Abstract: Self-monitoring activities are increasingly becoming part of people’s everyday lives. Some of these measurements are taken voluntarily rather than being referred by a physician and conducted because of either a preventive health interest or to better understand the body and its functions (the so-called Quantified Self). In this article, we explore socio-technical complexities that may occur when introducing preventive health-measurement technologies into older adults’ daily routines and everyday lives. In particular, the original study investigated blood pressure (BP) measurement in non-clinical settings, to understand existing challenges, and uncover opportunities for self-monitoring technologies to support preventive healthcare activities among older adults. From our study, several important aspects emerged to consider when designing preventive self-monitoring technology, such as the complexity of guidelines for self-measuring, the importance of interpretation, understanding and health awareness, sharing self-monitoring information for prevention, various motivational factors, the role of the doctor in prevention, and the home as a distributed information space. An awareness of these aspects can help designers to develop better tools to support people’s preventive self-monitoring needs, compared to existing solutions. Supporting the active and informed individual can help improve people’s self-care, awareness, and implementation of preventive care. Based on our study, we also reflect on the findings to illustrate how these aspects can both inform people engaged in Quantified Self activities and designers alike, and the tools and approaches that have sprung from the so-called Quantified Self movement.
2017-05-12T13:57:21Z
Fog Computing for Sustainable Smart Cities: A Survey
Perera, Charith
Qin, Yongrui
Estrella, Julio C.
Reiff-Marganiec, Stephan
Vasilakos, Athanasios V.
http://hdl.handle.net/2381/39682
2017-07-05T01:45:07Z
2017-04-21T11:05:47Z
Title: Fog Computing for Sustainable Smart Cities: A Survey
Authors: Perera, Charith; Qin, Yongrui; Estrella, Julio C.; Reiff-Marganiec, Stephan; Vasilakos, Athanasios V.
Abstract: The Internet of Things (IoT) aims to connect billions of smart objects to the Internet, which can bring a promising future to smart cities. These objects are expected to generate large amounts of data and send the data to the cloud for further processing, specially for knowledge discovery, in order that appropriate actions can be taken. However, in reality sensing all possible data items captured by a smart object and then sending the complete captured data to the cloud is less useful. Further, such an approach would also lead to resource wastage (e.g. network, storage, etc.). The Fog (Edge) computing paradigm has been proposed to counterpart the weakness by pushing processes of knowledge discovery using data analytics to the edges. However, edge devices have limited computational capabilities. Due to inherited strengths and weaknesses, neither Cloud computing nor Fog computing paradigm addresses these challenges alone. Therefore, both paradigms need to work together in order to build an sustainable IoT infrastructure for smart cities. In this paper, we review existing approaches that have been proposed to tackle the challenges in the Fog computing domain. Specifically, we describe several inspiring use case scenarios of Fog computing, identify ten key characteristics and common features of Fog computing, and compare more than 30 existing research efforts in this domain. Based on our review, we further identify several major functionalities that ideal Fog computing platforms should support and a number of open challenges towards implementing them, so as to shed light on future research directions on realizing Fog computing for building sustainable smart cities.
2017-04-21T11:05:47Z
Encoding Nearest Larger Values
Hoffmann, Michael
Iacono, John
Nicholson, Patrick K.
Raman, Rajeev
http://hdl.handle.net/2381/39591
2017-06-06T15:56:29Z
2017-03-27T15:17:39Z
Title: Encoding Nearest Larger Values
Authors: Hoffmann, Michael; Iacono, John; Nicholson, Patrick K.; Raman, Rajeev
Abstract: In nearest larger value (NLV) problems, we are given an array A[1..n] of distinct numbers, and need to preprocess A to answer queries of the following form: given any index i∈[1,n], return a “nearest” index j such that A[j]>A[i]. We consider the variant where the values in A are distinct, and we wish to return an index j such that A[j]>A[i] and|j−i| is minimized, the nondirectional NLV (NNLV) problem. We consider NNLV in the encoding model, where the array A is deleted after preprocessing.
The NNLV encoding problem turns out to have an unexpectedly rich structure: the effective entropy (optimal space usage) of the problem depends crucially on details in the definition of the problem. Of particular interest is the tiebreaking rule: if there exist two nearest indices j1,j2 such that A[j1]>A[i] and A[j2]>A[i] and |j1−i|=|j2−i|, then which index should be returned? For the tiebreaking rule where the rightmost (i.e., largest) index is returned, we encode a path-compressed representation of the Cartesian tree that can answer all NNLV queries in 1.89997n+o(n) bits, and can answer queries inO(1) time. An alternative approach, based on forbidden patterns , achieves a very similar space bound for two tiebreaking rules (including the one where ties are broken to the right), and (for a more flexible tiebreaking rule) achieves 1.81211n+o(n) bits. Finally, we develop a fast method of counting distinguishable configurations for NNLV queries. Using this method, we prove a lower bound of 1.62309n−Θ(1) bits of space for NNLV encodings for the tiebreaking rule where the rightmost index is returned.
Description: The file associated with this record is under embargo until 24 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2017-03-27T15:17:39Z
Self-Care Technologies in HCI: Trends, Tensions, and Opportunities
Nunes, Francisco
Verdezoto, Nervo
Fitzpatrick, Geraldine
Kyng, Morten
Grönvall, Erik
Storni, Cristiano
http://hdl.handle.net/2381/39577
2017-03-28T02:18:25Z
2017-03-27T11:04:26Z
Title: Self-Care Technologies in HCI: Trends, Tensions, and Opportunities
Authors: Nunes, Francisco; Verdezoto, Nervo; Fitzpatrick, Geraldine; Kyng, Morten; Grönvall, Erik; Storni, Cristiano
Abstract: Many studies show that self-care technologies can support patients with chronic conditions and their carers in understanding the ill body and increasing control of their condition. However, many of these studies have largely privileged a medical perspective and thus overlooked how patients and carers integrate self-care into their daily lives and mediate their conditions through technology. In this review, we focus on how patients and carers use and experience self-care technology through a Human-Computer Interaction (HCI) lens. We analyse studies of self-care published in key HCI journals and conferences using the Grounded Theory Literature Review (GTLR) method and identify research trends and design tensions. We then draw out opportunities for advancing HCI research in self-care, namely, focusing further on patients' everyday life experience, considering existing collaborations in self-care, and increasing the influence on medical research and practice around self-care technology.
2017-03-27T11:04:26Z
Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
Cook, Byron
Khlaaf, Heidy
Piterman, Nir
http://hdl.handle.net/2381/39502
2017-06-15T01:45:08Z
2017-03-20T09:56:18Z
Title: Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
Authors: Cook, Byron; Khlaaf, Heidy; Piterman, Nir
Abstract: Temporal logic is a formal system for specifying and reasoning about propositions qualified in terms of time.
It offers a unified approach to program verification as it applies to both sequential and parallel programs
and provides a uniform framework for describing a system at any level of abstraction. Thus a number of
automated systems have been proposed to exclusively reason about either Computation-Tree Logic (CTL)
or Linear Temporal Logic (LTL) in the infinite-state setting. Unfortunately, these logics have significantly
reduced expressiveness as they restrict the interplay between temporal operators and path quantifiers, thus
disallowing the expression of many practical properties, for example “along some future an event occurs
infinitely often”. Contrarily, CTL∗, a superset of both CTL and LTL, can facilitate the interplay between
path-based and state-based reasoning. CTL∗ thus exclusively allows for the expressiveness of properties
involving existential system stabilization and “possibility” properties. Until now, there have not existed
automated systems that allow for the verification of such expressive CTL∗ properties over infinite-state
systems. This paper proposes a method capable of such a task, thus introducing the first known fully automated
tool for symbolically proving CTL∗ properties of (infinite-state) integer programs. The method uses
an internal encoding that admits reasoning about the subtle interplay between the nesting of temporal operators
and path quantifiers that occurs within CTL∗ proofs. A program transformation is first employed that
trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future
outcomes when necessary. We then synthesize and quantify preconditions over the transformed program
that represent program states that satisfy a CTL∗ formula.
This paper demonstrates the viability of our approach in practice, thus leading to a new class of fullyautomated
tools capable of proving crucial properties that no tool could previously prove. Additionally, we
consider the linear-past extension to CTL∗ for infinite-state systems in which the past is linear and each
moment in time has a unique past. We discuss the practice of this extension and how it is further supported
through the use of history variables. We have implemented our approach and report our benchmarks carried
out on case studies ranging from smaller programs to demonstrate the expressiveness of CTL∗ specifications,
to larger code bases drawn from device drivers and various industrial examples
2017-03-20T09:56:18Z
On Succinct Representations of Binary Trees
Davoodi, Pooya
Raman, Rajeev
Srinivasa Rao Satti
http://hdl.handle.net/2381/39414
2017-04-19T10:42:00Z
2017-03-08T10:17:53Z
Title: On Succinct Representations of Binary Trees
Authors: Davoodi, Pooya; Raman, Rajeev; Srinivasa Rao Satti
Abstract: We observe that a standard transformation between ordinal trees (arbitrary rooted trees
with ordered children) and binary trees leads to interesting succinct binary tree representations.
There are four symmetric versions of these transformations. Via these transformations we get
four succinct representations of n-node binary trees that use 2n + n/(log n)
^Θ(1) bits and support
(among other operations) navigation, inorder numbering, one of preorder or postorder numbering,
subtree size and lowest common ancestor (LCA) queries. While this functionality, and more, is
also supported in O(1) time using 2n + o(n) bits by Davoodi et al.’s (Phil. Trans. Royal Soc.
A 372 (2014)) extension of a representation by Farzan and Munro (Algorithmica 6 (2014)), their
redundancy, or the o(n) term, is much larger, and their approach may not be suitable for practical
implementations.
One of these transformations is related to the Zaks’ sequence (S. Zaks, Theor. Comput. Sci.
10 (1980)) for encoding binary trees, and we thus provide the first succinct binary tree representation
based on Zaks’ sequence. The ability to support inorder numbering is crucial for the
well-known range-minimum query (RMQ) problem on an array A of n ordered values. Another of
these transformations is equivalent to Fischer and Heun’s (SIAM J. Comput. 40 (2011)) 2d-MinHeap
structure for this problem. Yet another variant allows an encoding of the Cartesian tree of
A to be constructed from A using only O(√n log n) bits of working space.
Description: The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2017-03-08T10:17:53Z
Uncertainty-Driven Black-Box Test Data Generation
Walkinshaw, Neil
Fraser, Gordon
http://hdl.handle.net/2381/39377
2017-02-25T03:55:42Z
2017-02-24T15:26:35Z
Title: Uncertainty-Driven Black-Box 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.
2017-02-24T15:26:35Z
Improved Lower Bounds for Online Hypercube Packing
Heydrich, Sandy
van Stee, Rob
http://hdl.handle.net/2381/39372
2017-02-25T04:03:56Z
2017-02-24T15:00:05Z
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, so-called Harmonic-type algorithms (in two or more dimensions). Lastly, we show that two adaptions of the ideas from the best known one-dimensional packing algorithm to square packing also do not help to break the barrier of 2.
2017-02-24T15:00:05Z
Online bin stretching with three bins
Böhm, Martin
Sgall, Jiri
van Stee, Rob
Veselý, Pavel
http://hdl.handle.net/2381/39336
2018-01-11T02:45:06Z
2017-02-06T16:50:54Z
Title: Online bin stretching with three bins
Authors: Böhm, Martin; Sgall, Jiri; van Stee, Rob; Veselý, Pavel
Abstract: Online Bin Stretching is a semi-online 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.
2017-02-06T16:50:54Z
Ensemble learning for data stream analysis: a survey
Krawczyk, Bartosz
Minku, Leandro L.
Gama, Joao
Stefanowski, Jerzy
Wozniak, Michal
http://hdl.handle.net/2381/39321
2017-03-06T16:37:44Z
2017-02-02T15:35:45Z
Title: Ensemble learning for data stream analysis: a survey
Authors: Krawczyk, Bartosz; Minku, Leandro L.; Gama, Joao; Stefanowski, Jerzy; Wozniak, Michal
Abstract: In many applications of information systems learning algorithms have to act in dynamic environments where data are collected in the form of transient data streams. Compared to static data mining, processing streams imposes new computational requirements for algorithms to incrementally process incoming examples while using limited memory and time. Furthermore, due to the non-stationary characteristics of streaming data, prediction models are often also required to adapt to concept drifts. Out of several new proposed stream algorithms, ensembles play an important role, in particular for non-stationary environments. This paper surveys research on ensembles for data stream classification as well as regression tasks. Besides presenting a comprehensive spectrum of ensemble approaches for data streams, we also discuss advanced learning concepts such as imbalanced data streams, novelty detection, active and semi-supervised learning, complex data representations and structured outputs. The paper concludes with a discussion of open research problems and lines of future research.
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.
2017-02-02T15:35:45Z
Emergent stem cell homeostasis in the C. elegans germline is revealed by hybrid modeling.
Hall, B. A.
Piterman, Nir
Hajnal, A.
Fisher, J.
http://hdl.handle.net/2381/39247
2017-01-21T03:44:59Z
2017-01-20T16:59:18Z
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 cell-cell interactions are required for the formation of three-dimensional 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/S0006-3495(15)00589-5.
2017-01-20T16:59:18Z
Temperature aware online algorithms for minimizing flow time
Birks, Martin
Fung, Stanley P. Y.
http://hdl.handle.net/2381/39199
2017-11-22T02:45:06Z
2017-01-18T10:06:37Z
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 1-competitive, 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.
2017-01-18T10:06:37Z
VOML: A Framework for Modelling Virtual Organizations and Virtual Breeding Environment
Rajper, N. J.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/39111
2017-01-11T03:20:37Z
2017-01-10T10:15:54Z
Title: VOML: A Framework for Modelling Virtual Organizations and Virtual Breeding Environment
Authors: Rajper, N. J.; Reiff-Marganiec, 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 sub-languages, 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.
2017-01-10T10:15:54Z
Relating two automata-based models of orchestration and choreography
Basile, D.
Degano, P.
Ferrari, G. L.
Tuosto, E.
http://hdl.handle.net/2381/39062
2017-01-05T03:24:16Z
2017-01-04T16:46:32Z
Title: Relating two automata-based models of orchestration and choreography
Authors: Basile, D.; Degano, P.; Ferrari, G. L.; Tuosto, E.
Abstract: We investigate the relations between two automata-based 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 channel-based 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 well-formed choreography. Then these results are extended to a more liberal notion of agreement and to a fully asynchronous semantics of communicating machines.
2017-01-04T16:46:32Z
Which Models of the Past Are Relevant to the Present? A software effort estimation approach to exploiting useful past models
Minku, Leandro L.
Yao, X.
http://hdl.handle.net/2381/39042
2017-01-05T03:24:06Z
2017-01-04T10:11:16Z
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 decision-support 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 (cross-company, 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 non-stationary 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 Cross-company 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.
2017-01-04T10:11:16Z
Uncovering Sustainability Concerns in Software Product Lines
Chitchyan, Ruzanna
Groher, Iris
Noppen, Joost
http://hdl.handle.net/2381/39032
2017-04-04T10:42:44Z
2017-01-03T14:19:40Z
Title: Uncovering Sustainability Concerns in Software Product Lines
Authors: Chitchyan, Ruzanna; Groher, Iris; Noppen, Joost
Abstract: Sustainable living, i.e., living within the bounds of the available environmental, social, and economic
resources, is the focus of many present-day 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 sustainability-related characteristics that arise in present-day
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 cross-relations
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 socio-technical system. The good representation of sustainability features in these models is also
validated with two additional case studies
Description: The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2017-01-03T14:19:40Z
Characterizing word problems of groups
Jones, S. A. M.
Thomas, Richard M.
http://hdl.handle.net/2381/38806
2016-12-03T03:57:44Z
2016-12-02T12:39:07Z
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 first-order 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 one-counter languages.
2016-12-02T12:39:07Z
Relation lifting, a survey
Kurz, Alexander
Velebil, J.
http://hdl.handle.net/2381/38793
2016-12-02T03:20:21Z
2016-12-01T15:46:25Z
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 many-valued relations. As applications, it is shown how different notions of bisimulation, simulation and modal logics do arise.
2016-12-01T15:46:25Z
Foreword: special issue on coalgebraic logic
DOBERKAT, E. E.
KURZ, ALEXANDER
http://hdl.handle.net/2381/38792
2016-12-02T03:20:20Z
2016-12-01T15:42:55Z
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.
2016-12-01T15:42:55Z
Asymptotically Optimal Encodings of Range Data Structures for Selection and Top-k Queries
Grossi, Roberto
Iacono, John
Navarro, Gonzalo
Raman, Rajeev
Satti, S. Rao
http://hdl.handle.net/2381/38768
2017-03-10T02:45:07Z
2016-12-01T09:47:09Z
Title: Asymptotically Optimal Encodings of Range Data Structures for Selection and Top-k Queries
Authors: Grossi, Roberto; Iacono, John; Navarro, Gonzalo; Raman, Rajeev; Satti, S. Rao
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) top-k 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 linear-space 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.
2016-12-01T09:47:09Z
Foundations of session types and behavioural contracts
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.
http://hdl.handle.net/2381/38761
2016-11-30T03:21:03Z
2016-11-29T15:45:36Z
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
2016-11-29T15:45:36Z
Compressed bit vectors based on variable-to-fixed encodings
Jo, Seungbum
Joannou, Stelios
Okanohara, Daisuke
Raman, Rajeev
Satti, Srinivasa Ra
http://hdl.handle.net/2381/38749
2017-12-29T02:45:07Z
2016-11-29T11:01:01Z
Title: Compressed bit vectors based on variable-to-fixed encodings
Authors: Jo, Seungbum; Joannou, Stelios; Okanohara, Daisuke; Raman, Rajeev; Satti, Srinivasa Ra
Abstract: We consider practical implementations of compressed bitvectors, which support rank and select
operations on a given bit-string, while storing the bit-string in compressed form. Our approach
relies on variable-to-fixed encodings of the bit-string, 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 bit-string), and is a flexible and promising solution to
the problem of supporting rank and select on moderately compressible bit-strings, such as those
encountered in real-world applications.
Description: Also Conference Paper in Proceedings of the Data Compression Conference March 2014 DOI: 10.1109/DCC.2014.85; The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2016-11-29T11:01:01Z
BTR: training asynchronous Boolean models using single-cell expression data.
Lim, C. Y.
Wang, H.
Woodhouse, S.
Piterman, Nir
Wernisch, L.
Fisher, J.
Göttgens, B.
http://hdl.handle.net/2381/38718
2016-11-26T04:12:07Z
2016-11-25T09:48:49Z
Title: BTR: training asynchronous Boolean models using single-cell 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 single-cell 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 single-cell 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 drop-outs. While many algorithms exist to infer a gene regulatory network, very few of them are able to harness the extra expression states present in single-cell 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 single-cell 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 single-cell 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 single-cell expression data. Boolean model is particularly useful for network reconstruction using single-cell data because it is more robust to the effect of drop-outs. 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 single-cell 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].
2016-11-25T09:48:49Z
SIGACT News Online Algorithms Column 28: Online Matching on the Line, Part 2
Van Stee, Rob
http://hdl.handle.net/2381/38659
2016-11-21T16:28:18Z
2016-11-21T16:27:44Z
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 k-server
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 well-known
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):99-111) 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.
2016-11-21T16:27:44Z
Multi-criteria IoT Resource Discovery: A Comparative Analysis
Nunes, Luiz Henrique
Estrella, Julio Cezar
Perera, Charith
Reiff-Marganiec, Stephan
Delbem, Alexandre Cláudio Botazzo
http://hdl.handle.net/2381/38617
2017-12-14T02:45:07Z
2016-11-18T09:09:25Z
Title: Multi-criteria IoT Resource Discovery: A Comparative Analysis
Authors: Nunes, Luiz Henrique; Estrella, Julio Cezar; Perera, Charith; Reiff-Marganiec, Stephan; Delbem, Alexandre Cláudio Botazzo
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
context-aware 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 context-aware 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 multi-criteria 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 multi-objective 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: The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2016-11-18T09:09:25Z
An Abstract Semantics of the Global View of Choreographies
Guanciale, R.
Tuosto, Emilio
http://hdl.handle.net/2381/38559
2016-11-16T03:22:59Z
2016-11-15T14:45:30Z
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 pre-orders 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
2016-11-15T14:45:30Z
On undefined and meaningless in Lambda definability
De Vries, Fer-Jan
http://hdl.handle.net/2381/38557
2016-11-16T03:22:57Z
2016-11-15T14:35:59Z
Title: On undefined and meaningless in Lambda definability
Authors: De Vries, Fer-Jan
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 lambda-definability, 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
2016-11-15T14:35:59Z
A Distributed Sensor Data Search Platform for Internet of Things Environments
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
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/38324
2016-11-03T03:25:31Z
2016-11-02T16:43:01Z
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; Reiff-Marganiec, 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 non-technical 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.
2016-11-02T16:43:01Z
Proof Transformation via Interpretation Functions: Results, Problems and Applications
Kosiuczenko, Piotr
http://hdl.handle.net/2381/38301
2016-11-01T03:16:48Z
2016-10-31T15:15:55Z
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.
2016-10-31T15:15:55Z
Resampling-based ensemble methods for online class imbalance learning
Wang, Shuo
Minku, Leandro L.
Yao, Xin
http://hdl.handle.net/2381/38239
2016-10-25T02:24:38Z
2016-10-24T15:38:20Z
Title: Resampling-based 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 real-world applications, such as fault diagnosis of real-time 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 time-decayed 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 minority-class 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.
2016-10-24T15:38:20Z
Direction-Reversible Self-Timed Cellular Automata for Delay-Insensitive Circuits
Ulidowski, Irek
Morrison, Daniel
http://hdl.handle.net/2381/38087
2018-01-01T02:45:10Z
2016-09-16T14:24:29Z
Title: Direction-Reversible Self-Timed Cellular Automata for Delay-Insensitive Circuits
Authors: Ulidowski, Irek; Morrison, Daniel
Abstract: We introduce a new Self-Timed Cellular Automaton capable of simulating reversible delay-insensitive circuits. In addition to a number of reversibility and determinism properties, our STCA exhibits direction-reversibility, 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 delay-insensitive circuits, including parallel circuits. We then show which of the reversibility, determinism and direction-reversibility properties hold for these classes of circuits
2016-09-16T14:24:29Z
Reordering Buffer Management with Advice
Van Stee, Rob
Rosen, Adi
Adamaszek, Anna
Renault, Marc. P.
http://hdl.handle.net/2381/38076
2017-06-17T01:45:05Z
2016-09-14T13:15:12Z
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 1-competitive algorithm.
Description: Following the embargo period the above license applies.
2016-09-14T13:15:12Z
Requirements: The Key to Sustainability
Becker, Christoph
Betz, Stefanie
Chitchyan, Ruzanna
Duboc, Leticia
Easterbrook, Steve M.
Penzenstadler, Birgit
Seyff, Norbert
Venters, Colin C.
http://hdl.handle.net/2381/37935
2016-08-10T02:18:04Z
2016-08-09T13:13:22Z
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 mind-set. This shift's focus begins in requirements engineering. This article is part of a special issue on the Future of Software Engineering.
2016-08-09T13:13:22Z
Complexities of Computation: A Survey Report
Jain, A. K.
Jain, Nitin Kumar
http://hdl.handle.net/2381/37604
2016-05-20T02:16:24Z
2016-05-19T10:59:37Z
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.
2016-05-19T10:59:37Z
Interaction Models and Automated Control under Partial Observable Environments
Braberman, Victor
D'Ippolito, Nicolas
Piterman, Nir
Uchitel, Sebastian
Ciolek, Daniel
http://hdl.handle.net/2381/37602
2016-11-25T09:51:46Z
2016-05-18T15:21:12Z
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 non-determinism 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 controller-to-be 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.
2016-05-18T15:21:12Z
Two Dimensional Range Minimum Queries and Fibonacci Lattices
Brodal, Gerth Stølting
Davoodi, Pooya
Lewenstein, Moshe
Raman, Rajeev
Srinivasa Rao, Satti
http://hdl.handle.net/2381/37491
2016-05-07T02:33:45Z
2016-05-06T09:25:06Z
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 (2D-RMQs) ask for the position of the minimum element in a rectangular range within the matrix. We study trade-offs between the query time and the additional space used by indexing data structures that support 2D-RMQs. Using a novel technique—the discrepancy properties of Fibonacci lattices—we give an indexing data structure for 2D-RMQs 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 24-month embargo from publication in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2016-05-06T09:25:06Z
Bin packing in multiple dimensions
van Stee, Rob
http://hdl.handle.net/2381/37457
2016-04-27T13:55:06Z
2016-04-27T13:54:43Z
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 two-dimensional
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 three-dimensional case. I will also survey other results in multidimensional
packing, that were left out in my previous column.
2016-04-27T13:54:43Z
Online algorithms with advice for bin packing and scheduling problems
Renault, Marc P.
Rosén, Adi
van Stee, Rob
http://hdl.handle.net/2381/37456
2016-07-31T01:45:07Z
2016-04-27T13:45:14Z
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 non-constant number (namely, at least (1-2mn)log m, where n is the number of jobs and m is the number of machines) of bits of advice per request is needed.
2016-04-27T13:45:14Z
The cost of selfishness for maximizing the minimum load on uniformly related machines
Epstein, L.
Kleiman, E.
Van Stee, Rob
http://hdl.handle.net/2381/37390
2016-04-20T09:17:08Z
2016-04-20T09:17:00Z
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.
2016-04-20T09:17:00Z
SIGACT news online algorithms column 23
van Stee, Rob
http://hdl.handle.net/2381/37389
2016-04-20T09:14:50Z
2016-04-20T09:13:06Z
Title: SIGACT news online algorithms column 23
Authors: van Stee, Rob
Description: timestamp: Sun, 04 May 2014 01:00:00 +0200 biburl: http://dblp.uni-trier.de/rec/bib/journals/sigact/Stee14 bibsource: dblp computer science bibliography, http://dblp.org
2016-04-20T09:13:06Z