DSpace Collection:
http://hdl.handle.net/2381/1116
20160214T23:03:37Z

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

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

Obligation Blackwell Games and pAutomata
http://hdl.handle.net/2381/36416
Title: Obligation Blackwell Games and pAutomata
Authors: Piterman, Nir; Chatterjee, Krishnendu
Abstract: We generalize winning conditions in twoplayer 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 turnbased 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 turnbased stochastic parity games with obligations is in NP\coNP.We also
show that obligation games provide a game framework for reasoning about pautomata.
Description: The file associated with this record is under a permanent embargo while publication is In Press in accordance with the publisher's selfarchiving policy. The full text may be available through the publisher links provided above.
20160127T11:09:15Z

Drug target optimization in chronic myeloid leukemia using innovative computational platform.
http://hdl.handle.net/2381/36302
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 userfriendly computational tool that allows us to do exactly that. We used BMA to build a CML networkmodel 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 Interleukin3.
20160118T14:25:25Z

Dynamic Software Project Scheduling through a Proactiverescheduling Method
http://hdl.handle.net/2381/36291
Title: Dynamic Software Project Scheduling through a Proactiverescheduling 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 realworld 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 Multiobjective 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 multiobjective evolutionary algorithm (MOEA)based proactiverescheduling 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 experimental results on 21 problem instances, including three instances derived from realworld 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 proactiverescheduling method achieves a very good overall performance in a dynamic environment.
20160115T12:18:43Z

Combining Time Series Prediction Models Using Genetic Algorithm to Autoscaling Web Applications Hosted in the Cloud Infrastructure
http://hdl.handle.net/2381/35972
Title: Combining Time Series Prediction Models Using Genetic Algorithm to Autoscaling Web Applications Hosted in the Cloud Infrastructure
Authors: Messias, V. R.; Estrella, J. C.; Ehlers, R.; Santana, M. J.; Santana, R. C.; ReiffMarganiec, 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 12month embargo from publication in accordance with the publisher's selfarchiving policy, available at http://www.springer.com/gp/openaccess/authorsrights/selfarchivingpolicy/2124. The full text may be available through the publisher links provided above.
20151202T09:22:30Z

Querycompetitive algorithms for cheapest set problems under uncertainty
http://hdl.handle.net/2381/35960
Title: Querycompetitive 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.
20151127T16:53:41Z

Performance Evaluation of Resource Management in Cloud Computing Environments
http://hdl.handle.net/2381/33451
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.; ReiffMarganiec, Stephan; Santana, M. J.; Santana, R. H. C.
Abstract: Cloud computing is a computational model in which resource providers can offer
ondemand 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
onthefly, 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.
20151102T11:44:33Z

Algorithms for Büchi Games
http://hdl.handle.net/2381/33349
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)
20151021T10:59:42Z

Encoding 2D Range Maximum Queries
http://hdl.handle.net/2381/33340
Title: Encoding 2D Range Maximum Queries
Authors: Golin, M. J.; Iacono, J.; Krizanc, D.; Raman, Rajeev; Rao, S. S.; Shende, S.
Abstract: We consider the twodimensional range maximum query (2DRMQ) problem: given an array $A$ of ordered values, to preprocess it so that we can find the position of the smallest element in the submatrix defined by a (userspecified) range of rows and range of columns. We focus on determining the effective entropy of 2DRMQ, i.e., how many bits are needed to encode $A$ so that 2DRMQ 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 identicallydistributed 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 2DRMQ queries rapidly.
Description: The file associated with this record is under a 24month embargo from publication in accordance with the publisher's selfarchiving policy, available at http://www.elsevier.com/about/companyinformation/policies/sharing. The full text may be available in the publisher links provided above.
20151021T10:36:44Z

Detecting and Refactoring Operational Smells within the Domain Name System
http://hdl.handle.net/2381/33171
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 delegationbased 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 highlevel 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
20151002T09:47:21Z

The Rabin index of parity games
http://hdl.handle.net/2381/33162
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 NPhard 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 overapproximates 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
20151001T15:23:39Z

Obligation Blackwell Games and pAutomata
http://hdl.handle.net/2381/33160
Title: Obligation Blackwell Games and pAutomata
Authors: Piterman, Nir; Chatterjee, Krishnendu
Abstract: We recently introduced pautomata, automata that read discretetime Markov chains. We used turnbased stochastic parity games to define acceptance of Markov chains by a subclass of pautomata. Definition of acceptance required a cumbersome and complicated reduction to a series of turnbased stochastic parity games. The reduction could not support acceptance by general pautomata, which was left undefined as there was no notion of games that supported it.
Here we generalize twoplayer 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 turnbased 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 turnbased 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 turnbased stochastic parity games with obligations. Finally, we show that obligation games provide the necessary framework for reasoning about pautomata and that they generalize the previous definition.
20151001T15:17:15Z

Fatal Attractors in Parity Games: Building Blocks for Partial Solvers
http://hdl.handle.net/2381/33159
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 fixedpoint 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 runtime 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.
20151001T15:12:37Z

Cellcycle regulation of NOTCH signaling during C. elegans vulval development.
http://hdl.handle.net/2381/33107
Title: Cellcycle regulation of NOTCH signaling during C. elegans vulval development.
Authors: NusserStein, Stefanie; Beyer, Antje; Rimann, Ivo; Adamczyk, Magdalene; Piterman, Nir; Hajnal, Alex; Fisher, Jasmin
Abstract: C. elegans vulval development is one of the bestcharacterized 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 cellcycle 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 CYD1 and CYE1 stabilize NOTCH, while the G2 cyclin CYB3 promotes NOTCH degradation. Our findings reveal a synchronization mechanism that coordinates NOTCH signaling with cellcycle progression and thus permits the formation of a stable cell fate pattern.
20150925T15:22:42Z

The Sorting Buffer Problem is NPhard
http://hdl.handle.net/2381/33106
Title: The Sorting Buffer Problem is NPhard
Authors: Chan, HoLeung; 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 randomaccess 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 NPhard 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.
20150925T15:14:43Z

Improved Practical Compact Dynamic Tries
http://hdl.handle.net/2381/33033
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 informationtheoretic 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, mBonsai, 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 mBonsai which uses considerably less memory and is slightly faster than the original Bonsai.
20150910T08:36:15Z

The infinitary lambda calculus of the infinite eta Böhm trees
http://hdl.handle.net/2381/32973
Title: The infinitary lambda calculus of the infinite eta Böhm trees
Authors: Severi, Paula; de Vries, FerJan
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.
20150824T14:09:28Z

A Forward Analysis for Recurrent Sets
http://hdl.handle.net/2381/32409
Title: A Forward Analysis for Recurrent Sets
Authors: Bakhirkin, Alexey; Berdine, J.; Piterman, Nir
Abstract: Nontermination of structured imperative programs is primarily due to infinite loops. An important class of nonterminating 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 SMTsolvers. 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.
20150623T10:23:14Z

SEPIA: Search for Proofs Using Inferred Automata
http://hdl.handle.net/2381/32390
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 statebased
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.
20150618T15:48:49Z

Mobile learning in a human geography field course
http://hdl.handle.net/2381/32345
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 insitu learning with spatiallyaccurate historical and contemporary multimedia, we developed a set of locationaware 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.
20150603T09:03:12Z

Online interval scheduling on uniformly related machines
http://hdl.handle.net/2381/32329
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 Cbenevolent instances, which is a wide class of instances
containing proportionalweight jobs), and cases which admit only a linear competitive ratio (unweighted
jobs and Dbenevolent 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/3competitive 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.5competitive.
Description: 12 mth embargo
20150601T15:36:42Z

A unified approach to truthful scheduling on related machines
http://hdl.handle.net/2381/32328
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 lpnorm 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 wellbehaved
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 gametheoretical 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 singleparameter agent.
The private information of an agent is its cost of processing a unitsized 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 singleparameter 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
20150601T15:24:13Z

The Price of Anarchy for Selfish Ring Routing is Two
http://hdl.handle.net/2381/32326
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
20150601T14:53:47Z

SIGACT news online algorithms column 24: 2014 so far
http://hdl.handle.net/2381/32323
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!
20150601T10:55:27Z

The Description Logic SHIQ with a Flexible Metamodelling Hierarchy
http://hdl.handle.net/2381/32284
Title: The Description Logic SHIQ with a Flexible Metamodelling Hierarchy
Authors: Severi, Paula G.; Motz, Regina; Rohrer, Edelweis
Abstract: This work is motivated by a realworld case study where it is necessary to integrate and relate existing ontologies through metamodelling. For this, we introduce the Description Logic SHIQM which is obtained from SHIQ byadding statements that equate individuals to concepts in a knowledge base. In this new extension, concepts can be individuals of another concept (called metaconcept) which itself can be an individual of yet another concept (called meta metaconcept ) and so on. We define an algorithm that checks consistency of SHIQM by modifying the Tableau algorithm for SHIQ. From the practical point of view, this has the advantage that we can reuse the code of existing OWL reasoners. From the theoretical point of view, it has a similar advantage of reuse. We make use of the existing results and proofs that lead to correctness of the algorithm for SHIQ in order to prove correctness of the algorithm for SHIQM.
20150519T10:58:05Z

HIAWSC: An Immune Algorithm Based Heuristic Web Service Composition Framework
http://hdl.handle.net/2381/32251
Title: HIAWSC: An Immune Algorithm Based Heuristic Web Service Composition Framework
Authors: Xu, J.; ReiffMarganiec, Stephan
Abstract: The introduction of of web services has led to web service composition being a focus of many researchers. Composing web services using workflows is seen as the most realistic method from an industrial viewpoint. Amongst other method, the use of natural computing methods has been proposed previously to automate web service composition. The need for a fast response when computing the most suitable sequence of services is addressed in this paper. In particular, we propose a novel heuristic immune algorithm with an efficient encoding and mutation method. The algorithm involves two steps: an immune selection operation, which is maintaining antibody population diversity and the clonal selection. The use of a vaccine during the evolution provides heuristic information that accelerates the convergence. Our experimental results illustrate that the proposed heuristic immune algorithm is very effective in improving the convergence speed. We also provide a schema analysis for this method.
20150508T14:39:51Z

Space Efficient Data Structures for Nearest Larger Neighbor
http://hdl.handle.net/2381/32214
Title: Space Efficient Data Structures for Nearest Larger Neighbor
Authors: Jayapaul, V.; Jo, S.; Raman, V.; Raman, Rajeev; Rao, S. R.
Abstract: Given a sequence of n elements from a totally ordered set, and a position in the sequence, the nearest larger neighbor (NLN) query
returns the position of the element which is closest to the query position, and is larger than the element at the query position.
The problem of finding all nearest larger neighbors has attracted interest due to its applications for parenthesis matching and in
computational geometry [1, 2, 3]. We consider a data structure version of this problem, which is to preprocess a given sequence of
elements to construct a data structure that can answer NLN queries efficiently. We consider timespace tradeoffs for the problem
in both the encoding (where the input is not accessible after the data structure has been created) and indexing model, and consider
cases when the input is in a one dimensional array, and also initiate the study of this problem on twodimensional arrays.
20150507T11:21:31Z

Decoding the regulatory network for blood development from single cell gene expression measurements
http://hdl.handle.net/2381/32202
Title: Decoding the regulatory network for blood development from single cell gene expression measurements
Authors: Piterman, Nir; Moignard, V.; Woodhouse, S.; Haghverdi, L.; Lilly, J.; Tanaka, Y.; Wilkinson, A.; Buettner, F.; Macaulay, I.; Jawaid, W.; Diamanti, E.; Nishikawa, S.I.; Kouskoff, V.; Theis, F.; Fisher, J.
Description: 6 month embargo
20150507T10:43:26Z

The Rabin Index of Parity Games: Its Complexity and Approximation
http://hdl.handle.net/2381/32196
Title: The Rabin Index of Parity Games: Its Complexity and Approximation
Authors: Huth, M.; Kuo, J. HP.; Piterman, Nir
Abstract: We study the descriptive complexity of parity games by taking into account the coloring of their game graphs whilst ignoring their ownership structure. Colorings of 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 P for k = 1 but NPhard for all fixed k>=2. 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 overapproximates the Rabin index in polynomial time. We evaluate this efficient algorithm as a preprocessor of solvers in detailed experiments: for Zielonka’s solver [17] on random and structured parity games and for the partial solver psolB [11] on random games.
Description: May be CCBY
20150507T10:39:37Z

Tree Compression with Top Trees Revisited
http://hdl.handle.net/2381/32187
Title: Tree Compression with Top Trees Revisited
Authors: HübschleSchneider, L.; Raman, Rajeev
Abstract: We revisit tree compression with top trees (Bille et al. Information & Computation 2015), and present several improvements to the compressor and its analysis. By significantly reducing the amount of information stored and guiding the compression step using a RePairinspired heuristic, we obtain a fast compressor achieving good compression ratios, addressing an open problem posed by Bille et al. We show how, with relatively small overhead, the compressed file can be converted into an inmemory representation that supports basic navigation operations in worstcase logarithmic time without decompression. We also show a much improved worstcase bound on the size of the output of toptree compression (answering an open question posed in a talk on this algorithm by Weimann in 2012).
20150507T10:28:34Z

Random access to grammarcompressed strings and trees
http://hdl.handle.net/2381/32182
Title: Random access to grammarcompressed strings and trees
Authors: Bille, P.; Landau, G. M.; Raman, Rajeev; Sadakane, K.; Satti, S. R.; Weimann, O.
Abstract: Grammar based compression, where one replaces a long string by a small contextfree
grammar that generates the string, is a simple and powerful paradigm that captures (sometimes with
slight reduction in efficiency) many of the popular compression schemes, including the LempelZiv
family, RunLength Encoding, BytePair Encoding, Sequitur, and RePair. In this paper, we present
a novel grammar representation that allows efficient random access to any character or substring
without decompressing the string.
Let S be a string of length N compressed into a contextfree grammar S of size n. We present
two representations of S achieving O(log N) random access time, and either O(n·αk(n)) construction
time and space on the pointer machine model, or O(n) construction time and space on the RAM.
Here, αk(n) is the inverse of the k th row of Ackermann’s function. Our representations also efficiently
support decompression of any substring in S: we can decompress any substring of length m in the
same complexity as a single random access query and additional O(m) time. Combining these
results with fast algorithms for uncompressed approximate string matching leads to several efficient
algorithms for approximate string matching on grammar compressed strings without decompression.
For instance, we can find all approximate occurrences of a pattern P with at most k errors in time
O(n(min{Pk, k^4 + P} + log N) + occ), where occ is the number of occurrences of P in S. Finally,
we generalize our results to navigation and other operations on grammarcompressed ordered trees.
All of the above bounds significantly improve the currently best known results. To achieve these
bounds, we introduce several new techniques and data structures of independent interest, including
a predecessor data structure, two “biased” weighted ancestor data structures, and a compact
representation of heavy paths in grammars.
Description: AMS subject classifications. 68P05, 68P30
20150507T10:26:27Z

Fast Data Processing for LargeScale SOA and EventBased Systems
http://hdl.handle.net/2381/32175
Title: Fast Data Processing for LargeScale SOA and EventBased Systems
Authors: Tilly, M.; ReiffMarganiec, Stephan
Abstract: The deluge of intelligent objects that are providing continuous access to data
and services on one hand and the demand of developers and consumers to
handle these data on the other hand require us to think about new
communication paradigms and middleware. In hyperscale systems, such as
in the Internet of Things, large scale sensor networks or even mobile
networks, one emerging requirement is to process, procure, and provide
information with almost zero latency. This work is introducing new concepts
for a middleware to enable fast communication by limiting information flow
with filtering concepts using policy obligations and combining data
processing techniques adopted from complex event processing.
20150507T10:22:56Z

A unified approach to truthful scheduling on related machines
http://hdl.handle.net/2381/32171
Title: A unified approach to truthful scheduling on related machines
Authors: Epstein, L.; Levin, A.; Van Stee, Rob
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 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. The idea of our novel method is to show that for goal functions that are sufficiently wellbehaved 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 gametheoretical 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 singleparameter agent. The private information of an agent is its cost of processing a unitsized 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 singleparameter 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.
20150507T10:20:21Z

DCASERVICES: A distributed and collaborative architecture for conducting experiments in service oriented systems
http://hdl.handle.net/2381/32151
Title: DCASERVICES: A distributed and collaborative architecture for conducting experiments in service oriented systems
Authors: Nunes, L. H.; Ferreira, C. H. G.; Nakamura, L. H. V.; Libardi, R. M. D. O.; de Oliveira, E. M.; Kuehne, B. T.; Souza, P. S. L.; Santana, R. H. C.; Santana, M. J.; Estrella, J. C.; ReiffMarganiec, Stephan
Abstract: Current distributed computing environments, such as Cloud Computing, Grid Computing and Internet of Things are
typically complex and present dynamic scenarios, which makes the execution of experiments, tests and performance
evaluations challenging. Performing large scale experiments in ServiceOriented Computing (SOC) environments can
be a difficult and complex task. In this paper, we propose a Distributed and Collaborative Architecture for Conducting
Experiments in Service Oriented Systems (DCASERVICES). DCASERVICES is a clientserver architecture that provides
a real environment to execute experiments in systems based on the SOC paradigm. Using the DCASERVICES and our
tool named Planning and Execution of Experiments in Service Oriented Systems (PEESOS) developed in our previously
work presented at ICWS 2014, we were able to execute experiments, tests, and analyze a target system environment
quickly and efficiently.
20150507T10:08:45Z

AWSCS  A system to evaluate different approaches for the automatic composition and execution of web services flows
http://hdl.handle.net/2381/32089
Title: AWSCS  A system to evaluate different approaches for the automatic composition and execution of web services flows
Authors: Kuehne, B. T.; Nunes, L. H.; Martins de Oliveira, E.; Nakamura, L.; Ferreira, C. H.; Estrella, J. C.; Santana, R.; Santana, M. J.; ReiffMarganiec, Stephan
Abstract: This paper proposes a system named AWSCS (Automatic Web Service Composition System) to evaluate
different approaches for automatic composition of Web services, based on QoS parameters that are
measured at execution time. The AWSCS is a system to implement different approaches for automatic
composition of Web services and also to execute the resulting flows from these approaches. Aiming at
demonstrating the results of this paper, a scenario was developed, where empirical flows were built to
demonstrate the operation of AWSCS, since algorithms for automatic composition are not readily available
to test. The results allows to study the behaviour of running composite Web services, when flows with
the same functionality but different problemsolving strategies were compared. Furthermore we observed
the influence of the load applied on the running system as the type of load submitted to the system
is an important factor to define which approach for the Web service composition can achieve the best
performance in production.
20150430T13:17:35Z

Assessing and generating test sets in terms of behavioural adequacy
http://hdl.handle.net/2381/31971
Title: Assessing and generating test sets in terms of behavioural adequacy
Authors: Fraser, G.; Walkinshaw, Neil
Editors: Offutt, J.
Abstract: Identifying a finite test set that adequately captures the essential behaviour of a program such that all faults are identified is a wellestablished problem. This is traditionally addressed with syntactic adequacy metrics (e.g. branch coverage), but these can be impractical and may be misleading even if they are satisfied. One intuitive notion of adequacy, which has been discussed in theoretical terms over the past three decades, is the idea of behavioural coverage: If it is possible to infer an accurate model of a system from its test executions, then the test set can be deemed to be adequate. Despite its intuitive basis, it has remained almost entirely in the theoretical domain because inferred models have been expected to be exact (generally an infeasible task) and have not allowed for any pragmatic interim measures of adequacy to guide test set generation. This paper presents a practical approach to incorporate behavioural coverage. Our bestest approach (1) enables the use of machine learning algorithms to augment standard syntactic testing approaches and (2) shows how searchbased testing techniques can be applied to generate test sets with respect to this criterion. An empirical study on a selection of Java units demonstrates that test sets with higher behavioural coverage significantly outperform current baseline test criteria in terms of detected faults.
20150410T10:17:43Z

Resolving nondeterminism in choreographies
http://hdl.handle.net/2381/31873
Title: Resolving nondeterminism in choreographies
Authors: Bocchi, L.; Melgratti, H.; Tuosto, Emilio
Abstract: Resolving nondeterministic choices of choreographies is a crucial task. We introduce a novel notion of realisability for choreographies called wholespectrum implementation that rules out deterministic implementations of roles that, no matter which context they are placed in, will never follow one of the branches of a nondeterministic choice. We show that, under some conditions, it is decidable whether an implementation is wholespectrum. As a case study, we analyse the POP protocol under the lens of wholespectrum implementation. © 2014 SpringerVerlag.
20150316T11:59:32Z

Inferring Extended Finite State Machine Models from Software Executions
http://hdl.handle.net/2381/31765
Title: Inferring Extended Finite State Machine Models from Software Executions
Authors: Walkinshaw, Neil; Taylor, R.; Derrick, J.
Editors: Robbes, R.; Oliveto, R.; Di Penta, M.
Abstract: The ability to reverseengineer models of software behaviour is valuable for a wide range of software maintenance, validation and verification tasks. Current reverseengineering techniques focus either on controlspecific behaviour (e.g., in the form of Finite State Machines), or dataspecific behaviour (e.g., as pre / postconditions or invariants). However, typical software behaviour is usually a product of the two; models must combine both aspects to fully represent the software's operation. Extended Finite State Machines (EFSMs) provide such a model. Although attempts have been made to infer EFSMs, these have been problematic. The models inferred by these techniques can be nondeterministic, the inference algorithms can be inflexible, and only applicable to traces with specific characteristics. This paper presents a novel EFSM inference technique that addresses the problems of inflexibility and nondeterminism. It also adapts an experimental technique from the field of Machine Learning to evaluate EFSM inference techniques, and applies it to three diverse software systems.
20150304T16:59:57Z

Querycompetitive algorithms for cheapest set problems under uncertainty
http://hdl.handle.net/2381/31664
Title: Querycompetitive algorithms for cheapest set problems under uncertainty
Authors: Erlebach, Thomas; Hoffmann, Michael; Kammer, F.
Abstract: Considering the model of computing under uncertainty where element weights are uncertain but can be obtained at a cost by query operations, we study the problem of identifying a cheapest (minimumweight) set among a given collection of feasible sets using a minimum number of queries of element weights. For the general case we present an algorithm that makes at most d·OPT+d queries, where d is the maximum cardinality of any given set and OPT is the optimal number of queries needed to identify a cheapest set. For the minimum multicut problem in trees with d terminal pairs, we give an algorithm that makes at most d·OPT+1 queries. For the problem of computing a minimumweight base of a given matroid, we give an algorithm that makes at most 2·OPT queries, generalizing a known result for the minimum spanning tree problem. For each of our algorithms we give matching lower bounds.
20150213T10:03:39Z

MultiType Display Calculus for Propositional Dynamic Logic
http://hdl.handle.net/2381/31644
Title: MultiType Display Calculus for Propositional Dynamic Logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander; Palmigiano, A.
Abstract: We introduce a multitype display calculus for Propositional Dynamic
Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnapstyle
cutelimination and subformula property.
20150211T11:12:31Z

A Multitype Display Calculus for Dynamic Epistemic Logic
http://hdl.handle.net/2381/31643
Title: A Multitype Display Calculus for Dynamic Epistemic Logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander; Palmigiano, A.; Sikimić, V.
Abstract: In the present paper, we introduce a multitype display calculus for dynamic
epistemic logic, which we refer to as Dynamic Calculus. The displayapproach
is suitable to modularly chart the space of dynamic epistemic logics
on weakerthanclassical propositional base. The presence of types endows
the language of the Dynamic Calculus with additional expressivity, allows
for a smooth prooftheoretic treatment, and paves the way towards a general
methodology for the design of proof systems for the generality of dynamic
logics, and certainly beyond dynamic epistemic logic. We prove that
the Dynamic Calculus adequately captures BaltagMossSolecki’s dynamic
epistemic logic, and enjoys Belnapstyle cut elimination.
20150211T11:06:46Z

A ProofTheoretic Semantic Analysis of Dynamic Epistemic Logic
http://hdl.handle.net/2381/31596
Title: A ProofTheoretic Semantic Analysis of Dynamic Epistemic Logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander H.; Palmigiano, A.; Sikimić, V.
Editors: Aucher, G.; Hjortland, O.; Roy, O.
Abstract: The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of prooftheoretic semantics. Dynamic epistemic logic is one of the bestknown members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the prooftheoretic treatment of which presents many difficulties. After an illustration of the prooftheoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a prooftheoretic paradigm that has been successfully employed to give a prooftheoretic semantic account of modal and substructural logics. Then, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reflect on them in the light of the previously introduced prooftheoretic semantic principles. The contributions of the present article include a generalization of Belnap's cutelimination metatheorem for display calculi, and a revised version of the displaystyle calculus D.EAK [30]. We verify that the revised version satisfies the previously mentioned prooftheoretic semantic principles, and show that it enjoys cutelimination as a consequence of the generalized metatheorem.
20150204T16:21:31Z

Mining sequential patterns from probabilistic databases
http://hdl.handle.net/2381/28949
Title: Mining sequential patterns from probabilistic databases
Authors: Muzammal, Muhammad; Raman, Rajeev
Abstract: This paper considers the problem of sequential pattern mining (SPM) in
probabilistic databases. Specifically, we consider SPM in situations where there is uncertainty
in associating an event with a source, model this kind of uncertainty in the probabilistic
database framework and consider the problem of enumerating all sequences
whose expected support is sufficiently large. We give an algorithm based on dynamic
programming to compute the expected support of a sequential pattern. Next, we propose
three algorithms for mining sequential patterns from probabilistic databases. The
first two algorithms are based on the candidate generation framework – one each based
on a breadthfirst (similar to GSP) and a depthfirst (similar to SPAM) exploration
of the search space. The third one is based on the pattern growth framework (similar
to PrefixSpan). We propose optimizations that mitigate the effects of the expensive
dynamic programming computation step. We give an empirical evaluation of the probabilistic
SPM algorithms and the optimizations, and demonstrate the scalability of the
algorithms in terms of CPU time and the memory usage. We also demonstrate the
effectiveness of the probabilistic SPM framework in extracting meaningful sequences in
the presence of noise.
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.
20140626T13:15:31Z

Encoding range minima and range top2 queries
http://hdl.handle.net/2381/28856
Title: Encoding range minima and range top2 queries
Authors: Davoodi, Pooya; Navarro, Gonzalo; Raman, Rajeev; Rao, S. Srinivasa
Abstract: We consider the problem of encoding range minimum queries (RMQs): given an array A[1..n] of distinct totally ordered values, to preprocess A and create a data structure that can answer the query RMQ(i,j), which returns the index containing the smallest element in A[i..j], without access to the array A at query time. We give a data structure whose space usage is 2n+o(n) bits, which is asymptotically optimal for worstcase data, and answers RMQs in O(1) worstcase time. This matches the previous result of Fischer and Heun, but is obtained in a more natural way. Furthermore, our result can encode the RMQs of a random array A in 1.919n+o(n) bits in expectation, which is not known to hold for Fischer and Heun’s result. We then generalize our result to the encoding range top2 query (RT2Q) problem, which is like the encoding RMQ problem except that the query RT2Q(i,j) returns the indices of both the smallest and second smallest elements of A[i..j]. We introduce a data structure using 3.272n+o(n) bits that answers RT2Qs in constant time, and also give lower bounds on the effective entropy of the RT2Q problem.
20140528T10:49:40Z

Optimal indexes for sparse bit vectors
http://hdl.handle.net/2381/28854
Title: Optimal indexes for sparse bit vectors
Authors: Golynski, Alexander; Orlandi, Alessio; Raman, Rajeev; Rao, S. Srinivasa
Abstract: We consider the problem of supporting rank and select operations on a bit vector of length m with n 1bits. The problem is considered in the succinct index model, where the bit vector is stored in "readonly" memory and an additional data structure, called the index is created during preprocessing to help answer the above queries. We give asymptotically optimal densitysensitive tradeoffs, involving both m and n, that relate the size of the index to the number of accesses to the bit vector (and processing time) needed to answer the above queries. The results are particularly interesting for the case where n=o(m).
20140527T10:19:32Z

An empirical evaluation of extendible arrays
http://hdl.handle.net/2381/28738
Title: An empirical evaluation of extendible arrays
Authors: Joannou, Stelios; Raman, Rajeev
Editors: Pardalos, PM; Rebennack, S
Abstract: We study the performance of several alternatives for implementing extendible arrays, which allow random access to elements stored
in them, whilst allowing the arrays to be grown and shrunk. The study
not only looks at the basic operations of grow/shrink and accessing data, but also the effects of memory fragmentation on performance.
Description: The final publication is
available at link.springer.com
20140409T10:40:44Z

Cellcycle regulation of NOTCH signaling during C. elegans vulval development
http://hdl.handle.net/2381/28643
Title: Cellcycle regulation of NOTCH signaling during C. elegans vulval development
Authors: NusserStein, 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.
20140307T13:50:41Z

Strongly complete logics for coalgebras
http://hdl.handle.net/2381/28587
Title: Strongly complete logics for coalgebras
Authors: Kurz, Alexander; Rosicky, Jiri
Abstract: Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for setbased coalgebras. In particular, a general construction of a logic from an arbitrary setfunctor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations and equations. Moreover, the presentation of the category of algebras for the functor is obtained compositionally from the presentations of the underlying category and of the functor. Part II investigates algebras for a functor over indcompletions and extends the theorem of J{'o}nsson and Tarski on canonical extensions of Boolean algebras with operators to this setting. Part III shows, based on Part I, how to associate a finitary logic to any finitesets preserving functor T. Based on Part II we prove the logic to be strongly complete under a reasonable condition on T.
20140214T10:52:40Z

Completeness for the coalgebraic cover modality
http://hdl.handle.net/2381/28586
Title: Completeness for the coalgebraic cover modality
Authors: Kupke, Clemens; Kurz, Alexander; Venema, Yde
Abstract: We study the finitary version of the coalgebraic logic introduced by L.Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a socalled coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation. As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically valid inequalities. Our soundness and completeness proof is algebraic, and we employ Pattinson's stratification method, showing that our derivation system can be stratified in countably many layers, corresponding to the modal depth of the formulas involved. In the proof of our main result we identify some new concepts and obtain some auxiliary results of independent interest. We survey properties of the notion of relation lifting, induced by an arbitrary but fixed set functor. We introduce a category of Boolean algebra presentations, and establish an adjunction between it and the category of Boolean algebras. Given the fact that our derivation system involves only formulas of depth one, it can be encoded as a endofunctor on Boolean algebras. We show that this functor is finitary and preserves embeddings, and we prove that the LindenbaumTarski algebra of our logic can be identified with the initial algebra for this functor.
20140214T10:40:06Z