Theoretical Computer Science Forum

Spring 2004

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

• 24.2.2004 Prof. Clement Lam (Department of Computer Science, Concordia University, Montreal): After n Years of Computing, Is the Answer Correct?

  Abstract: The area of enumerative search has an occupational hazard. After a long computation and finding an answer, is the answer correct? I will talk about some consistency checking techniques which can provide confidence that the computed answer is most-likely to be correct.

• 27.2.2004 The public defence of a doctoral thesis (at 12noon, CS building, lecture hall T2)
  Harri Haanpää: Constructing Certain Combinatorial Objects by Computational Methods [Link]

• 5.3.2004 Mikko Särelä: Measuring the Effects of Mobility on Reactive Ad Hoc Routing

  Abstract: Ad hoc networks can operate without need for fixed infrastructure and can survive rapid changes in the network topology. Ad hoc network can be considered a graph in which the set of edges varies in time. The main method for testing ad hoc networks is simulation. Choosing mobility model, which describes the movements of the nodes in statistical terms, is one of the most important choices of simulation parameters. This is because movements of nodes determine when any pair of nodes has a direct communication link. These links are used for creating routes between nodes that are not adjacent. When a link that is part of a route goes down, the route has to be renewed, causing delays, packet loss and routing protocol overhead in the network. This thesis proposes that the route life time presents an important measure for the effects of mobility for reactive ad hoc routing. A method for estimating the route life time distribution for shortest routes between random nodes is also proposed.

• 19.3.2004 Misa Keinänen: Solving Conjunctive/Disjunctive Boolean Equation Systems with Alternating Fixed Points

  Abstract: I will talk about resolution techniques for alternating Boolean equation systems which are in conjunctive/disjunctive forms. The techniques can be used to solve various verification problems on finite-state concurrent systems, by encoding the problems as equation systems and determining their local solutions.

• 4.6.2004 Toni Jussila: BMC via Dynamic Atomicity Analysis

  Abstract: This talk presents a non-standard execution model and its propositional encoding for effective bounded model checking of reachability properties. The execution model allows several visible actions from a single system component to be merged dynamically to an atomic block. Thus the bound needed to detect a violation of a property can be reduced. An implementation and results from several test cases are provided.

• 11.6.2004 Heikki Tauriainen: Nested Emptiness Search for Generalized Büchi Automata

  Abstract: We generalize the classic explicit state emptiness checking algorithm for Büchi word automata (the "nested depth-first search") into Büchi automata with multiple acceptance conditions. Bypassing an explicit acceptance condition reduction improves the algorithm's worst case memory requirements. The generalized algorithm is compatible with well-known probabilistic explicit state model checking techniques and model checking under fairness constraints.

• 18.6.2004 Timo Latvala: LTL Model Checking for Modular Petri Nets

  Abstract: We consider the problem of model checking modular Petri nets for the linear time logic LTL-X. An algorithm is presented which can use the synchronisation graph from modular analysis as presented by Christensen and Petrucci and perform LTL-X model checking. We have implemented our method in the reachability analyser Maria and performed experiments. As is the case for modular analysis in general, in some cases the gains can be considerable while in other cases the gain is negligible.