DSpace Collection:
http://hdl.handle.net/2381/1116
2016-10-27T13:00:08Z
2016-10-27T13:00:08Z
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
2016-09-16T15:13:08Z
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
2016-09-15T08:27:01Z
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-05-19T02:16:49Z
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
Dividing connected chores fairly
Heydrich, S.
van Stee, Rob
http://hdl.handle.net/2381/37387
2016-04-20T09:04:49Z
2016-04-20T09:04:38Z
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 so-called price of fairness, concerning fair division of cakes and chores with non-connected 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, envy-freeness 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 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-04-20T09:04:38Z
SIGACT News Online Algorithms Column 27: Online Matching on the Line, Part 1
Van Stee, Rob
http://hdl.handle.net/2381/37327
2016-04-18T09:47:12Z
2016-04-18T09:47:02Z
Title: SIGACT News Online Algorithms Column 27: Online Matching on the Line, Part 1
Authors: Van Stee, Rob
2016-04-18T09:47:02Z
A Unified Approach to Truthful Scheduling on Related Machines
Van Stee, Rob
Epstein, L.
Levin, A.
http://hdl.handle.net/2381/37326
2016-04-18T09:34:03Z
2016-04-18T09:33:53Z
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 p-norm 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 12-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-04-18T09:33:53Z
Run-Time Resolution of Service Property Conflicts in Web Service Composition
Xu, J.
Ning, X.
Reiff-Marganiec, Stephan
Duan, Q.
Zheng, Z.
http://hdl.handle.net/2381/37275
2016-04-14T02:15:31Z
2016-04-13T08:38:30Z
Title: Run-Time Resolution of Service Property Conflicts in Web Service Composition
Authors: Xu, J.; Ning, X.; Reiff-Marganiec, Stephan; Duan, Q.; Zheng, Z.
Abstract: With rapid development of Web service technologies, service composition has become a common approach to realizing complex business processes. Due to the large number of services developed and deployed independently by various providers, undesirable interactions between properties of different service components may occur when they are composed into a composite service. Such service property conflicts become a serious obstacle for service composition to meet users' requirements. Although traditional feature interaction techniques may prevent some property conflicts in service design stage, many conflicts occur during execution based on certain run-time data; therefore must be resolved online. In this paper, we propose a scheme to address the problem of run-time resolution of service property conflicts. We first formulate the conflict resolution problem with a bi-objective optimization model based on user's revenue, which represents the QoS and success rate of a service. Then we solve the bi-objective optimization model to obtain a set of Pareto solutions and rank the solutions to identify the optimal one, which gives the best roll back strategy and alternative service plan for resolving a service property conflict. We also implement the proposed scheme in a prototype of online shopping application and evaluate performance of the scheme through experiments. The obtained experimental results indicate that our scheme is effective and efficient in resolving service property conflicts at runtime.
Description: The file associated with this record is under a 6-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-04-13T08:38:30Z
The Best Two-Phase Algorithm for Bin Stretching
Böhm, M.
Sgall, J.
Van Stee, Rob
Veselý, P.
http://hdl.handle.net/2381/37201
2016-04-09T03:32:45Z
2016-04-08T09:22:21Z
Title: The Best Two-Phase Algorithm for Bin Stretching
Authors: Böhm, M.; Sgall, J.; Van Stee, Rob; Veselý, P.
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 $1.5$ for any number of bins. We build on previous algorithms and use a two-phase 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
2016-04-08T09:22:21Z
Dynamic Selection of Evolutionary Operators Based on Online Learning and Fitness Landscape Analysis
Consoli, P. A.
Mei, Y.
Minku, Leandro Lei
Yao, X.
http://hdl.handle.net/2381/37186
2016-04-08T02:24:53Z
2016-04-07T10:51:27Z
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: Self-adaptive 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.
2016-04-07T10:51:27Z
Honesty by typing
Bartoletti, M.
Scalas, A.
Tuosto, Emilio
Zunino, R.
http://hdl.handle.net/2381/37180
2016-04-08T02:24:50Z
2016-04-07T10:15:59Z
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.
2016-04-07T10:15:59Z
From orchestration to choreography through contract automata
Basile, D.
Degano, P.
Ferrari, G-L.
Tuosto, Emilio
http://hdl.handle.net/2381/37178
2016-04-08T02:24:41Z
2016-04-07T09:40:52Z
Title: From orchestration to choreography through contract automata
Authors: Basile, D.; Degano, P.; Ferrari, G-L.; 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 channel-based 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 well-formed choreography.
2016-04-07T09:40:52Z
Communicating machines as a dynamic binding mechanism of services
Vissani, I.
Pombo, C. G. L.
Tuosto, Emilio
http://hdl.handle.net/2381/37177
2016-04-08T02:24:47Z
2016-04-07T09:08:49Z
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, service-oriented 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 well-known formal orchestration model, based on hypergraphs, for the description of service-oriented 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.
2016-04-07T09:08:49Z
Choreography-Based Analysis of Distributed Message Passing Programs
Taylor, R.
Tuosto, E.
Walkinshaw, Neil
Derrick, J.
http://hdl.handle.net/2381/37150
2016-04-07T02:25:17Z
2016-04-06T08:45:42Z
Title: Choreography-Based Analysis of Distributed Message Passing Programs
Authors: Taylor, R.; Tuosto, E.; Walkinshaw, Neil; Derrick, J.
Abstract: x
2016-04-06T08:45:42Z
Data Mining for Software Engineering and Humans in the Loop
Minku, Leandro L.
Mendes, E.
Turhan, B.
http://hdl.handle.net/2381/37102
2016-04-01T02:31:42Z
2016-03-31T08:54:54Z
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.
2016-03-31T08:54:54Z
Online Ensemble Learning of Data Streams with Gradually Evolved Classes
Sun, Y.
Tang, K.
Minku, Leandro Lei
Wang, S.
Yao, X.
http://hdl.handle.net/2381/36721
2016-08-11T12:41:45Z
2016-02-16T11:35:26Z
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 real-world problems. This paper concerns the scenario where classes emerge or disappear gradually. A class-based ensemble approach, namely Class-Based 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 under-sampling method for the base learners is also proposed to handle the dynamic class-imbalance 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.
2016-02-16T11:35:26Z
Quasivarieties and varieties of ordered algebras : Regularity and exactness
Kurz, Alexander Herbert
Velebil, J.
http://hdl.handle.net/2381/36716
2016-07-18T01:45:07Z
2016-02-15T11:57:40Z
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 6-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-02-15T11:57:40Z
Multi-type display calculus for propositional dynamic logic
Frittella, S.
Greco, G.
Kurz, Alexander Herbert
Palmigiano, A.
http://hdl.handle.net/2381/36715
2016-02-16T03:27:11Z
2016-02-15T11:50:32Z
Title: Multi-type display calculus for propositional dynamic logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander Herbert; Palmigiano, A.
Abstract: We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.
2016-02-15T11:50:32Z
Positive Fragments Of Coalgebraic Logics
Balan, A.
Kurz, Alexander Herbert
Velebil, J.
http://hdl.handle.net/2381/36575
2016-02-05T03:27:16Z
2016-02-04T12:46:07Z
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 weak-pullback 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.
2016-02-04T12:46:07Z
Presenting Distributive Laws
Bonsangue, M. M.
Hansen, H. H.
Kurz, Alexander Herbert
Rot, J.
http://hdl.handle.net/2381/36574
2016-02-05T03:27:17Z
2016-02-04T12:43:36Z
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 algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved 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 context-free languages.
2016-02-04T12:43:36Z
Obligation Blackwell Games and p-Automata
Piterman, Nir
Chatterjee, Krishnendu
http://hdl.handle.net/2381/36416
2016-01-27T11:09:27Z
2016-01-27T11:09:15Z
Title: Obligation Blackwell Games and p-Automata
Authors: Piterman, Nir; Chatterjee, Krishnendu
Abstract: We generalize winning conditions in two-player games by adding a structural acceptance condition
called obligations. Obligations are orthogonal to the linear winning conditions that define whether a play
is winning. Obligations are a declaration that player 0 can achieve a certain value from a configuration. If the
obligation is met, the value of that configuration for player 0 is 1.
We define the value in such games and show that obligation games are determined. For Markov chains
with Borel objectives and obligations, and finite turn-based stochastic parity games with obligations we give an
alternative and simpler characterization of the value function. Based on this simpler definition we show that the
decision problem of winning finite turn-based stochastic parity games with obligations is in NP\co-NP.We also
show that obligation games provide a game framework for reasoning about p-automata.
Description: The file associated with this record is under a permanent embargo while publication is In Press in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.
2016-01-27T11:09:15Z
Drug target optimization in chronic myeloid leukemia using innovative computational platform.
Chuang, Ryan
Hall, Benjamin A.
Benque, David
Cook, Byron
Ishtiaq, Samin
Piterman, Nir
Taylor, Alex
Vardi, Moshe
Koschmieder, Steffen
Gottgens, Berthold
Fisher, Jasmin
http://hdl.handle.net/2381/36302
2016-01-19T03:08:06Z
2016-01-18T14:25:25Z
Title: Drug target optimization in chronic myeloid leukemia using innovative computational platform.
Authors: Chuang, Ryan; Hall, Benjamin A.; Benque, David; Cook, Byron; Ishtiaq, Samin; Piterman, Nir; Taylor, Alex; Vardi, Moshe; Koschmieder, Steffen; Gottgens, Berthold; Fisher, Jasmin
Abstract: Chronic Myeloid Leukemia (CML) represents a paradigm for the wider cancer field. Despite the fact that tyrosine kinase inhibitors have established targeted molecular therapy in CML, patients often face the risk of developing drug resistance, caused by mutations and/or activation of alternative cellular pathways. To optimize drug development, one needs to systematically test all possible combinations of drug targets within the genetic network that regulates the disease. The BioModelAnalyzer (BMA) is a user-friendly computational tool that allows us to do exactly that. We used BMA to build a CML network-model composed of 54 nodes linked by 104 interactions that encapsulates experimental data collected from 160 publications. While previous studies were limited by their focus on a single pathway or cellular process, our executable model allowed us to probe dynamic interactions between multiple pathways and cellular outcomes, suggest new combinatorial therapeutic targets, and highlight previously unexplored sensitivities to Interleukin-3.
2016-01-18T14:25:25Z
Dynamic Software Project Scheduling through a Proactive-rescheduling Method
Shen, Xiao - Ning
Minku, Leandro L.
Bahsoon, Rami
Yao, Xin
http://hdl.handle.net/2381/36291
2016-01-16T03:12:20Z
2016-01-15T12:18:43Z
Title: Dynamic Software Project Scheduling through a Proactive-rescheduling Method
Authors: Shen, Xiao - Ning; Minku, Leandro L.; Bahsoon, Rami; Yao, Xin
Abstract: Software project scheduling in dynamic and uncertain environments is of significant importance to real-world software development. Yet most studies schedule software projects by considering static and deterministic scenarios only, which may cause performance deterioration or even infeasibility when facing disruptions. In order to capture more dynamic features of software project scheduling than the previous work, this paper formulates the project scheduling problem by considering uncertainties and dynamic events that often occur during software project development, and constructs a mathematical model for the resulting Multi-objective Dynamic Project Scheduling Problem (MODPSP), where the four objectives of project cost, duration, robustness and stability are considered simultaneously under a variety of practical constraints. In order to solve MODPSP appropriately, a multi-objective evolutionary algo-rithm (MOEA)based proactive-rescheduling method is proposed, which generates a robust schedule predictively and adapts the previous schedule in response to critical dynamic events during the project execution. Extensive experi-mental results on 21 problem instances, including three instances derived from real-world software projects, show that our novel method is very effective. By introducing the robustness and stability objectives, and incorporating the dynamic optimization strategies specifically designed for MODPSP, our proactive-rescheduling method achieves a very good overall performance in a dynamic environment.
2016-01-15T12:18:43Z
Combining Time Series Prediction Models Using Genetic Algorithm to Auto-scaling Web Applications Hosted in the Cloud Infrastructure
Messias, V. R.
Estrella, J. C.
Ehlers, R.
Santana, M. J.
Santana, R. C.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/35972
2016-01-07T13:58:54Z
2015-12-02T09:22:30Z
Title: Combining Time Series Prediction Models Using Genetic Algorithm to Auto-scaling Web Applications Hosted in the Cloud Infrastructure
Authors: Messias, V. R.; Estrella, J. C.; Ehlers, R.; Santana, M. J.; Santana, R. C.; Reiff-Marganiec, Stephan
Abstract: In a cloud computing environment, companies have the ability to allocate resources according to demand. However, there is a delay that may take minutes between the request for a new resource and it being ready for using. This causes the reactive techniques, which request a new resource only when the system reaches a certain load threshold, to be not suitable for the resource allocation process. To address this problem, it is necessary to predict requests that arrive at the system in the next period of time to allocate the necessary resources, before the system becomes overloaded. There are several time series forecasting models to calculate the workload predictions based on history of monitoring data. However, it is difficult to know which is the best time series forecasting model to be used in each case. The work becomes even more complicated when the user does not have much historical data to be analyzed. Most related work considers only single methods to evaluate the results of the forecast. Other works propose an approach that selects suitable forecasting methods for a given context. But in this case, it is necessary to have a significant amount of data to train the classifier. Moreover, the best solution may not be a specific model, but rather a combination of models. In this paper we propose an adaptive prediction method using genetic algorithms to combine time series forecasting models. Our method does not require a previous phase of training, because it constantly adapts the extent to which the data are coming. To evaluate our proposal, we use three logs extracted from real Web servers. The results show that our proposal often brings the best result and is generic enough to adapt to various types of time series.
Description: The file associated with this record is under a 12-month embargo from publication in accordance with the publisher's self-archiving policy, available at http://www.springer.com/gp/open-access/authors-rights/self-archiving-policy/2124. The full text may be available through the publisher links provided above.
2015-12-02T09:22:30Z
Query-competitive algorithms for cheapest set problems under uncertainty
Erlebach, Thomas R.
Hoffmann, Michael
Kammer, Frank
http://hdl.handle.net/2381/35960
2015-11-28T03:03:31Z
2015-11-27T16:53:41Z
Title: Query-competitive algorithms for cheapest set problems under uncertainty
Authors: Erlebach, Thomas R.; Hoffmann, Michael; Kammer, Frank
Description: This file is under embargo for 18 months from first date of publication.
2015-11-27T16:53:41Z
Performance Evaluation of Resource Management in Cloud Computing Environments
Batista, B. G.
Estrella, J. C.
Ferreira, C. H. G.
Filho, D. M. L.
Nakamura, L. H. V.
Reiff-Marganiec, Stephan
Santana, M. J.
Santana, R. H. C.
http://hdl.handle.net/2381/33451
2015-11-03T03:00:39Z
2015-11-02T11:44:33Z
Title: Performance Evaluation of Resource Management in Cloud Computing Environments
Authors: Batista, B. G.; Estrella, J. C.; Ferreira, C. H. G.; Filho, D. M. L.; Nakamura, L. H. V.; Reiff-Marganiec, Stephan; Santana, M. J.; Santana, R. H. C.
Abstract: Cloud computing is a computational model in which resource providers can offer
on-demand services to clients in a transparent way. However, to be able to guarantee
quality of service without limiting the number of accepted requests, providers must be
able to dynamically manage the available resources so that they can be processed. This
dynamic resource management is not a trivial task, since it involves meeting several
challenges related to workload modeling, virtualization, performance modeling,
deployment and monitoring of applications on virtualized resources. This paper carries
out a performance evaluation of a module for resource management in a cloud
environment that includes handling available resources during execution time and
ensuring the quality of service defined in the service level agreement. An analysis was
conducted of different resource configurations to define which dimension of resource
scaling has a real influence on client requests. The results were used to model and
implement a simulated cloud system, in which the allocated resource can be changed
on-the-fly, with a corresponding change in price. In this way, the proposed module seeks
to satisfy both the client by ensuring quality of service, and the provider by ensuring
the best use of resources at a fair price.
2015-11-02T11:44:33Z
Algorithms for Büchi Games
Chatterjee, K.
Henzinger, Thomas A.
Piterman, Nir
http://hdl.handle.net/2381/33349
2015-10-22T02:00:41Z
2015-10-21T10:59:42Z
Title: Algorithms for Büchi Games
Authors: Chatterjee, K.; Henzinger, Thomas A.; Piterman, Nir
Abstract: The classical algorithm for solving B\"uchi games requires time $O(n\cdot m)$ for game graphs with $n$ states and $m$ edges. For game graphs with constant outdegree, the best known algorithm has running time $O(n^2/\log n)$. We present two new algorithms for B\"uchi games. First, we give an algorithm that performs at most $O(m)$ more work than the classical algorithm, but runs in time O(n) on infinitely many graphs of constant outdegree on which the classical algorithm requires time $O(n^2)$. Second, we give an algorithm with running time $O(n\cdot m\cdot\log\delta(n)/\log n)$, where $1\le\delta(n)\le n$ is the outdegree of the game graph. Note that this algorithm performs asymptotically better than the classical algorithm if $\delta(n)=O(\log n)$.
Description: 11 Pages, Published in GDV 06 (Games in Design and Verification)
2015-10-21T10:59:42Z
Encoding 2-D Range Maximum Queries
Golin, M. J.
Iacono, J.
Krizanc, D.
Raman, Rajeev
Rao, S. S.
Shende, S.
http://hdl.handle.net/2381/33340
2016-01-07T14:04:12Z
2015-10-21T10:36:44Z
Title: Encoding 2-D Range Maximum Queries
Authors: Golin, M. J.; Iacono, J.; Krizanc, D.; Raman, Rajeev; Rao, S. S.; Shende, S.
Abstract: We consider the two-dimensional range maximum query (2D-RMQ) problem: given an array $A$ of ordered values, to pre-process it so that we can find the position of the smallest element in the sub-matrix defined by a (user-specified) range of rows and range of columns. We focus on determining the effective entropy of 2D-RMQ, i.e., how many bits are needed to encode $A$ so that 2D-RMQ queries can be answered without access to $A$. We give tight upper and lower bounds on the expected effective entropy for the case when $A$ contains independent identically-distributed random values, and new upper and lower bounds for arbitrary $A$, for the case when $A$ contains few rows. The latter results improve upon previous upper and lower bounds by Brodal et al. (ESA 2010). In some cases we also give data structures whose space usage is close to the effective entropy and answer 2D-RMQ queries rapidly.
Description: The file associated with this record is under a 24-month embargo from publication in accordance with the publisher's self-archiving policy, available at http://www.elsevier.com/about/company-information/policies/sharing. The full text may be available in the publisher links provided above.
2015-10-21T10:36:44Z
Detecting and Refactoring Operational Smells within the Domain Name System
Radwan, Marwan
Heckel, Reiko
http://hdl.handle.net/2381/33171
2015-10-03T02:10:10Z
2015-10-02T09:47:21Z
Title: Detecting and Refactoring Operational Smells within the Domain Name System
Authors: Radwan, Marwan; Heckel, Reiko
Abstract: The Domain Name System (DNS) is one of the most important components of the Internet infrastructure. DNS relies on a delegation-based architecture, where resolution of names to their IP addresses requires resolving the names of the servers responsible for those names. The recursive structures of the inter dependencies that exist between name servers associated with each zone are called dependency graphs. System administrators' operational decisions have far reaching effects on the DNSs qualities. They need to be soundly made to create a balance between the availability, security and resilience of the system. We utilize dependency graphs to identify, detect and catalogue operational bad smells. Our method deals with smells on a high-level of abstraction using a consistent taxonomy and reusable vocabulary, defined by a DNS Operational Model. The method will be used to build a diagnostic advisory tool that will detect configuration changes that might decrease the robustness or security posture of domain names before they become into production.
Description: In Proceedings GaM 2015, arXiv:1504.02448
2015-10-02T09:47:21Z
The Rabin index of parity games
Huth, M
Kuo, JHP
Piterman, N
http://hdl.handle.net/2381/33162
2015-10-02T02:00:51Z
2015-10-01T15:23:39Z
Title: The Rabin index of parity games
Authors: Huth, M; Kuo, JHP; Piterman, N
Abstract: We study the descriptive complexity of parity games by taking into account the coloring of their game graphs whilst ignoring their ownership structure. Colored game graphs are identified if they determine the same winning regions and strategies, for all ownership structures of nodes. The Rabin index of a parity game is the minimum of the maximal color taken over all equivalent coloring functions. We show that deciding whether the Rabin index is at least k is in PTIME for k=1 but NP-hard for all fixed k > 1. We present an EXPTIME algorithm that computes the Rabin index by simplifying its input coloring function. When replacing simple cycle with cycle detection in that algorithm, its output over-approximates the Rabin index in polynomial time. Experimental results show that this approximation yields good values in practice.
Description: In Proceedings GandALF 2013, arXiv:1307.4162
2015-10-01T15:23:39Z
Obligation Blackwell Games and p-Automata
Piterman, Nir
Chatterjee, Krishnendu
http://hdl.handle.net/2381/33160
2015-10-02T02:00:49Z
2015-10-01T15:17:15Z
Title: Obligation Blackwell Games and p-Automata
Authors: Piterman, Nir; Chatterjee, Krishnendu
Abstract: We recently introduced p-automata, automata that read discrete-time Markov chains. We used turn-based stochastic parity games to define acceptance of Markov chains by a subclass of p-automata. Definition of acceptance required a cumbersome and complicated reduction to a series of turn-based stochastic parity games. The reduction could not support acceptance by general p-automata, which was left undefined as there was no notion of games that supported it.
Here we generalize two-player games by adding a structural acceptance condition called obligations. Obligations are orthogonal to the linear winning conditions that define winning. Obligations are a declaration that player 0 can achieve a certain value from a configuration. If the obligation is met, the value of that configuration for player 0 is 1.
One cannot define value in obligation games by the standard mechanism of considering the measure of winning paths on a Markov chain and taking the supremum of the infimum of all strategies. Mainly because obligations need definition even for Markov chains and the nature of obligations has the flavor of an infinite nesting of supremum and infimum operators. We define value via a reduction to turn-based games similar to Martin's proof of determinacy of Blackwell games with Borel objectives. Based on this definition, we show that games are determined. We show that for Markov chains with Borel objectives and obligations, and finite turn-based stochastic parity games with obligations there exists an alternative and simpler characterization of the value function. Based on this simpler definition we give an exponential time algorithm to analyze finite turn-based stochastic parity games with obligations. Finally, we show that obligation games provide the necessary framework for reasoning about p-automata and that they generalize the previous definition.
2015-10-01T15:17:15Z
Fatal Attractors in Parity Games: Building Blocks for Partial Solvers
Huth, M.
Kuo, J. H. P.
Piterman, Nir
http://hdl.handle.net/2381/33159
2015-10-02T02:00:50Z
2015-10-01T15:12:37Z
Title: Fatal Attractors in Parity Games: Building Blocks for Partial Solvers
Authors: Huth, M.; Kuo, J. H. P.; Piterman, Nir
Abstract: Attractors in parity games are a technical device for solving "alternating" reachability of given node sets. A well known solver of parity games - Zielonka's algorithm - uses such attractor computations recursively. We here propose new forms of attractors that are monotone in that they are aware of specific static patterns of colors encountered in reaching a given node set in alternating fashion. Then we demonstrate how these new forms of attractors can be embedded within greatest fixed-point computations to design solvers of parity games that run in polynomial time but are partial in that they may not decide the winning status of all nodes in the input game. Experimental results show that our partial solvers completely solve benchmarks that were constructed to challenge existing full solvers. Our partial solvers also have encouraging run times in practice. For one partial solver we prove that its run-time is at most cubic in the number of nodes in the parity game, that its output game is independent of the order in which monotone attractors are computed, and that it solves all Buechi games and weak games. We then define and study a transformation that converts partial solvers into more precise partial solvers, and we prove that this transformation is sound under very reasonable conditions on the input partial solvers. Noting that one of our partial solvers meets these conditions, we apply its transformation on 1.6 million randomly generated games and so experimentally validate that the transformation can be very effective in increasing the precision of partial solvers.
2015-10-01T15:12:37Z
Cell-cycle regulation of NOTCH signaling during C. elegans vulval development.
Nusser-Stein, Stefanie
Beyer, Antje
Rimann, Ivo
Adamczyk, Magdalene
Piterman, Nir
Hajnal, Alex
Fisher, Jasmin
http://hdl.handle.net/2381/33107
2015-09-26T02:00:42Z
2015-09-25T15:22:42Z
Title: Cell-cycle regulation of NOTCH signaling during C. elegans vulval development.
Authors: Nusser-Stein, Stefanie; Beyer, Antje; Rimann, Ivo; Adamczyk, Magdalene; Piterman, Nir; Hajnal, Alex; Fisher, Jasmin
Abstract: C. elegans vulval development is one of the best-characterized systems to study cell fate specification during organogenesis. The detailed knowledge of the signaling pathways determining vulval precursor cell (VPC) fates permitted us to create a computational model based on the antagonistic interactions between the epidermal growth factor receptor (EGFR)/RAS/MAPK and the NOTCH pathways that specify the primary and secondary fates, respectively. A key notion of our model is called bounded asynchrony, which predicts that a limited degree of asynchrony in the progression of the VPCs is necessary to break their equivalence. While searching for a molecular mechanism underlying bounded asynchrony, we discovered that the termination of NOTCH signaling is tightly linked to cell-cycle progression. When single VPCs were arrested in the G1 phase, intracellular NOTCH failed to be degraded, resulting in a mixed primary/secondary cell fate. Moreover, the G1 cyclins CYD-1 and CYE-1 stabilize NOTCH, while the G2 cyclin CYB-3 promotes NOTCH degradation. Our findings reveal a synchronization mechanism that coordinates NOTCH signaling with cell-cycle progression and thus permits the formation of a stable cell fate pattern.
2015-09-25T15:22:42Z
The Sorting Buffer Problem is NP-hard
Chan, Ho-Leung
Megow, Nicole
Stee, Rob van
Sitters, Rene
http://hdl.handle.net/2381/33106
2015-09-26T02:00:40Z
2015-09-25T15:14:43Z
Title: The Sorting Buffer Problem is NP-hard
Authors: Chan, Ho-Leung; Megow, Nicole; Stee, Rob van; Sitters, Rene
Abstract: We consider the offline sorting buffer problem. The input is a sequence of items of different types. All items must be processed one by one by a server. The server is equipped with a random-access buffer of limited capacity which can be used to rearrange items. The problem is to design a scheduling strategy that decides upon the order in which items from the buffer are sent to the server. Each type change incurs unit cost, and thus, the cost minimizing objective is to minimize the total number of type changes for serving the entire sequence. This problem is motivated by various applications in manufacturing processes and computer science, and it has attracted significant attention in the last few years. The main focus has been on online competitive algorithms. Surprisingly little is known on the basic offline problem. In this paper, we show that the sorting buffer problem with uniform cost is NP-hard and, thus, close one of the most fundamental questions for the offline problem. On the positive side, we give an O(1)-approximation algorithm when the scheduler is given a buffer only slightly larger than double the original size. We also give a dynamic programming algorithm for the special case of buffer size two that solves the problem exactly in linear time, improving on the standard DP which runs in cubic time.
2015-09-25T15:14:43Z
Improved Practical Compact Dynamic Tries
Poyias, Andreas
Raman, Rajeev
http://hdl.handle.net/2381/33033
2016-09-05T01:45:11Z
2015-09-10T08:36:15Z
Title: Improved Practical Compact Dynamic Tries
Authors: Poyias, Andreas; Raman, Rajeev
Abstract: We consider the problem of implementing a dynamic trie with an emphasis on good practical performance. For a trie with n nodes with an alphabet of size σ, the information-theoretic lower bound is nlogσ+O(n) bits. The Bonsai data structure [1] supports trie operations in O(1) expected time (based on assumptions about the behaviour of hash functions). While its practical speed performance is excellent, its space usage of (1+ϵ)n(logσ+O(loglogn)) bits, where ϵ is any constant >0, is not asymptotically optimal. We propose an alternative, m-Bonsai, that uses (1+ϵ)n(logσ+O(1)) bits in expectation, and supports operations in O(1) expected time (again based on assumptions about the behaviour of hash functions). We give a heuristic implementation of m-Bonsai which uses considerably less memory and is slightly faster than the original Bonsai.
2015-09-10T08:36:15Z
The infinitary lambda calculus of the infinite eta Böhm trees
Severi, Paula
de Vries, Fer-Jan
http://hdl.handle.net/2381/32973
2016-02-17T02:45:08Z
2015-08-24T14:09:28Z
Title: The infinitary lambda calculus of the infinite eta Böhm trees
Authors: Severi, Paula; de Vries, Fer-Jan
Abstract: In this paper, we introduce a strong form of eta reduction called etabang that we use to construct a confluent and normalising infinitary lambda calculus, of which the normal forms correspond to Barendregt's infinite eta Böhm trees. This new infinitary perspective on the set of infinite eta Böhm trees allows us to prove that the set of infinite eta Böhm trees is a model of the lambda calculus. The model is of interest because it has the same local structure as Scott's D∞-models, i.e. two finite lambda terms are equal in the infinite eta Böhm model if and only if they have the same interpretation in Scott's D∞-models.
2015-08-24T14:09:28Z
A Forward Analysis for Recurrent Sets
Bakhirkin, Alexey
Berdine, J.
Piterman, Nir
http://hdl.handle.net/2381/32409
2016-09-02T01:45:06Z
2015-06-23T10:23:14Z
Title: A Forward Analysis for Recurrent Sets
Authors: Bakhirkin, Alexey; Berdine, J.; Piterman, Nir
Abstract: Non-termination of structured imperative programs is primarily due to infinite loops. An important class of non-terminating loop behaviors can be characterized using the notion of recurrent sets. A recurrent set is a set of states from which execution of the loop cannot or might not escape. Existing analyses that infer recurrent sets to our knowledge rely on one of: the combination of forward and backward analyses, quantifier elimination, or SMT-solvers. We propose a purely forward abstract interpretation–based analysis that can be used together with a possibly complicated abstract domain where none of the above is readily available. The analysis searches for a recurrent set of every individual loop in a program by building a graph of abstract states and analyzing it in a novel way. The graph is searched for a witness of a recurrent set that takes the form of what we call a recurrent component which is somewhat similar to the notion of an end component in a Markov decision process.
2015-06-23T10:23:14Z
SEPIA: Search for Proofs Using Inferred Automata
Gransden, Thomas
Walkinshaw, Neil
Raman, Rajeev
http://hdl.handle.net/2381/32390
2016-08-01T01:45:08Z
2015-06-18T15:48:49Z
Title: SEPIA: Search for Proofs Using Inferred Automata
Authors: Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev
Abstract: This paper describes SEPIA, a tool for automated proof
generation in Coq. SEPIA combines model inference with interactive
theorem proving. Existing proof corpora are modelled using state-based
models inferred from tactic sequences. These can then be traversed automatically
to identify proofs. The SEPIA system is described and its
performance evaluated on three Coq datasets. Our results show that
SEPIA provides a useful complement to existing automated tactics in
Coq.
2015-06-18T15:48:49Z
Mobile learning in a human geography field course
Jarvis, Claire
Tate, Nicholas
Dickie, Jennifer
Brown, Gavin
http://hdl.handle.net/2381/32345
2015-06-04T02:00:18Z
2015-06-03T09:03:12Z
Title: Mobile learning in a human geography field course
Authors: Jarvis, Claire; Tate, Nicholas; Dickie, Jennifer; Brown, Gavin
Editors: Mitchell, J.
Abstract: This paper reports on reusable mobile digital learning resources designed to assist human geography undergraduate students in exploring the geographies of life in Dublin. Developing active learning that goes beyond data collection to encourage observation and thinking in the field is important. Achieving this in the context of large class sizes presents several challenges. Combining in-situ learning with spatially-accurate historical and contemporary multimedia, we developed a set of location-aware digital mobile tools or ‘mediascapes’. We explore how scaffolding can be achieved in such a context, focusing on the development of students’ observational, enquiry and thinking skills in the field.
2015-06-03T09:03:12Z
Online interval scheduling on uniformly related machines
Van Stee, Rob
Epstein, Leah
Jez, Lukasz
Sgall, Jiri
http://hdl.handle.net/2381/32329
2015-11-16T11:41:40Z
2015-06-01T15:36:42Z
Title: Online interval scheduling on uniformly related machines
Authors: Van Stee, Rob; Epstein, Leah; Jez, Lukasz; Sgall, Jiri
Abstract: We consider online preemptive scheduling of jobs with fixed starting times revealed at those times on
m uniformly related machines, with the goal of maximizing the total weight of completed jobs. Every job
has a size and a weight associated with it. A newly released job must be either assigned to start running
immediately on a machine or otherwise it is dropped. It is also possible to drop an already scheduled
job, but only completed jobs contribute their weights to the profit of the algorithm.
In the most general setting, no algorithm has bounded competitive ratio, and we consider a number of
standard variants. We give a full classification of the variants into cases which admit constant competitive
ratio (weighted and unweighted unit jobs, and C-benevolent instances, which is a wide class of instances
containing proportional-weight jobs), and cases which admit only a linear competitive ratio (unweighted
jobs and D-benevolent instances). In particular, we give a lower bound of m on the competitive ratio for
scheduling unit weight jobs with varying sizes, which is tight. For unit size and weight we show that
a natural greedy algorithm is 4/3-competitive and optimal on m = 2 machines, while for large m, its
competitive ratio is between 1.56 and 2. Furthermore, no algorithm is better than 1.5-competitive.
Description: 12 mth embargo
2015-06-01T15:36:42Z
A unified approach to truthful scheduling on related machines
Van Stee, Rob
Epstein, Leah
Levin, Asaf
http://hdl.handle.net/2381/32328
2015-11-20T14:56:40Z
2015-06-01T15:24:13Z
Title: A unified approach to truthful scheduling on related machines
Authors: Van Stee, Rob; Epstein, Leah; Levin, Asaf
Abstract: We present a unified framework for designing deterministic monotone polynomial time approximation
schemes (PTAS’s) 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 lp-norm 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.
The idea of our novel method is to show that for goal functions that are sufficiently well-behaved
functions of the machine loads, it is possible to compute in polynomial time a highly structured nearly
optimal schedule. An interesting aspect of our approach is that, in contrast to all known approximation
schemes, we avoid rounding any job sizes or speeds throughout. We can therefore find the exact best
structured schedule using dynamic programming. The state space encodes a sufficient amount of information
such that no postprocessing is needed, allowing an elegant and relatively simple analysis without
any special cases. The monotonicity is a consequence of the fact that we find the best schedule in a
specific collection of schedules.
In the game-theoretical setting of these scheduling problems, there is a social goal, which is one of
the objective functions that we study. Each machine is controlled by a selfish single-parameter agent.
The private information of an agent is its cost of processing a unit-sized job, which is also the inverse
of the speed of its machine. Each agent wishes to maximize its own profit, defined as the payment
it receives from the mechanism minus its cost for processing all jobs assigned to it, and places a bid
which corresponds to its private information. Monotone approximation schemes have an important role
in the emerging area of algorithmic mechanism design, as in the case of single-parameter agents, a
necessary and sufficient condition for truthfulness with respect to the bids is that the allocation algorithm
be monotone. For each one of the problems, we show that we can calculate payments that guarantee
truthfulness in an efficient manner. Thus, there exists a dominant strategy where agents report their true
speeds, and we show the existence of a truthful mechanism which can be implemented in polynomial
time, where the social goal is approximated within a factor of 1 + ε for every ε > 0.
Description: 12 mth embargo
2015-06-01T15:24:13Z
The Price of Anarchy for Selfish Ring Routing is Two
Chen, Xujin
Doerr, Benjamin
Doerr, Carola
Hu, Xiaodong
Ma, Weidong
van Stee, Rob
http://hdl.handle.net/2381/32326
2015-06-01T14:54:05Z
2015-06-01T14:53:47Z
Title: The Price of Anarchy for Selfish Ring Routing is Two
Authors: Chen, Xujin; Doerr, Benjamin; Doerr, Carola; Hu, Xiaodong; Ma, Weidong; van Stee, Rob
Abstract: We analyze the network congestion game with atomic players, asymmetric strategies, and the maximum latency among all players as social cost. This important social cost function is much less understood than the average latency. We show that the price of anarchy is at most two, when the network is a ring and the link latencies are linear. Our bound is tight. This is the first sharp bound for the maximum latency objective.
Description: © ACM, 2014. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Transactions on Economics and Computation archive
Volume 2 Issue 2, June 2014 http://doi.acm.org/10.1145/2548545
2015-06-01T14:53:47Z
SIGACT news online algorithms column 24: 2014 so far
van Stee, Rob
http://hdl.handle.net/2381/32323
2015-06-01T10:56:07Z
2015-06-01T10:55:27Z
Title: SIGACT news online algorithms column 24: 2014 so far
Authors: van Stee, Rob
Abstract: In this column, I will discuss some recent papers in online algorithms. It is pleasing to see there
were a number of papers about online algorithms in the top conferences this year. If I have missed
your paper and you want to write about it or about any other topic in online algorithms, don't
hesitate to contact me!
2015-06-01T10:55:27Z