[ 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.