|
Theoretical Computer Science Forum
Spring 2006
This is a forum for talks on theoretical computer science organized by the
TCS Laboratory at HUT. We meet usually on Fridays at 2 p.m. in room
B353 in the Computer Science building. Any exceptions to this rule
are reported below.
For further information, please contact
Tomi Janhunen.
Program
-
24.5.2006
Emilia Oikarinen
(TCS/TKK) :
Modular Equivalence for Normal Logic Programs
Note: the talk is given Wednesday afternoon at 14:15 in room B353
Abstract:
A Gaifman-Shapiro-style architecture of program modules is
introduced in the case of normal logic programs under stable model
semantics. The composition of program modules is suitably limited by
module conditions which ensure the compatibility of the module system
with stable models. The resulting module theorem properly strengthens
Lifschitz and Turner's splitting set theorem for normal logic
programs. Consequently, the respective notion of equivalence between
modules, i.e. modular equivalence, proves to be a congruence relation.
Moreover, it is shown how our translation-based verification method is
accommodated to the case of modular equivalence; and how the
verification of weak/visible equivalence can be optimized as a
sequence of module-level tests.
-
24.3.2006 Johan Wallén
(TCS/TKK) :
Improved Linear Distinguishers for SNOW 2.0
Abstract:
The stream cipher SNOW 2.0 was proposed by Ekdahl and Johansson in
2002 as a strengthened version of SNOW 1.0. Currently SNOW 2.0 is
considered as one of the most efficient stream ciphers and it is used
for benchmarking the performance and security of stream ciphers. SNOW
2.0 was also taken as a starting point for the ETSI project on a
design of a new UMTS encryption algorithm. Distinguishing attacks
using linear cryptanalysis (linear masking) were previously applied to
SNOW 2.0 by Watanabe et al. [1]. An efficient distinguisher can
be used to detect statistical bias in the key stream, and in some
cases, also derive the key or initial state of the key stream
generator. We present how the estimates of the biases of the linear
approximation of the FSM of SNOW 2.0 can be significantly improved by
using and extending previous results about linear approximation of
modular addition from [2]. Thanks to improved bias
estimates we find a new linear distinguisher with bias
2-86.9, which is significantly stronger than the
previously found one by Watanabe et al., with bias
2-107.3, and which enables, using workload
2174, to distinguish the output keystream of SNOW 2.0 of
length 2174 words from a truly random sequence. This
attack is currently the best known attack on SNOW 2.0 as it also
superceeds the recent distinguishing attack by Maximov and Johansson
[3] of complexity 2202.
- D. Watanabe, A. Biryukov, and C. De Cannière:
Distiguishing Attack of SNOW 2.0 with Linear Masking Method.
In Proc. SAC 2003, pp. 222-233.
- J. Wallén:
Linear Approximations of Addition Modulo 2n.
In Proc. FSE 2003, pp. 261-273.
- A. Maximov and T. Johansson:
Fast Computation of Large Distributions and
Its Cryptographic Applications.
In Proc. Asiacrypt 2005, pp. 313-332.
-
17.3.2006 Keijo Heljanko
(TCS/TKK) :
On checking distributed implementability
Abstract:
We consider the distributed implementability problem given as: Given a
labeled transition system TS together with a distribution of its
actions over a set of processes, does there exist a distributed system
such that its global transitions system is equivalent to TS? We
consider the distributed systems modeled as synchronous products of
transitions systems as well as asynchronous automata (a subclass of
labelled 1-safe Petri nets). In this work we provide complexity
bounds for the above problem with three interpretations for equivalent
above: as transition system isomorphism, as language equivalence, and
as bisimilarity. We also discuss an SMODELS -based
implementation of a distributed implementability check for the
isomorhism case.
-
3.3.2006
Petteri Kaski
(HIIT/BRU, Helsinki) :
On Combinatorial Landscapes Defined by Linear Equations Modulo 2
Abstract: Attempting to understand empirically observed
exponential scaling of local search algorithms on a family of
benchmark instances of the propositional satisfiability (SAT) problem
[1], I have been interested in the properties of combinatorial
landscapes [2] induced on the Boolean N-cube by a system of linear
equations modulo 2 over N variables, specifically in the case when the
system is selected uniformly at random subject to the following three
restrictions: (i) the system has at least one solution, (ii) every
variable occurs in 3 equations, (iii) every equation has 3 variables. I
will talk about work in progress to analyze landscapes of this type.
Properties studied include existence and number of local minima,
boundary expansion [3,4], the worst-case height of the potential
barrier surrounding a local minimum, and the expected number of
solutions.
- H. Haanpää, M. Järvisalo, P. Kaski, and
I. Niemelä:
Hard satisfiable clause sets for benchmarking equivalence
reasoning techniques. Journal on Satisfiability, Boolean
Modeling and Computation, to appear.
- C. Reidys, P. Stadler:
Combinatorial landscapes.
SIAM Review, 44 (2002) 3-54.
- E. Ben-Sasson, A. Wigderson:
Short proofs are narrow - resolution made simple.
Journal of the ACM, 48 (2001) 149-169.
- M. Alekhnovich, E. Hirsch, and D. Itsykson:
Exponential lower bounds for the running time of DPLL
algorithms on satisfiable formulas.
In Proc. ICALP 2004, pp. 84-96.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 04 August 2006.
Tomi Janhunen
|