TCS / Current / Theoretical Computer Science Forum / Spring 2006
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

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.

    1. 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.
    2. J. Wallén: Linear Approximations of Addition Modulo 2n. In Proc. FSE 2003, pp. 261-273.
    3. 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.

    1. 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.
    2. C. Reidys, P. Stadler: Combinatorial landscapes. SIAM Review, 44 (2002) 3-54.
    3. E. Ben-Sasson, A. Wigderson: Short proofs are narrow - resolution made simple. Journal of the ACM, 48 (2001) 149-169.
    4. 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