bluuebunny/crossref_metadata_2025 huggingface dataset:
Dynamic Linear Time Temporal Logic
Authors: Henriksen Jesper G. , Thiagarajan P. S.
Published: February 2016

A simple extension of the propositional temporal logic of linear
time is proposed. The extension consists of strengthening the until
operator by indexing it with the regular programs of propositional
dynamic logic (PDL). It is shown that DLTL, the resulting logic, is
expressively equivalent to S1S, the monadic second-order theory
of omega-sequences. In fact a sublogic of DLTL which corresponds
to propositional dynamic logic with a linear time semantics is
already as expressive as S1S. We pin down in an obvious manner
the sublogic of DLTL which correponds to the first order fragment
of S1S. We show that DLTL has an exponential time decision
procedure. We also obtain an axiomatization of DLTL. Finally,
we point to some natural extensions of the approach presented
here for bringing together propositional dynamic and temporal
logics in a linear time setting.
A Product Version of Dynamic Linear Time Temporal Logic
Authors: Henriksen Jesper G. , Thiagarajan P. S.
Published: February 2016

We present here a linear time temporal logic which simultaneously extends LTL, the propositional temporal logic of linear time, along two dimensions. Firstly, the until operator is strengthened by indexing it with the regular programs of propositional dynamic logic (PDL). Secondly, the core formulas of the logic are decorated with names of sequential agents drawn from fixed finite set. The resulting logic has a natural semantics in terms of the runs of a distributed program consisting of a finite set of sequential programs that communicate by performing common actions together. We show that our logic, denoted DLTL, admits an exponential time decision procedure. We also show that DLTL is expressively equivalent to the so called regular product languages.
Lower Bounds for Dynamic Algebraic Problems
Authors: Frandsen Gudmund Skovbjerg , Hansen Johan P. , Miltersen Peter Bro
Published: February 2016

We consider dynamic evaluation of algebraic functions (matrix multiplication, determinant, convolution, Fourier transform, etc.) in the model of Reif and Tate; i.e., if f(x1, . . . , xn) = (y1, . . . , ym) is an algebraic problem, we consider serving on-line requests of the form "change input xi to value v" or "what is the value of output yi?". We present techniques for showing lower bounds on the worst case time complexity per operation for such problems. The first gives lower bounds in a wide range of rather powerful models (for instance history dependent
algebraic computation trees over any infinite subset of a field, the integer RAM, and the generalized real RAM model of Ben-Amram and Galil). Using this technique, we show optimal  Omega(n) bounds for dynamic matrix-vector product, dynamic matrix multiplication and dynamic discriminant and an
Omega(sqrt(n)) lower bound for dynamic polynomial multiplication (convolution), providing a good match with Reif and
Tate's O(sqrt(n log n)) upper bound. We also show linear lower bounds for dynamic determinant, matrix adjoint and matrix inverse and an Omega(sqrt(n)) lower bound for the elementary symmetric functions. The second technique is the communication complexity technique of Miltersen, Nisan, Safra, and Wigderson which we apply to the setting
of dynamic algebraic problems, obtaining similar lower bounds in the word RAM model. The third technique gives lower bounds in the weaker straight line program model. Using this technique, we show an ((log n)2= log log n) lower bound for dynamic discrete Fourier transform. Technical ingredients of our techniques are the incompressibility technique of Ben-Amram and Galil and the lower bound for depth-two superconcentrators of Radhakrishnan and Ta-Shma. The incompressibility technique is extended to arithmetic computation in arbitrary fields.
The Hardness of Speeding-up Knapsack
Authors: Sen Sandeep
Published: February 2016

We show that it is not possible to speed-up the Knapsack problem efficiently in the parallel algebraic decision tree model. More specifically, we prove that any parallel algorithm in the fixed degree algebraic decision tree model that solves the decision version of the Knapsack problem requires  Omega(sqrt(n)) rounds even by using 2^sqrt(n) processors. We extend the result to the PRAM model without bit-operations. These results are consistent with Mulmuley's recent result on the separation of the strongly-polynomial class and the corresponding NC class in the arithmetic PRAM model.
Keywords lower-bounds, parallel algorithms, algebraic decision tree
An Extensional Characterization of Lambda-Lifting and Lambda-Dropping
Authors: Danvy Olivier
Published: February 2016

Lambda-lifting and lambda-dropping respectively transform a block-structured functional program into recursive equations and vice versa. Lambda-lifting is known since the early 80's, whereas lambda-dropping is more recent. Both are split into an analysis and a transformation. Published work, however, has only concentrated on the analysis part. We focus here on the transformation part and more precisely on its formal correctness, which is an open problem. One of our two main theorems suggests us to define extensional versions of lambda-lifting and lambda-dropping, which we visualize both using ML and using type-directed partial evaluation.

See revised version BRICS-RS-99-21.
Proving in Zero-Knowledge that a Number is the Product of Two Safe Primes
Authors: Camenisch Jan , Michels Markus
Published: February 2016

This paper presents the first efficient statistical zero-knowledge protocols to prove statements such as:
A committed number is a pseudo-prime.
A committed (or revealed) number is the product of two safe primes, i.e., primes p and q such that (p - 1)=2 and (q - 1)=2 are primes as well.
A given value is of large order modulo a composite number that consists of two safe prime factors.

So far, no methods other than inefficient circuit-based proofs are known for proving such properties. Proving the second property is for instance necessary in many recent cryptographic schemes that rely on both the hardness of computing discrete logarithms and of difficulty computing roots modulo a composite.
The main building blocks of our protocols are statistical zero-knowledge proofs that are of independent interest. Mainly, we show how to prove the correct computation of a modular addition, a modular multiplication, or a modular exponentiation, where all values including the modulus are committed but not
publicly known. Apart from the validity of the computation, no other information about the modulus (e.g., a generator which order equals the modulus) or any other operand is given. Our technique can be generalized to prove in zeroknowledge
that any multivariate polynomial equation modulo a certain modulus is satisfied, where only commitments to the variables of the polynomial and a commitment to the modulus must be known. This improves previous results,
where the modulus is publicly known.
We show how a prover can use these building blocks to convince a verifier that a committed number is prime. This finally leads to efficient protocols for proving that a committed (or revealed) number is the product of two safe primes. As a consequence, it can be shown that a given value is of large order modulo a
given number that is a product of two safe primes.

 

Keywords. RSA-based protocols, zero-knowledge proofs of knowledge, primality tests.
A Linear Metalanguage for Concurrency
Authors: Winskel Glynn
Published: February 2016

A metalanguage for concurrent process languages is introduced.
Within it a range of process languages can be defined, including
higher-order process languages where processes are passed and received as arguments. (The process language has, however, to be linear, in the sense that a process received as an argument can be run at most once, and not include name generation as in the Pi-Calculus.) The metalanguage is provided with two interpretations both of which can be understood as categorical models of a variant of linear logic. One interpretation is in a
simple category of nondeterministic domains; here a process will denote its set of traces. The other interpretation, obtained by direct analogy with the nondeterministic domains, is in a category of presheaf categories; the nondeterministic branching behaviour of a process is captured in its denotation as a presheaf. Every presheaf category possesses a notion of (open-map) bisimulation, preserved by terms of the metalanguage. The
conclusion summarises open problems and lines of future work.
Migration = Cloning ; Aliasing (Preliminary Version)
Authors: Hüttel Hans , Kleist Josva , Nestmann Uwe , Merro Massimo
Published: February 2016

In Obliq, a lexically scoped, distributed, object-based programming language, object migration was suggested as creating a (remote) copy of an object's state at the target site, followed by turning the (local) object itself into an alias, also called surrogate, for the just created remote copy. There is no proof that object migration in Obliq is safe in any sense.
We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce Øjeblik, a distribution-free subset of Obliq, and provide two formal semantics, one in an intuitive configuration style, the other in terms of pi-calculus. The intuitive semantics shows why surrogation is neither safe in Obliq, nor can it be so in full generality in Repliq (a repaired Obliq). The pi-calculus semantics allows us to prove that surrogation in Øjeblik is safe for certain well-identified cases, thus suggesting that migration in Repliq may be safe, accordingly.
On the (Im)possibility of Basing Oblivious Transfer and Bit Commitment on Weakened Security Assumptions
Authors: Damgård Ivan B. , Kilian Joe , Salvail Louis
Published: February 2016

We consider the problem of basing Oblivious Transfer (OT)
and Bit Commitment (BC), with information theoretic security, on seemingly weaker primitives.We introduce a general model for describing such primitives, called Weak Generic Transfer (WGT). This model includes as important special cases Weak Oblivious Transfer (WOT), where both
the sender and receiver may learn too much about the other party's input, and a new, more realistic model of noisy channels, called unfair noisy channels. An unfair noisy channel has a known range of possible noise levels; protocols must work for any level within this range against adversaries who know the actual noise level. We give a precise characterization for when one can base OT on WOT. When the deviation of the WOT from the ideal is above a certain threshold, we show that no information-theoretic reductions from OT (even against passive adversaries) and BC exist; when the deviation is below this threshold, we give a reduction from OT (and hence BC) that is information-theoretically secure against active adversaries.
For unfair noisy channels we show a similar threshold phenomenon for bit commitment. If the upper bound on the noise is above a threshold (given as function of the lower bound) then no information-theoretic reduction from OT (even against passive adversaries) or BC exist; when it is below this threshold we give a reduction from BC. As a partial result, we give
a reduction from OT to UNC for smaller noise intervals.
Semantics, Modularity, and Rewriting Logic
Authors: Mosses Peter D.
Published: February 2016

A complete formal semantic description of a practical programming language (such as Java) is likely to be a lengthy document, regardless of which semantic framework is being used. Good modularity of the description is important to the person(s) developing it, to facilitate reuse, change, and extension. Unfortunately, the conventional versions
of the major semantic frameworks have rather poor modularity.
 In this paper, we first recall some approaches that improve the modularity of denotational semantics, namely action semantics, modular monadic semantics, and a hybrid framework that combines these: modular monadic action semantics. We then address the issue of modularity in operational semantics, which appears to have received comparatively little attention so far, and report on some preliminary investigations of how one might achieve the same kind of modularity in structural operational semantics as the use of monad transformers
can provide in denotational semantics|this is the main technical contribution of the paper. Finally, we briefly consider the representation of structural operational semantics in rewriting logic, and speculate on the possibility of using it to interpret programs in the described language. Providing powerful meta-tools for such semantics-based interpretation
is an interesting potential application of rewriting logic;
good modularity of the semantic descriptions may be crucial for the practicality of using the tools.
Much of the paper consists of (very) simple examples of semantic descriptions in the various frameworks, illustrating the degree of reformulation needed when extending the described language|a strong indicator of modularity. Throughout, it is assumed that the reader has some familiarity with the concepts and notation of denotational and structural operational semantics. Familiarity with the basic notions of monads and monad transformers is not a prerequisite.
CASL: A Guided Tour of its Design
Authors: Mosses Peter D.
Published: February 2016

Casl is an expressive language for the specification of functional
requirements and modular design of software. It has been designed by CoFI, the international Common Framework Initiative for algebraic specification and development. It is based on a critical selection of features that have already been explored in various contexts, including subsorts, partial functions, first-order logic, and structured and architectural
specifications. Casl should facilitate interoperability of many existing algebraic prototyping and verification tools.
 This guided tour of the Casl design is based closely on a 1/2-day tutorial held at ETAPS'98 (corresponding slides are available from the CoFI archives). The major issues that had to be resolved in the design process are indicated, and all the main concepts and constructs of Casl are briefly explained and illustrated - the reader is referred to the Casl Language Summary for further details. Some familiarity with the fundamental concepts of algebraic specification would be advantageous.
Efficient Timed Reachability Analysis using Clock Difference Diagrams
Authors: Behrmann Gerd , Larsen Kim G. , Pearson Justin , Weise Carsten , Yi Wang
Published: February 2016

One of the major problems in applying automatic verication tools to industrial-size systems is the excessive amount of memory required during the state-space exploration of a
model. In the setting of real-time, this problem of state-explosion requires extra attention as information must be kept not only on the discrete control structure but also on the values of continuous clock variables. In this paper, we present Clock Dierence Diagrams, CDD's, a BDD-like data-structure for
representing and eectively manipulating certain non-convex subsets of the Euclidean space, notably those encountered during verication of timed automata. A version of the real-time verication tool Uppaal using CDD's as a compact datastructure
for storing explored symbolic states has been implemented. Our experimental results demonstrate signicant space-savings: for 8 industrial examples, the savings are between 46%
and 99% with moderate increase in runtime. We further report on how the symbolic state-space exploration itself may be carried out using CDD's.
Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure
Authors: Danvy Olivier , Schultz Ulrik P.
Published: February 2016

Lambda-lifting a block-structured program transforms it into a set of recursive equations. We present the symmetric transformation: lambda-dropping. Lambda-dropping a set of recursive equations restores block structure and lexical scope.

For lack of block structure and lexical scope, recursive equations must carry around all the parameters that any of their callees might possibly need. Both lambda-lifting and lambda-dropping thus require one to compute Def/Use paths:
for lambda-lifting: each of the functions occurring in the path of a free variable is passed this variable as a parameter;

for lambda-dropping: parameters which are used in the same scope as their definition do not need to be passed along in their path.
A program whose blocks have no free variables is scope-insensitive. Its blocks are then free to float (for lambda-lifting) or to sink (for lambda-dropping) along the vertices of the scope tree.

Our primary application is partial evaluation. Indeed, many partial evaluators for procedural programs operate on recursive equations. To this end, they lambda-lift source programs in a pre-processing phase. But often, partial evaluators [automatically] produce residual recursive equations with dozens of parameters, which most compilers do not handle efficiently. We solve this critical problem by lambda-dropping residual programs in a post-processing phase, which significantly improves both their compile time and their run time.

 Lambda-lifting has been presented as an intermediate transformation in compilers for functional languages. We study lambda-lifting and lambda-dropping per se, though lambda-dropping also has a use as an intermediate transformation in a compiler: we noticed that lambda-dropping a program corresponds to transforming it into the functional representation of its optimal SSA form. This observation actually led us to substantially improve our PEPM '97 presentation of lambda-dropping.

Superseded by BRICS-RS-99-27.
Marked Ancestor Problems (Preliminary Version)
Authors: Alstrup Stephen , Husfeldt Thore , Rauhe Theis
Published: February 2016

Consider a rooted tree whose nodes can be marked or unmarked. Given a node, we want to find its nearest marked ancestor. This generalises the well-known predecessor problem, where the tree is a path.
 We show tight upper and lower bounds for this problem. The lower bounds are proved in the cell probe model, the upper bounds run on a unit-cost RAM.
 As easy corollaries we prove (often optimal) lower bounds on a number of problems. These include planar range searching, including the existential or emptiness problem, priority search trees, static tree union-find, and several problems from dynamic computational geometry, including intersection problems, proximity problems, and ray shooting. Our upper bounds improve a number of algorithms from various fields, including dynamic dictionary matching and coloured ancestor problems.
Distributed Versions of Linear Time Temporal Logic: A Trace Perspective
Authors: Thiagarajan P. S. , Henriksen Jesper G.
Published: February 2016

Linear time Temporal Logic (LTL) as proposed by Pnueli [37] has become a well established tool for specifying the dynamic behaviour of distributed systems. A basic feature of LTL is that its formulas are interpreted over sequences. Typically, such a sequence will model a computation of a system; a sequence of states visited by the system or a sequence of actions executed by the system during the course of the computation. A system is said to satisfy a specification expressed as an LTL formula in case every computation of the system is a model of the formula. A rich theory of LTL is now available using which one can effectively verify whether a nite state system meets its specification [51]. Indeed, the verification task can be automated (for instance using the software packages SPIN [21] and FormalCheck [2]) to handle large systems of practical interest.
Hash and Displace: Efficient Evaluation of Minimal Perfect Hash Functions
Authors: Pagh Rasmus
Published: February 2016

A new way of constructing (minimal) perfect hash functions is described. The
technique considerably reduces the overhead associated with resolving buckets in two-level hashing schemes. Evaluating a hash function requires just one multiplication and a few additions apart from primitive bit operations. The number of accesses to memory is two, one of which is to a fixed location. This improves the probe performance of previous minimal perfect hashing schemes, and is shown to be optimal. The hash function description ("program") for a set of size n occupies O(n) words, and can be constructed in expected O(n) time.
Weak Bisimulation and Open Maps
Authors: Fiore Marcelo P. , Cattani Gian Luca , Winskel Glynn
Published: February 2016

A systematic treatment of weak bisimulation and observational congruence
on presheaf models is presented. The theory is developed with
respect to a "hiding" functor from a category of paths to observable
paths. Via a view of processes as bundles, we are able to account for
weak morphisms (roughly only required to preserve observable paths)
and to derive a saturation monad (on the category of presheaves over
the category of paths). Weak morphisms may be encoded as strong
ones via the Kleisli construction associated to the saturation monad.
A general notion of weak open-map bisimulation is introduced, and
results relating various notions of strong and weak bisimulation are
provided. The abstract theory is accompanied by the concrete study
of two key models for concurrency, the interleaving model of synchronisation
 trees and the independence model of labelled event structures.

To appear in Proceedings of the 14th Annual IEEE Symposium on Logic
in Computer science, LICS'99, IEEE Press, July 1999.

 
Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure
Authors: Danvy Olivier , Schultz Ulrik P.
Published: February 2016

Lambda-lifting a block-structured program transforms it into a set of
recursive equations. We present the symmetric transformation: lambda-dropping. Lambda-dropping a set of recursive equations restores block structure and lexical scope.
For lack of block structure and lexical scope, recursive equations must
carry around all the parameters that any of their callees might possibly
need. Both lambda-lifting and lambda-dropping thus require one to compute Def/Use paths:

- for lambda-lifting: each of the functions occurring in the path of a
free variable is passed this variable as a parameter;

- for lambda-dropping: parameters which are used in the same scope
as their definition do not need to be passed along in their path.

A program whose blocks have no free variables is scope-insensitive. Its
blocks are then free to float (for lambda-lifting) or to sink (for lambda-dropping) along the vertices of the scope tree.
Structural Operational Semantics
Authors: Aceto Luca , Fokkink Willem Jan , Verhoef Chris
Published: February 2016

The importance of giving precise semantics to programming and specification
languages was recognized since the sixties with the development of the
first high-level programming languages (cf. e.g. [30, 206] for some early accounts).
The use of operational semantics - i.e. of a semantics that explicitly
describes how programs compute in stepwise fashion, and the possible
state-transformations they perform - was already advocated by McCarthy
in [147], and elaborated upon in references like [142, 143]. Examples of full-blown
languages that have been endowed with an operational semantics are
Algol 60 [140], PL/I [173], and CSP [178].
On the Steiner Tree 3/2-Approximation for Quasi-Bipartite Graphs
Authors: Rizzi Romeo
Published: February 2016

Let G = (V,E) be an undirected simple graph and w : E -> R+ be
a non-negative weighting of the edges of G. Assume V is partitioned
as R union X. A Steiner tree is any tree T of G such that every node
in R is incident with at least one edge of T. The metric Steiner tree
problem asks for a Steiner tree of minimum weight, given that w is a
metric. When X is a stable set of G, then (G,R,X) is called quasi-bipartite.
 In [1], Rajagopalan and Vazirani introduced the notion of
quasi-bipartiteness and gave a ( 3/2 + epsilon) approximation algorithm
 for the metric Steiner tree problem, when (G,R,X) is quasi-bipartite. In this
paper, we simplify and strengthen the result of Rajagopalan and Vazirani.
We also show how classical bit scaling techniques can be adapted
to the design of approximation algorithms.

Key words: Steiner tree, local search, approximation algorithm, bit scaling.

 
Improved Bounds for Dictionary Look-up with One Error
Authors: Brodal Gerth Stølting , Venkatesh Srinivasan
Published: February 2016

Given a dictionary S of n binary strings each of length m,
we consider the problem of designing a data structure for S that
supports d-queries; given a binary query string q of length m, a
d-query reports if there exists a string in S within Hamming
distance d of q. We construct a data structure for the case d = 1, that
requires space O(n log m) and has query time O(1) in a cell probe
model with word size m. This generalizes and improves the
previous bounds of Yao and Yao for the problem in the bit probe
model.

Keywords: Data Structures, Dictionaries, Hashing, Hamming Distance

 
Model-Checking Real-Time Control Programs. Verifying LEGO Mindstorms Systems Using UPPAAL
Authors: Iversen Torsten K. , Kristoffersen Kåre J. , Larsen Kim G. , Laursen Morten , Madsen Rune G. , Mortensen Steffen K. , Pettersson Paul , Thomasen Chris B.
Published: February 2016

In this paper, we present a method for automatic verification
of real-time control programs running on LEGO
RCX bricks using the verification tool UPPAAL. The control
programs, consisting of a number of tasks running concurrently,
are automatically translated into the timed automata
model of UPPAAL. The fixed scheduling algorithm
used by the LEGO RCX processor is modeled in UPPAAL,
and supply of similar (sufficient) timed automata
models for the environment allows analysis of the overall
real-time system using the tools of UPPAAL. To illustrate
our techniques we have constructed, modeled and verified
a machine for sorting LEGO bricks by color.
Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL
Authors: Havelund Klaus , Larsen Kim G. , Skou Arne
Published: February 2016

A real-time system for power-down control in audio/video components
is modeled and verified using the real-time model checker UPPAAL. The
system is supposed to reside in an audio/video component and control (read from and write to) links to neighbor audio/video components such as TV, VCR and remote–control. In particular, the system is responsible for the powering up and down of the component in between the arrival of data, and in order to do so in a safe way without loss of data, it is essential that no link interrupts are lost. Hence, a component system is a multitasking system with hard real-time requirements, and we present techniques for modeling time consumption in such a multitasked,
prioritized system. The work has been carried out in a collaboration between Aalborg University and the audio/video company B&O. By modeling the system, 3 design errors were identified and corrected, and the following verification confirmed the validity of the design but also revealed the necessity for an upper limit of the interrupt frequency. The resulting design has been implemented and it is going to be incorporated as part of a new product line.
A Tough Nut for Tree Resolution
Authors: Dantchev Stefan , Riis Søren
Published: February 2016

One of the earliest proposed hard problems for theorem provers is
a propositional version of the Mutilated Chessboard problem. It is well
known from recreational mathematics: Given a chessboard having two
diagonally opposite squares removed, prove that it cannot be covered with
dominoes. In Proof Complexity, we consider not ordinary, but 2n * 2n
mutilated chessboard. In the paper, we show a 2^Omega(n) lower bound for tree resolution.
Modeling a Language for Embedded Systems in Timed Automata
Authors: Hune Thomas S.
Published: February 2016

We present a compositional method for translating real-time
programs into networks of timed automata. Programs are written in an
assembly like real-time language and translated into models supported
by the tool Uppaal. We have implemented the translation and give an
example of its application on a simple control program for a car. Some
properties of the behavior of the control program are verified using the
generated model.
Local Logics for Traces
Authors: Walukiewicz Igor
Published: February 2016

A mu-calculus over dependence graph representation of traces
is considered. It is shown that the mu-calculus cannot express all
monadic second order (MSO) properties of dependence graphs.
Several extensions of the mu-calculus are presented and it is proved
that these extensions are equivalent in expressive power to MSO
logic. The satisfiability problem for these extensions is PSPACE
complete.
2-Nested Simulation is not Finitely Equationally Axiomatizable
Authors: Aceto Luca , Fokkink Willem Jan , Ingólfsdóttir Anna
Published: February 2016

2-nested simulation was introduced by Groote and Vaandrager
 [10] as the coarsest equivalence included in completed trace equivalence
 for which the tyft/tyxt format is a congruence format. In the linear
time-branching time spectrum of van Glabbeek [8], 2-nested simulation
is one of the few equivalences for which no finite equational axiomatization
 is presented. In this paper we prove that such an axiomatization
does not exist for 2-nested simulation.

Keywords: Concurrency, process algebra, basic CCS, 2-nested simulation,
 equational logic, complete axiomatizations.
The Alternation Hierarchy for the Theory of mu-lattices
Authors: Santocanale Luigi
Published: February 2016

The alternation hierarchy problem asks whether every mu-term,
that is a term built up using also a least fixed point constructor
as well as a greatest fixed point constructor, is equivalent to a
mu-term where the number of nested fixed point of a different type
is bounded by a fixed number.
In this paper we give a proof that the alternation hierarchy
for the theory of mu-lattices is strict, meaning that such number
does not exist if mu-terms are built up from the basic lattice
operations and are interpreted as expected. The proof relies on the
explicit characterization of free mu-lattices by means of games and
strategies.
Dynamic Partitioning in Linear Relation Analysis. Application to the Verification of Synchronous Programs
Authors: Jeannet Bertrand
Published: February 2016

We apply linear relation analysis [CH78, HPR97] to the verification
of declarative synchronous programs [Hal98]. In this approach,
state partitioning plays an important role: on one hand the precision of the results highly depends on the fineness of the partitioning; on the other hand, a too much detailed partitioning may result in an exponential explosion of the analysis. In this paper we propose to consider very general partitions of the state space and to dynamically select a suitable partitioning according to the property to be proved. The presented approach is quite general and can be applied to other abstract interpretations.

Keywords and Phrases: Abstract Interpretation, Partitioning,
Linear Relation Analysis, Reactive Systems, Program Verification
A New Trade-off for Deterministic Dictionaries
Authors: Pagh Rasmus
Published: February 2016

We consider dictionaries over the universe U = {0, 1}^w on a unit-cost
RAM with word size w and a standard instruction set. We present
a linear space deterministic dictionary with membership queries in
time (log log n)^O(1) and updates in time (log n)^O(1), where n is the size
of the set stored. This is the first such data structure to simultaneously
achieve query time (log n)^o(1) and update time O(2 ^sqrt log n) ).
The DSD Schema Language and its Applications
Authors: Klarlund Nils , Møller Anders , Schwartzbach Michael I.
Published: February 2016

XML (eXtensible Markup Language), a linear syntax for trees, has gathered a remarkable amount of interest in industry. The acceptance of XML opens new venues for the application of formal methods such as specification of abstract syntax tree sets and tree transformations. A user domain may be specified as a set of trees. For example, XHTML is a user domain corresponding to the set of XML documents that make sense as
HTML. A notation for defining such a set of XML trees is called a schema language. We believe that a useful schema notation must identify most of the syntactic
requirements that the documents in the user domain follow; allow efficient parsing; be readable to the user; allow a declarative default notation `a la CSS; and be
modular and extensible to support evolving classes of XML documents. In the present paper, we give a tutorial introduction to the DSD (Document Structure Description) notation as our bid on how to meet these requirements. The
DSD notation was inspired by industrial needs, and we show how DSDs help manage aspects of complex XML software through a case study about interactive voice
response systems (automated telephone answering systems, where input is through the telephone keypad or speech recognition). The expressiveness of DSDs goes beyond the DTD schema concept that is already
part of XML. We advocate the use of nonterminals in a top-down manner, coupled with boolean logic and regular expressions to describe how constraints on tree nodes depend on their context. We also support a general, declarative mechanism for inserting default elements and attributes that is reminiscent of Cascading
Style Sheets (CSS), a way of manipulating formatting instructions in HTML that is built into all modern browsers. Finally, we include a simple technique for evolving DSDs through selective redefinitions. DSDs are in many ways much more expressive than XML Schema (the schema language proposed by the W3C), but their syntactic and semantic definition in English is only 1/8th the size. Also, the DSD notation is self-describable: the syntax of legal DSD documents and all static semantic requirements can be captured in a DSD document, called the meta-DSD.
A Discrete Stratety Improvement Algorithm for Solving Parity Games
Authors: Jurdzinski Marcin , Vöge Jens
Published: February 2016

A discrete strategy improvement algorithm is given for constructing
winning strategies in parity games, thereby providing
also a new solution of the model-checking problem for the modal
-calculus. Known strategy improvement algorithms, as proposed
for stochastic games by Homan and Karp in 1966, and for discounted payoff games and parity games by Puri in 1995, work with real numbers and require solving linear programming instances involving high precision arithmetic. In the present algorithm for parity games these difficulties are avoided by the use of discrete vertex valuations in which information about the relevance of vertices and certain distances is coded. An efficient implementation is given for a strategy improvement step. Another advantage of the present approach is that it provides a better conceptual understanding and easier analysis of strategy improvement algorithms for parity games. However, so far it is not known whether the present algorithm works in polynomial time. The long standing problem whether parity games can be solved in polynomial time remains open.
How to Convert a Flavor of Quantum Bit Commitment
Authors: Crépeau Claude , Légaré Frédéric , Salvail Louis
Published: February 2016

In this paper we show how to convert a statistically binding
but computationally concealing quantum bit commitment scheme into a computationally binding but statistically concealing scheme. For a security parameter n, the construction of the statistically concealing scheme requires O(n^2) executions of the statistically binding scheme. As a consequence, statistically concealing but computationally binding quantum bit commitments can be based upon any family of quantum one-way functions. Such a construction is not known to exist in the classical world.
Normalization by Evaluation with Typed Abstract Syntax
Authors: Danvy Olivier , Rhiger Morten , Rose Kristoffer H.
Published: February 2016

We present a simple way to implement typed abstract syntax for the
lambda calculus in Haskell, using phantom types, and we specify
normalization by evaluation (i.e., type-directed partial evaluation) to yield this
typed abstract syntax. Proving that normalization by evaluation preserves
 types and yields normal forms then reduces to type-checking the
specification.
A Temporal Concurrent Constraint Programming Calculus
Authors: Palamidessi Catuscia , Valencia Frank D.
Published: February 2016

The tcc model is a formalism for reactive concurrent constraint programming. In this paper we propose a model of temporal concurrent constraint programming which adds to tcc the capability of modeling asynchronous and non-deterministic timed behavior. We call this tcc extension the ntcc calculus. The expressiveness of ntcc is illustrated by modeling cells and asynchronous bounded broadcasting, by specifying temporal requirements such as response and invariance, and by modeling timed systems such as RCX controllers. We present a denotational semantics for modeling the strongest-postcondition behavior of ntcc processes, and, based on this semantics, we develop a proof system for proving linear temporal properties of these processes.
Equational Theories of Tropical Semirings
Authors: Aceto Luca , Ésik Zoltán , Ingólfsdóttir Anna
Published: February 2016

This paper studies the equational theory of various exotic semirings presented in the literature. Exotic semirings are semirings whose underlying carrier set is some subset of the set of real numbers equipped with binary operations of minimum or maximum as sum, and addition as product. Two prime examples of such structures are the  (max,+) semiring and the tropical semiring. It is shown that none of the exotic semirings commonly considered in the literature has a finite basis for its equations, and that similar results hold for the commutative idempotent weak semirings that underlie them. For each of these commutative idempotent weak semirings, the paper offers characterizations of the equations that hold in them, decidability results for their equational theories, explicit descriptions of the free algebras in the varieties they generate, and relative axiomatization results.
A Fully Equational Proof of Parikh's Theorem
Authors: Aceto Luca , Ésik Zoltán , Ingólfsdóttir Anna
Published: February 2016

We show that the validity of Parikh's theorem for context-free languages depends only on a few equational properties of least pre-fixed points. Moreover, we exhibit an infinite basis of mu-term equations of continuous commutative idempotent semirings.
A Unifying Approach to Goal-Directed Evaluation
Authors: Danvy Olivier , Grobauer Bernd , Rhiger Morten
Published: February 2016

Goal-directed evaluation, as embodied in Icon and Snobol, is built on the notions of backtracking and of generating successive results, and therefore it has always been something of a challenge to specify and implement. In this article, we address this challenge using computational monads and partial evaluation.

We consider a subset of Icon and we specify it with a monadic semantics and a list monad. We then consider a spectrum of monads that also fit the bill, and we relate them to each other. For example, we derive a continuation monad as a Church encoding of the list monad. The resulting semantics coincides with Gudeman's continuation semantics of Icon.

We then compile Icon programs by specializing their interpreter (i.e., by using the first Futamura projection), using type-directed partial evaluation. Through various back ends, including a run-time code generator, we generate ML code, C code, and OCaml byte code. Binding-time analysis and partial evaluation of the continuation-based interpreter automatically give rise to C programs that coincide with the result of Proebsting's optimized compiler.
Syntactic Theories in Practice
Authors: Danvy Olivier , Nielsen Lasse R.
Published: February 2016

The evaluation function of a syntactic theory is canonically defined as the transitive closure of (1) decomposing a program into an evaluation context and a redex, (2) contracting this redex, and (3) plugging the result in the context. Directly implementing this evaluation function therefore yields an interpreter with a quadratic time factor over its input. We present sufficient conditions over a syntactic theory to circumvent this quadratic factor, and illustrate the method with two programming-language interpreters and a transformation into continuation-passing style (CPS). In particular, we mechanically change the time complexity of this CPS transformation from quadratic to linear.
From Known-Plaintext Security to Chosen-Plaintext Security
Authors: Damgård Ivan B. , Nielsen Jesper Buus
Published: February 2016

We present a new encryption mode for block ciphers. The mode is efficient and is secure against chosen-plaintext attack (CPA) already if the underlying symmetric cipher is secure against known-plaintext attack (KPA). We prove that known (and widely used) encryption modes as CBC mode and counter mode do not have this property. In particular, we prove that CBC mode using a KPA secure cipher is KPA secure, but need not be CPA secure, and we prove that counter mode using a KPA secure cipher need not be even KPA secure. The analysis is done in a concrete security framework.
The Implicit Computational Complexity of Imperative Programming Languages
Authors: Kristiansen Lars
Published: February 2016

During the last decade Cook, Bellantoni, Leivant and others have developed the theory of implicit computational complexity, i.e. the theory of predicative recursion, tiered definition schemes, etcetera. We extend and modify this theory to work in a context of imperative programming languages, and characterise complexity classes like P, LINSPACE, PSPACE and the classes in the Grzegorczyk hiearchy. Our theoretical framework seems promising with respect to applications in engineering.
A First-Order One-Pass CPS Transformation
Authors: Danvy Olivier , Nielsen Lasse R.
Published: February 2016

We present a new transformation of call-by-value lambda-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation.

This new CPS transformation connects two separate lines of research. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.
Note on the Tableau Technique for Commutative Transition Systems
Authors: Srba Jirí
Published: February 2016

We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableau-based proof for BPP, that bisimilarity between any two states of such a transition system is decidable. It gives a general technique for extending decidability borders of strong bisimilarity for a wide class of infinite-state transition systems. This is demonstrated for several process formalisms, namely BPP process algebra, lossy BPP processes, BPP systems with interrupt and timed-arc BPP nets.
Temporal Logic with Cyclic Counting and the Degree of Aperiodicity of Finite Automata
Authors: Ésik Zoltán , Ito Masami
Published: February 2016

We define the degree of aperiodicity of finite automata and show that for every set M of positive integers, the class QA_M of finite automata whose degree of aperiodicity belongs to the division ideal generated by M is closed with respect to direct products, disjoint unions, subautomata, homomorphic images and renamings. These closure conditions define q-varieties of finite automata. We show that q-varieties are in a one-to-one correspondence with literal varieties of regular languages. We also characterize QA_M as the cascade product of a variety of counters with the variety of aperiodic (or counter-free) automata. We then use the notion of degree of aperiodicity to characterize the expressive power of first-order logic and temporal logic with cyclic counting with respect to any given set M of moduli. It follows that when M is finite, then it is decidable whether a regular language is definable in first-order or temporal logic with cyclic counting with respect to moduli in M.
Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation
Authors: Damian Daniel , Danvy Olivier
Published: February 2016

We show that a non-duplicating transformation into continuation-passing style (CPS) has no effect on control-flow analysis, a positive effect on binding-time analysis for traditional partial evaluation, and no effect on binding-time analysis for continuation-based partial evaluation: a monovariant control-flow analysis yields equivalent results on a direct-style program and on its CPS counterpart, a monovariant binding-time analysis yields less precise results on a direct-style program than on its CPS counterpart, and an enhanced monovariant binding-time analysis yields equivalent results on a direct-style program and on its CPS counterpart. Our proof technique amounts to constructing the CPS counterpart of flow information and of binding times.

Our results formalize and confirm a folklore theorem about traditional binding-time analysis, namely that CPS has a positive effect on binding times. What may be more surprising is that the benefit does not arise from a standard refinement of program analysis, as, for instance, duplicating continuations.

The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effect of syntactic change.
Static Validation of Dynamically Generated HTML
Authors: Brabrand Claus , Møller Anders , Schwartzbach Michael I.
Published: February 2016

We describe a static analysis of  programs that efficiently
decides if all dynamically computed XHTML documents presented
to the client will validate according to the official DTD. We employ
two interprocedural flow analyses to construct a graph summarizing
the possible documents. This graph is subsequently analyzed to
determine validity of those documents.
There and Back Again
Authors: Danvy Olivier , Goldberg Mayer
Published: February 2016

We present a programming pattern where a recursive function traverses a data structure--typically a list--at return time. The idea is that the recursive calls get us there (typically to a base case) and the returns get us back again while traversing the data structure. We name this programming pattern of traversing a data structure at return time ``There And Back Again'' (TABA).

The TABA pattern directly applies to computing a symbolic convolution. It also synergizes well with other programming patterns, e.g., dynamic programming and traversing a list at double speed. We illustrate TABA and dynamic programming with Catalan numbers. We illustrate TABA and traversing a list at double speed with palindromes and we obtain a novel solution to this traditional exercise.

A TABA-based function written in direct style makes full use of an Algol-like control stack and needs no heap allocation. Conversely, in a TABA-based function written in continuation-passing style, the continuation acts as a list iterator. In general, the TABA pattern saves one from constructing intermediate lists in reverse order.

See also BRICS-RS-05-3.