TCS / Current / Theoretical Computer Science Forum / Autumn 2003
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Theoretical Computer Science Forum

Autumn 2003

This is a forum for talks on theoretical computer science organized by the TCS Laboratory at HUT (previously known as the Formal Methods Forum). 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

  • 13.8.2003 Emilia Oikarinen: Testing the Equivalence of Disjunctive Logic Programs

    Note: The talk is held at 10.15 in the TML seminar room TTA328.

    Abstract: To solve a problem in answer set programming (ASP), one needs to construct a logic program so that its answer sets correspond to the solutions of the problem at hand and compute the answer sets of the program using a special purpose search engine. Due to the declarative nature of ASP, it is an appealing approach for solving a variety of problems. There are, however, some difficulties regarding the development of programs using the paradigm. The encodings for a particular problem are by no means unique. A programmer often develops several versions of the program, e.g., when optimizing the execution time and 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. Thus in ASP this means that one has to check whether given two logic programs P and Q have the same answer sets, i.e., whether they are semantically equivalent. This corresponds to the weaker notion of equivalence addressed by Lifschitz et al. The equivalence of logic programs P and Q can naturally be verified using an explicit cross-check of all the answer sets of both programs. However, a translation-based method for testing the equivalence of weight constraint programs supported by the SMODELS system has already been developed and experiments show it to be efficient in many cases. In this work, we generalize this translation-based method to the disjunctive case and report our experiments with an implementation of the method, a translator called DLPEQ.

  • 15.8.2003 Matthias Fischmann (Humboldt University, Berlin): On Reputation in Peer-to-Peer Networks

    Note: The talk is held at 14.15 in the TML seminar room TA346.

    Abstract: In peer-to-peer networks or ad-hoc networks, there is no dedicated infrastructure of servers. Instead, the resources (bandwith and routing services, disk space, content, manual work, etc.) are provided by the client nodes that are closest to the request and can spare them. Consequently, every node faces the problem of feeding its request queue in an order that guarantees fair sharing of resources. Since nodes come and go, a dynamic and decentralized reputation system is necessary for this to work. In this talk, I sketch a few ideas on how to implement such a reputation system from three modules.

    1. In the certificate distribution module, statements of the form "A claims B has property C" are distributed such that every node can easily retrieve them with high probability.
    2. In the reputation level module, functions of the form "f(C, B_1, ..., B_k) = (n_1, ..., n_k)" are defined that assign priority values to each node in a list of requestors, given a set C of certificates. These functions are to be used by nodes to decide whom to provide resources to.
    3. In the third module, game structures are imposed on the network that are suitable for alleviate or overcome the prisoner's dilemma of common resources. If effective, this will improve the utility of the network independently from the controversial question of whether the tragedy of the commons holds in a given scenario or not.
    Module 3 in particular, but also modules 1 and 2 are work in progress, and I hope to be entertaining and inspiring rather than presenting a full solution to the problem.

  • 22.8.2003 Edith Elkind (Princeton University): Frugality in Path Auctions

    Note: The talk is held at 14.15 in the TML seminar room TA346.

    Abstract: We consider the problem of picking (buying) an inexpensive s-t path in a graph where edges are owned by independent (selfish) agents, and the cost of an edge is known to its owner only. We focus on minimizing the buyer's total payments. First, we show that any mechanism with (weakly) dominant strategies (or, equivalently, any truthful mechansim) for the agents can force the buyer to make very large payments. Namely, for every such mechanism, the buyer can be forced to pay c(P) + n/2*(c(Q)-c(P)), where c(P) is the cost of the shortest path, c(Q) is the cost of the second-shortest path, and n is the number of edges in P. This extends the previous work of Archer and Tardos, who showed a similar lower bound for a subclass of truthful mechanisms called min-function mechanisms. Our lower bounds have no such limitations on the mechanism. Motivated by this lower bound, we study a wider class of mechanisms for this problem, namely ones that admit Nash equilibrium strategies.In this class, we identify the optimal mechanism with regard to total payment. We then demonstrate a separation in terms of average overpayments between the classical VCG mechanism and the optimal mechanism showing that under various natural distributions of edge costs, the optimal mechanism pays at most logarithmic factor more than the actual cost, whereas VCG pays $\sqrt{n}$ times the actual cost. On the other hand, we also show that the optimal mechanism does incur at least a constant factor overpayment in natural distributions of edge costs. Since our mechanism is optimal, this gives a lower bound on all mechanisms with Nash equilibria.

    This is joint work with Amit Sahai and Ken Steiglitz.

  • 26.8.2003 Prof. Ken Satoh (National Institute of Informatics, Foundations of Information Research Division, Japan): Speculative Computation by Abduction

    Note: The talk is held at 14.15 in room T3.

    Abstract: In multi-agent system, we often face incompleteness of information due to communication failure or other agent's suspension of decisions. To solve the incompleteness, we propose a speculative computation using abduction in the context of multi-agent systems and a procedure in abductive logic programming. In this study, a master agent prepares a default value for a question in advance and it performs speculative computation using the default without waiting for a reply for the question. This computation is effective unless the contradictory reply with the default is returned. We also discuss extension of this mechanism to more general MAS settings.

    (Joint work with Katsumi Inoue, Koji Iwanuma, Chiaki Sakama, Keiji Yamamoto)

  • 12.9.2003 Dr. Evan Griffiths: Randomness and Kolmogorov Complexity

    Abstract: Kolmogorov Complexity for finite strings provides a precise formalisation of the idea of which strings are difficult to compress, and, by implication, which strings contain a lot of information, lack a simple structure, or can be considered random. This notion can be extended to infinite binary strings (which we identify with real numbers between 0 and 1) and forms the basis of one of three main approaches to defining algorithmic randomness for reals. We discuss this incompressibility approach to defining random reals, and the two other approaches: lack of predictability of the bits (martingales), and passing statistical tests (effective null sets). We will take a very brief tour through connections to information theory, the structure of the Turing degrees, graph theory, and other topics.

    This talk is intended to be mostly self-contained and accessible to a wide audience.

  • 14.10.2003 Dr. Laura Heinrich-Litan (Abteilung für Mathematische Optimierung, Technische Universität Braunschweig): Computing the Center of Area of a Convex Polygon

    Note: The talk is held at 14.15 in room TB353.

    Abstract: The center of area of a planar convex set C is the point p for which the minimum area cut off from C by any halfplane containing p is maximized. Properties of this point were studied already long ago in classical geometry, but it is quite nontrivial to really determine this point for a given convex set. We describe a simple randomized linear-time algorithm for computing the center of area of a convex n-gon.

    (Joint work with Peter Brass and Pat Morin.)

  • 24.10.2003 Docent Kimmo Varpaaniemi: Modelling and Analysing a PLC-Based Railway Traffic Control System

    Abstract: This talk is a ``review'' of a case study where a distributed PLC-based railway traffic control system was modelled and analysed.
    Keywords: programmable logic controllers, railway traffic control, formal methods, bounded model checking

  • 30.10.2003 Prof. E. Allen Emerson (University of Texas at Austin): The States of Verification

    Note: The talk is held at on Thursday at 14.15 in Hall TU1 (New TUAS building).

    Abstract: We discuss the state(s) of formal verification. We claim that state-based model-theoretic methods (e.g., model checking) are more effective than proof-based approaches, despite state explosion. We argue that abstractions for systems comprised of many similar subcomponents are especially important in limiting state explosion. Economies of scale ensure that such replicated systems are common in practice. (Replicated systems are also common in nature: the universe is understood to be comprised of many protons, neutrons, and electrons.) We describe efficient techniques for verifying various classes of replicated systems, including many classical synchronization problems, resource allocation problems, and cache coherence protocols. Some of the technical work described was done jointly with Vineet Kahlon and Kedar Namjoshi. Finally, we discuss how Moore's law can be expected to make model checking and related methods increasingly effective over time.

  • 31.10.2003 The public defence of a doctoral thesis (at 12noon, CS building, lecture hall T2)
    Tommi Junttila: On the Symmetry Reduction Method for Petri Nets and Similar Formalisms [Link]

  • 7.11.2003 at 13:00 Johan Wallén: On the Differential and Linear Properties of Addition

    Abstract: We present a detailed analysis of some of the fundamental differential and linear properties of addition modulo $2^n$: the differential probability $\xdp^+$ of addition modulo $2^n$ when differences are expressed using exclusive-or, the dual differential probability $\adp^\oplus$ of exclusive-or when differences are expressed using addition modulo $2^n$ and the correlation $\lca$ of $\bin$-linear approximations of addition modulo $2^n$. We show that $\xdp^+$, $\adp^\oplus$ and $\lca$ can be viewed as formal rational series with linear representations in base $8$. For $\xdp^+$ and $\lca$, the linear representations give $\Theta(\log n)$-time algorithms for computing $\xdp^+$ and $\lca$, explicit descriptions of all differentials or linear approximations with a given probability or correlation, and allows us to determine the distributions of $\xdp^+$ and $\lca$. For $\adp^\oplus$, the linear representation immediately gives a linear-time algorithm for computing $\adp^\oplus$. We analyse the asymptotic average behaviour of $\adp^\oplus$. In particular, we derive a Fourier representation of a first-order summation function obtained by interpreting differentials as integers in a natural way.

  • 7.11.2003 at 14:15 Heikki Tauriainen: On Translating Linear Temporal Logic into Alternating and Nondeterministic Automata

    Abstract: Automata theory provides valuable tools for designing and implementing decision procedures for temporal logics and their applications to automatic verification of systems against their logical specifications. Implementing these decision procedures by analyzing automata built from the systems and their specifications with translation procedures is nevertheless very challenging in practice due to the tendency of the automata to grow easily unmanageably large as the size of the systems or (especially) the logical specifications increases.

    This thesis develops the theory of translating future-time propositional linear temporal logic (LTL) into nondeterministic automata via linear alternating automata. Unlike nondeterministic automata, linear alternating automata are expressively equivalent to LTL and allow a conceptually simple translation of LTL specifications into automata using a set of rules for building automata incrementally from smaller components. The proposed unified generalized definition for both alternating and nondeterministic automata facilitates combining the rules with new minimization heuristics for alternating automata, based on the general theory of using language containment tests and structural analysis of automata for removing transitions. The generalized definition supports translation of linear alternating automata into nondeterministic automata within the best known limit for the worst case increase in the number of states of the resulting automata. The translation construction also reveals a simple syntactic subclass of LTL for which the exponential increase in the number of states can always be avoided. Additionally, the emptiness of generalized nondeterministic automata is shown to be decidable without degeneralization by using a new variant of the well-known nested depth-first search algorithm.

  • 14.11.2003 Tommi Syrjänen: Logic Programming with Cardinality Constraints

    Abstract: Cardinality constraints extend the standard syntax of logic programs by allowing us to state conditions that depend on the number of satisfied literals that belong to some set. Most of the previous work on cardinality constraints has concentrated on variable-free programs. The main topic of this presentation is to define the stable model semantics for cardinality constraint programs with variables. The basic idea is to define the semantics of a program with respect to an external data model. In addition, a syntactic subset, omega-restricted programs, of general cardinality constraint programs is defined. The omega-restricted programs have the property that they are decidable even when they contain function symbols. The class of omega-restricted programs with variables is shown to be 2-NEXP-complete.

  • 28.11.2003 The public defence of a doctoral thesis (at 12noon, Main building, lecture hall E)
    Marko Mäkelä: Efficient Computer-Aided Verification of Parallel and Distributed Software Systems [Link]

  • 9.12.2003 Dr. Thomas Linke (Universität Potsdam, Institut für Informatik): Suitable Graphs for Answer Set Programming

    Abstract: Often graphs are used to investigate properties of logic programs. In general, different graphs represent different kinds of information of the corresponding programs. Sometimes this information is not sufficient for solving a certain problem. In this talk I define graphs which are suitable for computing answer sets of different classes of logic programs. Intuitively, a graph associated to a logic program is suitable for answer set semantics if its structure is sufficient to compute the answer sets of the corresponding program. That is, algorithms that use suitable graphs do not have to consider the original logic program any longer.

  • 18.12.2003 Matti Järvisalo: Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits

    Abstract: The efficiency of a typical Davis-Putnam method based SAT checking system depends on
       (i) the applied search space pruning techniques; and
       (ii) the splitting rule (i.e., on which gates the explicit cut is applied).
    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 by applying 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.

    [Joint work with Tommi Junttila and Ilkka Niemelä. The related extended abstract "Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits" has been accepted for presentation at the 8th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, USA, January 4-6, 2004.]


[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 09 January 2005. Ilkka Niemelä