Theoretical Computer Science Forum

Spring 2007

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.

The talks given at TCS Forum aim at presenting recent advances in theoretical computer science that can be expected to attract interested audience also beyond the research groups of the laboratory. The Friday afternoon time slot is occasionally used also for presentations about ongoing work and results from student's projects at what is called as TCS Lounge. The main goal of the TSC Lounge is to improve transfer of knowledge and ideas between the different research groups of the TCS laboratory.

For further information, please contact Kaisa Nyberg.

Program

Past presentations

• 4.5.2007 FORUM Tomi Janhunen , D.Sc.(Tech.), Docent, TCS/TKK:

  Modularity Aspects of Disjunctive Stable Models

  Abstract: Practically all programming languages used in software engineering allow to split a program into several modules. For fully declarative and nonmonotonic logic programming languages, however, the modular structure of programs is hard to realise, since the output of an entire program cannot in general be composed from the output of its component programs in a direct manner. In this paper, we consider these aspects for the stable-model semantics of disjunctive logic programs (DLPs). We define the notion of a DLP-function, where a well-defined input/output interface is provided, and establish a novel module theorem enabling a suitable compositional semantics for modules. The module theorem extends the well-known splitting-set theorem and allows also a generalisation of a shifting technique for splitting shared disjunctive rules among components. This is joint work with Emilia Oikarinen, Hans Tompits and Stefan Woltran.

• 2.3.2007 FORUM Timo Asikainen, Researcher, TKK, SoberIT :

  A Short Introduction to Software Variability Management

  Abstract: Variability is the ability of a system to be efficiently extended, changed, customised or configured for use in a particular context. There is an ever-growing demand for variability of software. Software product families have become an important means for implementing variability. A software product family may contain very large numbers of individual products. Hence, efficient methods for representing the variability and reasoning about it are needed. In this talk, we provide an overview of the concepts used for representing software variability and how these concepts can be provided with rigorous semantics. In addition, we discuss the tool support that can be provided for the configuration task, that is, resolving the variability in a product family to come up with an individual product matching a given set of requirements at hand. Finally, we discuss challenges related to representing and reasoning about variability.

• 23.2.2007 LOUNGE Tekn. yo Sami Kauppinen, VTT :

  Luottamuksen arviointi komponenttipohjaisessa ohjelmistoarkkitehtuurissa
  Diplomityöesitelmä

  Tiivistelmä: Luottamusta sosiaalisena käsitteenä on formalisoitu eri tavoin ja sovellettu myös dynaamisiin, hajautettuihin tietojärjestelmiin. Tavoitteena tällöin on parantaa järjestelmän hyödyllisyyttä sallimalla luotettujen toimijoiden tai järjestelmän osien välinen toiminta ja sulkemalla pois tai rajoittamalla epäluotettavien osien toimintaa.

  Esitelmässä tarkastellaan lähemmin Trust4All ITEA-projektissa hajautetussa käyttöympäristössä toimivan komponenttipohjaisen ohjelmistoarkkitehtuurin tarpeisiin määriteltyä luottamusmallia. Luottamusmalli määrittelee luottamus-käsitteen, luottamuksen kehittymiseen vaikuttavat tekijät sekä menettelytavat, joilla arviota kohteen luotettavuudesta muutetaan uuden todistusaineiston perusteella. Luottamus esitetään numeerisena luottamusarvona, jota käytetään hyväksi tehtäessä tilannesidonnaisia luottamuspäätöksiä.

  Malli sisältää useita parametreja, joiden vaikutusta luottamuksen kehittymiseen tutkitaan simulaatioiden avulla. Simulaation tulosten pohjalta voidaan tehdä päätelmiä parametrien soveltuvuudesta erilaisiin käyttötilanteisiin.

• 16.2.2007 FORUM Doctor Viktor Schuppan, Munich, Germany :

  Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties

  Abstract: Temporal logic is widely used for specifying hardware and software systems. Typically two types of properties are distinguished, safety and liveness properties. While safety can easily be checked by reachability analysis, and many efficient checkers for safety properties exist, more sophisticated algorithms have always been considered to be necessary for checking liveness. We describe an efficient translation of liveness checking problems into safety checking problems. The method applies to all $\omega$-regular properties and extends to a number of infinite state systems, namely, regular model checking, pushdown systems, and timed automata.

  Counterexamples are a salient feature of model checking that help developers to understand the problem in a faulty design. Short counterexamples are typically easier to understand. As safety is amenable to BFS, the above translation gives a practical method to find shortest fair lasso-shaped paths. Whether a shortest fair lasso in the product of a model and an automaton representing the specification indeed represents a shortest counterexample in the model depends on the translation of the specification into a Büchi automaton. We discuss requirements on Büchi automata that ensure that this is the case.

• 9.2.2007 FORUM Professor Erik Aurell , Division of Theoretical Biological Physics, Royal Institute of Technology (KTH), Stockholm :

  Some numerical experiments with local heuristics for 3SAT

  Abstract: We study a putative clustering transition in random 3SAT problem by solving one instance with a stochastic local search algorithm. For low alpha, the inter-solution distances are smoothly distributed around some average, which decreases with alpha. At higher values of alpha however, some inter-solution distances are much smaller than the rest, consistent with a "clustering transition", while at even higher alpha all found solutions are found at very small distance from one another. Various estimates of the tresholds and from simulations, and whether the these heuristics fail for energentic or entropic reasons will be given.

• 12.1.2007 FORUM Toimistopäällikkö, TkT, Dos. Juhani Hyvärinen, Säteilyturvakeskus (STUK) :

  Ydinvoimalaitosten automaatio ja sen viranomaisvalvonta

  Tiivistelmä: Ydinvoimalaitoksissa käytettävä automaatiotekniikka, tyypillisten järjestelmien pääpiirteet, automaatiota koskevat turvallisuusvaatimukset ja niiden täyttymisen arvioiminen.

  Esitelmän kalvot: [pdf]