bluuebunny/crossref_metadata_2025 huggingface dataset:
Stable Bistructure Models of PCF
Authors: Winskel Glynn
Published: February 2016

Stable bistructures are a generalisation of event structures to represent spaces of functions at higher types; the partial order of causal dependency is replaced by two orders, one associated with input and the other output in the behaviour of functions. They represent Berry's bidomains. The representation can proceed in two stages. Bistructures form a categorical model of Girard's linear logic consisting of a linear category together with a comonad. The comonad has a co-Kleisli category which is equivalent to a cartesian-closed full subcategory of Berry's bidomains. A main motivation for bidomains came from the full abstraction problem for Plotkin's functional language PCF. However, although the bidomain model incorporates both the Berry stable order and the Scott pointwise order, its PCF theory (those inequalities on terms which hold in the bidomain model) does not include that of the Scott model. With a simple modification we can obtain a new model of PCF, combining the Berry and Scott orders, which does not have this inadequacy.
Local Model Checking and Traces
Authors: Cheng Allan
Published: February 2016

We present a CTL-like logic which is interpreted over labeled asynchronous transition systems. The interpretation reflects the desire to reason about these only with respect their progress fair behaviours. For finite systems we provide a set of tableau rules and prove soundness and completeness with respect to the given interpretation of our logic. We also provide a model checking algorithm which solves the model checking problem in deterministic polynomial time in the size of the formula and the labelled asynchronous transition system. We then consider different extensions of the logic with modalities expressing concurrent behaviour and investigate how this affects the decidability of the satisfiability problem.
Strong Concatenable Processes: An Approach to the Category of Petri Net Computations
Authors: Sassone Vladimiro
Published: February 2016

We introduce the notion of strong concatenable process for Petri nets as the least refinement of non-sequential (concatenable) processes which can be expressed abstractly by means of a  functor Q[_] from the category of Petri nets to an appropriate category of symmetric strict monoidal categories with free non-commutative monoids of objects, in the precise sense that, for each net N, the strong concatenable processes of N are isomorphic to the arrows of Q[N]. This yields an axiomatization of the causal behaviour of Petri nets in terms of symmetric strict monoidal categories.

In addition, we identify a coreflection right adjoint to Q[_] and we characterize its replete image in the category of symmetric monoidal categories, thus yielding an abstract description of the category of net computations.
A Compositional Proof System for the Modal mu-Calculus
Authors: Andersen Henrik Reif , Stirling Colin , Winskel Glynn
Published: February 2016

We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal mu-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal mu-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes.
Partially Persistent Data Structures of Bounded Degree with Constant Update Time
Authors: Brodal Gerth Stølting
Published: February 2016

The problem of making bounded in-degree and out-degree data structures partially persistent is considered. The node copying method of Driscoll et al. is extended so that updates can be performed in worst-case constant time on the pointer machine model. Previously it was only known to be possible in amortised constant time [Driscoll89]. The result is presented in terms of a new strategy for Dietz and Raman's dynamic two player pebble game on graphs. It is shown how to implement the strategy, and the upper bound on the required number of pebbles is improved from 2b + 2d + O(sqrt(b)) to d + 2b, where b is the bound of the in-degree and d the bound of the out-degree. We also give a lower bound that shows that the number of pebbles depends on the out-degree d.
Enhancing the Strength of Conventional Cryptosystems
Authors: Damgård Ivan B. , Knudsen Lars Ramkilde
Published: February 2016

We look at various ways of enhancing the strength of conventional cryptosystems such as DES by building a new system which has longer keys and which uses the original system as a building block. We propose a new variant of two-key triple encryption which is not vulnerable to the meet in the middle attack by van Oorschot and Wiener. Under an appropriate assumption on the security of DES, we can prove that our system is at least as hard to break as single DES.
A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours (Revised Version)
Authors: Aceto Luca
Published: February 2016

One of the most satisfactory results in process theory is Milner's axiomatization of strong bisimulation for regular CCS. This result holds for open terms with finite-state recursion. Wang has shown that timed bisimulation can also be axiomatized, but only for closed terms without recursion. In this paper, we provide an axiomatization for timed bisimulation of open terms with finite-state recursion.
A HOL Basis for Reasoning about Functional Programs
Authors: Agerholm Sten
Published: February 2016

Domain theory is the mathematical theory underlying denotational semantics. This thesis presents a formalization of domain theory in the Higher Order Logic (HOL) theorem proving system along with a mechanization of proof functions and other tools to support reasoning about the denotations of functional programs. By providing a fixed point operator for functions on certain domains which have a special undefined (bottom) element, this extension of HOL supports the definition of recursive functions which are not also primitive recursive. Thus, it provides an approach to the long-standing and important problem of defining non-primitive recursive functions in the HOL system.

Our philosophy is that there must be a direct correspondence between elements of complete partial orders (domains) and elements of HOL types, in order to allow the reuse of higher order logic and proof infrastructure already available in the HOL system. Hence, we are able to mix domain theoretic reasoning with reasoning in the set theoretic HOL world to advantage, exploiting HOL types and tools directly. Moreover, by mixing domain and set theoretic reasoning, we are able to eliminate almost all reasoning about the bottom element of complete partial orders that makes the LCF theorem prover, which supports a first order logic of domain theory, difficult and tedious to use. A thorough comparison with LCF is provided.

The advantages of combining the best of the domain and set theoretic worlds in the same system are demonstrated in a larger example, showing the correctness of a unification algorithm. A major part of the proof is conducted in the set theoretic setting of higher order logic, and only at a late stage of the proof domain theory is introduced to give a recursive definition of the algorithm, which is not primitive recursive. Furthermore, a total well-founded recursive unification function can be defined easily in pure HOL by proving that the unification algorithm (defined in domain theory) always terminates; this proof is conducted by a non-trivial well-founded induction. In such applications, where non-primitive recursive HOL functions are defined via domain theory and a proof of termination, domain theory constructs only appear temporarily.
Synthesizing Distinguishing Formulae for Real Time Systems
Authors: Godskesen Jens Chr.
Published: February 2016

This paper describes a technique for generating diagnostic information for the timed bisimulation equivalence and the timed simulation preorder. More precisely, given two (parallel) networks of regular real-time processes, the technique will provide a logical formula that differentiates them in case they are not timed (bi)similar. Our method may be seen as an extension of the algorithm by Cerans for deciding timed bisimilarity in that information of time-quantities has been added sufficient for generating distinguishing formulae. The technique has been added to the automatic verification tool EPSILON and applied to various examples.
Dynamic Algorithms for the Dyck Languages
Authors: Frandsen Gudmund Skovbjerg , Husfeldt Thore , Miltersen Peter Bro , Rauhe Theis , Skyum Søren
Published: February 2016

We study dynamic membership problems for the Dyck languages,
the class of strings of properly balanced parentheses. We also study the Dynamic Word problem for the free group. We present deterministic algorithms and data structures which maintain a string under replacements of symbols, insertions, and deletions of symbols, and language membership queries. Updates and queries are handled in polylogarithmic time. We also give both Las Vegas- and Monte Carlo-type randomised algorithms to achieve better running times, and present lower bounds on the complexity for variants of the problems.
The Fourth Moment in Luby's Distribution
Authors: Dubhashi Devdatt P. , Pantziou Grammati E. , Spirakis Paul G. , Zaroliagis Christos D.
Published: February 2016

Luby[10] proposed a way to derandomize randomized computations which is based on the construction of a small probability space whose elements are 3-wise independent. In this paper we prove some new properties of Luby's space. More precisely, we analyze
the fourth moment and prove an interesting technical property which helps to understand better Luby's distribution. As an application, we study the behavior of random edge cuts in a weighted graph.

Keywords: Fourth moment, full independence, k-wise independence, derandomization.
The Constructive Lift Monad
Authors: Kock Anders
Published: February 2016

The lift monad is the construction which to a poset freely adjoins a bottom
element to it, or equivalently (from the classical viewpoint), the construction which freely adjoins suprema for subsets with at most one element. In constructive mathematics (i.e. inside a topos), these two constructions are no longer equivalent, since the equivalence is based on the boolean reasoning that a set with at most one element either is a singleton {x}, or is empty.
Likewise based on boolean reasoning is the proof of two important properties of the lift monad T :
1) If a poset C has filtered suprema, then so does TC.
2) Every poset with a bottom element ? is "free", i.e. comes about by
applying T to some poset (namely the original poset less the bottom).
Both these properties fail to hold constructively, if the lift monad is interpreted
as "adding a bottom"; see Remark below. If, on the other hand,
we interpret the lift monad as the one which freely provides supremum for
each subset with at most one element (which is what we shall do), then the first property holds; and we give a necessary and sufficient condition that the second does. Finally, we shall investigate the lift monad in the context of (constructive) locale theory. I would like to thank Bart Jacobs for guiding me to the literature on Z-systems; to Gonzalo Reyes for calling my attention to Barr's work on totally connected spaces; to Steve Vickers for some pertinent correspondence.
I would like to thank the Netherlands Science Organization (NWO) for supporting my visit to Utrecht, where a part of the present research was carried out, and for various travel support from BRICS.
Automata for the mu-calculus and Related Results
Authors: Janin David , Walukiewicz Igor
Published: February 2016

The propositional mu-calculus as introduced by Kozen in [4] is
considered. The notion of disjunctive formula is defined and it is shown
that every formula is semantically equivalent to a disjunctive formula.
For these formulas many difficulties encountered in the general case may
be avoided. For instance, satisfiability checking is linear for disjunctive
formulas. This kind of formula gives rise to a new notion of finite automaton
which characterizes the expressive power of the mu-calculus over
all transition systems.
Dynamic Maintenance of Majority Information in Constant Time per Update
Authors: Frandsen Gudmund Skovbjerg , Skyum Sven
Published: February 2016

We show how to maintain information about the existence of a
majority colour in a set of elements under insertion and deletion of
single elements using O(1) time and at most 4 equality tests on colours
per update. No ordering information is used.
Determinizing Asynchronous Automata on Infinite Inputs
Authors: Klarlund Nils , Mukund Madhavan , Sohoni Milind
Published: February 2016

Asynchronous automata are a natural distributed machine model
for recognizing trace languages - languages defined over an alphabet
equipped with an independence relation.
To handle infinite traces, Gastin and Petit introduced Buchi asynchronous
automata, which accept precisely the class of omega-regular trace
languages. Like their sequential counterparts, these automata need to
be non-deterministic in order to capture all omega-regular languages. Thus
complementation of these automata is non-trivial. Complementation
is an important operation because it is fundamental for treating the
logical connective "not" in decision procedures for monadic second-order
logics. Subsequently, Diekert and Muscholl solved the complementation
problem by showing that with a Muller acceptance condition, deterministic
automata suffice for recognizing omega-regular trace languages.
However, a direct determinization procedure, extending the classical
subset construction, has proved elusive.
In this paper, we present a direct determinization procedure for
Buchi asynchronous automata, which generalizes Safra's construction
for sequential Buchi automata. As in the sequential case, the blow-up
in the state space is essentially that of the underlying subset construction.
On the Finitary Bisimulation
Authors: Aceto Luca , Ingólfsdóttir Anna
Published: February 2016

The finitely observable, or finitary, part of bisimulation is a key tool in establishing full abstraction results for denotational semantics for process algebras with respect to bisimulation-based preorders. A bisimulation-like characterization of this relation for arbitrary transition systems is given, relying on Abramsky's characterization in terms of the finitary domain logic. More informative behavioural, observation-independent characterizations of the finitary bisimulation are also offered for several interesting classes of transition systems. These include transition systems with countable action sets, those that have bounded convergent sort and the sort-finite ones. The result for sort-finite transition systems sharpens a previous behavioural characterization of the finitary bisimulation for this class of structures given by Abramsky.

AMS Subject Classification (1991): 68Q10 (Modes of computation), 68Q55
(Semantics), 03B70 (Logic of Programming), 68Q90 (Transition nets).
Keywords and Phrases: Concurrency, labelled transition systems with divergence,
bisimulation preorder, finitary relations, domain logic for transition systems.
Specification and Automated Verification of Real-Time Behaviour —A Case Study
Authors: Andersen Jørgen H. , Kristensen Carsten H. , Skou Arne
Published: February 2016

In this paper we sketch a method for specification and automatic
verification of real-time software properties. The method combines
the IEC 848 norm and the recent specification techniques TCCS (Timed
Calculus of Communicating Systems) and TML (Timed Modal Logic)
 - supported by an automatic verification tool, Epsilon. The method
is illustrated by modelling a small real-life steam generator example and
subsequent automated analysis of its properties.

Keywords: Control system analysis; formal specification; formal verification; real-time systems; standards.
Partial and Higher Order Differentials and Applications to the DES
Authors: Knudsen Lars Ramkilde
Published: February 2016

In 1994 Lai considered higher order derivatives of discrete functions and
introduced the concept of higher order differentials. We introduce the concept
of partial differentials and present attacks on ciphers presumably secure
against differential attacks, but vulnerable to attacks using higher order and
partial differentials. Also we examine the DES for partial and higher order
differentials and give a differential attack using partial differentials on DES
reduced to 6 rounds using only 46 chosen plaintexts with an expected running time of about the time of 3,500 encryptions. Finally it is shown how to find a minimum nonlinear order of a block cipher using higher order differentials.
On the Idempotence of the CPS Transformation
Authors: Danvy Olivier , Malmkjær Karoline
Published: February 2016

The CPS (continuation-passing style) transformation on typed lambda-terms has an interpretation in many areas of Computer Science, such as programming languages and type theory. Programming intuition suggests that in effect, it is idempotent, but this does not directly hold for all existing CPS transformations (Plotkin, Reynolds, Fischer, etc.).

We rephrase the call-by-value CPS transformation to make it syntactically idempotent, modulo eta-reduction of the newly introduced continuation. Type-wise, iterating the transformation corresponds to refining the polymorphic domain of answers.
Eta-Expansion Does The Trick (Revised Version)
Authors: Danvy Olivier , Malmkjær Karoline , Palsberg Jens
Published: February 2016

Partial-evaluation folklore has it that massaging one's source programs can make them specialize better. In Jones, Gomard, and Sestoft's recent textbook, a whole chapter is dedicated to listing such "binding-time improvements": nonstandard use of continuation passing style, eta-expansion, and a popular transformation called "The Trick". We provide a unified view of these binding-time improvements, from a typing perspective.
Just as a proper treatment of product values in partial evaluation
requires partially static values, a proper treatment of disjoint sums requires moving static contexts across dynamic case expressions. This requirement precisely accounts for the nonstandard use of continuation-passing style encountered in partial evaluation. Eta-expansion thus
acts as a uniform binding-time coercion between values and contexts, be they of function type, product type, or disjoint-sum type. For the latter case, it enables "The Trick".
In this article, we extend Gomard and Jones's partial evaluator
for the lambda-calculus, lambda-Mix, with products and disjoint sums; we point
out how eta-expansion for (finite) disjoint sums enables The Trick; we generalize our earlier work by identifying that eta-expansion can be obtained in the binding-time analysis simply by adding two coercion rules; and we specify and prove the correctness of our extension to lambda-Mix.

Keywords: Partial evaluation, binding-time analysis, program specialization,
binding-time improvement, eta-expansion, static reduction.
Back to Direct Style II: First-Class Continuations
Authors: Danvy Olivier , Lawall Julia L.
Published: February 2016

The direct-style transformation aims at mapping continuation-passing programs back to direct style, be they originally written in continuation-passing style or the result of the continuation-passing-style transformation. In this paper, we continue to investigate the direct-style transformation by extending it to programs with first-class continuations.

First-class continuations break the stack-like discipline of continuations in that they are sent results out of turn. We detect them syntactically through an analysis of continuation-passing terms. We conservatively extend the direct-style transformation towards call-by-value functional terms (the pure lambda-calculus) by translating the declaration of a first-class continuation using the control operator call/cc, and by translating an occurrence of a first-class continuation using the control operator throw. We prove that our extension and the corresponding
extended continuation-passing-style transformation are inverses.
Rotation of Periodic Strings and Short Superstrings
Authors: Breslauer Dany , Jiang Tao , Jiang Zhigen
Published: February 2016

This paper presents two simple approximation algorithms for the shortest superstring problem, with approximation ratios 2.67 and 2.596, improving the best previously published 2.75
approximation. The framework of our improved algorithms is similar to that of previous algorithms in the sense that they construct a superstring by computing some optimal cycle covers on the distance graph of the given strings, and
then break and merge the cycles to finally obtain a Hamiltonian path, but we make use of new bounds on the overlap between two strings. We prove that for each periodic semi-infinite string alpha = a1 a2 ... of period q, there exists an integer k, such that for any (finite) string s of period p which is inequivalent to alpha, the overlap between s and the rotation alpha[k] = ak ak+1 ... is at most p+ q/2. Moreover, if p<=q, then the overlap between s and alpha[k]
is not larger than 2/3 (p+q). In the previous shortest superstring algorithms p+q was used as the standard bound on overlap between two strings with periods p and q.
An Equational Axiomatization for Multi-Exit Iteration
Authors: Aceto Luca , Fokkink Willem Jan
Published: February 2016

This paper presents an equational axiomatization of bisimulation equivalence over the language of Basic Process Algebra (BPA) with multi-exit iteration. Multi-exit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions
of systems of recursion equations of the form

X1 = P1 X2 + Q1
...
Xn = Pn X1 + Qn

where n is a positive integer, and the Pi and the Qi are process terms. The addition
of multi-exit iteration to BPA yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star (BPA). As a
consequence, the proof of completeness of the proposed equational axiomatization
for this language, although standard in its general structure, is much more involved
than that for BPA. An expressiveness hierarchy for the family of k-exit iteration operators proposed by Bergstra, Bethke and Ponse is also offered.

 
Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL
Authors: Jensen Henrik Ejersbo , Larsen Kim G. , Skou Arne
Published: February 2016

This paper compares the tools SPIN and UPPAAL by modelling and verifying a Collision Avoidance Protocol for an Ethernet-like medium. We find that SPIN is well suited for modelling the untimed aspects of the protocol processes and for expressing the relevant (untimed) properties.
However, the modelling of the media becomes awkward due to the lack of broadcast communication in the PROMELA language. On the other hand we find it easy to model the timed aspects using the UPPAAL tool. Especially, the notion of committed locations supports the modelling of broadcast communication. However, the property language of UPPAAL
lacks some expressivity for verification of bounded liveness properties, and we indicate how timed testing automata may be constructed for such properties, inspired by the (untimed) checking automata of SPIN.
Negative Dependence Through the FKG Inequality
Authors: Dubhashi Devdatt P. , Priebe Volker , Ranjan Desh
Published: February 2016

We investigate random variables arising in occupancy problems, and show the variables to be negatively associated, that is, negatively dependent in a strong sense. Our proofs are based on the FKG correlation inequality, and they suggest a useful, general technique for proving negative dependence among random variables. We also show that in the special case of two binary random variables, the notions of negative correlation and negative association coincide.
Names, Equations, Relations: Practical Ways to Reason about 'new'
Authors: Stark Ian
Published: February 2016

The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus has connections to other kinds of local declaration, and to the mobile processes of the pi-calculus.

This paper introduces a logic of equations and relations which allows one to reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.

See the revised version BRICS-RS-97-39.
Regular Trace Event Structures
Authors: Thiagarajan P. S.
Published: February 2016

We propose trace event structures as a starting point for constructing effective branching time temporal logics in a non-interleaved setting. As a first step towards achieving this goal, we define the notion of a regular trace event structure. We then provide some simple characterizations of this notion of regularity both in terms of recognizable trace languages and in terms of finite 1-safe Petri nets.
A Computational Formalization for Partial Evaluation (Extended Version)
Authors: Hatcliff John , Danvy Olivier
Published: February 2016

We formalize a partial evaluator for Eugenio Moggi's computational
metalanguage. This formalization gives an evaluation-order independent view of binding-time analysis and program specialization, including a proper treatment of call unfolding, and enables us to express the essence of "control-based binding-time improvements" for let expressions.
Specifically, we prove that the binding-time improvements
given by "continuation-based specialization" can be expressed in the metalanguage via monadic laws.
Presheaf Models for Concurrency
Authors: Cattani Gian Luca , Winskel Glynn
Published: February 2016

This paper studies presheaf models for concurrent computation. An aim is to harness the general machinery around presheaves for the purposes of process calculi. Traditional models like synchronisation trees and event structures have been shown to embed fully and faithfully in particular
presheaf models in such a way that bisimulation, expressed through the presence of a span of open maps, is conserved. As is shown in the work of Joyal and Moerdijk, presheaves are rich in constructions which preserve open
maps, and so bisimulation, by arguments of a very general nature. This paper contributes similar results but biased towards questions of bisimulation in process calculi. It is concerned with modelling process constructions on presheaves, showing these preserve open maps, and with transferring such
results to traditional models for processes. One new result here is that a wide range of left Kan extensions, between categories of presheaves, preserve open maps. As a corollary, this also implies that any colimit-preserving functor between presheaf categories preserves open maps. A particular left Kan extension is shown to coincide with a refinement operation on event structures. A broad class of presheaf models is proposed for a general process calculus. General arguments are given for why the operations of a presheaf model preserve open maps and why for specic presheaf models the operations coincide with those of traditional models.
Objects, Types and Modal Logics
Authors: Andersen Dan S. , Pedersen Lars H. , Hüttel Hans , Kleist Josva
Published: February 2016

In this paper we present a modal logic for describing properties of
terms in the object calculus of Abadi and Cardelli [AC96]. The logic is
essentially the modal mu-calculus of [Koz83]. The fragment allows us
to express the temporal modalities of the logic CTL [BAMP83]. We
investigate the connection between the type system Ob_1<:mu and the
mu-calculus, providing a translation of types into modal formulae and
an ordering on formulae that is sound w.r.t. to the subtype ordering
of Ob_1<:mu.
Theory and Practice of Action Semantics
Authors: Mosses Peter D.
Published: February 2016

Action Semantics is a framework for the formal description
of programming languages. Its main advantage over other frameworks
is pragmatic: action-semantic descriptions (ASDs) scale up smoothly to
realistic programming languages. This is due to the inherent extensibility
and modifiability of ASDs, ensuring that extensions and changes to
the described language require only proportionate changes in its description.
(In denotational or operational semantics, adding an unforeseen
construct to a language may require a reformulation of the entire description.)
After sketching the background for the development of action semantics,
we summarize the main ideas of the framework, and provide a simple
illustrative example of an ASD. We identify which features of ASDs
are crucial for good pragmatics. Then we explain the foundations of
action semantics, and survey recent advances in its theory and practical
applications. Finally, we assess the prospects for further development
and use of action semantics.
The action semantics framework was initially developed at the University
of Aarhus by the present author, in collaboration with David Watt
(University of Glasgow). Groups and individuals scattered around five
continents have since contributed to its theory and practice.
UPPAAL—a Tool Suite for Automatic Verification of Real–Time Systems
Authors: Bengtsson Johan , Larsen Kim G. , Larsson Fredrik , Pettersson Paul , Yi Wang
Published: February 2016

Uppaal is a tool suite for automatic verification of safety and
bounded liveness properties of real-time systems modeled as networks of
timed automata. It includes: a graphical interface that supports graphical
and textual representations of networks of timed automata, and automatic
transformation from graphical representations to textual format,
a compiler that transforms a certain class of linear hybrid systems to
networks of timed automata, and a model-checker which is implemented
based on constraint-solving techniques. Uppaal also supports diagnostic
model-checking providing diagnostic information in case verification of a
particular real-time systems fails.
The current version of Uppaal is available on the World Wide Web via
the Uppaal home page http://www.docs.uu.se/docs/rtmv/uppaal.
Compositional and Symbolic Model-Checking of Real-Time Systems
Authors: Larsen Kim G. , Pettersson Paul , Yi Wang
Published: February 2016

Efficient automatic model-checking algorithms for
real-time systems have been obtained in recent years
based on the state-region graph technique of Alur,
Courcoubetis and Dill. However, these algorithms are
faced with two potential types of explosion arising from
parallel composition: explosion in the space of control
nodes, and explosion in the region space over clock variables.
In this paper we attack these explosion problems by
developing and combining compositional and symbolic
model-checking techniques. The presented techniques
provide the foundation for a new automatic verification
tool Uppaal. Experimental results indicate that
Uppaal performs time- and space-wise favorably compared
with other real-time verification tools.
Partial Evaluation of the Euclidian Algorithm (Extended Version)
Authors: Danvy Olivier , Goldberg Mayer
Published: February 2016

Some programs are easily amenable to partial evaluation because
their control flow clearly depends on one of their parameters. Specializing
such programs with respect to this parameter eliminates the
associated interpretive overhead. Some other programs, however, do
not exhibit this interpreter-like behavior. Each of them presents a challenge
for partial evaluation. The Euclidian algorithm is one of them,
and in this article, we make it amenable to partial evaluation.
We observe that the number of iterations in the Euclidian algorithm
is bounded by a number that can be computed given either of the two
arguments. We thus rephrase this algorithm using bounded recursion.
The resulting program is better suited for automatic unfolding and
thus for partial evaluation. Its specialization is efficient.
Keywords: partial evaluation, scientific computation.
Trans-Dichotomous Algorithms without Multiplication —some Upper and Lower Bounds
Authors: Brodnik Andrej , Miltersen Peter Bro , Munro J. Ian
Published: February 2016

We show that on a RAM with addition, subtraction, bitwise
Boolean operations and shifts, but no multiplication, there is a
trans-dichotomous solution to the static dictionary problem using
linear space and with query time sqrt(log n(log log n)^(1+o(1))). On
the way, we show that two w-bit words can be multiplied in
time (log w)^(1+o(1)) and that time Omega(log w) is necessary, and that
Theta(log log w) time is necessary and sufficient for identifying the
least significant set bit of a word.
Error Correcting Codes, Perfect Hashing Circuits, and Deterministic Dynamic Dictionaries
Authors: Miltersen Peter Bro
Published: February 2016

We consider dictionaries of size n over the finite universe U ={0, 1}^w and introduce a new technique for their implementation: error correcting codes. The use of such codes makes it possible to replace the use of strong forms of hashing, such as universal hashing, with much weaker forms, such as clustering.
We use our approach to construct, for any epsilon > 0, a deterministic solution to the dynamic dictionary problem using linear space, with worst case time O(n) for insertions and deletions, and worst case time O(1) for lookups. This is the first deterministic solution to the dynamic dictionary problem with linear space, constant query time, and non-trivial update time. In particular, we get a solution to the static dictionary problem with O(n) space, worst case query time O(1), and deterministic initialization time O(n^(1+epsilon)). The best previous deterministic initialization time for such dictionaries, due to Andersson, is O(n^(2+epsilon)). The model of computation for these bounds is a unit cost RAM with word size w (i.e. matching the universe), and a standard instruction set. The constants in the big-O's are independent upon w. The solutions are weakly non-uniform in w, i.e. the code of the algorithm contains word sized constants, depending on w, which must be computed at compile-time, rather than at run-time, for the stated run-time bounds to hold.
An ingredient of our proofs, which may be interesting in its own right, is the following observation: A good error correcting code for a bit vector fitting into a word can be computed in O(1) time on a RAM with unit cost multiplication.
As another application of our technique in a different model of computation, we give a new construction of perfect hashing circuits, improving a construction by Goldreich and Wigderson. In particular, we show that for any subset S of {0;1}w of size n, there is a Boolean circuit C of size O(w log w) with w inputs and 2 log n outputs so that the function defined by C is 1-1 on S. The best previous bound on the size of such a circuit was O(w log w log log w).
Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL
Authors: Havelund Klaus , Skou Arne , Larsen Kim G. , Lund Kristian
Published: February 2016

A formal and automatic verification of a real-life protocol is presented. The protocol, about 2800 lines of assembler code, has been used in products from the audio/video company Bang & Olufsen throughout more than a decade, and its purpose
is to control the transmission of messages between audio/video components over a single bus. Such communications may collide, and one essential purpose of the protocol is to detect such collisions. The functioning is highly dependent on
real-time considerations. Though the protocol was known to be faulty in that messages were lost occasionally, the protocol was too complicated in order for Bang & Olufsen to locate the bug using normal testing. However, using the real-time verification
tool UPPAAL, an error trace was automatically generated, which caused the detection of “the error” in the implementation. The error was corrected and the correction was automatically proven correct, again using UPPAAL. A future, and more automated, version of the protocol, where this error is fatal, will incorporate the correction. Hence, this work is an elegant demonstration of how model checking has had an impact on practical software development. The effort of modeling this protocol has in addition generated a number of suggestions for enriching the UPPAAL language. Hence, it’s also an excellent example of the reverse impact.
Hardness Results for Dynamic Problems by Extensions of Fredman and Saks’ Chronogram Method
Authors: Husfeldt Thore , Rauhe Theis
Published: February 2016

We introduce new models for dynamic computation based on the cell probe model of Fredman and Yao. We give these models access to nondeterministic queries or the right answer +-1 as an oracle. We prove that for the dynamic partial sum problem, these new powers do not help, the problem retains its lower bound of  Omega(log n/log log n).
From these results we easily derive a large number of lower bounds of order Omega(log n/log log n) for conventional dynamic models like the random access machine. We prove lower bounds for dynamic algorithms for reachability in directed graphs, planarity testing, planar point location, incremental parsing, fundamental data structure problems like maintaining the majority of the prefixes of a string of bits and range queries. We characterise the complexity of maintaining the value of any symmetric function on the prefixes of a bit string.
A Theory of Recursive Domains with Applications to Concurrency
Authors: Cattani Gian Luca , Fiore Marcelo P. , Winskel Glynn
Published: February 2016

We develop a 2-categorical theory for recursively defined domains.
In particular, we generalise the traditional approach based on order-theoretic structures to category-theoretic ones. A motivation for this development is the need of a domain theory for concurrency, with an account of bisimulation. Indeed, the leading examples throughout the paper are provided by recursively defined presheaf models for concurrent process calculi. Further, we use the framework to study (open-map) bisimulation.
Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation (Preliminary Version)
Authors: Balat Vincent , Danvy Olivier
Published: February 2016

We investigate the synergy between type-directed partial evaluation and run-time code generation for the Caml dialect of ML. Type-directed partial evaluation maps simply typed, closed Caml values to a representation of their long beta-eta-normal form. Caml uses a virtual machine and has the capability to load byte code at run time. Representing the long beta-eta-normal forms as byte code gives us the ability to strongly normalize higher-order values (i.e., weak head normal forms in ML), to compile the resulting strong normal forms into byte code, and to load this byte code all in one go, at run time.
We conclude this note with a preview of our current work on scaling
up strong normalization by run-time code generation to the Caml
module language.
Distributed Safety Controllers for Web Services
Authors: Sandholm Anders B. , Schwartzbach Michael I.
Published: February 2016

We show how to use high-level synchronization constraints, written
in a version of monadic second-order logic on finite strings, to synthesize safety controllers for interactive web services. We improve on the naïve runtime model to avoid state-space explosions and to increase the flow capacities of services.
First-Order Logic with Two Variables and Unary Temporal Logic
Authors: Etessami Kousha , Vardi Moshe Y. , Wilke Thomas
Published: February 2016

We investigate the power of first-order logic with only two variables over
omega-words and finite words, a logic denoted by FO2. We prove that FO2 can
express precisely the same properties as linear temporal logic with only the unary temporal operators: “next”, “previously”, “sometime in the future”, and “sometime in the past”, a logic we denote by unary-TL. Moreover, our translation from FO2 to unary-TL converts every FO2 formula to an equivalent unary-TL formula that is at most exponentially larger, and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is optimal.
While satisfiability for full linear temporal logic, as well as for
unary-TL, is known to be PSPACE-complete, we prove that satisfiability
for FO2 is NEXP-complete, in sharp contrast to the fact that satisfiability
for FO3 has non-elementary computational complexity. Our NEXP time
upper bound for FO2 satisfiability has the advantage of being in terms of
the quantifier depth of the input formula. It is obtained using a small model property for FO2 of independent interest, namely: a satisfiable FO2 formula has a model whose “size” is at most exponential in the quantifier depth of the formula. Using our translation from FO2 to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.
Thunks and the lambda-Calculus (Extended Version)
Authors: Hatcliff John , Danvy Olivier
Published: February 2016

Plotkin, in his seminal article Call-by-name, call-by-value and the lambda-calculus, formalized evaluation strategies and simulations using operational semantics and continuations. In particular, he showed how
call-by-name evaluation could be simulated under call-by-value evaluation and vice versa. Since Algol 60, however, call-by-name is both implemented and simulated with thunks rather than with continuations. We recast this folk theorem in Plotkin's setting, and show that thunks, even though they are simpler than continuations, are sufficient for establishing all the correctness properties of Plotkin's call-by-name simulation.

Furthermore, we establish a new relationship between Plotkin's two continuation-based simulations Cn and Cv, by deriving Cn as the composition of our thunk-based simulation T and of Cv^+ - an extension of Cv handling thunks. Almost all of the correctness properties of Cn follow from the properties of T and Cv^+ . This simplifies reasoning about call-by-name continuation-passing style. We also give several applications involving factoring continuation-based transformations using thunks.
Functional Unparsing
Authors: Danvy Olivier
Published: February 2016

A string-formatting function such as printf in C seemingly requires
dependent types, because its control string determines the rest of its arguments.

Examples:
printf ("Hello world.\n");
printf ("The %s is %d.\n", "answer", 42);

We show how changing the representation of the control string
makes it possible to program printf in ML (which does not allow dependent types). The result is well typed and perceptibly more efficient than the corresponding library functions in Standard ML of New Jersey and in Caml.
Uniformly Generated Submodules of Permutation Modules
Authors: Riis Søren , Sitharam Meera
Published: February 2016

This paper is motivated by a link between algebraic proof
complexity and the representation theory of the finite symmetric
groups. Our perspective leads to a series of non-traditional
problems in the representation theory of Sn.
Most of our technical results concern the structure of "uniformly"
generated submodules of permutation modules. We consider
(for example) sequences Wn of submodules of the permutation
modules M(n−k;1k) and prove that if the modules Wn are
given in a uniform way - which we make precise - the dimension
p(n) of Wn (as a vector space) is a single polynomial with rational
coefficients, for all but finitely many "singular" values of n. Furthermore, we show that dim(Wn) < p(n) for each singular value of n >= 4k. The results have a non-traditional flavor arising from the study of the irreducible structure of the submodules Wn beyond isomorphism types. We sketch the link between our structure theorems and proof complexity questions, which can be viewed as special cases of the famous NP vs. co-NP problem in complexity theory. In particular, we focus on the efficiency of proof systems for showing membership in polynomial ideals, for example, based on Hilbert's Nullstellensatz.
A Group Signature Scheme Based on an RSA-Variant
Authors: Camenisch Jan , Michels Markus
Published: February 2016

The concept of group signatures allows a group member to sign messages anonymously on behalf of the group. However, in the case of a dispute, the identity of a signature’s originator can be revealed by a designated entity. In this paper we propose a new group signature scheme that is well suited for large groups, i.e., the length of the group’s public key and of signatures do not
depend on the size of the group. Our scheme is based on a variation of the RSA problem called strong RSA assumption. It is also more efficient than previous ones satisfying these requirements.
Low Redundancy in Dictionaries with O(1) Worst Case Lookup Time
Authors: Pagh Rasmus
Published: February 2016

A static dictionary is a data structure for storing subsets of a finite universe U, so that membership queries can be answered efficiently. We study this problem in a unit cost RAM model with word size  Omega(log |U|), and show that for n-element subsets,
constant worst case query time can be obtained using B +O(log log |U|)+o(n) bits of storage, where B = [log2 (|U| / n)]
is the minimum number of bits needed to represent all
such subsets. The solution for dense subsets uses B + O( |U| log log |U| / log |U| ) bits of storage, and supports constant time rank queries. In a dynamic setting, allowing insertions and deletions, our techniques give an O(B) bit space usage.
The Complexity of Identifying Large Equivalence Classes
Authors: Binderup Peter G. , Frandsen Gudmund Skovbjerg , Miltersen Peter Bro , Skyum Sven
Published: February 2016

We prove that at least (3k−4) / k(2k−3) n(n-1)/2 − O(k) equivalence tests and no
more than 2/k n(n-1)/2 + O(n)
equivalence tests are needed in the worst case to identify the equivalence classes with at least k members in set of n elements. The upper bound is an improvement by a factor 2 compared to known results. For k = 3 we give tighter bounds. Finally, for k > n/2 we prove that it is necessary and it suffices to make 2n − k − 1 equivalence tests which generalizes a known result for k = [(n+1)/2] .
An Operational Investigation of the CPS Hierarchy
Authors: Danvy Olivier , Yang Zhe
Published: February 2016

We explore the hierarchy of control induced by successive transformations into continuation-passing style (CPS) in the presence of "control delimiters'' and "composable continuations''. Specifically, we investigate the structural operational semantics associated with the CPS hierarchy.

To this end, we characterize an operational notion of continuation semantics. We relate it to the traditional CPS transformation and we use it to account for the control operator shift and the control delimiter reset operationally. We then transcribe the resulting continuation semantics in ML, thus obtaining a native and modular implementation of the entire hierarchy. We illustrate it with a few examples, the most significant of which is layered monads.

P.S. Not published. No full text available.