bluuebunny/crossref_metadata_2025 huggingface dataset:
Testing Hennessy-Milner Logic with Recursion
Authors: Aceto Luca , Ingólfsdóttir Anna
Published: February 2016

This study offers a characterization of the collection of properties
expressible in Hennessy-Milner Logic (HML) with recursion that can be tested
using finite LTSs. In addition to actions used to probe the behaviour of the
tested system, the LTSs that we use as tests will be able to perform a distinguished action nok to signal their dissatisfaction during the interaction with the tested process. A process s passes the test T iff T does not perform the action nok when it interacts with s. A test T tests for a property phi in HML with recursion iff it is passed by exactly the states that satisfy phi. The paper gives an expressive completeness result offering a characterization of the collection of properties in HML with recursion that are testable in the above sense.
A Relational Account of Call-by-Value Sequentiality
Authors: Riecke Jon G. , Sandholm Anders B.
Published: February 2016

We construct a model for FPC, a purely functional, sequential, call-by-value
language. The model is built from partial continuous functions,
in the style of Plotkin, further constrained to be uniform with respect to
a class of logical relations. We prove that the model is fully abstract.
Solving Bit-Vector Equations of Fixed and Non-Fixed Size
Authors: Möller M. Oliver , Ruess Harald
Published: February 2016

This report is concerned with solving equations on fixed and
non-fixed size bit-vector terms. We define an equational transformation
system for solving equations on terms where all sizes of
bit-vectors and extraction positions are known. This transformation
system suggests a generalization for dealing with bit-vectors
of unknown size and unknown extraction positions. Both solvers
adhere to the principle of splitting bit-vectors only on demand,
thereby making them quite effective in practice.
On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers
Authors: Aceto Luca , Ésik Zoltán , Ingólfsdóttir Anna
Published: February 2016

This paper shows that the collection of identities in two variables
which hold in the algebra N of the natural numbers with constant
zero, and binary operations of sum and maximum does not have a
finite equational axiomatization. This gives an alternative proof of the
non-existence of a finite basis for N - a result previously obtained by
the authors. As an application of the main theorem, it is shown that
the language of Basic Process Algebra (over a singleton set of actions),
with or without the empty process, has no finite omega-complete equational
axiomatization modulo trace equivalence.

AMS Subject Classification (1991): 08A70, 08B05, 03C05, 68Q70.
ACM Computing Classification System (1998): F.4.1.
Keywords and Phrases: Equational logic, varieties, complete axiomatizations,
process algebra, trace equivalence.
A Fully Abstract Presheaf Semantics of SCCS with Finite Delay
Authors: Hildebrandt Thomas Troels
Published: February 2016

We present a presheaf model for the observation of infinite as well
as finite computations. We apply it to give a denotational semantics of
SCCS with finite delay, in which the meanings of recursion are given by
final coalgebras and meanings of finite delay by initial algebras of the
process equations for delay. This can be viewed as a first step in representing
fairness in presheaf semantics. We give a concrete representation
of the presheaf model as a category of generalised synchronisation
trees and show that it is coreflective in a category of generalised transition
systems, which are a special case of the general transition systems
of Hennessy and Stirling. The open map bisimulation is shown to coincide
with the extended bisimulation of Hennessy and Stirling. Finally
we formulate Milners operational semantics of SCCS with finite delay
in terms of generalised transition systems and prove that the presheaf
semantics is fully abstract with respect to extended bisimulation.
Is your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics
Authors: Aceto Luca , Laroussinie Francois
Published: February 2016

This paper studies the structural complexity of model checking
for (variations on) the specification formalisms used in the tools CMC
and Uppaal, and fragments of a timed alternation-free mu-calculus. For
each of the logics we study, we characterize the computational complexity
of model checking, as well as its specification and program complexity,
using timed automata as our system model.
Detachments Preserving Local Edge-Connectivity of Graphs
Authors: Jordán Tibor , Szigeti Zoltán
Published: February 2016

Let G = (V +s,E) be a graph and let S = (d1, ..., dp) be a set of positive integers with
Sum dj = d(s). An S-detachment splits s into a set of p independent vertices s1, ..., sp with
d(sj) = dj, 1 <= j <= p. Given a requirement function r(u, v) on pairs of vertices of V , an
S-detachment is called r-admissible if the detached graph G' satisfies lambda_G' (x, y) >= r(x, y)
for every pair x, y in V . Here lambda_H(u, v) denotes the local edge-connectivity between u and v
in graph H.
We prove that an r-admissible S-detachment exists if and only if (a) lambda_G(x, y) >= r(x, y),
and (b) lambda_G−s(x, y) >= r(x, y) − Sum |dj/2| hold for every x, y in V .
The special case of this characterization when r(x, y) = lambda_G(x, y) for each pair in V was conjectured by B. Fleiner. Our result is a common generalization of a theorem of W. Mader on edge splittings preserving local edge-connectivity and a result of B. Fleiner on detachments preserving global edge-connectivity. Other corollaries include previous results of L. Lov´asz and C.J.St.A. Nash-Williams on edge splittings and detachments, respectively. As a new application, we extend a theorem of A. Frank on local edge-connectivity augmentation to the case when stars of given degrees are added.
Constrained Edge-Splitting Problems
Authors: Jordán Tibor
Published: February 2016

Splitting off two edges su, sv in a graph G means deleting su, sv and
adding a new edge uv. Let G = (V +s,E) be k-edge-connected in V
(k >= 2) and let d(s) be even. Lov´asz proved that the edges incident to s
can be split off in pairs in such a way that the resulting graph on vertex
set V is k-edge-connected. In this paper we investigate the existence of
such complete splitting sequences when the set of split edges has to meet
additional requirements. We prove structural properties of the set of those
pairs u, v of neighbours of s for which splitting off su, sv destroys k-edge-connectivity. This leads to a new method for solving problems of this type.

By applying this method we obtain a short proof for a recent result of
Nagamochi and Eades on planarity-preserving complete splitting sequences and prove the following new results: let G and H be two graphs on the same set V + s of vertices and suppose that their sets of edges incident to s coincide. Let G (H) be k-edge-connected (l-edge-connected, respectively) in V and let d(s) be even. Then there exists a pair su, sv which can be split off in both graphs preserving k-edge-connectivity (l-edge-connectivity, resp.) in V , provided d(s) >= 6. If k and l are both even then such a pair always exists. Using these edge-splitting results and the polymatroid intersection theorem we give a polynomial algorithm for the problem of simultaneously augmenting the edge-connectivity of two graphs by adding a (common) set of new edges of (almost) minimum size.
Verification of State/Event Systems by Quotienting
Authors: Bodentien Nicky O. , Vestergaard Jacob , Friis Jacob , Kristoffersen Kåre J. , Petersen Kim G.
Published: February 2016

A rather new approach towards compositional verification of concurrent systems is the quotient technique, where components are gradually removed from the concurrent system while transforming the specification accordingly. When the intermediate specifications can be kept small using heuristics for minimization, the state explosion problem
is avoided and there are already promising experimental results for systems with an interleaving semantics, including real-time systems. This paper extends the quotienting approach to deal with a synchronous framework in the shape of state/event systems.
A state/event system is a concurrent system with a set of interdependent components operating synchronously according to stimuli (input events) provided by an environment while producing output events in return for the environment. A compositional modal logic M suitable for expressing general safety and liveness properties subsystems is introduced. A quotient construction for building components from a state/event system into the specification is presented and heuristics for minimizing formulae are proposed. The techniques are demonstrated on an example. The correctness of the techniques are justified by proofs in an appendix.
What is a ‘Good’ Encoding of Guarded Choice?
Authors: Nestmann Uwe
Published: February 2016

The pi-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the pi-calculus with asynchronous output and no choice. This result was recently proved by Palamidessi and, as a corollary, she showed that there is no fully compositional encoding from the former into the latter that preserves divergence-freedom and symmetries. This paper argues that there are nevertheless `good' encodings between these calculi.
 In detail, we present a series of encodings for languages with (1) input-guarded choice, (2) both input- and output-guarded choice, and (3) mixed-guarded choice, and investigate them with respect to compositionality and divergence-freedom. The first and second encoding satisfy all of the above criteria, but various `good' candidates for the third encoding - inspired by an existing distributed implementation - invalidate one or the other criterion. While essentially confirming Palamidessi's result, our study suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes.
Derandomizing Arthur-Merlin Games using Hitting Sets
Authors: Miltersen Peter Bro , Variyam Vinodchandran N.
Published: February 2016

We prove that AM (and hence Graph Nonisomorphism) is in NP
if for some epsilon > 0, some language in NE intersection coNE requires nondeterministic
circuits of size 2^(epsilon n). This improves recent results of Arvind
and K¨obler and of Klivans and Van Melkebeek who proved the same
conclusion, but under stronger hardness assumptions, namely, either
the existence of a language in NE intersection coNE which cannot be approximated
by nondeterministic circuits of size less than 2^(epsilon n) or the existence
of a language in NE intersection coNE which requires oracle circuits of size 2^(epsilon n)
with oracle gates for SAT (satisfiability).
The previous results on derandomizing AM were based on pseudorandom
generators. In contrast, our approach is based on a strengthening
of Andreev, Clementi and Rolim's hitting set approach to derandomization.
As a spin-off, we show that this approach is strong enough
to give an easy (if the existence of explicit dispersers can be assumed
known) proof of the following implication: For some epsilon > 0, if there is
a language in E which requires nondeterministic circuits of size 2^(epsilon n),
then P=BPP. This differs from Impagliazzo and Wigderson's theorem
"only" by replacing deterministic circuits with nondeterministic
ones.
Foundations of Modular SOS
Authors: Mosses Peter D.
Published: February 2016

A novel form of labelled transition system is proposed, where
the labels are the arrows of a category, and adjacent labels in computations
 are required to be composable. Such transition systems provide the
foundations for modular SOS descriptions of programming languages.
Three fundamental ways of transforming label categories, analogous to
monad transformers, are provided, and it is shown that their applications
preserve computations in modular SOS. The approach is illustrated with
fragments taken from a modular SOS for ML concurrency primitives.
A Modular SOS for Action Notation
Authors: Mosses Peter D.
Published: February 2016

Modularity is an important pragmatic aspect of semantic
descriptions: good modularity is needed to allow the reuse of existing descriptions when extending or changing the described language. In denotational semantics, the issue of modularity has received much attention, and appropriate abstractions have been introduced, so that definitions of semantic functions may be independent of the details of how computations are modeled. In structural operational semantics (SOS), however, this issue has largely been neglected, and SOS descriptions of programming languages typically exhibit rather poor modularity; the original SOS given for Action Notation (the notation for the semantic entities used in action semantics) suffered from the same problem.
This paper recalls a recent proposal, called MSOS, for obtaining a high
degree of modularity in SOS, and presents an MSOS description of Action
Notation. Due to its modularity, the MSOS description pinpoints some
complications in the design of Action Notation, and should facilitate the
design of an improved version of the notation. It also provides a major
example of the applicability of the MSOS framework.
The reader is assumed to be familiar with conventional SOS and with
the basic concepts and constructs of Action Notation. The description
of Action Notation is formulated almost entirely in Casl, the common
algebraic specification language.
A Modular SOS for ML Concurrency Primitives
Authors: Mosses Peter D.
Published: February 2016

Modularity is an important pragmatic aspect of semantic
descriptions. In denotational semantics, the issue of modularity has
received much attention, and appropriate abstractions have been
introduced, so that definitions of semantic functions may be independent of
the details of how computations are modeled. In structural operational
semantics (SOS), however, this issue has largely been neglected, and
SOS descriptions of programming languages typically exhibit rather poor
modularity| - for instance, extending the described language may entail
a complete reformulation of the description of the original constructs.
A proposal has recently been made for a modular approach to SOS, called
MSOS. The basic definitions of the Modular SOS framework are recalled
here, but the reader is referred to other papers for a full introduction.
This paper focuses on illustrating the applicability of Modular SOS, by
using it to give a description of a sublanguage of Concurrent ML (CML);
the transition rules for the purely functional constructs do not have to be
reformulated at all when adding references and/or processes. The paper
concludes by comparing the MSOS description with previous operational
descriptions of similar languages.
The reader is assumed to be familiar with conventional SOS, with the
concepts of functional programming languages such as Standard ML, and
with fundamental notions of concurrency.
Measures on Hidden Markov Models
Authors: Lyngsø Rune B. , Pedersen Christian N. S. , Nielsen Henrik
Published: February 2016

Hidden Markov models were introduced in the beginning of
the 1970's as a tool in speech recognition. During the last decade
they have been found useful in addressing problems in computational
biology such as characterising sequence families, gene finding,
structure prediction and phylogenetic analysis. In this paper
we propose several measures between hidden Markov models. We
give an efficient algorithm that computes the measures for leftright
models, e.g. profile hidden Markov models, and discuss how
to extend the algorithm to other types of models. We present an
experiment using the measures to compare hidden Markov models
for three classes of signal peptides.
On Ajtai’s Lower Bound Technique for R-way Branching Programs and the Hamming Distance Problem
Authors: Pagter Jakob
Published: February 2016

In this report we study the proof employed by Miklos Ajtai
[Determinism versus Non-Determinism for Linear Time RAMs
with Memory Restrictions, 31st Symposium on Theory of
Computation (STOC), 1999] when proving a non-trivial lower bound
in a general model of computation for the Hamming Distance
problem: given n elements: decide whether any two of them have
"small" Hamming distance. Specifically, Ajtai was able to show
that any R-way branching program deciding this problem using
time O(n) must use space Omega(n lg n).
We generalize Ajtai's original proof allowing us to prove a
time-space trade-off for deciding the Hamming Distance problem
 in the R-way branching program model for time between n
and alpha n lg n / lg lg n, for some suitable 0 < alpha < 1. In particular we prove
that if space is O(n^(1−epsilon)), then time is Omega(n lg n / lg lg n).
Language, Semantics, and Methods for Cryptographic Protocols
Authors: Crazzolara Federico , Winskel Glynn
Published: February 2016

In this report we present a process language for security protocols together
with an operational semantics and an alternative semantics in terms of sets
 of events. The denotation of process is a set of events, and as each event specifies
 a set of pre- and postconditions, this denotation can be viewed as a Petri net.
This Petri-net semantics has a strong relation to both Paulson's inductive set
of rules [Pau98] and strand spaces [THG98c]. By means of an example we
illustrate how the Petri-net semantics can be used to prove properties such as
secrecy and authentication.
Characteristic Formulae for Timed Automata
Authors: Aceto Luca , Ingólfsdóttir Anna , Pedersen Mikkel Lykke , Poulsen Jan
Published: February 2016

This paper offers characteristic formula constructions in the real-
time logic L for several behavioural relations between (states of)
timed automata. The behavioural relations studied in this work are
timed (bi)similarity, timed ready simulation, faster-than bisimilarity
and timed trace inclusion. The characteristic formulae delivered by
our constructions have size which is linear in that of the timed
automaton they logically describe. This also applies to the characteristic
formula for timed bisimulation equivalence, for which an exponential
space construction was previously offered by Laroussinie, Larsen and
Weise.
A Higher-Order Colon Translation
Authors: Danvy Olivier , Nielsen Lasse R.
Published: February 2016

A lambda-encoding such as the CPS transformation gives rise to administrative redexes. In his seminal article "Call-by-name, call-by-value and the lambda-calculus", 25 years ago, Plotkin tackled administrative reductions using a so-called colon translation. In "Representing control,
a study of the CPS transformation", 15 years later, Danvy and Filinski integrated administrative reductions in the CPS transformation, making it operate in one pass. This one-pass transformation is higher-order, and can be used for other lambda-encodings, but we do not see its associated proof technique used in practice - instead, Plotkin's colon translation appears to be favored. Therefore, in an attempt to link the higher-order transformation and Plotkin's proof technique, we recast Plotkin's proof of Indifference and Simulation in a higher-order setting. To this end, we extend the colon translation from first order to higher order.

Keywords: Call by name, call by value, lambda-calculus, continuation-passing style
(CPS), CPS transformation, administrative reductions, colon translation, one-
pass CPS transformation, Indifference, Simulation.

 
Guided Synthesis of Control Programs for a Batch Plant using UPPAAL
Authors: Hune Thomas S. , Larsen Kim G. , Pettersson Paul
Published: February 2016

In this paper we address the problem of scheduling and
synthesizing distributed control programs for a batch production plant. We use a timed automata model of the batch plant and the verification tool Uppaal to solve the scheduling problem.
In modeling the plant, we aim at a level of abstraction which is sufficiently accurate in order that synthesis of control programs from generated timed traces is possible. Consequently, the models quickly become too detailed and complicated for immediate automatic synthesis. In fact, only models of plants producing two batches can be analyzed directly! To
overcome this problem, we present a general method allowing the user to guide the model-checker according to heuristically chosen strategies. The guidance is specified by augmenting the model with additional guidance variables and by decorating transitions with extra guards on these. Applying this method has made synthesis of control programs feasible for
a plant producing as many as 60 batches.
The synthesized control programs have been executed in a physical plant.

Besides proving useful in validating the plant model and in finding some modeling errors, we view this final step as the ultimate litmus test of our methodology's ability to generate executable (and executing) code from basic plant models.
PowerForms: Declarative Client-Side Form Field Validation
Authors: Brabrand Claus , Møller Anders , Christensen Ricky Mikkel , Schwartzbach Michael I.
Published: February 2016

All uses of HTML forms may benefit from validation of the specified
input field values. Simple validation matches individual values against specified formats, while more advanced validation may involve interdependencies of form fields.
There is currently no standard for specifying or implementing such validation. Today, CGI programmers often use Perl libraries for simple server-side validation or program customized JavaScript solutions for client-side validation.
We present PowerForms, which is an add-on to HTML forms that
allows a purely declarative specification of input formats and sophisticated interdependencies of form fields. While our work may be seen as inspiration for a future extension of HTML, it is also available for CGI programmers today through a preprocessor that translates a PowerForms
document into a combination of standard HTML and JavaScript that works on all combinations of platforms and browsers.
The definitions of PowerForms formats are syntactically disjoint from the form itself, which allows a modular development where the form is perhaps automatically generated by other tools and the formats and interdependencies are added separately.
PowerForms has a clean semantics defined through a fixed-point process that resolves the interdependencies between all field values. Text fields are equipped with status icons (by default traffic lights) that continuously reflect the validity of the text that has been entered so far, thus providing immediate feed-back for the user. For other GUI components the available options are dynamically filtered to present only the allowed values. PowerForms are integrated into the  system for generating interactive Web services, but is also freely available in an Open Source distribution as a stand-alone package.
A Generalisation, a Simplification and some Applications of Paillier’s Probabilistic Public-Key System
Authors: Damgård Ivan B. , Jurik Mads J.
Published: February 2016

We propose a generalisation of Paillier's probabilistic public
key system, in which the expansion factor is reduced and which allows to adjust the block length of the scheme even after the public key has been fixed, without losing the homomorphic property. We show that
the generalisation is as secure as Paillier's original system.
We construct a threshold variant of the generalised scheme as well as zero-knowledge protocols to show that a given ciphertext encrypts one of a set of given plaintexts, and protocols to verify multiplicative relations on plaintexts. We then show how these building blocks can be used for applying the
scheme to efficient electronic voting. This reduces dramatically the work needed to compute the final result of an election, compared to the previously best known schemes. We show how the basic scheme for a yes/no vote can be easily adapted to casting a vote for up to t out of L candidates. The same basic building blocks can also be adapted to provide receipt-free elections, under appropriate physical assumptions. The scheme for 1 out of L elections can be optimised such that for a certain
range of parameter values, a ballot has size only O(log L) bits.
Efficient Protocols based on Probabilistic Encryption using Composite Degree Residue Classes
Authors: Damgård Ivan B. , Jurik Mads J.
Published: February 2016

We study various applications and variants of Paillier's
probabilistic encryption scheme. First, we propose a threshold variant of the
scheme, and also zero-knowledge protocols for proving that a given
ciphertext encodes a given plaintext, and for verifying multiplication of
encrypted values.
We then show how these building blocks can be used for applying the
scheme to efficient electronic voting. This reduces dramatically the work
needed to compute the final result of an election, compared to the previously
 best known schemes. We show how the basic scheme for a yes/no
vote can be easily adapted to casting a vote for up to t out of L
candidates. The same basic building blocks can also be adapted to
provide receipt-free elections, under appropriate physical assumptions. The
scheme for 1 out of L elections can be optimised such that for a certain
range of parameter values, a ballot has size only O(log L) bits.
Finally, we propose a variant of the encryption scheme, that allows
reducing the expansion factor of Paillier's scheme from 2 to almost 1.
From HUPPAAL to UPPAAL - A Translation from Hierarchical Timed Automata to Flat Timed Automata
Authors: David Alexandre , Möller M. Oliver
Published: February 2016

We present a hierarchical version of timed automata, equipped with data types,
hand-shake synchronization, and local variables. We describe the formal semantics of this hierarchical timed automata (HTA) formalism in terms of a transition system. We report on the implementation of a flattening algorithm, that translates our formalism to a network of Uppaal timed automata. We establish a correspondence between symbolic states of an HTA and its translations, and thus are able to make use of Uppaal’s simulator and model checking engine.
This technique is exemplified with a cardiac pacemaker model. Here, the overhead
introduced by the translation is tolerable. We give run-time data for deadlock checking, timed reachability, and timed response analysis.
Effective Bounds on Strong Unicity in L1-Approximation
Authors: Kohlenbach Ulrich , Oliva Paulo B.
Published: February 2016

In this paper we present another case study in the general project of Proof Mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation (developed in [17]) to analyze Cheney's simplification [6] of Jackson's original proof [9] from 1921 of the uniqueness of the best L1-approximation of continuous functions f in C[0, 1] by polynomials p in Pn of degree <= n. Cheney's proof is non-effective in the sense that it is based on classical logic and on the non-computational principle WKL (binary K¨onig lemma). The result of our analysis provides the first effective (in all parameters f, n and epsilon) uniform modulus of uniqueness (a concept which
generalizes `strong uniqueness' studied extensively in approximation theory). Moreover, the extracted modulus has the optimal epsilon-dependence as follows from Kroo [20]. The paper also describes how the uniform modulus of uniqueness can be used to compute the best L1-approximations of a fixed f in C[0, 1] with arbitrary precision, and includes some remarks on the case of best Chebychev approximation.
Some Complexity Problems on Single Input Double Output Controllers
Authors: Hangos Katalin M. , Tuza Zsolt , Yeo Anders
Published: February 2016

We investigate the time complexity of constructing single input
double output state feedback controller structures, given the
directed structure graph G of a system. Such a controller structure
defines a restricted type of P3-partition of the graph G. A necessary
 condition (*) has been found and two classes of graphs have
been identified where the search problem of finding a feasible P3-
partition is polynomially solvable and, in addition, (*) is not only
necessary but also sufficient for the existence of a P3-partition. It
is shown further that the decision problem on two particular graph
classes - defined in terms of forbidden subgraphs - remains NP-
complete, but is polynomially solvable on the intersection of those
two classes. Moreover, for every natural number m, a stabilizing
structure with Single Input m-Output controllers can be found in
polynomial time for the system in question, if it admits one.
Cuckoo Hashing
Authors: Pagh Rasmus , Rodler Flemming Friche
Published: February 2016

We present a simple and efficient dictionary with worst case constant lookup time, equaling the theoretical performance of the classic dynamic perfect hashing scheme of Dietzfelbinger et al. (Dynamic perfect hashing: Upper and lower bounds. SIAM J. Comput., 23(4):738-761, 1994). The space usage is similar to that of binary search trees, i.e., three words per key on average. The practicality of the scheme is backed by extensive experiments and comparisons with known methods, showing it to be quite competitive also in the average case.
A General Schema for Constructing One-Point Bases in the Lambda Calculus
Authors: Goldberg Mayer
Published: February 2016

In this paper, we present a schema for constructing one-point bases for recursively enumerable sets of lambda terms. The novelty of the approach is that we make no assumptions about the terms for which the one-point basis is constructed: They need not be combinators and they may contain constants and free variables. The significance of the construction is twofold: In the context of the lambda calculus, it characterises one-point bases as ways of ``packaging'' sets of terms into a single term; And in the context of realistic programming languages, it implies that we can define a single procedure that generates any given recursively enumerable set of procedures, constants and free variables in a given programming language.
Cache Oblivious Search Trees via Binary Trees of Small Height
Authors: Brodal Gerth Stølting , Fagerberg Rolf , Jacob Riko
Published: February 2016

We propose a version of cache oblivious search trees which is simpler than the previous proposal of Bender, Demaine and Farach-Colton and has the same complexity bounds. In particular, our data structure avoids the use of weight balanced B-trees, and can be implemented as just a single array of data elements, without the use of pointers. The structure also improves space utilization.

For storing n elements, our proposal uses (1+epsilon)n times the element size of memory, and performs searches in worst case O(log_B n) memory transfers, updates in amortized O((log^2 n)/(epsilon B)) memory transfers, and range queries in worst case O(log_B n + k/B) memory transfers, where k is the size of the output.

The basic idea of our data structure is to maintain a dynamic binary tree of height log n + O(1) using existing methods, embed this tree in a static binary tree, which in turn is embedded in an array in a cache oblivious fashion, using the van Emde Boas layout of Prokop.

We also investigate the practicality of cache obliviousness in the area of search trees, by providing an empirical comparison of different methods for laying out a search tree in memory.

The source code of the programs, our scripts and tools, and the data we present here are available online under ftp.brics.dk/RS/01/36/Experiments/.
Free De Morgan Bisemigroups and Bisemilattices
Authors: Ésik Zoltán
Published: February 2016

We give a geometric representation of free De Morgan bisemigroups, free commutative De Morgan bisemigroups and free De Morgan bisemilattices, using labeled graphs.
Perfect Hiding and Perfect Binding Universally Composable Commitment Schemes with Constant Expansion Factor
Authors: Damgård Ivan B. , Nielsen Jesper Buus
Published: February 2016

Canetti and Fischlin have recently proposed the security notion universal composability for commitment schemes and provided two examples. This new notion is very strong. It guarantees that security is maintained even when an unbounded number of copies of the scheme are running concurrently, also it guarantees non-malleability, resilience to selective decommitment, and security against adaptive adversaries. Both of their schemes uses Theta(k) bits to commit to one bit and can be based on the existence of trapdoor commitments and non-malleable encryption.

We present new universally composable commitment schemes based on the Paillier cryptosystem and the Okamoto-Uchiyama cryptosystem. The schemes are efficient: to commit to k bits, they use a constant number of modular exponentiations and communicates O(k) bits. Furthermore the scheme can be instantiated in either perfectly hiding or perfectly binding versions. These are the first schemes to show that constant expansion factor, perfect hiding, and perfect binding can be obtained for universally composable commitments.

We also show how the schemes can be applied to do efficient zero-knowledge proofs of knowledge that are universally composable.
An Extended Quadratic Frobenius Primality Test with Average Case Error Estimates
Authors: Damgård Ivan B. , Frandsen Gudmund Skovbjerg
Published: February 2016

We present an Extended Quadratic Frobenius Primality Test (EQFT), which is related to the Miller-Rabin test and the Quadratic Frobenius test (QFT) by Grantham. EQFT is well-suited for generating large, random prime numbers since on a random input number, it takes time about equivalent to 2 Miller-Rabin tests, but has much smaller error probability. EQFT extends QFT by verifying additional algebraic properties related to the existence of elements of order 3 and 4. We obtain a simple closed expression that upper bounds the probability of acceptance for any input number. This in turn allows us to give strong bounds on the average-case behaviour of the test: consider the algorithm that repeatedly chooses random odd k bit numbers, subjects them to t iterations of our test and outputs the first one found that passes all tests. We obtain numeric upper bounds for the error probability of this algorithm as well as a general closed expression bounding the error. For instance, it is at most 2^{-143} for k=500, t=2 . Compared to earlier similar results for the Miller-Rabin test, the results indicates that our test in the average case has the effect of 9 Miller-Rabin tests, while only taking time equivalent to about 2 such tests. We also give bounds for the error in case a prime is sought by incremental search from a random starting point. While EQFT is slower than the average case on a small set of inputs, we present a variant that is always fast, i.e. takes time about 2 Miller-Rabin tests. The variant has slightly larger worst case error probability than EQFT, but still improves on previous proposed tests.
Extracting Witnesses from Proofs of Knowledge in the Random Oracle Model
Authors: Groth Jens
Published: February 2016

We prove that a 3-move interactive proof system with the special soundness property made non-interactive by applying the Fiat-Shamir heuristic is almost a non-interactive proof of knowledge in the random oracle model. In an application of the result we demonstrate that the Damgård-Jurik voting scheme based on homomorphic threshold encryption is secure against a nonadaptive adversary according to Canetti's definition of multi-party computation security.
Extending Java for High-Level Web Service Construction
Authors: Christensen Aske Simon , Møller Anders , Schwartzbach Michael I.
Published: February 2016

We incorporate innovations from the  project into the Java language to provide high-level features for Web service programming. The resulting language, JWIG, contains an advanced session model and a flexible mechanism for dynamic construction of XML documents, in particular XHTML. To support program development we provide a suite of program analyses that at compile-time verify for a given program that no run-time errors can occur while building documents or receiving form input, and that all documents being shown are valid according to the document type definition for XHTML 1.0.

We compare JWIG with Servlets and JSP which are widely used Web service development platforms. Our implementation and evaluation of JWIG indicate that the language extensions can simplify the program structure and that the analyses are sufficiently fast and precise to be practically useful.
On the Number of Maximal Independent Sets in a Graph
Authors: Nielsen Jesper Makholm
Published: February 2016

We show that the number of maximal independent sets of size exactly k in any graph of size n is at most [ n/k ]^{k-(n mod k)} ([ n/k ] +1)^{n mod k}. For maximal independent sets of size at most k the same bound holds for k <= n/3. For k > n/3 a bound of approximately 3^{n/3} is given. All the bounds are exactly tight and improve Eppstein (2001) who give the bound 3^{4k-n}4^{n-3k} on the number of maximal independent sets of size at most k, which is the same for n/4 <= k <= n/3, but larger otherwise. We give an algorithm listing the maximal independent sets in a graph in time proportional to these bounds (ignoring a polynomial factor), and we use this algorithm to construct algorithms for 4- and 5- colouring running in time O(1.7504^n) and O(2.1593^n), respectively.
Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds
Authors: Srba Jirí
Published: February 2016

In this paper we study bisimilarity problems for simple process algebras. In particular, we show PSPACE-hardness of the following problems:
strong bisimilarity of Basic Parallel Processes (BPP),

strong bisimilarity of Basic Process Algebra (BPA),

strong regularity of BPP, and

strong regularity of BPA.
We also demonstrate NL-hardness of strong regularity problems for the normed subclasses of BPP and BPA.

Bisimilarity problems for simple process algebras are introduced in a general framework of process rewrite systems, and a uniform description of the new techniques used for the hardness proofs is provided.
Deciding Framed Bisimilarity
Authors: Hüttel Hans
Published: February 2016

The spi-calculus, proposed by Abadi and Gordon, is a process calculus based on the -calculus and is intended for reasoning about the behaviour of cryptographic protocols. We consider the finite-control fragment of the spi-calculus, showing it to be Turing-powerful (a result which is joint work with Josva Kleist, Uwe Nestmann, and Björn Victor.) Next, we restrict our attention to finite (non-recursive) spi-calculus. Here, we show that framed bisimilarity, an equivalence relation proposed by Abadi and Gordon, showing that it is decidable for this fragment.
Mann Iterates of Directionally Nonexpansive Mappings in Hyperbolic Spaces
Authors: Kohlenbach Ulrich , Leustean Laurentiu
Published: February 2016

In a previous paper, the first author derived an explicit quantitative version of a theorem due to Borwein, Reich and Shafrir on the asymptotic behaviour of Mann iterations of nonexpansive mappings of convex sets C in normed linear spaces. This quantitative version, which was obtained by a logical analysis of the ineffective proof given by Borwein, Reich and Shafrir, could be used to obtain strong uniform bounds on the asymptotic regularity of such iterations in the case of bounded C and even weaker conditions. In this paper we extend these results to hyperbolic spaces and directionally nonexpansive mappings. In particular, we obtain significantly stronger and more general forms of the main results of a recent paper by W.A. Kirk with explicit bounds. As a special feature of our approach, which is based on logical analysis instead of functional analysis, no functional analytic embeddings are needed to obtain our uniformity results which contain all previously known results of this kind as special cases.
A Foundation for Embedded Languages
Authors: Rhiger Morten
Published: February 2016

Recent work on embedding object languages into Haskell use ``phantom types'' (i.e., parameterized types whose parameter does not occur on the right-hand side of the type definition) to ensure that the embedded object-language terms are simply typed. But is it a safe assumption that only simply-typed terms can be represented in Haskell using phantom types? And conversely, can all simply-typed terms be represented in Haskell under the restrictions imposed by phantom types? In this article we investigate the conditions under which these assumptions are true: We show that these questions can be answered affirmatively for an idealized Haskell-like language and discuss to which extent Haskell can be used as a meta-language.
Some Remarks on Regular Words
Authors: Bloom Stephen L. , Ésik Zoltán
Published: February 2016

In the late 1970's, Courcelle introduced the class of ``arrangements'', or labeled linear ordered sets, here called just ``words''. He singled out those words which are solutions of finite systems of fixed point equations involving finite words, which we call the ``regular words''. The current paper contains some new descriptions of this class of words related to properties of regular sets of binary strings, and uses finite automata to decide various natural questions concerning these words. In particular we show that a countable word is regular iff it can be defined on an ordinary regular language (which can be chosen to be a prefix code) ordered by the lexicographical order such that the labeling function satisfies a regularity condition. Those regular words whose underlying order is ``discrete'' or ``scattered'' are characterized in several ways.
Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators
Authors: Ésik Zoltán
Published: February 2016

We associate a modal operator with each language belonging to a given class of regular languages and use the (reverse) wreath product of monoids with distinguished generators to characterize the expressive power of the resulting logic.
Composing Strand Spaces
Authors: Crazzolara Federico , Winskel Glynn
Published: February 2016

The strand space model for the analysis of security protocols is known to have some limitations in the patterns of nondeterminism it allows and in the ways in which strand spaces can be composed. Its successful application to a broad range of security protocols may therefore seem surprising. This paper gives a formal explanation of the wide applicability of strand spaces. We start with an extension of strand spaces which permits several operations to be defined in a compositional way, forming a process language for building up strand spaces. We then show, under reasonable conditions how to reduce the extended strand spaces to ones of a traditional kind. For security protocols we are mainly interested in their safety properties. This suggests a strand-space equivalence: two strand spaces are equivalent if and only if they have essentially the same sets of bundles. However this equivalence is not a congruence with respect to the strand-space operations. By extending the notion of bundle we show how to define the strand-space operations directly on ``bundle spaces''. This leads to a characterisation of the largest congruence within the strand-space equivalence. Finally, we relate strand spaces to event structures, a well known model for concurrency.
A Lambda-Revelation of the SECD Machine
Authors: Danvy Olivier
Published: February 2016

We present a simple inter-derivation between lambda-interpreters, i.e., evaluation functions for lambda-terms, and abstract reduction machines for the lambda-calculus, i.e., transition functions. The two key derivation steps are the CPS transformation and Reynolds's defunctionalization. By transforming the interpreter into continuation-passing style (CPS), its flow of control is made manifest as a continuation. By defunctionalizing this continuation, the flow of control is materialized as a first-order data structure.

The derivation applies not merely to connect independently known lambda-interpreters and abstract machines, it also applies to construct the abstract machine corresponding to a lambda-interpreter and to construct the lambda-interpreter corresponding to an abstract machine. In this article, we treat in detail the canonical example of Landin's SECD machine and we reveal its denotational content: the meaning of an expression is a partial endo-function from a stack of intermediate results and an environment to a new stack of intermediate results and an environment. The corresponding lambda-interpreter is unconventional because (1) it uses a control delimiter to evaluate the body of each lambda-abstraction and (2) it assumes the environment to be managed in a callee-save fashion instead of in the usual caller-save fashion.
Garden of Eden-konfigurationer i cellulære automater
Authors: Skyum Sven
Published: February 2016

This publication is Sven Skyum's master's thesis. The first chapters contain some general results about cellular automata (the existence of a universal computerconstructor, self-reproducing automata etc.). In the last chapters the connection between unambiguity and the existence of Garden of Eden configurations in cellular automata is examined.
Family Genericity
Authors: Ernst Erik
Published: February 2016

Type abstraction in object-oriented languages embody two techniques, each with its own strenghts and weaknesses. The first technique is extension, yielding abstraction mechanisms with good support for gradual specification.
The prime example is inheritance. The second technique is functional abstraction, yielding more precise knowledge about the outcome. The prime example is type parameterized classes. This paper argues that these techniques should be
clearly separated to work optimally, and also that current languages fail to do this.We have applied this design philosophy to a language based on an extension mechanism, namely virtual classes. As a result, some elements based on functional abstraction have been introduced, but they are simple and only used for things where they excel; conversely, the virtual classes have become more flexible, because their role is now more well-defined.We designate the result as family genericity. The presented language design has been implemented.
Scavenger - Mobile Remote Execution
Authors: Kristensen Mads Darø
Published: February 2016

This report describes the design and implementation of a mobile, peerto- peer, remote execution system called Scavenger. A peer running Scavenger is capable of automatically discovering available, unused computing resources in its vicinity, and, by means of mobile code, utilising these resources to its own good.
Designing a system such as Scavenger a number of challenges are raised. In this report only the two main challenges are presented: service discovery and mobile code security.
Service discovery in a fixed network is a well-documented process, but mobile service discovery is less so. Scavenger assumes nothing about its operating environment—it may be executing services on stationary as well as mobile peers—and it therefore needs a highly flexible service discovery protocol.

When working with mobile code, security becomes paramount since peers are executing unknown (and thus untrusted) code. Scavenger uses the Python programming language for its mobile code, and Python does not, like for example Java, have any built-in security models that enable the user to sandbox a Python process. When using such an ”insecure” programming language in a mobile code setting, other means of securing the code must be employed. This report describes the development of such a safe execution environment where mobile Python may be executed in a secure manner.