[ Homepage ] [ Koduleht ] [ Mājaslapa ]

*Slides of the talk:* [ pptx ] [ pdf ]

*Abstract:* In this talk, we describe two
recent developments in quantum algorithms. The first new development is
a quantum algorithm for evaluating a Boolean formula consisting of AND
and OR gates of size N in time O(√N).
This provides quantum speedups for any problem that can be expressed
via Boolean formulas. This result can be also extended to span
problems, a generalization of Boolean formulas. This provides an
optimal quantum algorithm for any Boolean function in the black-box
query model.

The second new development is a quantum algorithm for solving
systems of linear equations. In contrast with traditional algorithms
that run in time O(N ^{2.37...}) where N is the
size of the system, the quantum algorithm runs in time O(log ^{c}
N). It outputs a quantum state describing the solution of the
system.

*Slides of the talk:* [ pdf ]

*Abstract:* It is conventional for Java
developers to access database engines through standard JDBC API which
requires passing SQL queries in plain Java strings. This is referred to
as embedding of SQL queries into Java. The strings are not checked at
compile time, and errors in the queries (e.g. syntax errors or
misspelled names) are usually detected only by testing. In this
presentation we describe a tool which statically analyzes SQL queries
embedded into Java programs. It combines a sound syntactic analyzer
with semantic tests performed by actual database engine. The tool is
implemented as a plug-in for Eclipse IDE.

(Joint work with Andrey Breslav, Jevgeni Kabanov, Varmo Vene.)

*Slides of the talk:* [ pdf ]

*Abstract:* Grover's algorithm is a quantum
algorithm for searching an unstructured search space in which some
elements are solutions to our search problem. The access to the search
space is via an oracle, which given i, answers whether i is a solution.
We analyze a modification of Grover's quantum search algorithm in which
the oracle acts with mistakes. That is, for each solution the oracle
answers that the element is a solution with probability 1-p_i and that
the element is not a solution with probability p_i. We show that if we
run Grover's algorithm for sufficiently many steps, the probability of
finding each solution approaches 1/(k+1) where k is the number of
solution. We also bound the speed with which the probability approaches
its limit value.

*Slides of the talk:* [ ppt ] [ pdf ]

*Abstract:* We compare probabilistic and
deterministic reductions. We show that for every rational k/l >
1/2 there exist sets A and B such that A can be probabilistically
many-one reduced to B with probability k/l, but A cannot be
probabilistically many-one reduced to B with any probability greater
than p such that k/l <= 2 - 1/p. We show that probabilistic
truth-table reduction with probability greater that 2/3 has the same
reduction power as deterministic truth-table reduction, however we
provide an example where probabilistic truth-table reduction with
probability 2/3 is possible, but no deterministic truth-table
reduction. We show that probabilistic Turing reduction with probability
greater than 1/2 has the same reduction power as deterministic Turing
reduction. We prove some other basic probabilistic reduction properties.

*Slides of the talk:* [ ppt ] [ pdf ]

*Abstract:* Combinatorics on words is an area of discrete
mathematics connected to computer science. We analyze finite, generated
bi-ideals from given generating systems {u_0,...,u_m-1} and
{u_0',...,u_n-1'}, investigating the case when all words u_i are of
equal length, whereas all words u_j' are also of equal, but different
length than u_i. A relation between such different bi-ideals
(a/2)*|v_i'|=(b/3)*|v_i|+(b/3)*|v_i-1|+a*b/6 is found. This relation
for two different bi-ideals compares appropriate letters of bi-ideals.

The problem concerning such bi-ideal equality is investigated. It is proved that if such bi-ideals are equal, they are also periodic. The solutions of these problem special cases are given in this paper and it substantially not only uses relation (a/2)*|v_i'|=(b/3)*|v_i|+(b/3)*|v_i-1|+a*b/6, but also some facts from number theory.

*Slides of the talk:* [ pdf ]

*Abstract:* Cellular automata (CA) are models
of parallel
synchronous computation. They are characterized by finite-range
interactions and spatial uniformity. They are employed in qualitative
analysis of complex systems, but also provide a challenging subject for
decidability and complexity questions.

We will first describe
CA in the standard combinatorial way. Then we will introduce a
description in terms of coKleisli maps on a comonad. We will show how
the latter approach allows retrieving several established results of CA
theory as special cases of well-known facts about comonads.

(Joint work with Tarmo Uustalu.)

*Slides of the talk:* [ ppt ] [ pdf ]

*Abstract:* In mainstream notations for
business process
modeling, such as the Business Process Modeling Notation (BPMN), a
process model is composed of nodes (e.g. tasks, events,
gateways)
connected by a flow relation. Although BPMN and similar notations allow
process models to have almost any topology, it is often preferable that
process models follow some structural rules. In this respect, a
well-known property of process models is that of well-structuredness,
meaning that for every node with multiple outgoing arcs (a split) there
is a corresponding node with multiple incoming arcs (a join), such that
the set of nodes between the split and the join form a
single-entry-single-exit region.

In the context of flowcharts (which represent sequential processes) it has been shown that any unstructured flowchart can be transformed into a structured one. If we add parallel splits and joins and we adopt fully-concurrent bisimulation as a notion of equivalence, this result no longer holds: There exist unstructured process models that do not have equivalent structured ones.

This talk presents a necessary and sufficient condition for an acyclic process model to have an equivalent structured process model under fully-concurrent bisimulation. An extension of this result for cyclic process models is also sketched.

(Joint work with Luciano García Bañuelos and Artem Polyvyanyy.)

*Abstract:* When D. Hilbert used
nonconstructive methods in his famous paper on invariants (1888), P.
Gordan tried to prevent the publication of this paper considering these
methods as non-mathematical. L.E.J. Brouwer in the early twentieth
century initiated intuitionist movement in mathematics. His slogan was
``nonconstructive arguments have no value for mathematics''. However,
P. Erdős got many exciting results in discrete mathematics by
nonconstructive methods. It is widely believed that these results
either cannot be proved by constructive methods or the proofs
would have been prohibitively complicated. The author earlier proved
that nonconstructive methods in coding theory are related to the notion
of Kolmogorov complexity. We study the problem of the
quantitative characterization of the amount of nonconstructiveness in
nonconstructive arguments. We limit ourselves to computation by
deterministic finite automata. The notion of nonconstructive
computation by finite automata is introduced. Upper and lower bounds of
nonconstructivity are proved.

*Slides of the talk:* [ pptx ] [ pdf ]

*Abstract:* We apply tools from algebraic
automata theory to study the class of languages recognized by
quantum finite automata (QFA) and probabilistic reversible automata
(PRA). We give a complete characterization of R-trivial idempotent
languages recognized by QFA and PRA.

*Slides of the talk:* [ pdf ]

*Abstract:* We motivate and explore
the security of a setting, where an
adversary against a signature scheme can access signatures on
key-dependent
messages. We propose a way to formalize the security of signature
schemes in
the presence of key-dependent signatures (KDS). It turns out that the
situation is quite different from key-dependent encryption: already to
achieve KDS-security under non-adaptive chosen message attacks, the use
of a
stateful signing algorithm is inevitable---even in the random oracle
model.
We also discuss the connection between key-dependent signing and
forward
security.

(Joint work with Rainer Steinwandt.)

*Slides of the talk:* [ pdf ]

*Abstract:* Flat languages are introduced as
a class of
declarative languages for specifying software in a domain-specific
manner. From such specifications, given a problem statement, programs
can be automatically constructed that compute the required goals. The
semantics of specifications in flat languages is given by means of
higher-order attribute models. We present an instance of a flat
language -- a specification language that consists of a core language
translatable into attribute models and extensions that include tuples,
wildcards and equations. The specification language is built on top of
the Java language. This enables us to use primitive and object types of
Java in specifications and the specifications themselves are embedded
into Java classes. This gives natural and flexible interoperability
between models and the actual code. With higher-order attribute
dependencies, it is possible to synthesize programs withloops,
recursion and conditionals.

*Slides of the talk:* [ pps ] [ pdf ]

*Abstract:* We consider the problem of
applying nonconstructive computation methods to the inductive inference
paradigm known as identification (or identification in the limit) due
to Gold. We define our model at the most abstract level and then give
and discuss three precise definitions. Both function learning and
language learning are studied. Connection to other modifications of
Gold's model, such as identification in the $k$-limit, is shown. At the
end, we present some recent results on reliable nonconstructivity.

*Slides of the talk:* [ pdf ]

*Abstract:* When discussing protocol
properties in the symbolic (Dolev-Yao;
term-based) model of cryptography, the set of cryptographic primitives
is
defined by the constructors of the term algebra and by the equational
theory
on top of it. The set of considered primitives is not easily modifiable
during the discussion. In particular, it is unclear what it means to
define
a new primitive from the existing ones, or why a primitive in the
considered
set may be unnecessary because it can be modeled using other
primitives.
This is in stark contrast to the computational model of cryptography
where
the constructions and relationships between primitives are at the very
foundation of the theory. In this talk, we explore how a primitive may
be
constructed from other primitives in the symbolic model, such that no
protocol breaks if an atomic primitive is replaced by the construction.
As
an example, we show the construction of (symbolic) "randomized"
symmetric
encryption from (symbolic) one-way functions and exclusive or.

*Slides of the talk:* [ pdf ]

*Abstract:* Estonia is already
implementing Internet voting in the national scale. In Norway, the plan
is to have pilot elections in 2011 and full-scale elections in 2017.
Differently from Estonia, Norwegian elections are supposed to be
verifiable. Moreover, they should remain verifiable even in the
presence of untrusted voter PCs. In 2009, we proposed a setting
("code-verification") for Norwegian Internet voting, that was also
adopted in Norway. In this talk, I will explain the setting and two
different code-verification voting protocols. The first protocol was
originally proposed in 2009. Norway is going to use another protocol,
which is more efficient but less secure. The second protocol we explain
is as efficient as the official Norwegian protocol but achieves better
security.

Links to the original papers: [ paper1 ] [ paper2 ]

*Slides of the talk:* [ pptx ] [ pdf ]

*Abstract:* High electricity consumption,
associated with
running Internet scale server farms, not only reflect on the data
center's footprint, but also increases of running the data center
itself. Green computing is a new paradigm which considers not only the
performance of a computing system, but also it's energy efficiency.

In this paper we consider the problem of maximizing the revenues of service providers running large scale data centers subject to setup costs by trimming down their electricity bill. As a solution, we present and evaluate the performance of allocation policies which dynamically power servers up and down according to changes in user demand with the aim of maximizing the users' experience while minimizing the amount of electricity required to run the IT infrastructure. The results of several experiments are presented, showing that the proposed scheme performs well under different trafficconditions.

*Slides of the talk:* [ ppt ] [ pdf ]

*Abstract:* The Grover's algorithm is a
quantum search algorithm solving the unstructured search problem in
about (π/4)√N
queries. It is known to be optimal - no quantum algorithm can solve the
problem in less than the number of steps proportional to √N
[1] . Moreover, for any number of queries up to about (π/4)√N
, the Grover's algorithm ensures the maximal possible probability of
finding the desired element [2]. However, it is still possible to
reduce the average number of steps required to find the desired element
by ending the computation earlier and repeating the algorithm if
necessary. This fact was mentioned by Christof Zalka as a short remark
on analysis of the Grover's algorithm [2]. We give a detailed
description of this simple fact.

References

[1]
Lov Grover. A fast quantum mechanical algorithm for database search.
Proceedings, 28th Annual ACM Symposium on the Theory of Computing
(STOC), May 1996, pages 212-219, also arXiv: quant-ph/9605043

[2] Christof Zalka. Grovers quantum searching algorithm is optimal. arXiv: quant-ph/9711070

[3] C. Bennett et al. Strengths and Weaknesses of Quantum Computing. SIAM Journal on Computing (special issue on quantum computing) volume 26, number 5, pages 1510-1523. arXiv: quant-ph/9701001

(Joint work with Aleksandrs Rivošs.)

*Slides of the talk:* [ pdf ]

*Abstract:* We present a denotational
semantics for a simply
typed call-by-need letrec calculus, which distinguishes direct cycles,
such as let rec x = x in x and let rec x = y and y = x + 1 in x, and
looping recursion, such as let rec f = lambda x . f x in f 0.
In
this semantics the former denote an exception whereas the latter
denotes divergence.

The distinction is motivated by ``lazy evaluation'' as implemented in OCaml and Racket: when a delayed variable is dereferenced for the first time, it is first pre-initialized to an exception-raising thunk and is updated afterward by the value obtained by evaluating the expression bound to the variable. Any attempt to dereference the variable during the initialization raises an exception rather than diverges. This way, lazy evaluation provides a useful measure to initialize recursive bindings by exploring a successful initialization order of the bindings at runtime and by signaling an exception when there is no such order. It is also used for the initialization semantics of the object system in the F# programming language.

The denotational semantics is proved adequate with respect to a referential operational semantics.

*Slides of the talk:* [ pdf ]

*Abstract:* Random Oracle model
popularized by Bellare and Rogaway in 93 has
proven to be hugely successful, allowing cryptographers to give
security
proofs for very efficient and practical schemes. In this paper, we
discuss
the possibility of using an incompressible but fixed, ?algorithmically
random? oracle instead of the standard random oracle and show that this
approach allows for rather similar results to be proven but in a
completely
different way. We also show that anything provably secure in the
standard
random oracle model is also secure with respect to any algorithmically
random oracle and then discuss the implications of that rather
surprising
result.

*Slides of the talk:* [ ppt ] [ pdf ]

*Abstract:* The topic presents overview of
game theory aspects and current research directions including

1)
Classical game tree search algorithms and new fuzzified search
techniques which are based on the idea that exact game tree evaluation
is not required to find the best move. Thus pruning techniques may be
applied earlier resulting in faster search and greater performance.

2)
Machine learning approaches applied to real domain game with element of
chance backgammon demonstrating ability of the program to learn from
“zero” knowledge and reach strong level of play

3) Introduction to card games and common problems in the Texas Hold’em poker.

*Slides of the talk:* [ pdf ]

*Abstract:* We extend the simple imperative
language While with
a parallel-construct and transactions and endow it with a "weak"
small-step operational semantics that models optimistic concurrency
control. In order to show the correctness of this implementation of
transactional memory, we also define a "strong" operational semantics
that executes transactions literally atomically (in one small step),
hence sequentially. We show that every run in the "weak" model has a
corresponding run in the "strong" model and thus satisfies the
correctness criterion of opacity.

(Joint work with Tarmo Uustalu.)

*Slides of the talk:* [ ppt ] [ pdf ]

*Abstract:* Many of the talks of this event
are on quantum
computing topics; on the other hand not all of the participants are
closely familiar with this field of reasearch. Therefore we deemed it
useful to present a short tutorial on quantum computing (QC). We will
concentrate on the mathematical side of QC based on only few basic
principles of quantum mechanics. The topics will include: how the state
(or "memory") of a quantum computer can be described; how the state can
be transformed (and thus computation performed); how the outcome of the
computation can be read; the main features differentiating the quantum
computation from the classical one: superposition, interference and
entanglement; examples showing how these features can be used
for
efficient computation or data communication.

*Slides of the talk:* [ pptx ] [ pdf ]

*Abstract:* Bell inequalities were created to
show the difference between clasical - local world and quantum world
that supports non-locality. One of the best models to show the
difference between locality and non-locality is the CHSH
game. We study a generalized CHSH game for n-players and with
nonuniform input.

*Slides of the talk:* [ pdf ]

*Abstract:* Residual finite state automata
(RFSA) are a
subclass of nondeterministic finite automata (NFA) with the property
that every state of an RFSA defines a residual language of the language
accepted by the RFSA. Recently, a notion of a biresidual automaton
(biRFSA) -- an RFSA such that its reversal automaton is also an RFSA --
was introduced by Latteux, Roos, and Terlutte. They studied
minimality issues of biRFSAs, and among other things, they showed that
a subclass of biRFSAs called biseparable automata consists of unique
state-minimal NFAs for their languages.

We present some new minimality results concerning biRFSAs and biseparable automata. We consider two lower bound methods for the number of states of NFAs -- the fooling set and the extended fooling set technique -- and present two results related to these methods. First, we show that the lower bound provided by the fooling set technique is tight for and only for biseparable automata. And second, we prove that the lower bound provided by the extended fooling set technique is tight for any language accepted by a biRFSA. Also, as a third result, we show that any reversible canonical biRFSA is a transition-minimal \epsilon-NFA. To prove this result, the theory oftransition-minimal \epsilon-NFAs by S. John is extended.

*Slides of the talk:* [ pdf ]

*Abstract:* Specifying and verifying model
transformations is
of central concern in the Model Driven Engineering (MDE). There exist
many techniques to verify (\emph{certify}) the correctness of
transformations based on their specifications, ranging from plain
testing to theorem proving. In critical application domains however,
both, the transformation engine and the verification tool(s) are
subject to a formal process called \emph{qualification}, which places
strong constraints on the available design choices. In this talk we
will present ongoing work on specifying and verifying
modeltransformations in a qualifiable embedded code generator
Gene-Auto.

*Slides of the talk:* [ pdf ]

*Abstract:* DNA sequence analysis methods,
such as motif
discovery, gene detection or phylogeny reconstruction, can often
provide important input for biological studies. Many of such methods
require a

\emph{background model}, representing the expected
distribution of short substrings in a given DNA region. Most current
techniques for modeling this distribution disregard the evolutionary
processes underlying DNA formation. We propose a novel approach for
modeling DNA $k$-mer distribution that is capable of taking the notions
of evolution and natural selection into account. We derive a
computionally tractable approximation for estimating $k$-mer
probabilities at genetic equilibrium, given a description of
evolutionary processes in terms of fitness and mutation probabilities.
We assess the goodness of this approximation via numerical experiments.
Besides providing a generative model for DNA sequences, our method has
further applications in motif discovery.

(Joint work with Meelis Kull, Jaak Vilo.)

*Abstract:* Most programming languages allow
nonterminating
program runs, i.e., runs that never stop. For semantics and logics of
programming languages, the possibility of nontermination is a
complication that can be handled by ignoring it (pretending that the
nonterminating runs are not there) or facing it (by properly accounting
for them in some useful way). In this overview talk, I demonstrate how
nontermination from looping can be analyzed in terms of possibly
infinite datastructures, corecursion and coinduction. I will first
discuss a simple imperative language and then move on to a
call-by-value functional language with a general effect.

(Based partly on joint work with Keiko Nakata.)

*Slides of the talk:* [ ppt ] [ pdf ]

*Abstract:*
Study of gene network behaviour is one of the central topics of systems
biology. No comprehensive definition of a gene network can be given
easily, but roughly - DNA encodes proteins, a complex cellular
machinery 'reads' the DNA and makes (expresses) these proteins, the
proteins then interact with other proteins and with the DNA, and these
interactions sometimes change the rate of expression. This dynamics
leads to complex biological behaviour such as cell growth, division,
differentiation, death, and other types of qualitative behaviour. When
describing gene networks we can distinguish between (1) network
topology - a diagram showing which protein interact with what other
elements of the network influencing the expression of which other
proteins, and (2) numerical parameters characterizing the strength of
such interaction and their quantitative effects on expression. Note
that experimentally it is often difficult to measure the quantitative
model parameters accurately. Assuming that it is possible to separate
between the topology and quantitative parameters in the model, we can
study to what extent the qualitative behaviour of the system depends on
the topological structure of the network, and to what extent the exact
quantitative values (relative or absolute) of the parameters are
crucial.

Here we address this question. To describe gene
networks we use a mathematical formalism called hybrid systems, which
provides a direct way of modelling both discrete events, such as
protein binding on one hand, and continuous behaviour, such as protein
concentration changes on the other hand. Hybrid systems also provide a
natural separation between the description of the network topology and
quantitative model parameters. Dynamic behaviour of a hybrid system can
be described as a path through a potentially infinite state space, each
state being characterized by the discrete mode of the system (e.g.,
which proteins have bound DNA) at that point in time, and the values of
the continuous variables (e.g., protein concentrations). We define
formally qualitative observable behaviour of a hybrid system and show
that it is related to the models attractor structure. An attractor is a
region in the state space to which the system may converge and from
some point in time never leaves. It has been hypothesized that the
attractors in a biological system correspond to the possible
phenotypes, such as cell types. Our method enables us to study the
attractor structure of the hybrid system and its dependence on the
systems topology as well as the concrete (absolute or relative)
parameter values.

(Joint work with Alvis Brāzma, Kārlis Čerāns, Dace Rukliša, Thomas Schlitt.)

*Slides of the talk:* [ pdf ]

*Abstract:* We investigate an open problem
about maximum separation between two complexity measures of Boolean
functions, namely the sensitivity and block sensitivity. We improve the
best known estimates between those complexity measures. Our work makes
extensive use of experimental mathematics; we also report results
obtained this way.

*Slides of the talk:* [ pdf ]

*Abstract:* This talk will introduce
several new efficient protocols that
allow secret-shared multi-party computation frameworks (like Sharemind)
to
be used as oblivious database engines. We construct an nearly
constant-round
(1, n)-OT protocols with different time-memory tradeoffs and oblivious
random shuffle protocols to protect the privacy of the underlying
dataset.
The latter will allow us to construct an efficient multi-query (m,
n)-OT
protocol as well.

(Joint work with Sven Laur and Jan Willemson.)

*Slides of the talk:* [ pdf ]

*Abstract:* CHSH game is 2 player 1 verifier
game where
verifier gives to each player one bit and each player responds with one
bit. Players win if XOR of responded bits equals AND of given bits.
This game has been designed to show the difference between classical
and quantum strategies.

In this talk we will present ideas how to solve 3 parallel CHSH games and also present algorithm how to experimentally prove best result for 4 parallel CHSH games. We will also sketch a combinatorial way how to improve naive upper bound for n parallel games, but we should mention that there exist better result for n parallel games.