462 Works

Organizational Processes for Supporting Sustainable Security (Dagstuhl Seminar 12501)

Lizzie Coles-Kemp, Carrie Gates, Dieter Gollmann, Sean Peisert & Christian Probst
This report documents the program and the outcomes of Dagstuhl Seminar 12501 "Organizational Processes for Supporting Sustainable Security" which ran from December 9 to 12, 2012 and was held in Schloss Dagstuhl--Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. We also ran a number of collaborative sessions designed to promote the development of design principles for sustainably secure organizational processes. The first...

Parameterized Verification of Many Identical Probabilistic Timed Processes

Nathalie Bertrand & Paulin Fournier
Parameterized verification aims at validating a system's model irrespective of the value of a parameter. We introduce a model for networks of identical probabilistic timed processes, where the number of processes is a parameter. Each process is a probabilistic single-clock timed automaton and communicates with the others by broadcasting. The number of processes either is constant (static case), or evolves over time through random disappearances and creations (dynamic case). An example of relevant parameterized verification...

Verification of redecoration for infinite triangular matrices using coinduction

Ralph Matthes & Celia Picard
Finite triangular matrices with a dedicated type for the diagonal elements can be profitably represented by a nested data type, i. e., a heterogeneous family of inductive data types, while infinite triangular matrices form an example of a nested coinductive type, which is a heterogeneous family of coinductive data types. Redecoration for infinite triangular matrices is taken up from previous work involving the first author, and it is shown that redecoration forms a comonad with...

Pattern Generation by Cellular Automata (Invited Talk)

Jarkko Kari
A one-dimensional cellular automaton is a discrete dynamical system where a sequence of symbols evolves synchronously according to a local update rule. We discuss simple update rules that make the automaton perform multiplications of numbers by a constant. If the constant and the number base are selected suitably the automaton becomes a universal pattern generator: all finite strings over its state alphabet appear from a finite seed. In particular we consider the automata that multiply...

Using Self-learning and Automatic Tuning to Improve the Performance of Sexual Genetic Algorithms for Constraint Satisfaction Problems

Hu Xu, Karen Petrie & Iain Murray
Currently the parameters in a constraint solver are often selected by hand by experts in the field; these parameters might include the level of preprocessing to be used and the variable ordering heuristic. The efficient and automatic choice of a preprocessing level for a constraint solver is a step towards making constraint programming a more widely accessible technology. Self-learning sexual genetic algorithms are a new approach combining a self-learning mechanism with sexual genetic algorithms in...

Replica Placement via Capacitated Vertex Cover

Sonika Arora, Venkatesan T. Chakaravarthy, Neelima Gupta, Koyel Mukherjee & Yogish Sabharwal
In this paper, we study the replica placement problem on trees and present a constant factor approximation algorithm (with an additional additive constant factor). This improves the best known previous algorithm having an approximation ratio dependent on the maximum degree of the tree. Our techniques also extend to the partial cover version. Our algorithms are based on the LP rounding technique. The core component of our algorithm exploits a connection between the natural LP solutions...

Abusing the Tutte Matrix: An Algebraic Instance Compression for the K-set-cycle Problem

Magnus Wahlström

An Optimal Real-time Pricing Algorithm for the Smart Grid: A Bi-level Programming Approach

Fan-Lin Meng & Xiao-Jun Zeng

Non-constructive complex analysis in Coq

Aloïs Brunel
Winding numbers are fundamental objects arising in algebraic topology, with many applications in non-constructive complex analysis. We present a formalization in Coq of the wind- ing numbers and their main properties. As an application of this development, we also give non-constructive proofs of the following theorems: the Fundamental Theorem of Algebra, the 2-dimensional Brouwer Fixed-Point theorem and the 2-dimensional Borsuk-Ulam theorem.

Normalized Completion Revisited

Sarah Winkler & Aart Middeldorp

On Infinite Words Determined by Stack Automata

Tim Smith
We characterize the infinite words determined by one-way stack automata. An infinite language L determines an infinite word alpha if every string in L is a prefix of alpha. If L is regular or context-free, it is known that alpha must be ultimately periodic. We extend this result to the class of languages recognized by one-way nondeterministic checking stack automata (1-NCSA). We then consider stronger classes of stack automata and show that they determine a...

Character Networks for Narrative Generation: Structural Balance Theory and the Emergence of Proto-Narratives

Graham Alexander Sack
This paper models narrative as a complex adaptive system in which the temporal sequence of events constituting a story emerges out of cascading local interactions between nodes in a social network. The approach is not intended as a general theory of narrative, but rather as a particular generative mechanism relevant to several academic communities: (1) literary critics and narrative theorists interested in new models for narrative analysis, (2) artificial intelligence researchers and video game designers...

Computing With a Fixed Number of Pointers (Invited Talk)

Martin Hofmann & Ramyaa Ramyaa
Consider the P-complete problem Horn which asks whether a given set of Horn clauses is (un)satisfiable. To solve it one keeps a dynamic set of atoms that are forced to be true. Using the clauses one then adds atoms to this set until saturation is reached. It is easy to see that this dynamic set will in general more than constant size even if we allow to discard already proved atoms. Given that we need...

Mortality of Iterated Piecewise Affine Functions over the Integers: Decidability and Complexity (extended abstract)

Amir M. Ben-Amram
In the theory of discrete-time dynamical systems, one studies the limiting behaviour of processes defined by iterating a fixed function f over a given space. A much-studied case involves piecewise affine functions on R^n. Blondel et al. (2001) studied the decidability of questions such as mortality for such functions with rational coefficients. Mortality means that every trajectory includes a 0; if the iteration is seen as a loop while (x \ne 0) x := f(x),...

Illustrating the Mezzo programming language

Jonathan Protzenko
When programmers want to prove strong program invariants, they are usually faced with a choice between using theorem provers and using traditional programming languages. The former requires them to provide program proofs, which, for many applications, is considered a heavy burden. The latter provides less guarantees and the programmer usually has to write run-time assertions to compensate for the lack of suitable invariants expressible in the type system. We introduce Mezzo, a programming language in...

Supporting Separate Compilation in a Defunctionalizing Compiler

Georgios Fourtounis & Nikolaos S. Papaspyrou
Defunctionalization is generally considered a whole-program transformation and thus incompatible with separate compilation. In this paper, we formalize a modular variant of defunctionalization which can support separate compilation. Our technique allows modules in a Haskell-like language to be separately defunctionalized and compiled, then linked together to generate an executable program. We provide a prototype implementation of our modular defunctionalization technique and we discuss the experiences of its application in a compiler from a large subset...

Achieving Superscalar Performance without Superscalar Overheads - A Dataflow Compiler IR for Custom Computing

Ali Mustafa Zaidi & David J. Greaves
The difficulty of effectively parallelizing code for multicore processors, combined with the end of threshold voltage scaling has resulted in the problem of 'Dark Silicon', severely limiting performance scaling despite Moore's Law. To address dark silicon, not only must we drastically improve the energy efficiency of computation, but due to Amdahl's Law, we must do so without compromising sequential performance. Designers increasingly utilize custom hardware to dramatically improve both efficiency and performance in increasingly heterogeneous...

Towards Efficient Decoding of Classical-Quantum Polar Codes

Mark M. Wilde, Olivier Landon-Cardinal & Patrick Hayden
Known strategies for sending bits at the capacity rate over a general channel with classical input and quantum output (a cq channel) require the decoder to implement impractically complicated collective measurements. Here, we show that a fully collective strategy is not necessary in order to recover all of the information bits. In fact, when coding for a large number N uses of a cq channel W, N*I(W_{acc}) of the bits can be recovered by a...

Evolution and Evaluation of the Penalty Method for Alternative Graphs

Moritz Kobitzsch, Marcel Radermacher & Dennis Schieferdecker
Computing meaningful alternative routes in a road network is a complex problem -- already giving a clear definition of a best alternative seems to be impossible. Still, multiple methods describe how to compute reasonable alternative routes, each according to their own quality criteria. Among these methods, the penalty method has received much less attention than the via-node or plateaux based approaches. A mayor cause for the lack of interest might be the unavailability of an...

On the Query Complexity of Perfect Gate Discrimination

Giulio Chiribella, Giacomo Mauro D'Ariano & Martin Roetteler
We investigate the problem of finding the minimum number of queries needed to perfectly identify an unknown quantum gate within a finite set of alternatives, considering both deterministic strategies. For unambiguous gate discrimination, where errors are not tolerated but inconclusive outcomes are allowed, we prove that parallel strategies are sufficient to identify the unknown gate with minimum number of queries and we use this fact to provide upper and lower bounds on the query complexity....

Refactoring Boundary

Tim Wood & Sophia Drossopoulou
We argue that the limit of the propagation of the heap effects of a source code modification is determined by the aliasing structure of method parameters in a trace of the method calls that cross a boundary which partitions the heap. Further, that this aliasing structure is sufficient to uniquely determine the state of the part of the heap which has not been affected. And we give a definition of what it means for a...

Dequantizing Read-once Quantum Formulas

Alessandro Cosentino, Robin Kothari & Adam Paetznick
Quantum formulas, defined by Yao [FOCS'93], are the quantum analogs of classical formulas, i.e., classical circuits in which all gates have fanout one. We show that any read-once quantum formula over a gate set that contains all single-qubit gates is equivalent to a read-once classical formula of the same size and depth over an analogous classical gate set. For example, any read-once quantum formula over Toffoli and single-qubit gates is equivalent to a read-once classical...

Global semantic typing for inductive and coinductive computing

Daniel Leivant
Common data-types, such as N, can be identified with term algebras. Thus each type can be construed as a global set; e.g. for N this global set is instantiated in each structure S to the denotations in S of the unary numerals. We can then consider each declarative program as an axiomatic theory, and assigns to it a semantic (Curry-style) type in each structure. This leads to the intrinsic theories of [Leivant, 2002], which provide...

Elementary Modal Logics over Transitive Structures

Jakub Michaliszyn & Jan Otop
We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K...

A Configuration Model for the Line Planning Problem

Ralf Borndörfer, Heide Hoppmann & Marika Karbstein
We propose a novel extended formulation for the line planning problem in public transport. It is based on a new concept of frequency configurations that account for all possible options to provide a required transportation capacity on an infrastructure edge. We show that this model yields a strong LP relaxation. It implies, in particular, general classes of facet defining inequalities for the standard model.

Registration Year

  • 2013

Resource Types

  • Text