|
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.
- 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.
- 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.
- 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ä
|