DSpace Collection:
http://hdl.handle.net/2381/1116
2015-10-09T10:32:17Z
2015-10-09T10:32:17Z
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
2015-09-11T02:00:34Z
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
2015-08-25T02:00:47Z
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
2015-09-17T08:54:29Z
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
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
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
The Description Logic SHIQ with a Flexible Meta-modelling Hierarchy
Severi, Paula G.
Motz, Regina
Rohrer, Edelweis
http://hdl.handle.net/2381/32284
2015-08-20T14:09:52Z
2015-05-19T10:58:05Z
Title: The Description Logic SHIQ with a Flexible Meta-modelling Hierarchy
Authors: Severi, Paula G.; Motz, Regina; Rohrer, Edelweis
Abstract: This work is motivated by a real-world case study where it is necessary to integrate and relate existing ontologies through meta-modelling. 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 meta-concept) which itself can be an individual of yet another concept (called meta meta-concept ) 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.
2015-05-19T10:58:05Z
HIAWSC: An Immune Algorithm Based Heuristic Web Service Composition Framework
Xu, J.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32251
2015-09-04T01:45:07Z
2015-05-08T14:39:51Z
Title: HIAWSC: An Immune Algorithm Based Heuristic Web Service Composition Framework
Authors: Xu, J.; Reiff-Marganiec, 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.
2015-05-08T14:39:51Z
Decoding the regulatory network for blood development from single cell gene expression measurements
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.
http://hdl.handle.net/2381/32202
2015-09-26T01:45:07Z
2015-05-07T10:43:26Z
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
2015-05-07T10:43:26Z
Tree Compression with Top Trees Revisited
Hübschle-Schneider, L.
Raman, Rajeev
http://hdl.handle.net/2381/32187
2015-06-29T08:41:04Z
2015-05-07T10:28:34Z
Title: Tree Compression with Top Trees Revisited
Authors: Hübschle-Schneider, 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 RePair-inspired 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 in-memory representation that supports basic navigation operations in worst-case logarithmic time without decompression. We also show a much improved worst-case bound on the size of the output of top-tree compression (answering an open question posed in a talk on this algorithm by Weimann in 2012).
2015-05-07T10:28:34Z
Random access to grammar-compressed strings and trees
Bille, P.
Landau, G. M.
Raman, Rajeev
Sadakane, K.
Satti, S. R.
Weimann, O.
http://hdl.handle.net/2381/32182
2015-06-03T02:00:11Z
2015-05-07T10:26:27Z
Title: Random access to grammar-compressed 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 context-free
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 Lempel-Ziv
family, Run-Length Encoding, Byte-Pair Encoding, Sequitur, and Re-Pair. 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 context-free 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{|P|k, 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 grammar-compressed 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
2015-05-07T10:26:27Z
Assessing and generating test sets in terms of behavioural adequacy
Fraser, G.
Walkinshaw, Neil
http://hdl.handle.net/2381/31971
2015-04-11T02:03:09Z
2015-04-10T10:17:43Z
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 well-established 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 search-based 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.
2015-04-10T10:17:43Z
Resolving non-determinism in choreographies
Bocchi, L.
Melgratti, H.
Tuosto, Emilio
http://hdl.handle.net/2381/31873
2015-03-17T02:02:13Z
2015-03-16T11:59:32Z
Title: Resolving non-determinism in choreographies
Authors: Bocchi, L.; Melgratti, H.; Tuosto, Emilio
Abstract: Resolving non-deterministic choices of choreographies is a crucial task. We introduce a novel notion of realisability for choreographies -called whole-spectrum 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 non-deterministic choice. We show that, under some conditions, it is decidable whether an implementation is whole-spectrum. As a case study, we analyse the POP protocol under the lens of whole-spectrum implementation. © 2014 Springer-Verlag.
2015-03-16T11:59:32Z
Inferring Extended Finite State Machine Models from Software Executions
Walkinshaw, Neil
Taylor, R.
Derrick, J.
http://hdl.handle.net/2381/31765
2015-04-17T09:31:09Z
2015-03-04T16:59:57Z
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 reverse-engineer models of software behaviour is valuable for a wide range of software maintenance, validation and verification tasks. Current reverse-engineering techniques focus either on control-specific behaviour (e.g., in the form of Finite State Machines), or data-specific behaviour (e.g., as pre / post-conditions 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 non-deterministic, 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 non-determinism. 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.
2015-03-04T16:59:57Z
Query-competitive algorithms for cheapest set problems under uncertainty
Erlebach, Thomas
Hoffmann, Michael
Kammer, F.
http://hdl.handle.net/2381/31664
2015-02-14T02:01:39Z
2015-02-13T10:03:39Z
Title: Query-competitive 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 (minimum-weight) 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 multi-cut 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 minimum-weight 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.
2015-02-13T10:03:39Z
Multi-Type Display Calculus for Propositional Dynamic Logic
Frittella, S.
Greco, G.
Kurz, Alexander
Palmigiano, A.
http://hdl.handle.net/2381/31644
2015-02-12T02:01:31Z
2015-02-11T11:12:31Z
Title: Multi-Type Display Calculus for Propositional Dynamic Logic
Authors: Frittella, S.; Greco, G.; Kurz, Alexander; 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.
2015-02-11T11:12:31Z
A Multi-type Display Calculus for Dynamic Epistemic Logic
Frittella, S.
Greco, G.
Kurz, Alexander
Palmigiano, A.
Sikimić, V.
http://hdl.handle.net/2381/31643
2015-02-12T02:01:30Z
2015-02-11T11:06:46Z
Title: A Multi-type 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 multi-type 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 weaker-than-classical propositional base. The presence of types endows
the language of the Dynamic Calculus with additional expressivity, allows
for a smooth proof-theoretic 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 Baltag-Moss-Solecki’s dynamic
epistemic logic, and enjoys Belnap-style cut elimination.
2015-02-11T11:06:46Z
A Proof-Theoretic Semantic Analysis of Dynamic Epistemic Logic
Frittella, S.
Greco, G.
Kurz, Alexander H.
Palmigiano, A.
Sikimić, V.
http://hdl.handle.net/2381/31596
2015-02-05T02:01:33Z
2015-02-04T16:21:31Z
Title: A Proof-Theoretic 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 proof-theoretic semantics. Dynamic epistemic logic is one of the best-known members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the proof-theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a proof-theoretic paradigm that has been successfully employed to give a proof-theoretic 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 proof-theoretic semantic principles. The contributions of the present article include a generalization of Belnap's cut-elimination metatheorem for display calculi, and a revised version of the display-style calculus D.EAK [30]. We verify that the revised version satisfies the previously mentioned proof-theoretic semantic principles, and show that it enjoys cut-elimination as a consequence of the generalized metatheorem.
2015-02-04T16:21:31Z
Mining sequential patterns from probabilistic databases
Muzammal, Muhammad
Raman, Rajeev
http://hdl.handle.net/2381/28949
2015-07-24T01:45:06Z
2014-06-26T13:15:31Z
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 breadth-first (similar to GSP) and a depth-first (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.
2014-06-26T13:15:31Z
Encoding range minima and range top-2 queries
Davoodi, Pooya
Navarro, Gonzalo
Raman, Rajeev
Rao, S. Srinivasa
http://hdl.handle.net/2381/28856
2015-04-22T01:45:07Z
2014-05-28T10:49:40Z
Title: Encoding range minima and range top-2 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 pre-process 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 worst-case data, and answers RMQs in O(1) worst-case 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 top-2 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.
2014-05-28T10:49:40Z
Optimal indexes for sparse bit vectors
Golynski, Alexander
Orlandi, Alessio
Raman, Rajeev
Rao, S. Srinivasa
http://hdl.handle.net/2381/28854
2014-05-28T01:01:25Z
2014-05-27T10:19:32Z
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 1-bits. The problem is considered in the succinct index model, where the bit vector is stored in "read-only" memory and an additional data structure, called the index is created during pre-processing to help answer the above queries. We give asymptotically optimal density-sensitive trade-offs, 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).
2014-05-27T10:19:32Z
An empirical evaluation of extendible arrays
Joannou, Stelios
Raman, Rajeev
http://hdl.handle.net/2381/28738
2014-04-10T01:01:14Z
2014-04-09T10:40:44Z
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
2014-04-09T10:40:44Z
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/28643
2014-03-08T02:01:51Z
2014-03-07T13:50:41Z
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.
2014-03-07T13:50:41Z
Strongly complete logics for coalgebras
Kurz, Alexander
Rosicky, Jiri
http://hdl.handle.net/2381/28587
2014-02-14T10:52:56Z
2014-02-14T10:52:40Z
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 set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor 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 ind-completions 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 finite-sets preserving functor T. Based on Part II we prove the logic to be strongly complete under a reasonable condition on T.
2014-02-14T10:52:40Z
Completeness for the coalgebraic cover modality
Kupke, Clemens
Kurz, Alexander
Venema, Yde
http://hdl.handle.net/2381/28586
2014-02-14T10:41:31Z
2014-02-14T10:40:06Z
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 so-called 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 endo-functor on Boolean algebras. We show that this functor is finitary and preserves embeddings, and we prove that the Lindenbaum-Tarski algebra of our logic can be identified with the initial algebra for this functor.
2014-02-14T10:40:06Z
Succinct representations of permutations and functions
Munro, J. Ian
Raman, Rajeev
Raman, Venkatesh
Rao, Satti Srinivasa
http://hdl.handle.net/2381/28330
2013-10-29T02:02:10Z
2013-10-28T12:29:09Z
Title: Succinct representations of permutations and functions
Authors: Munro, J. Ian; Raman, Rajeev; Raman, Venkatesh; Rao, Satti Srinivasa
Abstract: We investigate the problem of succinctly representing an arbitrary permutation, π, on {0, . . . , n−1} so that π[superscript k](i) can be computed quickly for any i and any (positive or negative) integer power k. A representation taking (1 + ϵ)n lg n + O(1) bits suffices to compute arbitrary powers in constant time, for any positive constant ϵ ≤ 1. A representation taking the optimal ⌈lg n!⌉ + o(n) bits can be used to compute arbitrary powers in O(lg n/ lg lg n) time.
We then consider the more general problem of succinctly representing an arbitrary function, f : [n] → [n] so that f[superscript k](i) can be computed quickly for any i and any integer power k. We give a representation that takes (1 + ϵ)n lg n + O(1) bits, for any positive constant ϵ ≤ 1, and computes arbitrary positive powers in constant time. It can also be used to compute f[superscript k](i), for any negative integer k, in optimal O(1+ | f[superscript k](i) |) time. We place emphasis on the redundancy, or the space beyond the information-theoretic lower bound that the data structure uses in order to support operations efficiently. A number of lower bounds have recently been shown on the redundancy of data structures. These lower bounds confirm the space–time optimality of some of our solutions.
Furthermore, the redundancy of one of our structures "surpasses" a recent lower bound by Golynski [Golynski, SODA 2009], thus demonstrating the limitations of this lower bound.
Description: NOTICE: this is the author’s version of a work that was accepted for publication in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Theoretical Computer Science, 2012, 438, pp. 47-88, DOI: 10.1016/j.tcs.2012.03.005.
2013-10-28T12:29:09Z
Attitudes towards User Experience (UX) Measurement
Law, Lai-Chong
van Schaik, Paul
http://hdl.handle.net/2381/28125
2013-10-11T13:48:32Z
2013-09-03T14:47:00Z
Title: Attitudes towards User Experience (UX) Measurement
Authors: Law, Lai-Chong; van Schaik, Paul
Editors: Wiedenbeck, S
Abstract: User experience (UX), as an immature research area, is still haunted by the challenges of defining the scope of UX in general and operationalising experiential qualities in particular. To explore the basic question whether UX constructs are measurable, we conducted semi-structured interviews with eleven UX professionals where a set of questions in relation to UX measurement were explored. The interviewees expressed scepticism as well as ambivalence towards UX measures and shared anecdotes related to such measures in different contexts. Besides, the data suggested that design-oriented UX professionals tended to be sceptical about UX measurement. To examine whether such an attitude prevailed in the HCI community, we conducted a survey with essentially the same set of questions used in the interviews. Altogether 367 responses were received; 170 of them were valid and analysed. The survey provided empirical evidence on this issue as a baseline for progress in UX measurement. Overall, results indicated that attitude was favourable and there were nuanced views on details of UX measurement, implying good prospects for its acceptance, given further progress in research and education in UX measurement where UX modelling grounded in theories can play a crucial role. Mutual recognition of the value of objective measures and subjective accounts of user experience can enhance the maturity of this area.
2013-09-03T14:47:00Z
PCTL model checking of Markov chains: Truth and falsity as winning strategies in games
Fecher, H
Huth, M
Piterman, N
Wagner, D
http://hdl.handle.net/2381/26567
2012-10-24T09:21:52Z
2012-10-24T09:21:52Z
Title: PCTL model checking of Markov chains: Truth and falsity as winning strategies in games
Authors: Fecher, H; Huth, M; Piterman, N; Wagner, D
2012-10-24T09:21:52Z
A hierarchy of reverse bisimulations on stable configuration structures
Phillips, I
Ulidowski, I
http://hdl.handle.net/2381/26332
2012-10-24T09:21:34Z
2012-10-24T09:21:34Z
Title: A hierarchy of reverse bisimulations on stable configuration structures
Authors: Phillips, I; Ulidowski, I
2012-10-24T09:21:34Z
Enriched Logical Connections
Kurz, A
Velebil, J
http://hdl.handle.net/2381/21632
2012-10-24T09:10:17Z
2012-10-24T09:10:17Z
Title: Enriched Logical Connections
Authors: Kurz, A; Velebil, J
2012-10-24T09:10:17Z
Soft constraints of difference and equality
Hebrard, E
Marx, D
O'Sullivan, B
Razgon, I
http://hdl.handle.net/2381/21619
2012-10-24T09:10:16Z
2012-10-24T09:10:16Z
Title: Soft constraints of difference and equality
Authors: Hebrard, E; Marx, D; O'Sullivan, B; Razgon, I
2012-10-24T09:10:16Z
Relation liftings on preorders and posets
Bílková, M
Kurz, A
Petrişan, D
Velebil, J
http://hdl.handle.net/2381/21605
2012-10-24T09:10:16Z
2012-10-24T09:10:16Z
Title: Relation liftings on preorders and posets
Authors: Bílková, M; Kurz, A; Petrişan, D; Velebil, J
2012-10-24T09:10:16Z
Finitary functors: From set to Preord and Poset
Balan, A
Kurz, A
http://hdl.handle.net/2381/21606
2012-10-24T09:10:16Z
2012-10-24T09:10:16Z
Title: Finitary functors: From set to Preord and Poset
Authors: Balan, A; Kurz, A
2012-10-24T09:10:16Z
The semantics of x86-CC multiprocessor machine code
Sarkar, S
Sewell, P
Nardelli, FZ
Owens, S
Ridge, T
Braibant, T
Myreen, MO
Alglave, J
http://hdl.handle.net/2381/20788
2012-10-24T09:08:59Z
2012-10-24T09:08:59Z
Title: The semantics of x86-CC multiprocessor machine code
Authors: Sarkar, S; Sewell, P; Nardelli, FZ; Owens, S; Ridge, T; Braibant, T; Myreen, MO; Alglave, J
2012-10-24T09:08:59Z
Efficient algorithms for finding a longest common increasing subsequence
Chan, W-T
Zhang, Y
Ye, D
Fung, SPY
Zhu, H
http://hdl.handle.net/2381/20787
2012-10-24T09:08:59Z
2012-10-24T09:08:59Z
Title: Efficient algorithms for finding a longest common increasing subsequence
Authors: Chan, W-T; Zhang, Y; Ye, D; Fung, SPY; Zhu, H
2012-10-24T09:08:59Z
Rigorous protocol design in practice: An optical packet-switch MAC in HOL
Biltcliffe, A
Ridge, T
Sewell, P
Dales, M
Jansen, S
http://hdl.handle.net/2381/20790
2012-10-24T09:08:59Z
2012-10-24T09:08:59Z
Title: Rigorous protocol design in practice: An optical packet-switch MAC in HOL
Authors: Biltcliffe, A; Ridge, T; Sewell, P; Dales, M; Jansen, S
2012-10-24T09:08:59Z
Verifying Distributed Systems: the Operational Approach
Ridge, T
http://hdl.handle.net/2381/20789
2012-10-24T09:08:59Z
2012-10-24T09:08:59Z
Title: Verifying Distributed Systems: the Operational Approach
Authors: Ridge, T
2012-10-24T09:08:59Z
Measuring teachers' readiness for E-learning in higher education institutions associated with the subject of electricity in Turkey
Akaslan, D
Law, EL-C
http://hdl.handle.net/2381/20593
2012-10-24T09:08:51Z
2012-10-24T09:08:51Z
Title: Measuring teachers' readiness for E-learning in higher education institutions associated with the subject of electricity in Turkey
Authors: Akaslan, D; Law, EL-C
2012-10-24T09:08:51Z
Modelling user experience - An agenda for research and practice
Law, EL-C
Van Schaik P
http://hdl.handle.net/2381/20594
2012-10-24T09:08:51Z
2012-10-24T09:08:51Z
Title: Modelling user experience - An agenda for research and practice
Authors: Law, EL-C; Van Schaik P
2012-10-24T09:08:51Z
On coalgebras over algebras
Balan, A
Kurz, A
http://hdl.handle.net/2381/20595
2012-10-24T09:08:51Z
2012-10-24T09:08:51Z
Title: On coalgebras over algebras
Authors: Balan, A; Kurz, A
2012-10-24T09:08:51Z
Algebraic semantics for coalgebraic logics
Kupke, C
Kurz, A
Pattinson, D
http://hdl.handle.net/2381/20607
2012-10-24T09:08:51Z
2012-10-24T09:08:51Z
Title: Algebraic semantics for coalgebraic logics
Authors: Kupke, C; Kurz, A; Pattinson, D
2012-10-24T09:08:51Z
Coalgebraic representations of distributive lattices with operators
Bonsangue, MM
Kurz, A
Rewitzky, IM
http://hdl.handle.net/2381/20605
2012-10-24T09:08:51Z
2012-10-24T09:08:51Z
Title: Coalgebraic representations of distributive lattices with operators
Authors: Bonsangue, MM; Kurz, A; Rewitzky, IM
2012-10-24T09:08:51Z
Stone coalgebras
Kupke, C
Venema, Y
Kupke, C
Kurz, A
http://hdl.handle.net/2381/20608
2012-10-24T09:08:51Z
2012-10-24T09:08:51Z
Title: Stone coalgebras
Authors: Kupke, C; Venema, Y; Kupke, C; Kurz, A
2012-10-24T09:08:51Z
Coalgebras and modal expansions of logics
Kurz, A
Palmigiano, A
http://hdl.handle.net/2381/20606
2012-10-24T09:08:51Z
2012-10-24T09:08:51Z
Title: Coalgebras and modal expansions of logics
Authors: Kurz, A; Palmigiano, A
2012-10-24T09:08:51Z