| CIDEC ÜIK |
Estonian Winter Schools in Computer Science Eesti arvutiteaduse talvekoolid |
EWSCS 2004 EATTK 2004 |
Frederik Armknecht
University of Mannheim, Germany
Due to their efficiency, LFSR-based stream ciphers are widely used in practice (e.g., mobile phones) to ensure the secrecy of transmitted data. Modern cryptographic techniques made it possible to improve the resistance against well-known attacks like correlation attacks.
Recently, a new kind of attack came up: algebraic attacks. They proved to be more successful against certain stream ciphers than all other kinds of attacks known before (e.g., against the keystream generator used in the Bluetooth standard). Algebraic attacks are based on finding and solving a system of nonlinear equations. The efficiency of these attacks greatly depends on the degree of the nonlinear equations.
For this purpose, fast algebraic attacks were proposed (Courtois; Crypto 2003). The main idea is to decrease the degree of the equations using a precomputation algorithm. Unfortunately, the correctness of the precomputation step was neither proven, nor was it obvious in general. Recent results are a correctness proof under rather weak assumptions and a modified precomputation step which is better in several ways (Armknecht; FSE 2004).
This talk provides an introduction into the field of (fast) algebraic attacks and discusses the results mentioned above.
Liliana Cojocaru
Rovira i Virgili University of Tarragona, GRLMC; Al. I. Cuza University of Iasi, Computer Science, Spain
Communication is anywhere two or more sides of a (living or artificial) system need to collaboratively perform a given task. It is required either by the lack of information or by the necessity of improving the system performances. Communication complexity (introduced in 1979, by Yao) represents the amount of information exchanged during a computational process, in which two (or more) players, each of them having access to partial information of the input, have to collaboratively evaluate a function by minimizing the communication between them. The flow of information (the number of exchanged bits) is measured by ignoring the other cost, such as time and space.
Cooperating Distributed (CD) or Parallel Communicating (PC) Grammar Systems (set of grammars that function together according to a specified protocol of cooperation), Lindenmayer Systems (parallel rewriting systems that simulate the growing of plants), P-Systems (parallel biological membrane computing systems), etc, have been conceived in order to overtake the large variety of the existing type and data communication from the real life. My PhD dissertation deals with the mathematical interpretation of different aspects of communication complexity, tackled by the above devices, for different types of communication processes (sequential, parallel or distributive, synchronized or not; one-way or two-way, deterministic or not). We focus on several inquiries of the complexity theory, such as: how the communication process can be mathematically formalized, which are the lower and the upper bounds that embed a communicating system, which are the evidences of tractability and intractability related to this communication measure.
Among others, we give an overview of several theoretical results known in the literature for the communication complexity of PCGS, and we preset our own attempts, done so far, in the fields of communication complexity of CDGS, L-Systems and P-systems. The communication structure (the shape of the communication graphs) and the communication complexity (the number of exchanged messages between the components of the system - grammars or membranes) by minimizing the communication between them, is defined and studied in a very first draft of a doctoral thesis named “The Communication Complexity of Parallel and Distributive Computing”.
References (among other)
J. Hromkovič, J. Kari, L. Kari, Some hierarchies for the communication complexity measures of cooperating grammar systems. Theoretical Computer Science, 127 (1994) 123-147.
E. Kushilevitz, N. Nisan. Communication Complexity. Cambridge University Press, 1997.
D. Pardubská, The communication complexity hierarchy of parallel communicating systems. IMYCS’92.
Juhan Ernits
Institute of Cybernetics, Estonia
The work focuses on a synchronous system containing buffers, registers and memory interconnected by several shared and proprietary busses. The concrete example is based on a radar system memory interface case study from the IST AMETIST project. The correct operation of the memory interface board implies that it provides an uninterrupted stream of processed data and that none of the input buffers ever experiences any overflows. The analysis of this system concentrates on the problems related to concurrency, in particular, on how to manage the shared resources in such a way that the system operates correctly.
The existence of a solution to the latter problem under further restrictions on resources yields optimisation as a by-product of formal analysis. The contribution of the work is a way to partition the problem into independent subproblems that enable to abstract away details that are irrelevant with respect to the concurrency issue while still guaranteeing correct behaviour in the concrete system. This is necessary to make the problem solvable by a model checker.
Christian Mahesh Hansen
Department of Informatics, University of Oslo, Norway
Free variable tableaux has until recently suffered from two major shortcomings. One is that the tableaux rules that introduce new free variables are too restrictive, i.e. they generate dependencies in the proof objects, which are not logically necessary. The other is the backtracking closure procedure, known as iterative deepening, used by virtually all tableaux implementations. Some limit is put on the search space, and if a proof is not found within the limit, the proof search is restarted with an increased limit, discarding all collected data. Backtracking is induced by the closure procedure, not by the tableaux calculus itself.
Waaler and Antonsen at the PMA group, Department of Informatics, University of Oslo, have addressed the first problem in their paper "A free variable sequent calculus with uniform variable splitting", first presented at TABLEAUX 2003. They introduce variable splitting and a simple indexing system for formulae, variables and Skolem functions, and achieve a calculus in which derivations are invariant under permutations and the term universe can be restricted branchwise. This can, in extreme cases, result in exponentially shorter proofs.
Martin Giese at Chalmers University of Technology, Göteborg, has addressed the second problem in his PhD thesis "Proof Search Without Backtracking for Free Variable Tableaux". In his recursive definition of sets of closing instantiations for free variables, the tableau expansion and the search for closing unifiers is conducted simultaneously until a global unifier that closes the whole tableau is found, thus eliminating the need for backtracking.
I will present the outline of my master thesis work, which goal is to combine the incremental closure procedure with the free variable sequent calculus in a unifying formal specification and a working implementation. The recursive definition by Giese must be extended to handle the increased complexity of the splitting and indexing introduced in the sequent calculus. Another problem is the choice of implementation platform. An executable inductive definition in Maude is highly desired, but some critical parts of the incremental closure procedure suggest an object-oriented approach, in which the increased control of imperative programming is helpful.
My master thesis is part of the TAcS - Tableaux with Accelerated Search - research project at the Department of Informatics, University of Oslo, under supervision by Arild Waaler. The TAcS project relates closely to the KeY project, which aims at developing a framework for integrating formal software specification and verification into industrial software engineering.
Matti Järvisalo
Helsinki University of Technology, Laboratory for Theoretical Computer Science, Finland
Propositional satisfiability checkers have been applied successfully to many interesting domains. Most successful SAT checkers assume that the input formulae are in conjunctive normal form (CNF). However, using CNF makes efficient modeling of an application cumbersome. Therefore one usually employs a more general formula representation and then transforms the formula into CNF by using a standard translation. This translation introduces a new variable for each Boolean connective in the formula, resulting in a linear size CNF translation.
As an alternative representation, Boolean circuits are interesting because they allow for a compact and natural representation in many domains, in which the representation can be simplified by sharing common subexpressions and by preserving natural structures and concepts of the domain. A tableau method that works directly with Boolean circuits has been developed. It can be seen as a lifting of the Davis-Putnam procedure for CNF to Boolean circuits. Instead of standard (cut free) tableau techniques it employs a direct cut rule combined with deterministic (non-branching) deduction rules. The aim is to achieve high performance and to avoid some computational problems in cut free tableaux.
The efficiency of a typical Davis-Putnam method based SAT checking system depends
(i) on the applied search space pruning techniques
and
(ii) on the splitting rule (i.e., on which gates it is possible to apply the explicit cut).
In this work, we focus on the splitting/cut rule. The research problem is:
How do restrictions on the use of the cut rule effect the proof complexity in Boolean circuit satisfiability checking based on tableaux?
For instance, it has been proposed that one could benefit from restricting the cuts to the input gates only as they determine the values of all other gates. Our results show that doing so can, in the worst case, result in exponentially larger proofs compared to the unrestricted cut rule. In addition to the input gate restricted cuts, we study several other natural locality based restrictions of the cut rule. Our results show that restricting the cut in any of the considered ways can result in exponentially larger proofs than the unrestricted cut. In addition, we show that there are also exponential differences in the proof complexity between the restricted versions of the cut rule.
The results directly apply to SAT checkers for CNF formulae in the case the formulae are obtained from circuits by using the standard linear size translation.
Alexander Kulikov
St. Petersburg State University, Russia
Splitting method is one of the most powerful and well-studied approaches for solving various NP-hard problems. The main idea of this method is to split an input instance of a problem into several simpler instances further simplified by certain simplification rules, such that by finding the solution for all of them one can in polynomial time construct the solution for initial instance. There exists a huge number of articles describing algorithms of this type and usually a considerable part of such an article is devoted to case analysis. In this paper we give several ideas describing how to write a program that given simplification rules would automatically generate a proof (i.e., the corresponding case analysis) of upper bound on the running time of splitting algorithm that uses these rules. As an example we report the results of experiments with such a program for (n,3)MAXSAT problem (MAXSAT problem for the case when every variable in the formula appears at most three times). The new bound for this problem obtained by our program is O(1.2852^n) (where n is the number of variables in input formula), the previous known bound is O(1.324719^n) due to Bansal and Raman.
Yury Lifshits
St.Petersburg State University, Russia
We study multiparty communication complexity of the Polygon Function and Polygon Inequality Function. Communication complexity is an important part of complexity theory. We recall the notion of multiparty communication complexity. Let F(x_1, ... ,x_k) be a binary function of k variables. Each variable x_i takes values from some finite set D_i. Suppose that there are k participants trying to compute this function. Agent i knows the values of all variables except the i-th one. To achieve their goal, participants have to send some information to each other. The minimal amount of information they have to send is k-party communication complexity of the function F.
In this work we consider two following functions F and G. Given positive integers n and k>1, integers 1<= a_1, ... ,a_k <= n, the value of F(a_1, ... ,a_k) equals one if there exists a polygon with lengths of sides a_1, ... ,a_k and zero otherwise. We call this function Polygon Function. Second binary function G(a_1, ... ,a_k)=1 iff a_1<a_2+...+a_k. We call this function Polygon Inequality Function.
We are interested in Polygon Inequality Function because it is both very simple and provides nontrivial lower bound for communication complexity. Our result shows that communication complexity is not bounded. This is just the first step towards proving more precise lower bounds. The crucial tool is a multidimensional generalization of van der Waerden theorem due to Gallai and Witt. Our technique could be useful for proving lower bounds for communication complexity of other functions.
Tommi Meskanen
University of Turku, Dept. of Mathematics, Finland
The NTRU cryptosystem is based on lattices. The hard problem behind it is finding the shortest (or at least very short) vector from the lattice. All required operations are relatively fast and the key sizes are small.
In its previous version NTRUEncrypt has the peculiar property that the decryption does not always work in a constant time: Sometimes a legally generated cryptotext needs several tries before decryption succeeds. These are called wrap failures. The encrypter does not know when this will happen. Our attack is based on encrypting selected messages and observing how long it takes to decrypt them.
Depending on the private key some messages that are harder to decrypt than the others. In our attack we try to find what these types of messages are. We do this in three steps. With every step we find out more about the private key. Thus we can make wrap failures more frequent and get more accurate information about the private key. After the last step we have found out the private key with a considerable probability.
After this and several slightly different attacks the standard was changed. With the new version of the NTRUEncrypt this attack no longer works. We present some methods to ease the shortest vector problem and try to approximate the complexity with actual parameters.
Emilia Oikarinen
Helsinki University of Technology, Laboratory for Theoretical Computer Science, Finland
To solve a problem in answer set programming (ASP), one constructs a logic program so that its answer sets correspond to the solutions of the problem and computes the answer sets of the program using a special purpose search engine. The encodings are not unique, i.e. several versions of a program can be used e.g. in optimizing the execution time or space. Since the solutions to the problem correspond to answer sets of the program, it is necessary to ensure that the different encodings yield the same output. In ASP this means that one has to check whether given two logic programs have the same answer sets, i.e., whether they are semantically equivalent. We consider in this work the class of disjunctive logic programs that form a proper generalization of normal logic programs.
The equivalence of logic programs P and Q can naturally be verified using an explicit crosscheck of all the answer sets of both programs. The aim in this work is, however, to develop a systematic method for testing the equivalence so that a naive crosscheck of answer sets is not needed. The idea is to translate logic programs P and Q into a single logic program that has an answer set if and only if P has an answer set that is not an answer set of Q. Thus answer sets of the translation (if found), act as a counter-examples for the equivalence of P and Q. The counter-examples for equivalence divide naturally in two types. Thus the search for counter-examples can be performed separately for both types using a two-phased translation.
We have implemented the translation functions. Experiments with the implementation show that in several cases the translation-based approach is superior to the naive crosschecking approach, especially, if the programs to be tested have several answer sets and are likely to be nonequivalent. If the number of answer sets is low, then the naive cross-checking approach is likely to be faster. Furthermore, in general it is faster to use the two-phased translation.
Lutz Strassburger
Loria & INRIA Lorraine, Nancy, France, France
The calculus of structures is a proof theoretical formalism, like natural deduction and the sequent calculus, for specifying logical systems and studying their properties. In this talk I will present its basic principles and its main features. For example, due to a new up-down symmetry, the identity axiom and the cut rule become syntactically dual. This allows to reduce the cut to an atomic version without going through a cut elimination argument. Furthermore, in the calculus of structures one can present new types of inference rules that allow to design logical systems that are completely local. More precisely, the contraction rule can be reduced to an atomic version (in the same way as it is usually done for the identity), and the promotion rule of linear logic can be presented in a local form. I will also present decomposition theorems which provide new types of normal forms for proofs and which are independent from cut elimination.
Johan Wallén
Helsinki University of Technology, Finland
It has recently been observed that formal rational series, as defined in formal language theory, provides a very convenient framework for studying the differential and linear properties of addition modulo a power of two. These properties are needed for applying differential and linear cryptanalysis to ciphers that use addition as a building block. The approach based on rational series gives straightforward derivations of the results of Lipmaa and Moriai at Fast Software Encryption 2001 and Wallén at Fast Software Encryption 2003, and allows us to study several related (and dual) problems. In this talk, we give an overview of rational series, how they can be used in cryptanalysis, and discuss their limitations.
The talk is partially based on the paper
Joakim Bjørk
Department of Informatics, University of Oslo, Norway
In this talk, we consider a translation of a graphical representation of a Petri Net to a Maude module representing the same Net based on rewriting logic.
A Petri Net is a graphical model of a system or algorithm. It is a directed graph with two kinds of nodes places and transitions. The places represents the local states of the system, while the transitions represents the changes. The Petri Net formalism was introduced by Carl Adam Petri in 1962 and has over the years turned into many dialects.
The basic axioms in rewriting logic are rewriting rules of the form t1 -> t2 (possibly with conditions). Logically it means that we can derive the formula t2 from the formula t1. Computationally the rewriting rule is interpreted as a local transition in a concurrent system from an instance of a pattern t1 to an instance of pattern t2.
Maude is an executable program language based on rewriting logic with extensive analyzing tools to reason about properties like liveness, invariants, deadlocks and so on.
Petri Nets are given by a precise mathematical semantics, but it is not obvious how an operational or symbolic semantics should look like. The Maude modules are examples on what they can look like.
With a translation from graphical Petri Nets to Maude modules we can use the analyzing techniques of Maude to simulate and analyze the nets. We will investigate Maude provides an addition to the analyzing techniques we have in an typical Petri Net tool. Another advantage is to get a unifying framework for many dialects of Petri Nets. Means to achieve this have been carried out by M.O.Stehr, J. Meseguer and P. Olveczky.
We will expand their translation to handle Timed Petri Nets and also build an interpreter that translates an xml document representing a Net, generated by a graphical Petri Net tool (Design/CPN), to a Maude module.
Ieva Bolakova
Daugavpils University, Dept. of Computer Science, Latvia
In this paper, two inductive learning algorithms C4.5 and CN2 are considered and also the analysis of them is given, estimating quality and efficiency of the received results. The algorithm C4.5 is one of more popular decision tree construction algorithms. In turn CN2 is an algorithm in which the stage of decision tree construction is missed - the rules set is created at once.
Both algorithms C4.5 and CN2 were applied in a task of Latin alphabet letters classification. All 26 letters were drawn in the stencil with 20 elements. The solution of the task is shared into two stages – from the beginning all letters are divided into 6 groups, depending on that, how many horizontal, vertical and diagonal elements are in them, and at this stage we need to define, to which group each letter belongs. In the second stage we need to find the rules for the recognition of each specific letter.
In the first experiment the rules set which we have received with the algorithm CN2 is lesser than the rules set received by the C4.5. CN2 recognizes the first group of letters by two rules, but C4.5 distinguishes the same group by three rules. If we pay attention to quantity of checked conditions in the rules here again algorithm CN2 is the author of more qualitative rules - separate rules check smaller quantity of attributes than the rules received with C4.5.
It is necessary to note also, that in both rule sets there are only two identical rules.
In the second experiment in which we receive letters recognition rules, the size of the rules set is identical in both algorithms.
The purpose of the experiments considered in this paper was to analyze two inductive learning algorithms CN2 and C4.5, applying them to the concrete task – the classification rules induction of the Latin alphabet letters. The analysis of the received results is based on an estimation of quality of the rule sets - quantity of the rules in the sets and quantity of the considered conditions in the rules.
We can draw a conclusion that both algorithms work well - rules for recognition of the letter groups and also rules for classification of all letters are received. However in a specific task algorithm CN2 appeared more qualitative – there is smaller quantity of the conditions in the received rules.
Diana Dubu
West University from Timisoara, Faculty of Mathematics and CS, Research Inst. e-Austria Timisoara, Romania
Mathematical reasoning and computation addresses a wide variety of problems in various domains. As scientific and engineering applications are increasing both in problem size and problem complexity they require very often high performance computing components [1]. As a result of the rapid spread of clusters and computers in the academic and industrial environments, parallel and distributed computing proved to be a scalable solution to the demands of speed and performance [2]. Moreover, the emerging grid computing focused on providing a "flexible, secure, coordinated resource sharing among dynamic collections of individuals, institutions and resources" [3]. For such reasons, access to the computational power of current computer algebra systems (CAS) can be provided by grid-enabling them.
We propose a Java-based middleware, which allows a connection between the current Maple version and the computational grids. We have been encouraged in this decision by Maple's features, as it is well known that Maple excels other CAS in solving selected classes of problems like systems of nonlinear equations or inequalities. The new release allows calls of external functions written in other programming languages (such as C, Fortran or Java). Maple has a sockets library for communicating over the internet and a library for parsing XML ad transforming its output in MathML [4].
Our grid-aware CAS can initiate a communication with external services by activating the proxy through a command issued by the user. The proxy is acting as a middleware between Maple and the grid services. The process continues by either initiating or searching for a gatekeeper and establishing a link with its location. User commands are then received from the user's Maple interface via sockets and parsed accordingly to RSL syntax. As a result the proxy queries the contacted services, which in turn send back the results to the main Maple interface. The aforementioned Maple commands are implemented in our package maple2g.
As a further work we aim at providing access to such computing from Internet browsers, which would activate a Maple kernel, by relying on Maple's functionality of parsing the output in MathML format.
Marina Issakova
University of Tartu, Inst. of Computer Science, Estonia
In year 2004 a group of people from Institute of Computer Science of University of Tartu will be engaged in T-algebra project. The idea of T-algebra project is to create an environment that enables step-by-step solution of problems in four mathematical areas: calculation of value of numerical expressions, operations with fractions, linear equations, inequalities and systems of linear equations solving, and multinomial problems.
The following text describes the work with problem solving environment T-algebra. A set of rules will be realized in program, so that each rule leaves the part of the work to be done by the student and the other part is done by the program. This gives the possibility to diagnose student’s knowledge of different rules. When solving a problem the student is given freedom for choosing the rule to apply next, that allows diagnosing the student knowledge of solution algorithms. The program should also be intelligent enough to provide the student different kinds of help during solution.
T-algebra project has two basic goals: the first is to give a problem solving environment for Estonian schools and the second is to create the research tool for doctoral studies.
My part in this project is to design and realize linear equations, inequalities and systems of linear equations solving. These tasks contain different smaller problems (such as reduction of similar terms etc.), each of them needs introducing one or more rules. In my talk I will speak about user interface of equations solving, problems, which appear during design and programming and try to give solutions to arisen problems. I’ll also present some rules that are needed for solving equations, describe them and give some examples of applying them.
Arturas Katutis
Kaunas University of Technology, Lithuania
One of the main features of good and acceptable for user software is fast execution of operations. The majority of software has a great functionality; however the speed of operations does not surprise users - operations are executed too long. It happens when developing software we give more attention to functionality and / or user-friendliness of user interface, but less attention to optimization of operations.
The article overviews several ways of Microsoft Visual C# .NET code optimization. Analyzing and comparing not optimized with optimized operations also giving operations’ executions’ times and gauges of optimization in percent. It is hard to make software run fast and use resources efficiently without understanding how resources are handled by the framework. So, every step in creating software has to be considered carefully. And after applying code optimizations that are analyzed in this article can increase operations speed more then twice thus making software run faster.
Irina Lovcova
Riga Technical University, Dept. of Modelling and Simulation, Latvia
During the winter school I would like to present a poster that reflects the results of my Master’s thesis. The study conducted in my thesis examines the behaviour of genetic algorithm in the task of multimodal function optimisation (a function with several local and global extrema). The major part of the study was devoted to the comparison of three crossover operators: combination, square and diagonal crossover (the first is one of the more popular operators, while the latter two are its modifications). Two multimodal functions have been used to compare performance of the operators – the so-called “Griewank” and “Binary f6” functions, each with its own unique properties.
The results of the experiments show that different crossover operators perform differently. Some of the advantages of genetic algorithms have been revealed as well. The considered functions are rather complicated (in the sense that it is not a trivial task to find their optima), so the results present an insight into the capabilities of different crossover operators, which reflect different heuristic approaches.
Sigita Misiņa
Riga Technical University, Faculty of CS and IT, Latvia
This paper describes and analyses on-line learning algorithms, their structure, application and classification. In incremental learning, the class is not assumed to be constant, the algorithm learns by incremental processing the examples one by one. This kind of learning has some advantages and disadvantages. The disadvantage is, after a certain time examples classified before may not be correctly classified. The advantage is, in case of knowledge aging, the incremental learning algorithm will pay more attention to new context examples and class description changes.
In comparing algorithms FLORA2, FLORA3 and FLORA4, one can say that FLORA2 is the algorithm, which stores in memory all possible context descriptions, dividing them into three description sets and allowing the algorithm to learn in incremental way, that is, start with empty description set. The FLORA2 algorithm can automatically detect and change the window size flexibly. But algorithm FLORA3 is better in case of a context drift - it does not reconsider the old concepts after each new training instance but only when the window adjustment heuristic WAH suspects a concept drift. The FLORA4 algorithm is effective against noise in data and is quick in the recognition of and adaptive to the target class drift. It can be concluded that recent algorithm FLORA4 is the most effective, but in domains where no noisy data are expected, algorithm FLORA3 can be used too. If no considerable concept drift is expected, algorithm FLORA2 can also be used.
FLORA2 incremental learning process is showed by the example of logical function approximation.
Aleksandrs Vališevskis
Technical University of Riga, Latvia
During this winter school I would like to present a poster that shows several interesting results obtained by Kosko, which I have discovered when I was studying his definition of fuzzy entropy. They concern such things as paradoxes in two-valued logic and set theory, randomness, dice, God and similar topics, which were raised last year by professor Chaitin. Thus, I think that it will be interesting for other participants to see such a sequel of the year-old discussion. And for me personally it will be interesting to get feedback about the definition of entropy presented by Kosko, as it is very possible that I will use its idea in my Thesis. Moreover, I see a broad ground for discussion in this topic.
The basic idea adopted by Kosko is to represent fuzzy sets as points in the unit hypercube. Location of points in the hypercube depends on the fuzziness of the corresponding set (e.g., a nonfuzzy set is a vertex of the cube and a fuzzy set is a point in the cube). One particular cube point that I would like to consider in the poster is the midpoint of the hypercube. Nothing is certain in the midpoint and, according to Kosko, it is where all the so called “midpoint paradoxes” are (such as Russell’s set of all sets or the liar from Crete who said that all Cretans are liars). Nothing is distinguishable in the midpoint and Kosko denotes it as the “black hole of set theory”. Moreover, it is shown how these paradoxes can be modelled using fuzzy arithmetic.
At a particular point in his book Kosko compares randomness and fuzziness and comes to the conclusion that fuzziness does not require that “God play dice”. If space limits allow it, I will include all the interesting ideas described by Kosko.
http://www.cs.ioc.ee/yik/schools/win2004/
Modified Thursday, Jan 01, 1970 at 3:00 MSK+0300 by monika(at)cs.ioc.ee