Theoretical Computer Science Forum

Spring 2005

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.

For further information, please contact Ilkka Niemelä.

Program

• 14.1.2005 Ammar Alkassar (University of Saarland, Germany): Secure Object Identification - Or: How To Solve The Chess-Grandmaster-Problem

  Abstract: Many applications of cryptographic identification protocols are vulnerable against physical adversaries who perform real time attacks. For instance, when identifying a physical object like a person requesting access to a restricted area, common identification schemes can be bypassed by faithfully relaying all messages between the communicating participants. This attack is known as mafia fraud. In my talk I will give an overview over different approaches to cope with that fraud. One approach, the Probabilistic Channel Hopping system, solves this problem by hiding the conversation channel between the participants. The security of this approach is based on the assumption that an adversary cannot efficiently relay all possible communication channels of the PCH system in parallel. Finally, I will present a concrete, zero-knowledge based identification scheme and give a sketch of the proof idea.

• 3.3.2005 Prof. Michael Kaminski (Technion, Computer Science Department, Israel): Invariance under Stuttering in a Temporal Logic of Actions
  Note: the talk is at 14:15 in room A328

  Abstract: We show that some simple and useful stutter-invariant properties definable in the language of Lamport's Simple Temporal Logic of Actions (STLA) are not definable in STLA and present a natural extension of STLA that allows one to express all stutter-invariant properties definable in the language of STLA. The example of a stutter-invariant property not expressible in STLA is based on a version of Ehrenfeught-Fraisse games on temporal interpretations.

• 15.3.2005 Prof. Gerhard Brewka (Computer Science Institute, University of Leipzig): Component Systems: Bridging the Gap Between CP-Nets and Answer Set Optimization
  Note: the talk is at 9:15 in room A346

  Abstract: We introduce a flexible framework to specify problem solutions (outcomes) and preferences among them. The proposal combines ideas from answer-set programming (ASP), answer-set optimization (ASO) and CP-nets. The problem domain is structured into components. ASP techniques are used to specify values of components, as well as global (inter-component) constraints among these values. ASO methods are used to describe preferences among the values of a component, CP-net techniques to represent inter-component dependencies and corresponding preferences.
  (Joint work with I. Niemelä and M. Truszczynski)

• 16.3.2005 Prof. Torsten Schaub (Universität Potsdam, Institut für Informatik) Platypus: A Platform for Distributed Answer Set Solving
  Note: the talk is at 9:15 in room B353

  Abstract: We propose a model to manage the distributed computation of answer sets within a general framework, incorporating a variety of software and hardware architectures to allow its easy use with a diverse cadre of computational elements. Starting from a generic algorithmic scheme, we develop a platform for distributed answer set computation, describe its current state of implementation, and give some experimental results.
  (Joint work with Jean Gressmann, Tomi Janhunen, Robert E. Mercer, Richard Tichy, Sven Thiele.)

• 17.3.2005 Dipl.-Inf. Martin Gebser (Universität Potsdam, Institut für Informatik) Foundations of clause learning in ASP solving
  Note: the talk is at 9:15 in room B353

  Abstract: Implication/conflict graphs form the fundament for enhancing the Davis-Putnam procedure, dealing with propositional CNF formulas, by clause learning. Basic algorithms of ASP solvers smodels and nomore are very similar to the Davis-Putnam procedure. Nonetheless, there has almost no work been done on customizing clause learning for ASP solvers. This talk is dedicated to developing implication/conflict graphs of smodels and nomore in a systematic manner by characterizing inference rules in terms of clauses.

• 21.4.2005 Misa Keinänen: Solving Boolean Equation Systems
  Note: the talk is at 15:15 in room A106

  Abstract: Boolean equation systems are ordered sequences of Boolean equations decorated with fixpoint operators. Boolean equation systems provide a useful framework for computer aided verification because various specification and verification problems can be encoded as the problem of solving such fixpoint equation systems. In this thesis, techniques for finding solutions to Boolean equation systems are studied, and new methods for solving such systems are devised. An approach to solve a general form Boolean equation system, which simplifies the process of finding the solution by dividing the system into more simple subsystems and solving these by optimized procedures, is introduced and analyzed. New solution algorithms for disjunctive and conjunctive classes of Boolean equation systems are presented, together with an implementation and experimental evaluation of a solver for these classes. A novel translation of the problem of solving a general form Boolean equation system into the problem of finding a stable model of a logic program is given. The translation allows to use an implementation of an answer set programming framework, the Smodels system, to solve Boolean equation systems. Experimental tests have been performed using the presented approach, and these experiments indicate the effectiveness of using answer set programming in this problem domain.

• 22.4.2005 Dr. Supriya Krishnamurthy (Swedish Institute of Computer Science, Stockholm): The Statistical Mechanics of Dynamic Peer-to-Peer Networks

  Abstract: In Peer-to-Peer (P2P) networks, every member of the network has equal capability and responsibility in contrast to traditional client/server network architectures. These networks have been the subject of much current research, for their intrinsic interest as well as their potential for being deployed in applications. The membership of these networks is however dynamic, so that both the network as well as the function it serves has to be robust against constant change. Earlier studies of these systems have either depended on simulations as the primary investigation tool, or on establishing theoretical bounds. In this talk, we present a different approach to looking at these networks using a master-equation-based approach, used traditionally in non-equilibrium statistical mechanics to describe steady-state or transient phenomena. Simulations are used to verify all theoretical predictions. We demonstrate the application of our methodology to Chord, a recently introduced and very well-studied P2P network.

• 27.5.2005 Prof. Pekka Orponen: Focused Local Search for Random 3-Satisfiability

  Abstract: An important heuristic in local search algorithms for Satisfiability is focusing, i.e. restricting the selection of flipped variables to those appearing in presently unsatisfied clauses. We consider the behaviour on large randomly generated 3-SAT instances of three focused solution methods: the well-known WalkSAT algorithm, the straightforward algorithm obtained by imposing a focusing constraint on basic Metropolis dynamics, and a less-known but very well performing method, the Focused Record-to-Record Travel algorithm. We observe that both WalkSAT and the Focused Metropolis Search method are quite sensitive to the proper choice of their "noise" and "temperature" parameters, and attempt to estimate ideal values for these, such that the algorithms exhibit generically linear solution times as close to the satisfiability transition threshold alpha_c = 4.267 as possible. With an appropriate choice of parameters, the linear time regime of both algorithms seems to extend well into clauses-to-variables ratios alpha > 4.2, which is much further than has generally been assumed in the literature.
  (Joint work with Sakari Seitz and Mikko Alava.)

• 3.6.2005 Dr. Tommi Junttila: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic

  Abstract: The problem of deciding the satisfiability of a quantifier-free formula with respect to a background theory, also known as Satisfiability Modulo Theories (SMT), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of real-world problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems). This talk presents a new decision procedure for the satisfiability of Linear Arithmetic Logic (LAL), i.e. boolean combinations of propositional variables and linear constraints over numerical variables. The approach is based on the well known integration of a propositional SAT procedure with theory deciders, enhanced in the following ways. First, the procedure relies on an incremental solver for linear arithmetic, that is able to exploit the fact that it is repeatedly called to analyze sequences of increasingly large sets of constraints. Reasoning in the theory of LA interacts with the boolean top level by means of a stack-based interface, that enables the top level to add constraints, set points of backtracking, and backjump, without restarting the procedure from scratch at every call. Sets of inconsistent constraints are found and used to drive backjumping and learning at the boolean level, and theory atoms that are consequences of the current partial assignment are inferred. Second, the solver is layered: a satisfying assignment is constructed by reasoning at different levels of abstractions (logic of equality, real values, and integer solutions). Cheaper, more abstract solvers are called first, and unsatisfiability at higher levels is used to prune the search. In addition, theory reasoning is partitioned in different clusters, and tightly integrated with boolean reasoning. The effectiveness of the approach is demonstrated by means of a thorough experimental evaluation: our approach is competitive with and often superior to several state-of-the-art decision procedures.

  The presentation is based on the TACAS 2005 article "An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic" co-authored with Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Peter van Rossum, Stephan Schulz, and Roberto Sebastiani.

• 10.6.2005 Dr. Keijo Heljanko: Incremental and Complete Bounded Model Checking for Full PLTL

  Abstract: Bounded model checking is an efficient method for finding bugs in system designs. The major drawback of the basic method is that it cannot prove properties, only disprove them. Recently, some progress has been made towards proving properties of LTL using bounded model checking. We present an incremental and complete bounded model checking method for the full linear temporal logic with past (PLTL). Compared to previous works, our method both improves and extends current results in many ways: (i) our encoding is incremental, resulting in improvements in performance, (ii) we can prove non-existence of a counterexample at shallower depths in many cases, and (iii) we support full PLTL. We have implemented our method in the NuSMV2 model checker and report encouraging experimental results.
  (Joint work with Timo Latvala and Tommi Junttila.)