Doktorandseminarier vårterminen 2006 / PhD Student Seminars Spring Term 2006

Måndag 6 februari, kl 13.15-14.00, CID-torget, Lindstedtsvägen 5, plan 6 (OBS! lokalen): Bulgarisk patiens och andra roliga dynamiska system (Henrik Eriksson, Teorigruppen, KTH CSC)

Game of Life, den mest kända cellautomaten, är oavgörbar, men vi ska se på några liknande system som är avgörbara, om än med viss ansträngning. Det allra enklaste, bulgarisk patiens, använder korthögar och ett drag består av att man tar ett kort från varje hög och bildar en ny hög. Exempel:

6+3+1 » 5+2+3 » 4+1+2+3 » 3+1+2+4 » 2+1+3+4 » 1+2+3+4 » 1+2+3+4

och man har nått en fixpunkt. Gör man alltid det? Och vad har det här att göra med företagskonsulter och trummisar?

(Seminariet baserat på en artikel för Am.Math.Monthly och en för J.Comb.Th.A.)

Måndag 20 februari, kl 13.15, rum 1537: A Tree-Based Gibbs Motif Sampler for Unaligned Orthologous Upstream Sequences (Jens Lagergren, Teorigruppen, KTH CSC och Stockholm Bioinformatics Center)

Most studies of gene evolution focus on the coding part of genes rather than their regulatory regions. However, comparative genomics provides one of the most powerful approaches to identification of transcription factor binding sites; consequently, knowledge of how binding sites evolve facilitates construction of better identification algorithms.

In phylogenetic foot-printing, putative regulatory elements are found in upstream regions of orthologous genes by searching for common motifs. Gibbs sampling is one successful method for finding common motifs. Since the orthologous sequences are related by a tree and differences between motif instances, in different upstream regions, are caused by mutational events along its edges, taking advantage of the tree in the motif search is an obvious as well as appealing idea.

We describe the Tree-Based Gibbs motif sampler, which is a Gibbs sampler based on a general tree which takes unaligned sequences as input. An implementation of the tree based sampler will be described as well as in silico experimental results that show clear advantages of the method.

Måndag 6 mars, kl 13.15, rum 1537: Temporal Logic, Process Algebra and State Space Representation for Verification of Open Systems (Irem Aktug, Teorigruppen, KTH CSC)

This seminar will consist of two parts (probably with a break in between).

1) Introduction to Temporal Logic and Process Algebra (ca. 30 min.)

I will give a short introduction to temporal logic, especially modal mu-calculus. I will try to illustrate through examples how this logic can be used to specify properties of processes.This part of the talk aims to give background information which will make the second part of the talk easier to understand.

2) State Space Representation for Verification of Open Systems (ca. 40 min.)

When designing an open system, there might be no implementation available for certain components at verification time. For such systems, verification has to be based on assumptions on the underspecified components. When component assumptions are expressed in Hennessy-Milner logic (HML), the state space of open systems can be naturally represented with modal transition systems (MTS), a graphical specification language equiexpressive with HML. Having an explicit state space representation supports state space exploration based verification techniques and enables proof reuse and facilitates visualization for the user guiding the verification process in interactive verification. As an intuitive representation of system behavior, it aids debugging when proof generation fails in automatic verification.

We extend MTSs to represent the state space of open systems where component assumptions are specified in modal mu-calculus. We present a two-phase construction from process algebraic open system descriptions to such state space representations. The first phase deals with component assumptions, and is essentially a maximal model construction for the modal mu-calculus. In the second phase, the models obtained are combined according to the structure of the open system to form the complete state space. The construction is sound and complete for systems with a single unknown component and sound for those without dynamic process creation. For establishing open system properties based on the representation, we present a proof system which is sound and complete for prime formulae.

Måndag 27 mars, kl 13.15, rum 1537: Generic Attacks on Stream Ciphers (John Mattsson) [slides ]

Today when so much information is transmitted over open channels like the Internet and wireless channels (GSM, UMTS, Wi-Fi, WiMAX etc.), cryptography is more important than ever. The benefits of stream ciphers compared to block ciphers (like AES) are that they are generally much faster, have low hardware complexity, and no or limited error propagation.

I will first give a short introduction to stream ciphers and how attacks are classified depending on the information avalable to the attacker and the aim of the attack. I will then present the most important generic attacks including distinguishing attacks, time memory tradeoffs, correlation attacks, algebraic attacks, and side channel attacks.

The talk will be given in Swedish or English depending on the participants, and is intended to last for about one hour.

Måndag 3 april, kl 13.15-15.00, rum 1537: Short Proofs Are Narrow (Well, Sort of), But Are They Tight? (Jakob Nordström, Teorigruppen, KTH CSC) [slides ]

A propositional proof system is an algorithm P(F, π) that runs in time polynomial in the sizes |F| and |π| of the inputs and has the property that

• for every valid formula, or tautology, F there is a proof π such that P(F, π) = 1,
• for every non-tautological formula F it holds that P(F, π) = 0 for all purported proofs π.

The study of propositional proof complexity is important both from a theoretical and a practical point of view. On the one hand, it is closely related to central questions in computational complexity, in view of the fact that separating NP and co-NP (which would imply P ≠ NP) is equivalent to proving that there is no propositional proof systems where all tautologies F have proofs π of size at most polynomial in the size of F. On the other hand, designing efficient algorithms for proving tautologies, or equivalently refuting unsatisfiable formulas, is a very important problem in applied research and in industry, e.g. in the context of formal methods.

In this talk, we will focus on resolution, which proves tautologies by showing that their negations, expressed as CNF formulas, are unsatisfiable. It is perhaps the single most studied propositional proof system, and many real-world automated theorem provers are based on it.

In 1999, Ben-Sasson and Wigderson proved a strong (and perhaps somewhat surprising) correlation between the size and the width of proofs, where the width is the size of the largest disjunction in the proof. Another well-studied measure in resolution is space, which intuitively is the maximal number of clauses one needs to keep in memory while verifying the proof. Interestingly, all lower bounds proven so far on space in resolution has turned out to match exactly lower bounds on width. In 2003, Atserias and Dalmau showed the (arguably even more surprising) result that this is true in general.

We will first give an introduction to proof complexity in general and resolution in particular. Then we will provide a fairly detailed overview of the above-mentioned results. Finally, if time permits we will also discuss some open questions (one of which we managed to solve recently and which will be the subject of a separate talk in the TCS seminar series on May 15th [later moved to June 8th]).

The talk will be given in Swedish or English depending on the participants, and is intended to last for 2x45 minutes.

Måndag 24 april, kl 13.15 - ca 14.15, rum 1537: Ultimatumspelet i laboratorium (Kimmo Eriksson, Institutionen för matematik och fysik, Mälardalens högskola)

Det så kallade "ultimatumspelet" för två personer går till så att en person föreslår en uppdelning av en pott och den andra personen får acceptera eller förkasta förslaget. Om hon förkastar det går potten till spillo.

Ultimatumspelet är den mest kända spelsituation där spelteoretiska förutsägelser om hur människor bör bete sig inte alls överenstämmer med faktiskt beteende i experiment. Hundratals experimentella studier av ultimatumspelet har bekräftat detta, och genom att studera olika påhittiga varianter av spelet har man försökt reda ut vad som pågår, bl.a. i syfte att kunna formulera en bättre matematisk modell.

I mitt spellaboratorium på Mälardalens högskola har examensarbetaren Micael Ehn och jag nyligen utfört ännu en studie med ännu en variant av ultimatumspelet. Jag kommer att berätta om ultimatumspel och spelteoretiska modeller i allmänhet, och om vår studie i synnerhet.

Onsdag 10 maj, kl 14.15 (OBS! dagen och tiden), rum 1537: Dags att visa L ≠ P? (Jakob Nordström, Teorigruppen, KTH CSC)

Jag tänkte hålla ett väldigt informellt seminarium om ett roligt föredrag som hölls på Dagstuhl-seminariet "Complexity of Boolean Functions" i mars i år. Föredraget är baserat på en ECCC-artikel av Gal, Koucky och McKenzie, där den bakomliggande motivationen är att försöka visa LOGSPACE ≠ PTIME.

Som en bonuseffekt formuleras detta i termer av ett mycket lättbegripligt och roligt problem, som man enkelt ritar upp på servetten för sitt bordssällskap om det skulle saknas samtalsämnen nästa gång man är på restaurang. Ett garanterat partytrick!

Det är fortfarande ganska långt kvar (minst sagt) till en separation av LOGSPACE och PTIME, men det artikelförfattarna har gjort är att visa vissa starka undre gränser som ger intuition för vad det är man skulle behöva göra för att visa LOGSPACE ≠ PTIME. (De undre gränserna ger mer eller mindre intution beroende på hur starka man tycker att begränsningarna i deras artikel är).

Jag tänkte försöka ge ett referat av artikeln på kanske 30-45 minuter. Sedan hoppas jag på en diskussion om detta resultat är något att vara entusiastisk över eller inte, och om det finns några roliga problem här som man skulle kunna försöka angripa.

Måndag 29 maj, kl 13.15-15.00, rum 1537: The π-Calculus and Nominal Logic (Joachim Parrow och Jesper Bengtson, Institutionen för informationsteknologi, Uppsala universitet) [slides ]

The π-calculus is a basic formalism for description of parallel processes that exchange data and where connectivity between processes can change during execution.

In the first part of the talk we give a brief overview of the calculus. In the second part we we show how it can be formalised using nominal logic (by Pitts et al.) and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics and to use them to prove fundamental theorems, such as bisimulation equivalence being a congruence.

The significant gain in our formulation is that agents are identified up to α-equivalence, and thus no arguments need ever be conducted about their bound names. This is normal strategy for manual proofs about the π-calculus, but that kind of hand waving has previously been impossible to incorporate smoothly in an automated proof assistant.