TCS / Current / Formal Methods Forum / Spring 2000
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Formal Methods Forum

Spring 2000

This is a seminar on formal methods in computer science and engineering organized by the Laboratory for Theoretical Computer Science at HUT. 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

  • 4.2.2000 Keijo Heljanko: Complexity of Model Checking with Finite Complete Prefixes

    Abstract: McMillan has presented a verification method for finite-state Petri nets based on finite complete prefixes of net unfoldings. We discuss the computational complexity of some model checking questions when a finite complete prefix is used as a symbolic representation of the state space of a net system. Previously deadlock and reachability checking have been shown to be NP-complete in the size of the finite complete prefix. We show that there are prefixes for which model checking temporal formulas containing nested temporal modalities is PSPACE-complete in the size of the prefix. We also discuss the relevance of the result to the design of practical prefix-based verification algorithms.

  • 11.2.2000 Tommi Syrjänen: A Rule-Based Formal Model for Software Configuration

    Abstract: A rule-based approach for software configuration is presented. The configuration knowledge is stored in two distinct models: a configuration model that encodes rules to form valid configurations and a diagnostic model that can be used to find errors in user requirements. As a case study, a subset of the configuration problem of the Debian GNU/Linux system is formalized.

  • 18.2.2000 Tommi Junttila: Detecting and Exploiting Data Type Symmetries of Algebraic System Nets During Reachability Analysis

    Abstract: The symmetry reduction method is a technique designed to alleviate the combinatorial explosion problem occurring in state-space based verification. We present a way how state space symmetries of a high-level Petri net formalism, algebraic system nets, can be detected and exploited during the state-space analysis. The main idea is that permuting the domains of data types used in nets produces corresponding permutations to the state space level. As the main result a sufficient condition is defined for data type domain permutations ensuring that the produced state space permutations are actually automorphisms i.e. symmetries. Since verification of the condition is shown to be a co-NP-complete problem, an approximation rule for the condition is also given. Use of the developed theory is illustrated by defining the class of extended well-formed nets and by examining data type symmetries of such nets.

  • 25.2.2000 Prof. Pierre Azema (LAAS-CNRS, Toulouse, France):
    Protocol Specification and Debugging by Message Sequences.

    Abstract: The framework of this talk is the protocol design by means of high level Petri nets. The basic idea is to study a protocol behavior by taking into account operational input/output sequences, such as message sequence charts (MSC). These sequences are used for debugging purpose. A prototyping environment is introduced. This environment is based upon communicating agents, whose behavior is depicted by Petri nets. Furthermore, the agent number and their interactions may change on line. A distributed channel allocation algorithm for mobile computing is used as illustrative example.

  • 10.3.2000 Nisse Husberg: A Uniform Approach to Petri Nets and Transition Systems

    Abstract: In addition to several different approaches to formalisms for concurrent systems the development of many different Petri net classes has created a situation where it is difficult to understand and apply concepts defined for one specific class. There is, however, work going on to create a uniform approach using abstract formalisms. Typically the net structure and the data parts are separated and parameterised in these approaches. This talk is mainly about the uniform approach developed in Berlin (Padberg and Ehrig) and the distributed transition systems defined by the author. Both approaches use category theory and abstract data types to model both high-level and low-level nets. Some examples from the net description language of the Maria analyser are also presented.

  • 24.3.2000 Tuomas Aura: Denial-of-Service Resistant Authentication

    Abstract: Denial of service by server resource exhaustion has become a primary security threat in open communications networks. Public-key authentication does not completely protect against the attacks because the authentication protocols often leave ways for an unauthenticated client to consume a server's memory space and computational resources by beginning a large number of protocol runs and leaving them in some middle state. We show how stateless authentication protocols and the client puzzles of Juels and Brainard can be used to prevent such attacks.

    The talk is based on a joint work with Pekka Nikander and Jussipekka Leiwo.

  • 2.5.2000 Prof. Mirek Truszczynski (Univ. of Kentucky): Answer Set Programming and DATALOG with Constraints

    Abstract: Answer-set programming (ASP) has emerged recently as a viable programming paradigm well attuned to search problems in AI, constraint satisfaction, combinatorial optimization and combinatorics. In the talk we give a brief overview of the roots of ASP and comment on its potential. The bulk of the talk is devoted to a discussion of a recently introduced ASP system - DATALOG with constraints (DC, in short). Informally, $\datac$ theories consist of propositional clauses (constraints) and of Horn rules. The semantics is a simple and natural extension of the semantics of the propositional logic. We describe the syntax and semantics of DC, and study its properties. We discuss an implementation of DC and present results of experimental study of the effectiveness of DC, comparing it with the csat satisfiability checker and smodels2.

    (joint work with Deborah East)

  • 5.5.2000 Patric Östergård: Isomorph-Free Generation of Combinatorial Objects

    Abstract: In the study of combinatorial objects, one is often facing the problems of counting the number of nonisomorphic (or nonequivalent, depending on the terminology used) objects with given parameters or of constructing these. We shall look at some fundamental methods for such isomorph-free construction of various types of objects; in particular, so-called orderly generation of t-designs is considered. For example, a recent computation shows that there are 242,995,846 2-(12,3,2) designs. Classification of various other objects, for example, Petri nets, will also be discussed.

  • 19.5.2000 Kari Nurmela: Peittävien taulukoiden (covering arrays) muodostamisesta

    Abstract: Peittävät taulukot ovat tietyntyyppisiä kombinatorisia sommitelmia, joita voidaan käyttää mm. järjestelmien testauksessa. Tavoitteena on muodostaa mahdollisimman pieni sellainen testitapauksien joukko, johon jokainen parametrien arvopari (tai t-monikko) sisältyy ainakin kerran. Jos kukin parametri voi saada vain kaksi eri arvoa ja t=2, optimaaliset taulukot tunnetaan. Muissa tapauksissa tunnetaan vain ylä- ja alarajoja optimaalisten taulukoiden koolle. Tässä esitelmässä näytetään, miten tabuhakua voidaan käyttää peittävien taulukoiden etsimiseen ja esitetään joitakin uusia peittävien taulukoiden konstruktioita. Myös joitain uusia alarajoja on saavutettu täydellisellä haulla; yksi uusi peittävä taulukko tiedetään nyt optimaaliseksi.

  • 26.5.2000 Tommi A. Junttila: Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking

    Abstract: Boolean circuits offer a natural, structured, and compact representation of Boolean functions for many application domains. In this talk a tableau method for solving satisfiability problems for Boolean circuits is devised. The method employs a direct cut rule combined with deterministic deduction rules. Simplification rules for circuits and a search heuristic attempting to minimize the search space are developed. Experiments in symbolic model checking domain indicate that the method is competitive against state-of-the-art satisfiability checking techniques and a promising basis for further work.

  • 9.6.2000 Harri Haanpää: Alarajoja Ramseyn luvuille

    Abstract: Miten tahansa m solmun täydellisen graafin kaaret väritetäänkin kahdella värillä, jos m vain on riittävän suuri, värityksestä löytyy aina k solmun täydellinen graafi, jonka kaikki kaaret ovat samanvärisiä. Pienimpiä riittävän suuria m:n arvoja kutsutaan Ramseyn luvuiksi. Ramseyn lukujen määrittäminen on varsin vaikeaa. Tässä esitelmässä esitellään menetelmiä, joilla on todistettu alarajoja Ramseyn luvuille.


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